aboutsummaryrefslogtreecommitdiffstats
path: root/src
Commit message (Expand)AuthorAgeFilesLines
* 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-022-39/+61
* 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
* 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
* [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
| |\
| * | Use topological sort for nowYann Herklotz2021-02-161-4/+9
| * | Add schedule for new RTLPar typeYann Herklotz2021-02-161-29/+42
| * | Fix RTLPar to use instr list list listYann Herklotz2021-02-163-25/+33
| * | Replace original gather function with new constraintsYann Herklotz2021-02-151-15/+16
| * | Add resource constraintsYann Herklotz2021-02-151-6/+71
| * | Add information about pipeline and comb_delayYann Herklotz2021-02-151-8/+41
| * | Add data and control dependencies to reworked graphYann Herklotz2021-02-151-43/+236
| * | Make the schedule a bit neaterYann Herklotz2021-02-151-74/+63
| * | Use proper graph for DFGYann Herklotz2021-02-151-77/+113
* | | Add idle state after returnMichalis Pardalos2021-03-012-33/+37
* | | Typos in VeriloggenMichalis Pardalos2021-03-011-2/+2
* | | Unset finish signal on resetMichalis Pardalos2021-02-281-1/+3
* | | Merge branch 'master' into michalis-mergeYann Herklotz2021-02-163-1/+621
|\ \ \ | | |/ | |/|
| * | Remove dependency on TacticsYann Herklotz2021-02-161-1/+0
generated by cgit (git 2.34.1) at 2024-07-02 17:57:57 +0000