aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'master' into michalis-mergemichalis-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
| * Add wires and use them for output of instancesMichalis Pardalos2020-11-205-23/+55
| * Separate HTL instantiations from Verilog onesMichalis Pardalos2020-11-207-21/+30
| * 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 variablesmichalis_merge_2dev/improved-namesYann Herklotz2021-02-121-1/+17
* | Add signed and unsigned divisionYann Herklotz2021-02-122-0/+339
* | Add temporary fixes to get everything to compiledev/predicated-executionYann 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
* | 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
generated by cgit (git 2.34.1) at 2024-05-01 10:44:44 +0000