Disabling the assertion when sig2 goes down seems to do the trick. Is this approach correct?
NO!
// The throughout operator specifies that a signal (expression) must hold throughout a sequence.
( b throughout R )[/b] is equivalent to [b]( b [*0:$] intersect R )
// Use the
sequenc1 interesect sequence2 // and sequence1 is
($stable(sig1)[*1:$] ##1 !sig2) // Thus, if sig2==0 after 4 cycles,
// the consequent thread that will match will be
($stable(sig1)[*3] ##1 !sig2 // sig2==0 at cycle 4
property sig1_stable_throughout_sig2 (logic sig1, sig2);
$rose(sig2) |-> ##1 ($stable(sig1)[*1:$] ##1 !sig2) intersect !sig2[->1];
endproperty
// As mentioned in a previous post, I prefer to use |-> ##1 instead |=>
// See my next post
Another option is to use the until
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true.
property_expr1 until property_expr2
property sig1_stable_throughout_sig2 (logic sig1, sig2);
$rose(sig2) |=> $stable(sig1) until !sig2; // Need the |=> because the until is a property
endproperty
// same as
$rose(sig2) |=> $stable(sig1)[*0:$] ##1 !sig2; // also OK.
In reply to Ankit Bhange:
Consider the following model where all 3 assertions are different. The annotated assertion thread viewer address cases that demonstrate why they are different. It is always preferable to test the assertions in a small model using constrained-random tests.
module top;
timeunit 1ns; timeprecision 100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, sig1, sig2;
initial forever #10 clk = !clk;
ap_sig1_stable_throughout_sig2 : assert property(@(posedge clk)
$rose(sig2) |=> ($stable(sig1)[*1:$] ##1 !sig2) intersect !sig2[->1]);
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) until !sig2); // Need the |=> because the until is a property
ap_sig1_stable_throughout_sig2_B : assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) throughout (sig2[*1:$] ##1 $fell(sig2)) );
initial begin
repeat (200) begin
@(posedge clk);
if (!randomize(sig1, sig2) with {
sig1 dist {1'b1 := 10, 1'b0 := 1};
sig2 dist {1'b1 := 6, 1'b0 := 1};
})
`uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
Hi
We usually use $stable(signa_name) to see a signal must be stable in from previous clk cycle. How to check that a signal must be stable within clk cycle
Thank you for the thorough explanation, Ben. It seems like
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) until !sig2); // Need the |=> because the until is a property
is what meets my requirements. However, for some reason I am getting a syntax error when trying to use the ‘until’ property. I think it is a tool issue.
Could you share any alternatives for until?
In reply to Ankit Bhange:
An until property of the non-overlapping form (i.e., until, s_until) evaluates to true if property_expr1 evaluates to true at every clock tick beginning with the starting clock tick of the evaluation attempt and continuing until at least one tick before a clock tick where property_expr2 (called the terminating property) evaluates to true. The until, s_until operators have an implicit repetition until the terminating condition (i.e., property_expr2) occurs. Specifically, with a strong until (e.g., s_until), if the simulation completes but the terminating condition is pending, the assertion fails, unlike the weak until where the assertion is evaluated as vacuously true.
$rose(req) |=> busy until ready); // Enhanced readability, and Identical to
// $rose(req) |=> busy[*0:$] ##1 ready ; // equivalent property expression
// Thus,
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1) until !sig2);
// can be written as
ap_until_sig1_stable_throughout_sig2: assert property(@(posedge clk)
$rose(sig2) |=> $stable(sig1)[*0:$] ##1 !sig2);
// When sig2==0, sig1 need not be stable
