diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2021-04-07 01:11:04 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2021-04-07 01:11:04 +0100 |
| commit | 8573889ca84a84475761b4d75d55547a2995c831 (patch) | |
| tree | cb1c78a976b0f03c9dbb46b521696bc4f90fa825 /src/hls/HTLgenspec.v | |
| parent | 6b56454246620cc1a0cda6949c524e20264d1935 (diff) | |
| download | vericert-8573889ca84a84475761b4d75d55547a2995c831.tar.gz vericert-8573889ca84a84475761b4d75d55547a2995c831.zip | |
Basically done with proof
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -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 6a10fa2..16bdcaf 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -178,12 +178,12 @@ Hint Constructors tr_code : htlspec. Inductive tr_module (f : RTL.function) : module -> Prop := tr_module_intro : - forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls wf1 wf2 wf3, + forall data control fin rtrn st stk stk_len m start rst clk scldecls arrdecls 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 None wf1 wf2 wf3) -> + st stk stk_len fin rtrn start rst clk scldecls arrdecls None wf1 wf2 wf3 wf4) -> (forall pc i, Maps.PTree.get pc f.(RTL.fn_code) = Some i -> tr_code f.(RTL.fn_code) pc i data control fin rtrn st stk) -> stk_len = Z.to_nat (f.(RTL.fn_stacksize) / 4) -> |