| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Guard join state with called module finish | Michalis Pardalos | 2021-09-11 | 1 | -3/+4 |
| * | Fix error in map_externctrl | Michalis Pardalos | 2021-09-03 | 1 | -1/+1 |
| * | Get HTLgen compiling with RAM inference | Michalis Pardalos | 2021-08-31 | 1 | -9/+9 |
| * | WIP | Michalis Pardalos | 2021-08-30 | 1 | -11/+0 |
| * | Merge branch 'oopsla21' into sharing-merge | Michalis Pardalos | 2021-08-26 | 1 | -24/+53 |
| |\ | |||||
| | * | Basically done with proof | Yann Herklotz | 2021-04-07 | 1 | -4/+6 |
| | * | Finish load and store proof, but broke top-level | Yann Herklotz | 2021-04-06 | 1 | -24/+24 |
| | * | Add RAM to HTL | Yann Herklotz | 2021-03-02 | 1 | -0/+1 |
| * | | Find called module in Icall proof | Michalis Pardalos | 2021-08-19 | 1 | -7/+1 |
| * | | Complete HTLspec (mostly) | Michalis Pardalos | 2021-08-12 | 1 | -34/+64 |
| * | | Tie clocks in the ApplyExternctrl pass | Michalis Pardalos | 2021-08-12 | 1 | -1/+0 |
| * | | Correct lookup for called funcs, simplify tr_module | Michalis Pardalos | 2021-08-04 | 1 | -8/+24 |
| * | | Check whether callee is internal for Icall | Michalis Pardalos | 2021-08-02 | 1 | -19/+24 |
| * | | Add "join state is <=Int.max_unsigned" to HTLgenspec | Michalis Pardalos | 2021-06-10 | 1 | -9/+11 |
| * | | Move HTL renaming pass to own file | Michalis Pardalos | 2021-06-06 | 1 | -240/+0 |
| * | | Most of Ireturn proof | Michalis Pardalos | 2021-05-16 | 1 | -11/+17 |
| * | | Prove a spec for the mapping of function params | Michalis Pardalos | 2021-05-06 | 1 | -5/+12 |
| * | | Define map_incr to clarify st_incr | Michalis Pardalos | 2021-05-05 | 1 | -9/+13 |
| * | | Rewrite transf_instr, move complicated part up | Michalis Pardalos | 2021-05-03 | 1 | -6/+6 |
| * | | Add externctrl props to HTLgen's st_prop | Michalis Pardalos | 2021-05-03 | 1 | -41/+44 |
| * | | Use ltac:() instead of Program in HTLgen | Michalis Pardalos | 2021-05-03 | 1 | -140/+116 |
| * | | Use Defined for obligations in Program Definitions | Michalis Pardalos | 2021-05-02 | 1 | -12/+12 |
| * | | Give a (questionable) translation spec for HTLgen | Michalis Pardalos | 2021-05-02 | 1 | -27/+37 |
| * | | Fix HTLgen using wrong register in call wait state | Michalis Pardalos | 2021-05-01 | 1 | -2/+3 |
| * | | Tie all modules' clock to main | Michalis Pardalos | 2021-04-30 | 1 | -6/+6 |
| * | | Fix map_externctrl double-incrementing freshreg | Michalis Pardalos | 2021-04-30 | 1 | -3/+2 |
| * | | Delete unused get_main_clk function from HTLgen | Michalis Pardalos | 2021-04-30 | 1 | -11/+0 |
| * | | Map clock correctly in RTL->HTL | Michalis Pardalos | 2021-04-29 | 1 | -15/+9 |
| * | | Renumber AssocMaps in HTL modules too | Michalis Pardalos | 2021-04-20 | 1 | -7/+24 |
| * | | Move renumbering to be HTL->HTL | Michalis Pardalos | 2021-04-20 | 1 | -0/+213 |
| * | | [WIP] Re-implement translation of calls. | Michalis Pardalos | 2021-04-19 | 1 | -33/+67 |
| * | | [WIP] Use Program instead of state_incr lemmas | Michalis Pardalos | 2021-04-18 | 1 | -165/+40 |
| * | | [WIP] Generate calling verilog in RTL->HTL | Michalis Pardalos | 2021-04-18 | 1 | -15/+40 |
| * | | [WIP] Remove extra statements from HTL. | Michalis Pardalos | 2021-04-18 | 1 | -17/+14 |
| * | | Fix merge error in oshrximm | Michalis Pardalos | 2021-04-09 | 1 | -1/+3 |
| * | | Add idle state after return | Michalis Pardalos | 2021-03-01 | 1 | -6/+7 |
| * | | 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 michali... | Yann Herklotz | 2021-02-16 | 1 | -2/+2 |
| |/ | |||||
| * | Fix imports to remove warnings when compiling | Yann Herklotz | 2021-01-22 | 1 | -9/+20 |
| * | Add correct copyright notices in files | Yann Herklotz | 2021-01-10 | 1 | -0/+1 |
| * | Change and add back HTLgen | Yann Herklotz | 2020-11-09 | 1 | -4/+4 |
| * | Add RTLBlock intermediate language | Yann Herklotz | 2020-08-30 | 1 | -0/+654 |
 |
index : vericert | |
| Vericert is a formally verified high-level synthesis tool. |
| aboutsummaryrefslogtreecommitdiffstats |