Simply porperty and clarify goto and intersect

fennecJ · Oct 27, 2024 · b4f8e84 · b4f8e84
1 parent ae7c9fc
commit b4f8e84
Show file tree

Hide file tree

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

diff --git a/property/isa.sv b/property/isa.sv
@@ -320,8 +320,7 @@ module isa (
             previous_jal_pc  <= 32'd0;
             previous_jal_imm <= 21'd0;
         end else begin
-            if ((wb_inst_dc.opcode == OPC_JAL) && (!core_wb_stall) &&
-                (wb_pipeline_info.bubble == 1'b0)) begin
+            if ((wb_inst_dc.opcode == OPC_JAL) && (wb_pipeline_info.inst_valid)) begin
                 previous_jal_pc  <= wb_pipeline_info.inst_pc.pc;
                 previous_jal_imm <= wb_inst_dc.imm21_j;
             end
@@ -652,9 +651,10 @@ module isa (
     endproperty : E2E_JAL_RD
 
     property E2E_JAL_WE1;  // rd != 0 -> must enable write;
-        @(posedge clk) disable iff (rst) VALID_JAL |-> (|wb_inst_dc.rd |-> (core.wb_we == 1));
+        @(posedge clk) disable iff (rst) VALID_JAL && (|wb_inst_dc.rd)  |-> (core.wb_we == 1);
     endproperty : E2E_JAL_WE1
 
+    // [->x] goto : means that goto the x-th time the sequence is pulled up.
     sequence valid_jal_followed_valid_1;
         (VALID_JAL ##1 wb_pipeline_info.inst_valid [->1]);
     endsequence : valid_jal_followed_valid_1
@@ -801,6 +801,7 @@ module isa (
     e2e_jal_we1 :
     assert property (E2E_JAL_WE1);
 
+    // a intersect b : it means that a and b will have the same starting point and endpoint
     check_jal_coverage :
     assert property (@(posedge clk) disable iff (rst) (VALID_JAL) |->
                      valid_jal_followed_valid_1 intersect valid_jal_followed_valid_2);