If you really want a 0 delay when “delay”==0, you could write this
property assert_check;
int v; // variable "delay" can be >0
// If set to "0", then no delay,
@(posedge clk) disable iff(disable_assertion)
($rose(a), v=delay+1'b1) |-> (1, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;
endproperty : assert_check
Thanks for your reply Ben…
But I have a question on this.
I want something like…
Assertion should start with $rose(a)
Then after “Delay” value ‘b’ should be high. ‘b’ must be high only after specific “Delay”. {Delay is a variable".
I am trying to inject an error but it is not firing.
Can you please confirm that its doing same thing.
property assert_check;
int v; // variable "delay" can be >0
// If set to "0", then no delay,
@(posedge clk) disable iff(disable_assertion)
($rose(a), v=delay+1'b1) |-> (1, v=v-1'b1)[*0:$] ##1 v==0 ##0 b == 1;
endproperty : assert_check
I want something like…
Assertion should start with $rose(a)
Then after “Delay” value ‘b’ should be high. ‘b’ must be high only after specific “Delay”. {Delay is a variable".
I am trying to inject an error but it is not firing.
Can you please confirm that its doing same thing.
When I first looked at your code, I concentrated on the property. Looking again at your code, I see that your “a” is a 4-bit vector. So if “a” goes from 4’b1000 to 4’b0100 the $rose(a) is 0, no change. In my first look, I assumed that “a” was a single bit.
Thus, the point I am making is that our $rose(a) is ambiguous. If you mean a change in “a”, you could use " $changed(a) " or " !$statble(a) " instead of " $rose(a) ".
What I wrote says that if a rose of a (i.e., vector goes from a value of 0 to a value of 1, then if the dealy has a value of 3, v=4; then in the same cycle, v gets decremented immediately, and then after every cycle until v==0. So, in 3 cycles, v==0, and at that time. b vector should be ==1 (i.e., the “b” should be greater than 0.
Watch your “bits” and “bit vectors”, there is a difference. If your vector b should be equal to your original vector a after a delay, you can do the following:
logic [3:0] delay,a,b;
property assert_check;
int v_delay, v_b; // variable "delay" can be 0
@(posedge clk) disable iff(disable_assertion)
($changed(a), v=delay+1'b1, v_b=a) |-> (1, v_delay=v_delay-1'b1)[*0:$]
##1 v_delay==0 ##0 b == v_b;
endproperty : assert_check
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)
