diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 13:27:48 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-08-31 13:56:58 +0100 |
| commit | c88e9f6153195090dcb43b291016b237cacc7656 (patch) | |
| tree | e1d9642f2452691c8a1fe33a8ebbec564a343114 | |
| parent | 02a9b97ccb1a5ca5a29adfa0d6dc9a595cdca4b7 (diff) | |
| download | vericert-c88e9f6153195090dcb43b291016b237cacc7656.tar.gz vericert-c88e9f6153195090dcb43b291016b237cacc7656.zip | |
Get HTLgenspec compiling with RAM inference
| -rw-r--r-- | src/hls/HTLgenspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index 934f3f4..b46fd3b 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -121,12 +121,12 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (ge : RTL.genv) (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls externctrl wf, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls externctrl wf1 wf2 wf3 wf4, m = (mkmodule f.(RTL.fn_params) data control f.(RTL.fn_entrypoint) - st stk stk_len fin rtrn start rst clk scldecls arrdecls externctrl wf) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls externctrl None wf1 wf2 wf3 wf4) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code ge f.(RTL.fn_code) pc data control externctrl fin rtrn st stk i) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> |