From 2a5b73153060ff9f69403ca81d29c9c9761623d8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 17 Nov 2020 13:14:56 +0000
Subject: Add changes for proof of reset signals with Resetstate

---
 src/hls/HTL.v | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/src/hls/HTL.v b/src/hls/HTL.v
index 620ef14..cfc7aa3 100644
--- a/src/hls/HTL.v
+++ b/src/hls/HTL.v
@@ -120,6 +120,8 @@ Inductive step : genv -> state -> Events.trace -> state -> Prop :=
         ctrl
         (Verilog.mkassociations basr1 nasr1)
         (Verilog.mkassociations basa1 nasa1) ->
+      basr1!(mod_reset m) = Some (ZToValue 0) ->
+      basr1!(mod_finish m) = Some (ZToValue 0) ->
       basr1!(m.(mod_st)) = Some (posToValue st) ->
       Verilog.stmnt_runp f
         (Verilog.mkassociations basr1 nasr1)
-- 
cgit