aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Collapse)AuthorAgeFilesLines
* Delete inv_incr tactic (unused)Michalis Pardalos2021-05-101-51/+0
|
* Get entire HTLgenspec proof passingMichalis Pardalos2021-05-102-14/+36
|
* Progress on tr_module proofMichalis Pardalos2021-05-082-52/+82
|
* Fully clean up the iter_expand_instr_spec proofMichalis Pardalos2021-05-072-146/+80
|
* Complete iter_expand_instr_spec proofMichalis Pardalos2021-05-071-14/+23
|
* Prove a spec for the mapping of function paramsMichalis Pardalos2021-05-063-49/+128
| | | | | Extracted the traversal of call args into a function and gave it a spec, so that it can be used to prove the overall spec for the Icall instruction.
* Solve easier branches of the transf_instr proofMichalis Pardalos2021-05-061-29/+64
| | | | What remains is the ones about the mapping of parameter registers.
* Define map_incr to clarify st_incrMichalis Pardalos2021-05-051-9/+13
|
* Clean up iter_expand_instr_spec proofMichalis Pardalos2021-05-051-21/+10
|
* Solve iter_expand_instr_spec by tactic (not Icall)Michalis Pardalos2021-05-052-107/+182
|
* Rewrite transf_instr, move complicated part upMichalis Pardalos2021-05-031-6/+6
| | | | | Mapping the externctrl for the parameters requires a traversal on a list. Moved it up to the top of the branch to make it stand out in the proof.
* Add lemmas relating to new HTLgen operationsMichalis Pardalos2021-05-032-51/+73
|
* Add some statements about externctrl to tr_codeMichalis Pardalos2021-05-031-9/+13
|
* Add externctrl props to HTLgen's st_propMichalis Pardalos2021-05-032-41/+51
|
* Use ltac:() instead of Program in HTLgenMichalis Pardalos2021-05-031-140/+116
| | | | Program rewrites match statements, making proofs much harder.
* Use Defined for obligations in Program DefinitionsMichalis Pardalos2021-05-021-12/+12
| | | | The created terms might need to be inspected.
* Give a (questionable) translation spec for HTLgenMichalis Pardalos2021-05-022-39/+61
| | | | | I am not yet convinced it is the right one, particularly around the way I've used existentials. I will be updating it as I progress with the proof.
* Simplify some HTLgenspec proofsMichalis Pardalos2021-05-022-2/+7
|
* Handle declarations of externctrl regs in VerilogMichalis Pardalos2021-05-012-24/+48
|
* Remove some dead code from VeriloggenMichalis Pardalos2021-05-011-17/+0
|
* Fix HTLgen using wrong register in call wait stateMichalis Pardalos2021-05-011-2/+3
|
* Fix typo bug in applying externctrlMichalis Pardalos2021-05-011-2/+2
|
* Print externctrl in HTL debug outputMichalis Pardalos2021-05-012-6/+31
|
* Apply externctrl mapping in HTL->Verilog stageMichalis Pardalos2021-04-301-22/+147
|
* Tie all modules' clock to mainMichalis Pardalos2021-04-304-16/+47
|
* Fix map_externctrl double-incrementing freshregMichalis Pardalos2021-04-301-3/+2
|
* Delete unused get_main_clk function from HTLgenMichalis Pardalos2021-04-301-11/+0
|
* Map clock correctly in RTL->HTLMichalis Pardalos2021-04-291-15/+9
| | | | Remove the renumber_clk param of the renumber state
* Renumber AssocMaps in HTL modules tooMichalis Pardalos2021-04-202-7/+25
|
* Move renumbering to be HTL->HTLMichalis Pardalos2021-04-204-237/+234
|
* Get HTLgenproof to compileMichalis Pardalos2021-04-202-279/+280
|
* Update HTLPargen for new HTLMichalis Pardalos2021-04-201-30/+25
|
* Update ocaml code match HTL changesMichalis Pardalos2021-04-201-25/+2
|
* [WIP] Re-implement translation of calls.Michalis Pardalos2021-04-192-33/+84
| | | | | Add an explicit map of local HTL registers to control signals and params of other modules, used to implement calls.
* [WIP] Use Program instead of state_incr lemmasMichalis Pardalos2021-04-181-165/+40
|
* [WIP] Generate calling verilog in RTL->HTLMichalis Pardalos2021-04-182-15/+48
|
* [WIP] Remove extra statements from HTL.Michalis Pardalos2021-04-182-73/+18
|
* [WIP] HTLgenspec proofMichalis Pardalos2021-04-171-46/+34
|
* Fix up rest of HTLgenproofMichalis Pardalos2021-04-091-62/+46
|
* Fix merge error in oshrximmMichalis Pardalos2021-04-091-1/+3
|
* Get HTLgenproof to compileMichalis Pardalos2021-04-081-87/+89
|
* [WIP] Add semantics for new HTL instructionsMichalis Pardalos2021-04-021-38/+72
|
* Merge remote-tracking branch 'upstream/master' into dev-michalisMichalis Pardalos2021-03-299-262/+560
|\
| * 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
| |\
generated by cgit (git 2.34.1) at 2024-07-04 22:30:55 +0000