Disabling all essertions but row 4

YoannPruvost · Jun 17, 2024 · 41c33ec · 41c33ec
1 parent bdd5253
commit 41c33ec
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/scripts/formal/src/cv32e40p_EX_assert.sv b/scripts/formal/src/cv32e40p_EX_assert.sv
@@ -66,9 +66,9 @@ module cv32e40p_EX_assert import cv32e40p_pkg::*;
             (apu_rvalid_q && ~(( ~apu_read_dep_for_jalr_o && (ctrl_transfer_insn_in_dec_i==2)) && regfile_alu_we_i) && ~((data_misaligned_i || data_misaligned_ex_i) || ((data_req_i || data_rvalid_i) && regfile_alu_we_i)) && mulh_active) |-> mult_operator_i == MUL_H;
     endproperty
 
-    assert_unreachable_ex_211: assert property(unreachable_ex_211);
-    assert_unreachable_ex_237: assert property(unreachable_ex_237);
-    assert_unreachable_ex_387: assert property(unreachable_ex_387);
-    assert_unreachable_ex_396: assert property(unreachable_ex_396);
+    // assert_unreachable_ex_211: assert property(unreachable_ex_211);
+    // assert_unreachable_ex_237: assert property(unreachable_ex_237);
+    // assert_unreachable_ex_387: assert property(unreachable_ex_387);
+    // assert_unreachable_ex_396: assert property(unreachable_ex_396);
 
 endmodule
diff --git a/scripts/formal/src/cv32e40p_ID_assert.sv b/scripts/formal/src/cv32e40p_ID_assert.sv
@@ -42,5 +42,5 @@ module cv32e40p_ID_assert import cv32e40p_pkg::*;
             (alu_op_c_mux_sel == OP_C_REGC_OR_FWD) && (~(alu_op_b_mux_sel == OP_B_BMASK) && ((alu_op_a_mux_sel != OP_A_REGC_OR_FWD) && (ctrl_transfer_target_mux_sel != JT_JALR)) && ~alu_bmask_b_mux_sel) |-> alu_op_b_mux_sel == OP_B_IMM;
     endproperty
 
-    assert_unreachable_id_872: assert property(unreachable_id_872);
+    // assert_unreachable_id_872: assert property(unreachable_id_872);
 endmodule
diff --git a/scripts/formal/src/cv32e40p_controller_assert.sv b/scripts/formal/src/cv32e40p_controller_assert.sv
@@ -64,11 +64,11 @@ module cv32e40p_controller_assert import cv32e40p_pkg::*;
             ((ctrl_fsm_cs == DBG_FLUSH) && !data_err_i) && (~debug_req_entry_q && ~((debug_mode_q | trigger_match_i) | (ebrk_force_debug_mode & ebrk_insn_i))) |-> !data_load_event_i;
     endproperty
 
-    assert_all_true_ctrl_1187_1189_and_1191: assert property(all_true_ctrl_1187_1189_and_1191);
-    assert_all_true_ctrl_1210_and_1212 : assert property(all_true_ctrl_1210_and_1212);
+    // assert_all_true_ctrl_1187_1189_and_1191: assert property(all_true_ctrl_1187_1189_and_1191);
+    // assert_all_true_ctrl_1210_and_1212 : assert property(all_true_ctrl_1210_and_1212);
     //This one is inconclusive with questa formal. To avoid long run keep it disabled
-    // assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
-    assert_unreachable_ctrl_1241_row_5 : assert property(unreachable_ctrl_1241_row_5);
-    assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10);
+    assert_unreachable_ctrl_1241_row_4 : assert property(unreachable_ctrl_1241_row_4);
+    // assert_unreachable_ctrl_1241_row_5 : assert property(unreachable_ctrl_1241_row_5);
+    // assert_unreachable_ctrl_1241_row_10: assert property(unreachable_ctrl_1241_row_10);
 
 endmodule
diff --git a/scripts/formal/src/fpnew_divsqrt_th_32_assert.sv b/scripts/formal/src/fpnew_divsqrt_th_32_assert.sv
@@ -37,6 +37,6 @@ module fpnew_divsqrt_th_32_assert (
             (op_starting && unit_ready_q) |-> !(ex2_inst_wb && ex2_inst_wb_vld_q);
     endproperty
 
-    assert_unreachable_divsqrt_th_288: assert property(unreachable_divsqrt_th_288);
+    // assert_unreachable_divsqrt_th_288: assert property(unreachable_divsqrt_th_288);
 
 endmodule