aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Typos in VeriloggenMichalis Pardalos2021-03-011-2/+2
|
* Unset finish signal on resetMichalis Pardalos2021-02-281-1/+3
|
* Add details to polybench runner csvMichalis Pardalos2021-02-281-1/+6
|
* Increase polybench runner timeoutMichalis Pardalos2021-02-281-1/+1
|
* Apply shellcheck suggestions to polybench runnerMichalis Pardalos2021-02-281-17/+16
|
* Use michalis branch for compcertMichalis Pardalos2021-02-281-0/+0
|
* Add timeout to polybench runnerMichalis Pardalos2021-02-281-5/+12
|
* Polybench - don't print PASS if test has failedMichalis Pardalos2021-02-231-22/+12
|
* polybench run-vericert passes args to vericertMichalis Pardalos2021-02-231-1/+1
|
* Merge branch 'master' into michalis-mergeYann Herklotz2021-02-161-1/+1
|\
| * Use dune_2 insteadYann Herklotz2021-02-161-1/+1
| |
* | Merge branch 'master' into michalis-mergeYann Herklotz2021-02-163-1/+621
|\|
| * Remove dependency on TacticsYann Herklotz2021-02-161-1/+0
| |
| * 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 signed and unsigned divisionYann Herklotz2021-02-122-0/+339
| |
* | Add temporary fixes to get everything to compileYann Herklotz2021-02-129-45/+514
| |
* | Fix state generation for if-conversionYann Herklotz2021-02-034-14/+21
| |
* | Fix scheduling for if-conversionYann Herklotz2021-02-031-14/+90
| |
generated by cgit (git 2.34.1) at 2024-07-07 16:46:52 +0000