From 2429e158ecdb4ab8150fa26af776e806d7fd019c Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Fri, 14 May 2021 19:59:16 +0100
Subject: Update HTL proof for resource sharing (WIP)

---
 src/hls/HTLgenspec.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/hls/HTLgenspec.v')

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.
-- 
cgit