Verify all properties at once

fennecJ · Oct 23, 2024 · 27a7e62 · 27a7e62
1 parent db9dc09
commit 27a7e62
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 15 deletions.
diff --git a/isa.tcl b/isa.tcl
@@ -36,16 +36,16 @@ proc setCheckFlag {flagName flagValue} {
 }
 
 # set check flag
-setCheckFlag "CheckInstValidAssume" 0
-setCheckFlag "RegFileStable" 0
-setCheckFlag "PipeFollower" 0
+setCheckFlag "CheckInstValidAssume" 1
+setCheckFlag "RegFileStable" 1
+setCheckFlag "PipeFollower" 1
 setCheckFlag "ISA_GROUP_A" 1
     # Following Flag works only when "ISA_GROUP_A" set to 1
-    setCheckFlag "xori" 0
-    setCheckFlag "lb" 0
+    setCheckFlag "xori" 1
+    setCheckFlag "lb" 1
     setCheckFlag "blt" 1
-    setCheckFlag "jal" 0
-    setCheckFlag "auipc" 0
+    setCheckFlag "jal" 1
+    setCheckFlag "auipc" 1
 
 eval $ANALYZE_COMMAND
 

diff --git a/property/isa.sv b/property/isa.sv
@@ -789,17 +789,17 @@ module isa (
 `endif  // blt
 
 `ifdef jal
-    // e2e_jal_rd_correct :
-    // assert property (E2E_JAL_RD_IS_PC_PLUS_4);
+    e2e_jal_rd_correct :
+    assert property (E2E_JAL_RD_IS_PC_PLUS_4);
 
-    // e2e_jal_pc_jump_correct :
-    // assert property (E2E_JAL_NEXT_VALID_INST_IS_CORRECT);
+    e2e_jal_pc_jump_correct :
+    assert property (E2E_JAL_NEXT_VALID_INST_IS_CORRECT);
 
-    // e2e_jal_rd :
-    // assert property (E2E_JAL_RD);
+    e2e_jal_rd :
+    assert property (E2E_JAL_RD);
 
-    // e2e_jal_we1 :
-    // assert property (E2E_JAL_WE1);
+    e2e_jal_we1 :
+    assert property (E2E_JAL_WE1);
 
     check_goto_meaning :
     assert property (@(posedge clk) disable iff (rst) (VALID_JAL) |->