aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HTLgen.v
Commit message (Expand)AuthorAgeFilesLines
* Find called module in Icall proofMichalis Pardalos2021-08-191-7/+1
* Complete HTLspec (mostly)Michalis Pardalos2021-08-121-34/+64
* Tie clocks in the ApplyExternctrl passMichalis Pardalos2021-08-121-1/+0
* Correct lookup for called funcs, simplify tr_moduleMichalis Pardalos2021-08-041-8/+24
* Check whether callee is internal for IcallMichalis Pardalos2021-08-021-19/+24
* Add "join state is <=Int.max_unsigned" to HTLgenspecMichalis Pardalos2021-06-101-9/+11
* Move HTL renaming pass to own fileMichalis Pardalos2021-06-061-240/+0
* Most of Ireturn proofMichalis Pardalos2021-05-161-11/+17
* Prove a spec for the mapping of function paramsMichalis Pardalos2021-05-061-5/+12
* Define map_incr to clarify st_incrMichalis Pardalos2021-05-051-9/+13
* Rewrite transf_instr, move complicated part upMichalis Pardalos2021-05-031-6/+6
* Add externctrl props to HTLgen's st_propMichalis Pardalos2021-05-031-41/+44
* Use ltac:() instead of Program in HTLgenMichalis Pardalos2021-05-031-140/+116
* Use Defined for obligations in Program DefinitionsMichalis Pardalos2021-05-021-12/+12
* Give a (questionable) translation spec for HTLgenMichalis Pardalos2021-05-021-27/+37
* Fix HTLgen using wrong register in call wait stateMichalis Pardalos2021-05-011-2/+3
* Tie all modules' clock to mainMichalis Pardalos2021-04-301-6/+6
* 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
* Renumber AssocMaps in HTL modules tooMichalis Pardalos2021-04-201-7/+24
* Move renumbering to be HTL->HTLMichalis Pardalos2021-04-201-0/+213
* [WIP] Re-implement translation of calls.Michalis Pardalos2021-04-191-33/+67
* [WIP] Use Program instead of state_incr lemmasMichalis Pardalos2021-04-181-165/+40
* [WIP] Generate calling verilog in RTL->HTLMichalis Pardalos2021-04-181-15/+40
* [WIP] Remove extra statements from HTL.Michalis Pardalos2021-04-181-17/+14
* Fix merge error in oshrximmMichalis Pardalos2021-04-091-1/+3
* Add idle state after returnMichalis Pardalos2021-03-011-6/+7
* Add changes to HTL as they weren't mergedYann Herklotz2021-02-161-53/+122
* Merge branch 'michalis' of https://github.com/mpardalos/vericert into michali...Yann Herklotz2021-02-161-2/+2
* Fix imports to remove warnings when compilingYann Herklotz2021-01-221-9/+20
* Add correct copyright notices in filesYann Herklotz2021-01-101-0/+1
* Change and add back HTLgenYann Herklotz2020-11-091-4/+4
* Add RTLBlock intermediate languageYann Herklotz2020-08-301-0/+654
generated by cgit (git 2.34.1) at 2024-07-04 20:54:11 +0000