aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| * | Add data and control dependencies to reworked graphYann Herklotz2021-02-151-43/+236
| * | Make the schedule a bit neaterYann Herklotz2021-02-151-74/+63
| * | Use proper graph for DFGYann Herklotz2021-02-151-77/+113
* | | Add a script to count calls in benchmarksMichalis Pardalos2021-03-291-0/+89
* | | Add a gitignore for benchmark folderMichalis Pardalos2021-03-091-0/+6
* | | Parallelize runner script, make it work on other benchmarksMichalis Pardalos2021-03-092-53/+78
* | | Remove non-functioning polybench testsMichalis Pardalos2021-03-011-3/+0
* | | Rename quartus synthesis files to match vivadoMichalis Pardalos2021-03-012-0/+0
* | | Add scripts for remote synthesis with vivadoMichalis Pardalos2021-03-013-0/+85
* | | Turn off -fschedule in test runner. Breaks sharingMichalis Pardalos2021-03-011-1/+1
* | | Polybench runner report iverilog, vericert failureMichalis Pardalos2021-03-011-1/+10
* | | Increase polybench runner timeout to 1mMichalis Pardalos2021-03-011-1/+1
* | | Add idle state after returnMichalis Pardalos2021-03-012-33/+37
* | | 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 michali...Yann Herklotz2021-02-1614-183/+769
|\ \ | |/ |/|
| * 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
| * 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
| * Add todo for missing logic around instantiationsMichalis Pardalos2020-11-201-0/+1