aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/hls/RTLBlockgenproof.v3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/hls/RTLBlockgenproof.v b/src/hls/RTLBlockgenproof.v
index e33e3a3..d62ccf9 100644
--- a/src/hls/RTLBlockgenproof.v
+++ b/src/hls/RTLBlockgenproof.v
@@ -230,6 +230,9 @@ Section CORRECTNESS.
/\ match_states (RTL.State s f sp pc' rs m) s2'.
Proof.
intros s f sp pc rs m pc' H.
+ inversion 1; simplify. inv H1. inv H0. inv BB0.
+ inv PC0.
+ -
Admitted.
Lemma transl_Iop_correct: