Hi Ben,
I tried your code but its not working while I want to check for a error condition.
Here is the snippet code for the same,
int delay=3;
property txeidle_0;
int x;
@(posedge clk) ($fell(sig),x=y) |-> ((1,x=x-1) [*0:$] ##1 (x==0)) ##0 ((xp != xn) [*0:$] ##1 $rose(sig));
endproperty
Here the delay is 3, means 3 clock cycle or what ?
2.If I check for the scenario where xp != xn will assert after delay times means I want to check for the error condition.
help me out from this.
let’s say for example the interface is parametrized with parameter “sva_parameter”
and you want to wait no. of clock cycles equal to this parameter, then using ##sva_parameter will not be allowed!
then you need to make a sequence, this sequence will take the generic or the parameter as an input and it works!
Kindly check the following example:
// 1) Following assertion can never fail because if the *0:$] and b==0
($rose(a), v=delay+1'b1) |-> (v>0, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;
// 2) Following assertion CAN fail because of the first_match() if b==0
($rose(a), v=delay+1'b1) |->
first_match((v>0, v=v-1'b1)[*0:$] ##1 v==0) ##0 b == 1;
// 3) Consider the following example
int v=5;
ap_1: assert property( x|-> ##2 b ##v c); // illegal in 1800'2012
/* If the variable used to define the delay has values that are within a constraint
range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example: */
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate
// 4) When a parameter is used, the value is static (and does not change) after elaboration, prior to sim.
In reply to sharadha:
I put a lot of thought into Mantis 5067 (for 1800’2018) where delays and repeat operators can use module variables as the value for the delays or repeat. I now believe that the best approach would be to specify something like the following:
The range for the delay or repeat cannot be greater than 32, as specified by a bit vector of no more than 5 bits.
The delay or repeat statement is in a sequence that is used as a property, and not as a sequence (e.g., no end points, no implication operator after the sequence).
Thus,
bit[2:0] v=3;
ap_delay: assert property( $rose(a) |-> d ##v b);
// The compiler would automatically implement something like the following:
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_delay_gen: assert property ($rose(a) |-> d ##0 v==g_i |-> ##g_i b);
end endgenerate
The above approach is simple to implement, fits most applications, and is more generic conceptually.
The use of local variables is complex, but feasible. But the use of the generate statement is much easier to express and understand.
Ben Cohen http://www.systemverilog.us/
I want to check b rose 6 cycle after a raises, and during 6 cycle b should be zero, should not toggle.
Two solutions:
fixed 6 cycles for rose(b)
Delay-based on a variable
module m_rose;
bit clk, a, b;
bit[3:0] delay=6;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// I want to check b rose 6 cycle after a raises,
// and during 6 cycle b should be zero, should not toggle.
ap_ab: assert property(
$rose(a) |=> !b[*5] ##1 $rose(b));
generate for (genvar g_i=0; g_i<16; g_i++) begin
if(g_i ==0)
ap_delay_gen: assert property ($rose(a) && g_i==delay
|=> !b[*g_i] ##1 $rose(b)); // same as |=> $rose(b)
else
ap_delay_gen: assert property ($rose(a) && g_i==delay
|=> !b[*g_i-1'b1] ##1 $rose(b));
end endgenerate
I tried above thing but for me g_i is not fixed It will changes during run.
It depends on some other variable in the simulation and that variable changes based on setting.
In reply to ben@SystemVerilog.us:
I tried above thing but for me g_i is not fixed It will changes during run.
It depends on some other variable in the simulation and that variable changes based on setting.
You missed my main point on the generate. The following code generates 16 separate assertions: Thus, the variable can change value. Note that in eh antecedent I have
$rose(a) && g_i==delay, thus, if among those 16 assertions, the ones that don’t match the delay create vacuous assertions. The only one that matches and has a successful $rose fire.
generate for (genvar g_i=0; g_i<16; g_i++) begin
if(g_i ==0)
ap_delay_gen: assert property ($rose(a) && g_i==delay
|=> !b[*g_i] ##1 $rose(b)); // same as |=> $rose(b)
else
ap_delay_gen: assert property ($rose(a) && g_i==delay
|=> !b[*g_i-1'b1] ##1 $rose(b));
end
endgenerate
The use of the generate is good for a small number of assertions.
You should be able to use a property with a local variable. Clarify your requirements and do a trial on a case. I’ll see if I can optimize it for you. Right now it is late for me, I can look at it in the morning.
Ben
In reply to ben@SystemVerilog.us:
If you don’t want to use the generate, you can do the following:
property p_delay;
int v;
($rose(a), v=delay+1'b1) |->
first_match((v>0 && !b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
// New comment: No need for the first_match because of the v>0 test
// Need of first_match() if we use the following instead
// first_match((!b, v=v-1'b1)[*0:$] ##1 v==0) ##0 $rose(b);
endproperty
// You need the first_match() because without it, id no $rose(b)
// the repeats keeps on counting forever.
I think this should work.
If first cycle value of b is zero, then b should have zero till end of count. at end it will check for rose of b.other wise assertion fails,(If I understood correctly)
module m_rose;
bit clk, a, b;
bit[3:0] delay=6;
int cycle=0;
let VACUOUSOFF = 11; // assertion control type
initial begin
$assertpasson(0);
$assertcontrol( VACUOUSOFF); //
end
always @(posedge clk) cycle <= cycle +1'b1;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
// I want to check b rose 6 cycle after a raises,
// and during 6 cycle b should be zero, should not toggle.
property p_delay;
int v;
($rose(a), v=delay+1'b1, $display("Cycle=%d, START, time=%t, DELAY= %d", cycle, $time, delay)) |->
(v>0 && !b, v=v-1'b1)[*0:$] ##1 v==0 ##0 $rose(b);
endproperty
ap_delay: assert property(p_delay) $display("Cycle=%d, PASS", $sampled(cycle));
else $display("Cycle=%d, FAIL", $sampled(c