diff options
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. |