aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Fix proof with new array matchingYann Herklotz2021-03-171-20/+47
|
* Fix main proofs with smaller admitsYann Herklotz2021-03-171-25/+50
|
* Proof of equivalent stmnt runs with matching startYann Herklotz2021-03-171-155/+263
|
* Prove one case of transf_code correctYann Herklotz2021-03-161-1/+54
|
* Greatly simplify proofYann Herklotz2021-03-161-44/+23
|
* Finish proof of simple transformationYann Herklotz2021-03-161-0/+90
|
* Fix memory inferrence generationYann Herklotz2021-03-151-28/+32
|
* Move implicit argsYann Herklotz2021-03-151-2/+2
|
* Fix Verilog importsYann Herklotz2021-03-141-14/+20
|
* 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-025-3/+12
|
* 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 benchmark run for masterYann Herklotz2021-03-011-2/+2
|
* 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-167-6/+33
|
* Merge branch 'master' into developYann Herklotz2021-02-165-12/+623
|\
| * Remove the documentation stagesYann Herklotz2021-02-161-8/+0
| |
| * Pin nixpkgsYann Herklotz2021-02-161-2/+1
| |
| * Use dune_2 insteadYann Herklotz2021-02-161-1/+1
| |
| * 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 variablesYann Herklotz2021-02-121-1/+17
|
* Add signed and unsigned divisionYann Herklotz2021-02-122-0/+339
|
generated by cgit (git 2.34.1) at 2024-07-01 01:43:19 +0000