aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
* Remove comments in Verilog.vYann Herklotz2021-03-141-194/+0
* Prove top-level theorem with admitted theoremsYann Herklotz2021-03-122-159/+193
* Try and fix identity proof in MemorygenYann Herklotz2021-03-121-1/+12
* Prove idempotency of array mergeYann Herklotz2021-03-112-20/+86
* Update RAM generation proofsYann Herklotz2021-03-093-70/+472
* Add negative edge reasoning to HTLgenproofYann Herklotz2021-03-092-12/+109
* Add RAM semantics to HTL and fix proofYann Herklotz2021-03-034-18/+132
* Add implementationYann Herklotz2021-03-022-29/+80
* Add option to turn on/off ram inferrenceYann Herklotz2021-03-024-2/+9
* Add RAM to HTLYann Herklotz2021-03-024-1/+4
* Fix memory generation by generating a power of 2Yann Herklotz2021-03-021-34/+50
* Print Verilog in reverse orderYann Herklotz2021-03-021-1/+1
* Add Verilog generation for ramsYann Herklotz2021-03-021-18/+47
* Admit VeriloggenproofYann Herklotz2021-03-021-2/+3
* Finish initial implementation of memory genYann Herklotz2021-03-012-2/+89
* Change lists in case statements to stmnt_listYann Herklotz2021-03-016-12/+30
* Add initial memory generationYann Herklotz2021-03-011-0/+17
* Fix printing of the final cycle countYann Herklotz2021-02-211-2/+15
* Fix bug in scheduleYann Herklotz2021-02-191-2/+1
* Fix schedule for nowYann Herklotz2021-02-181-1/+2
* Add udiv and sdiv to constraintsYann Herklotz2021-02-171-12/+20
* Remove dead code and add more constraintsYann Herklotz2021-02-171-107/+16
* Add option to turn off if-conversionYann Herklotz2021-02-165-4/+29
* Merge branch 'master' into developYann Herklotz2021-02-163-1/+621
|\
| * Remove dependency on TacticsYann Herklotz2021-02-161-1/+0
| * Add functional units and SatYann Herklotz2021-02-162-0/+621
* | Use topological sort for nowYann Herklotz2021-02-161-4/+9
* | Add schedule for new RTLPar typeYann Herklotz2021-02-161-29/+42
* | Fix RTLPar to use instr list list listYann Herklotz2021-02-163-25/+33
* | Replace original gather function with new constraintsYann Herklotz2021-02-151-15/+16
* | Add resource constraintsYann Herklotz2021-02-151-6/+71
* | Add information about pipeline and comb_delayYann Herklotz2021-02-151-8/+41
* | 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 more legible names to variablesmichalis_merge_2dev/improved-namesYann Herklotz2021-02-121-1/+17
* Add temporary fixes to get everything to compiledev/predicated-executionYann 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
generated by cgit (git 2.34.1) at 2024-06-26 21:17:31 +0000