Commit message (Collapse) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | Merge remote-tracking branch 'upstream/master' into dev-michalis | Michalis Pardalos | 2021-03-29 | 9 | -262/+560 |
|\ | |||||
| * | Fix printing of the final cycle count | Yann Herklotz | 2021-02-21 | 1 | -2/+15 |
| | | |||||
| * | Fix bug in schedule | Yann Herklotz | 2021-02-19 | 1 | -2/+1 |
| | | |||||
| * | Fix schedule for now | Yann Herklotz | 2021-02-18 | 1 | -1/+2 |
| | | |||||
| * | Add udiv and sdiv to constraints | Yann Herklotz | 2021-02-17 | 1 | -12/+20 |
| | | |||||
| * | Remove dead code and add more constraints | Yann Herklotz | 2021-02-17 | 1 | -107/+16 |
| | | |||||
| * | Add option to turn off if-conversion | Yann Herklotz | 2021-02-16 | 5 | -4/+29 |
| | | |||||
| * | Merge branch 'master' into develop | Yann Herklotz | 2021-02-16 | 3 | -1/+621 |
| |\ | |||||
| * | | Use topological sort for now | Yann Herklotz | 2021-02-16 | 1 | -4/+9 |
| | | | |||||
| * | | Add schedule for new RTLPar type | Yann Herklotz | 2021-02-16 | 1 | -29/+42 |
| | | | |||||
| * | | Fix RTLPar to use instr list list list | Yann Herklotz | 2021-02-16 | 3 | -25/+33 |
| | | | |||||
| * | | Replace original gather function with new constraints | Yann Herklotz | 2021-02-15 | 1 | -15/+16 |
| | | | |||||
| * | | Add resource constraints | Yann Herklotz | 2021-02-15 | 1 | -6/+71 |
| | | | |||||
| * | | Add information about pipeline and comb_delay | Yann Herklotz | 2021-02-15 | 1 | -8/+41 |
| | | | |||||
| * | | Add data and control dependencies to reworked graph | Yann Herklotz | 2021-02-15 | 1 | -43/+236 |
| | | | |||||
| * | | Make the schedule a bit neater | Yann Herklotz | 2021-02-15 | 1 | -74/+63 |
| | | | |||||
| * | | Use proper graph for DFG | Yann Herklotz | 2021-02-15 | 1 | -77/+113 |
| | | | |||||
* | | | Add idle state after return | Michalis Pardalos | 2021-03-01 | 2 | -33/+37 |
| | | | |||||
* | | | Typos in Veriloggen | Michalis Pardalos | 2021-03-01 | 1 | -2/+2 |
| | | | |||||
* | | | Unset finish signal on reset | Michalis Pardalos | 2021-02-28 | 1 | -1/+3 |
| | | | |||||
* | | | Merge branch 'master' into michalis-merge | Yann Herklotz | 2021-02-16 | 3 | -1/+621 |
|\ \ \ | | |/ | |/| | |||||
| * | | Remove dependency on Tactics | Yann Herklotz | 2021-02-16 | 1 | -1/+0 |
| | | | |||||
| * | | Add functional units and Sat | Yann Herklotz | 2021-02-16 | 2 | -0/+621 |
| |/ | |||||
* | | Make top-level theorems pass | Yann Herklotz | 2021-02-16 | 3 | -48/+53 |
| | | |||||
* | | Add changes to HTL as they weren't merged | Yann Herklotz | 2021-02-16 | 1 | -53/+122 |
| | | |||||
* | | Merge branch 'michalis' of https://github.com/mpardalos/vericert into ↵ | Yann Herklotz | 2021-02-16 | 14 | -183/+769 |
|\ \ | |/ |/| | | | michalis-merge | ||||
| * | Implement join. Completes implementation | Michalis Pardalos | 2021-02-15 | 1 | -4/+8 |
| | | |||||
| * | Group all verilog translation code | Michalis Pardalos | 2021-02-15 | 1 | -43/+44 |
| | | |||||
| * | Make HTLFork translation use renumbered registers | Michalis Pardalos | 2021-02-15 | 1 | -63/+69 |
| | | |||||
| * | Add PTree traversal functions for vericert monads | Michalis Pardalos | 2021-02-15 | 1 | -1/+20 |
| | | |||||
| * | Add an indexed filter function to PTree | Michalis Pardalos | 2021-02-12 | 1 | -0/+27 |
| | | |||||
| * | Implemented fork and wait (incorrectly) | Michalis Pardalos | 2021-02-12 | 1 | -46/+70 |
| | | |||||
| * | Reformat | Michalis Pardalos | 2021-02-09 | 1 | -5/+5 |
| | | |||||
| * | Add wait instruction to HTL control path | Michalis Pardalos | 2021-01-26 | 7 | -76/+152 |
| | | |||||
| * | Separate HTL call into fork and join | Michalis Pardalos | 2021-01-26 | 5 | -20/+62 |
| | | |||||
| * | Inlined modules are valid verilog, use correct clk | Michalis Pardalos | 2021-01-26 | 3 | -16/+50 |
| | | |||||
| * | Renumbering removes name conflicts | Michalis Pardalos | 2021-01-25 | 1 | -197/+226 |
| | | |||||
| * | Implement renumbering (wrong) | Michalis Pardalos | 2021-01-25 | 4 | -51/+269 |
| | | |||||
| * | Get everything compiling | Michalis Pardalos | 2021-01-18 | 2 | -2/+5 |
| | | |||||
| * | Get top-level proofs passing. | Michalis Pardalos | 2020-12-01 | 1 | -28/+26 |
| | | | | | | | | Needed change because inlining was removed. | ||||
| * | Get proofs in HTLgenproof to pass | Michalis Pardalos | 2020-12-01 | 1 | -11/+6 |
| | | |||||
| * | Update proofs in HTLgenspec | Michalis Pardalos | 2020-12-01 | 1 | -4/+17 |
| | | |||||
| * | Declare dst reg for call instr | Michalis Pardalos | 2020-12-01 | 1 | -0/+1 |
| | | |||||
| * | Add a call instruction to HTL. Use it for Icall. | Michalis Pardalos | 2020-11-30 | 8 | -97/+190 |
| | | |||||
| * | Revert changes relating to instance generation | Michalis Pardalos | 2020-11-27 | 8 | -205/+60 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Revert "Add todo for missing logic around instantiations" This reverts commit 303a45374643f75698c61f062899973d2c297831. Revert "Add wires and use them for output of instances" This reverts commit a72f26319dabca414a2b576424b9f72afaca161c. Revert "Separate HTL instantiations from Verilog ones" This reverts commit 653c8729f4322f538aa7116c5e311c884b3c5047. Revert "Translate instantiations from HTL to verilog" This reverts commit 982e6c69a52e8ec4e677147004cc5472f8a80d6d. Revert "Print instantiations in HTL output" This reverts commit 9b87637d3e4d6a75dee1221b017e3ccf6632642e. Revert "Add a field in HTL modules for instances" This reverts commit d79dae026b150e9671e0aa7262f6aa2d1d302502. Revert "Generate (invalid) module instantiations for calls" This reverts commit dfaa3a9cbc07649feea3220693a8a854a32eafb6. | ||||
| * | Add todo for missing logic around instantiations | Michalis Pardalos | 2020-11-20 | 1 | -0/+1 |
| | | |||||
| * | Add wires and use them for output of instances | Michalis Pardalos | 2020-11-20 | 5 | -23/+55 |
| | | | | | | | | | | | | | | | | [WIP] Add wires to HTL [WIP] Add wires to verilog [WIP] Use wire for finished signal [WIP] merge wire and scl [WIP] Fix wrong reg in ICall translation | ||||
| * | Separate HTL instantiations from Verilog ones | Michalis Pardalos | 2020-11-20 | 7 | -21/+30 |
| | | | | | | | | | | | | | | | | | | | | | | In HTL, they reference their data arguments, destination, and finished control signal. Meanwhile, in Verilog, they just contain an unstructured list of parameters. This is done because when modules are generated in the HTL stage we do not have access to any of the instantiating module's control signals (they are declared after the entirety of the module has been translated). Also, I believe, these signals are not part of the HTL semantics. | ||||
| * | Print HTL args as reg_{n}, not x{n} | Michalis Pardalos | 2020-11-20 | 1 | -7/+7 |
| | | |||||
| * | Translate instantiations from HTL to verilog | Michalis Pardalos | 2020-11-20 | 3 | -2/+7 |
| | |