aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
...
| * 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 variablesYann Herklotz2021-02-121-1/+17
* | Add temporary fixes to get everything to compileYann 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
* | Finish all proofs except executing basic blocksYann Herklotz2021-01-271-1/+4
* | Add more proofs for RTLPargen correctnessYann Herklotz2021-01-273-26/+97
* | Add basic block matching and proofYann Herklotz2021-01-261-3/+78
* | Remove the schedule oracleYann Herklotz2021-01-262-518/+515
* | Add an inductive to enter the basic blockYann Herklotz2021-01-261-3/+3
* | Use basic blocks in context to help proofYann Herklotz2021-01-261-11/+15
* | Add destruction to context match expressionsYann Herklotz2021-01-261-2/+5
* | Remove match on basic blocksYann Herklotz2021-01-231-6/+0
* | Add match_states for RTLPargen proofYann Herklotz2021-01-222-4/+78
* | Fix imports to remove warnings when compilingYann Herklotz2021-01-227-49/+101
* | Fix types with new changes in RTLBlockYann Herklotz2021-01-224-91/+133
* | Define RTLPar semanticsYann Herklotz2021-01-222-172/+85
* | Add top-level semantics definitionsYann Herklotz2021-01-221-0/+17
* | Add semantics for RTLBlockYann Herklotz2021-01-222-12/+68
* | Add semantics for RTLBlockInstr and RTLBlockYann Herklotz2021-01-222-22/+72
generated by cgit (git 2.34.1) at 2024-07-07 13:23:53 +0000