diff --git a/cdc/fpv/BUILD.bazel b/cdc/fpv/BUILD.bazel
index b07af6dd3..bc069ee1a 100644
--- a/cdc/fpv/BUILD.bazel
+++ b/cdc/fpv/BUILD.bazel
@@ -263,6 +263,7 @@ br_verilog_fpv_test_tools_suite(
 
 br_verilog_fpv_test_tools_suite(
     name = "br_cdc_fifo_ctrl_1r1w_test_suite",
+    gui = True,
     illegal_param_combinations = {
         (
             "Depth",
diff --git a/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv
index 570f4f8f9..fcd905ebf 100644
--- a/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv
+++ b/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv
@@ -211,4 +211,35 @@ module br_cdc_fifo_basic_fpv_monitor #(
   // ----------Critical Covers----------
   `BR_COVER_CR(fifo_full_c, push_full, push_clk, push_rst)
 
+  // ----------assert reset again----------
+  localparam int ResetLen = NumSyncStages + 2;
+  logic [1:0] push_rst_cnt, pop_rst_cnt;
+  logic push_rst_d, pop_rst_d;
+  logic push_rst_flg, pop_rst_flg;
+
+  `BR_REGNX(push_rst_d, push_rst, push_clk);
+  `BR_REGNX(pop_rst_d, pop_rst, pop_clk);
+  `BR_REGLX(push_rst_cnt, push_rst_cnt + 1, !push_rst && push_rst_d, push_clk, rst)
+  `BR_REGLX(pop_rst_cnt, pop_rst_cnt + 1, !pop_rst && pop_rst_d, pop_clk, rst)
+  `BR_REGLX(push_rst_flg, 1, push_rst && !push_rst_d, push_clk, rst)
+  `BR_REGLX(pop_rst_flg, 1, pop_rst && !pop_rst_d, pop_clk, rst)
+
+  `BR_ASSUME_CR(push_rst_twice_a, push_rst_cnt <= 2, push_clk, rst)
+  `BR_ASSUME_CR(pop_rst_twice_a, pop_rst_cnt <= 2, pop_clk, rst)
+  `BR_ASSUME_CR(push_rst_rise_once_a, push_rst_flg |-> !$rose(push_rst), push_clk, rst)
+  `BR_ASSUME_CR(pop_rst_rise_once_a, pop_rst_flg |-> !$rose(pop_rst), pop_clk, rst)
+  `BR_COVER_CR(push_rst_twice_c, push_rst_cnt == 2, push_clk, rst)
+  `BR_COVER_CR(pop_rst_twice_c, pop_rst_cnt == 2, pop_clk, rst)
+  // push and pop reset must overlap
+  `BR_ASSUME_CR(no_push_rst_rise_a, (pop_rst_cnt != 'd1) |-> !$rose(push_rst), push_clk, rst)
+  `BR_ASSUME_CR(no_pop_rst_rise_a, (push_rst_cnt != 'd1) |-> !$rose(pop_rst), pop_clk, rst)
+  `BR_ASSUME_CR(push_rst_rise_a, $rose(push_rst) |-> push_rst until_with pop_rst, push_clk, rst)
+  `BR_ASSUME_CR(pop_rst_rise_a, $rose(pop_rst) |-> pop_rst until_with push_rst, pop_clk, rst)
+  // Don't assert reset until NumSyncStages + 2 cycles after the other side's reset is deasserted
+  `BR_ASSUME_CR(no_push_rst_a, $fell(pop_rst) |-> !$rose(push_rst) [* ResetLen], push_clk, rst)
+  `BR_ASSUME_CR(no_pop_rst_a, $fell(push_rst) |-> !$rose(pop_rst) [* ResetLen], pop_clk, rst)
+  // Don't deassert reset until NumSyncStages + 2 cycles after the other side's reset is asserted
+  `BR_ASSUME_CR(hold_push_rst_a, $rose(pop_rst) |-> !$fell(push_rst) [* ResetLen], push_clk, rst)
+  `BR_ASSUME_CR(hold_pop_rst_a, $rose(push_rst) |-> !$fell(pop_rst) [* ResetLen], pop_clk, rst)
+
 endmodule : br_cdc_fifo_basic_fpv_monitor
diff --git a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv.jg.tcl
index 311a0c4b5..270b95bf7 100644
--- a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv.jg.tcl
@@ -14,8 +14,8 @@ assume -name deassert_rst {##1 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}
 
diff --git a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv.jg.tcl
index 4aec86eb6..bbb58bd6e 100644
--- a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv.jg.tcl
@@ -9,13 +9,13 @@ clock pop_clk -from 1 -to 10 -both_edges
 # declare always_in system clock
 reset -none
 assume -reset -name set_rst_during_reset {rst}
-assume -bound 1 -name delay_rst {rst}
-assume -name deassert_rst {##1 !rst}
+assume -bound 30 -name delay_rst {rst}
+assume -name deassert_rst {##30 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}
 
diff --git a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv.jg.tcl
index dfee7200b..24731fcb6 100644
--- a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv.jg.tcl
@@ -9,13 +9,13 @@ clock pop_clk -from 1 -to 10 -both_edges
 # declare always_in system clock
 reset -none
 assume -reset -name set_rst_during_reset {rst}
-assume -bound 1 -name delay_rst {rst}
-assume -name deassert_rst {##1 !rst}
+assume -bound 30 -name delay_rst {rst}
+assume -name deassert_rst {##30 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}
 
diff --git a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv.jg.tcl
index b856ac5be..dff82db75 100644
--- a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv.jg.tcl
@@ -9,13 +9,13 @@ clock pop_clk -from 1 -to 10 -both_edges
 # declare always_in system clock
 reset -none
 assume -reset -name set_rst_during_reset {rst}
-assume -bound 1 -name delay_rst {rst}
-assume -name deassert_rst {##1 !rst}
+assume -bound 30 -name delay_rst {rst}
+assume -name deassert_rst {##30 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}
 
diff --git a/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl
index 186aa2bef..d6c6068ed 100644
--- a/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl
@@ -9,13 +9,13 @@ clock pop_clk -from 1 -to 10 -both_edges
 # declare always_in system clock
 reset -none
 assume -reset -name set_rst_during_reset {rst}
-assume -bound 1 -name delay_rst {rst}
-assume -name deassert_rst {##1 !rst}
+assume -bound 30 -name delay_rst {rst}
+assume -name deassert_rst {##30 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}
 
diff --git a/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv.jg.tcl
index 25698188e..f6e111806 100644
--- a/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv.jg.tcl
+++ b/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv.jg.tcl
@@ -9,13 +9,13 @@ clock pop_clk -from 1 -to 10 -both_edges
 # declare always_in system clock
 reset -none
 assume -reset -name set_rst_during_reset {rst}
-assume -bound 1 -name delay_rst {rst}
-assume -name deassert_rst {##1 !rst}
+assume -bound 30 -name delay_rst {rst}
+assume -name deassert_rst {##30 !rst}
 # reset are ready at different times
 assume -env {rst |-> push_rst}
 assume -env {rst |-> pop_rst}
-assume -env {!push_rst |=> !push_rst}
-assume -env {!pop_rst |=> !pop_rst}
+#assume -env {!push_rst |=> !push_rst}
+#assume -env {!pop_rst |=> !pop_rst}
 assume -env {s_eventually !push_rst}
 assume -env {s_eventually !pop_rst}