| Commit message (Collapse) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | Guard join state with called module finish | Michalis Pardalos | 2021-09-11 | 1 | -3/+4 |
| | | | | | | | Needed to match RTL semantics, since the join state executes once before the call is initiated, and we need the destination register to not be affected until after the call has returned. | ||||
| * | 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 |
| | | | | | | | | | | | 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. | ||||
| * | | 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 |
| | | | | | | | | | | | 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 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 |
| | | | | | | | | | Program rewrites match statements, making proofs much harder. | ||||
| * | | Use Defined for obligations in Program Definitions | Michalis Pardalos | 2021-05-02 | 1 | -12/+12 |
| | | | | | | | | | The created terms might need to be inspected. | ||||
| * | | Give a (questionable) translation spec for HTLgen | Michalis Pardalos | 2021-05-02 | 1 | -27/+37 |
| | | | | | | | | | | | 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. | ||||
| * | | 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 |
| | | | | | | | | | Remove the renumber_clk param of the renumber state | ||||
| * | | 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 |
| | | | | | | | | | | | 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 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 ↵ | Yann Herklotz | 2021-02-16 | 1 | -2/+2 |
| |/ | | | | michalis-merge | ||||
| * | 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 |