diff options
| author | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-14 19:59:16 +0100 |
|---|---|---|
| committer | Michalis Pardalos <m.pardalos@gmail.com> | 2021-05-14 19:59:16 +0100 |
| commit | 2429e158ecdb4ab8150fa26af776e806d7fd019c (patch) | |
| tree | 0d9e936ba696877a505531ec5d1a501cd1649962 /src/hls/HTLgenspec.v | |
| parent | 30780c235b712f42beda87397020ed8e4bad9949 (diff) | |
| download | vericert-2429e158ecdb4ab8150fa26af776e806d7fd019c.tar.gz vericert-2429e158ecdb4ab8150fa26af776e806d7fd019c.zip | |
Update HTL proof for resource sharing (WIP)
Diffstat (limited to 'src/hls/HTLgenspec.v')
| -rw-r--r-- | src/hls/HTLgenspec.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/hls/HTLgenspec.v b/src/hls/HTLgenspec.v index bd8a2e7..1c2d090 100644 --- a/src/hls/HTLgenspec.v +++ b/src/hls/HTLgenspec.v @@ -132,6 +132,7 @@ Inductive tr_module (f : RTL.function) : module -> Prop := (fin > st)%positive -> (rtrn > fin)%positive -> (stk > rtrn)%positive -> + (forall r, (exists x, externctrl!r = Some x) -> (r > stk /\ start > r)%positive) -> (start > stk)%positive -> (rst > start)%positive -> (clk > rst)%positive -> @@ -463,4 +464,5 @@ Proof. some_incr; simplify; unfold Ple in *; lia ]. -Qed. + admit. (* No control registers are in externctrl *) +Admitted. |