aboutsummaryrefslogtreecommitdiffstats
path: root/src/translation
Commit message (Collapse)AuthorAgeFilesLines
* Inlined modules are valid verilog, use correct clkMichalis Pardalos2021-01-261-16/+27
|
* Renumbering removes name conflictsMichalis Pardalos2021-01-251-197/+226
|
* Implement renumbering (wrong)Michalis Pardalos2021-01-252-40/+243
|
* Get everything compilingMichalis Pardalos2021-01-182-2/+5
|
* 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-305-66/+132
|
* Revert changes relating to instance generationMichalis Pardalos2020-11-273-155/+41
| | | | | | | | | | | | | | | | | | | | | | | 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 instantiationsMichalis Pardalos2020-11-201-0/+1
|
* Add wires and use them for output of instancesMichalis Pardalos2020-11-202-13/+42
| | | | | | | | [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 onesMichalis Pardalos2020-11-202-3/+10
| | | | | | | | | | | 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.
* Translate instantiations from HTL to verilogMichalis Pardalos2020-11-201-1/+4
|
* Add a field in HTL modules for instancesMichalis Pardalos2020-11-202-32/+97
|
* Generate (invalid) module instantiations for callsMichalis Pardalos2020-11-202-5/+14
|
* Add html generation and clean Coq filesYann Herklotz2020-08-131-2/+1
|
* Finished all the proofsv1.0.0Yann Herklotz2020-08-133-39/+46
| | | | Removed support for case statements temporarily.
* Remove unnecessary commented proofYann Herklotz2020-08-121-23/+0
|
* Finish proof of conditionalsYann Herklotz2020-08-121-4/+11
|
* Nearly finished all proofsYann Herklotz2020-08-121-48/+228
|
* Remove alignment constraint during translation.James Pollard2020-08-112-67/+69
| | | | This is now inferred from the memory model.
* Remove last admits from istoreYann Herklotz2020-08-041-2/+3
|
* Finish istore and iload without any admitsYann Herklotz2020-08-041-118/+113
|
* No admitted in iload proofYann Herklotz2020-08-041-38/+72
|
* Merge remote-tracking branch 'james/develop' into developYann Herklotz2020-08-041-5/+6
|\
| * Fix broken proof.James Pollard2020-08-041-5/+6
| |
* | Add expr_ok proofYann Herklotz2020-08-041-11/+25
|/
* Fix first part of istoreYann Herklotz2020-08-041-40/+43
|
* Fix iload proofYann Herklotz2020-08-041-43/+48
|
* Add proof of divisibilityYann Herklotz2020-08-041-21/+14
|
* More renames to get it to compileYann Herklotz2020-07-241-2/+3
|
* Change name to VericertYann Herklotz2020-07-145-19/+18
|
* Fixes to operatorsYann Herklotz2020-07-072-3/+8
|
* Finished transl_condYann Herklotz2020-07-072-62/+45
|
* Only translate_cond leftYann Herklotz2020-07-073-16/+249
|
* No admitted in Deterministic proofYann Herklotz2020-07-071-2/+2
|
* A few operations leftYann Herklotz2020-07-071-30/+88
|
* Proof of TransfHTLLink DONEYann Herklotz2020-07-071-1/+14
|
* Add top level backward simulationYann Herklotz2020-07-061-72/+77
|
* HTLgenproof compiles againYann Herklotz2020-07-061-14/+30
| | | | - Commented out Iload, Istore proofs for now
* Fix InopYann Herklotz2020-07-054-47/+58
|
* Fix HTLgenspecYann Herklotz2020-07-051-3/+4
|
* No addmitted in VeriloggenproofYann Herklotz2020-07-053-92/+233
| | | | However, there may have been breaking changes to HTLgenproof.
* Remove admitted in mis_stepp_VdeclYann Herklotz2020-07-052-5/+9
|
* Finish most of VeriloggenproofYann Herklotz2020-07-052-24/+196
|
* Make HTLgen compile againYann Herklotz2020-07-041-3/+11
|
* Fixing HTLgenproofYann Herklotz2020-07-033-28/+47
|
* Add new value type to fix Iop proofYann Herklotz2020-07-031-2/+2
|
* Updates to Iop proofYann Herklotz2020-07-032-91/+101
|
* Switch to uvalueToZ in lessdef.James Pollard2020-07-021-36/+31
|
generated by cgit (git 2.34.1) at 2024-07-07 15:02:22 +0000