aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
...
| * | Add functional units and SatYann Herklotz2021-02-162-0/+621
| |/
* | Make top-level theorems passYann Herklotz2021-02-163-48/+53
| |
* | Add changes to HTL as they weren't mergedYann Herklotz2021-02-161-53/+122
| |
* | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵Yann Herklotz2021-02-1614-183/+769
|\ \ | |/ |/| | | michalis-merge
| * Implement join. Completes implementationMichalis Pardalos2021-02-151-4/+8
| |
| * Group all verilog translation codeMichalis Pardalos2021-02-151-43/+44
| |
| * Make HTLFork translation use renumbered registersMichalis Pardalos2021-02-151-63/+69
| |
| * Add PTree traversal functions for vericert monadsMichalis Pardalos2021-02-151-1/+20
| |
| * Add an indexed filter function to PTreeMichalis Pardalos2021-02-121-0/+27
| |
| * Implemented fork and wait (incorrectly)Michalis Pardalos2021-02-121-46/+70
| |
| * ReformatMichalis Pardalos2021-02-091-5/+5
| |
| * Add wait instruction to HTL control pathMichalis Pardalos2021-01-267-76/+152
| |
| * Separate HTL call into fork and joinMichalis Pardalos2021-01-265-20/+62
| |
| * Inlined modules are valid verilog, use correct clkMichalis Pardalos2021-01-263-16/+50
| |
| * Renumbering removes name conflictsMichalis Pardalos2021-01-251-197/+226
| |
| * Implement renumbering (wrong)Michalis Pardalos2021-01-254-51/+269
| |
| * Get everything compilingMichalis Pardalos2021-01-182-2/+5
| |
| * Get top-level proofs passing.Michalis Pardalos2020-12-011-28/+26
| | | | | | | | Needed change because inlining was removed.
| * Get proofs in HTLgenproof to passMichalis Pardalos2020-12-011-11/+6
| |
| * Update proofs in HTLgenspecMichalis Pardalos2020-12-011-4/+17
| |
| * Declare dst reg for call instrMichalis Pardalos2020-12-011-0/+1
| |
| * Add a call instruction to HTL. Use it for Icall.Michalis Pardalos2020-11-308-97/+190
| |
| * Revert changes relating to instance generationMichalis Pardalos2020-11-278-205/+60
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Revert "Add todo for missing logic around instantiations" This reverts commit 303a45374643f75698c61f062899973d2c297831. Revert "Add wires and use them for output of instances" This reverts commit a72f26319dabca414a2b576424b9f72afaca161c. Revert "Separate HTL instantiations from Verilog ones" This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047. Revert "Translate instantiations from HTL to verilog" This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d. Revert "Print instantiations in HTL output" This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e. Revert "Add a field in HTL modules for instances" This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502. Revert "Generate (invalid) module instantiations for calls" This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6.
| * Add todo for missing logic around instantiationsMichalis Pardalos2020-11-201-0/+1
| |
| * Add wires and use them for output of instancesMichalis Pardalos2020-11-205-23/+55
| | | | | | | | | | | | | | | | [WIP] Add wires to HTL [WIP] Add wires to verilog [WIP] Use wire for finished signal [WIP] merge wire and scl [WIP] Fix wrong reg in ICall translation
| * Separate HTL instantiations from Verilog onesMichalis Pardalos2020-11-207-21/+30
| | | | | | | | | | | | | | | | | | | | | | In HTL, they reference their data arguments, destination, and finished control signal. Meanwhile, in Verilog, they just contain an unstructured list of parameters. This is done because when modules are generated in the HTL stage we do not have access to any of the instantiating module's control signals (they are declared after the entirety of the module has been translated). Also, I believe, these signals are not part of the HTL semantics.
| * Print HTL args as reg_{n}, not x{n}Michalis Pardalos2020-11-201-7/+7
| |
| * Translate instantiations from HTL to verilogMichalis Pardalos2020-11-203-2/+7
| |
| * Print instantiations in HTL outputMichalis Pardalos2020-11-203-14/+29
| |
| * Add a field in HTL modules for instancesMichalis Pardalos2020-11-205-37/+102
| |
| * Print all modules in verilog outputMichalis Pardalos2020-11-201-13/+11
| |
| * Generate (invalid) module instantiations for callsMichalis Pardalos2020-11-205-14/+29
| |
* | Add more legible names to variablesYann Herklotz2021-02-121-1/+17
| |
* | Add temporary fixes to get everything to compileYann Herklotz2021-02-127-36/+386
| |
* | Fix state generation for if-conversionYann Herklotz2021-02-034-14/+21
| |
* | Fix scheduling for if-conversionYann Herklotz2021-02-031-14/+90
| |
* | Add predicated values and instructionsYann Herklotz2021-02-027-41/+92
| |
* | Add if conversion passYann Herklotz2021-02-021-3/+65
| |
* | Add if conversion passYann Herklotz2021-02-021-0/+32
| |
* | Add Vrange and predicatesYann Herklotz2021-02-028-66/+95
| |
* | Fix OCaml files for compilationYann Herklotz2021-01-314-92/+94
| |
* | Fix compilation of CoqYann Herklotz2021-01-302-19/+48
| |
* | Fix proofs with better defined equalityYann Herklotz2021-01-302-31/+57
| |
* | Fix definitions of proofs some moreYann Herklotz2021-01-294-106/+162
| |
* | Fix the proof for RTLPargenYann Herklotz2021-01-291-32/+33
| |
* | Fix HTLPargen and RTLPargenYann Herklotz2021-01-292-56/+178
| |
* | Refactoring RTLBlock and RTLParYann Herklotz2021-01-293-297/+205
| |
* | Finish all proofs except executing basic blocksYann Herklotz2021-01-271-1/+4
| |
* | Add more proofs for RTLPargen correctnessYann Herklotz2021-01-273-26/+97
| |
* | Add basic block matching and proofYann Herklotz2021-01-261-3/+78
| |
generated by cgit (git 2.34.1) at 2024-07-07 15:48:02 +0000