Change comments and labels

tests/staged_sim_and_verif/Req_Ack.sv

@@ -50,26 +50,31 @@ module DUT (
                 phase1_reqs_seen: cover(reqs_seen == 2);
         end
 
-        // In phase 2, assume that there's no more reqs; cover that an ack will
+        // In phase 2, cover that the first ack arrives within a bounded window
-        // eventually come for the second req, and separately prove bounded
+        // after the first req + another req arrives.
-        // counts for reqs/acks.
+        phase2_cover_ack_and_new_req: cover property (@(posedge clk)
-        always @ (posedge clk) begin
+                $rose(ack) ##[1:$] (reqs_seen == 3)
-                phase2_shared_no_new_req: assume(!req);
-        end
-
-        always @(posedge clk) begin
-                phase2a_cover_ack: cover(ack);
-        end
-
-        // Assert the second ack arrives within a bounded window after the second
-        // request, and also that ack count never exceeds the expected two.
-        phase2b_assert_ack_reaches_two: assert property (@(posedge clk)
-                $rose(reqs_seen == 2) |-> ##[1:8] acks_seen == 2
         );
-        always @(posedge clk) begin
+
-                phase2b_assert_ack_stable: assert(acks_seen <= 2);
+
+        // In phase 3, assume that there's no more reqs.
+        always @ (posedge clk) begin
+                phase3_shared_no_new_req: assume(!req);
         end
 
+        // In phase 3a, cover the second ack arriving eventually.
+        always @(posedge clk) begin
+                phase3a_cover_ack: cover(ack);
+        end
+
+        // Assert the second ack arrives within a bounded window after beginning
+        // phase 3, and furthermore after that point no further acks arrive.
+        property p_acks_seen_hits_3_and_stays;
+                @(posedge clk) ##[0:8] $rose(acks_seen == 3) ##1 (acks_seen == 3)[*0:$];
+        endproperty
+
+        phase3b_acks_seen_hits_3_and_stays: assert property (p_acks_seen_hits_3_and_stays);
+
 
 `endif