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
ncsim: *E,MSSYSTF (./test_2.sv,8|14): User Defined system task or function ($assertpasson) registered during elaboration and used within the simulation has not been registered during simulation.
$assertcontrol( VACUOUSOFF); //
I am getting above error.
In reply to tirumalrao_m:
This forum’s emphasis in on language usage and purposely avoids addressing tool issues, as those should be addressed directly with the vendor.
On this particular note, my guess is that the simulator was commanded (or started) into an optimized mode versus a debug mode. You typically do not want to slow the simulator with lots of messages, particularly on PASSONs.
Ben Cohen http://www.systemverilog.us/
SystemVerilog Assertions Handbook 4th Edition, 2016 ISBN 978-1518681448
Seems interesting topic. Is there any simple way to check signal pipeline variable delay. let’s consider 2 signals x1 and x2. Here x2 is delayed version on x1 and this delay is programmable with some variable. I don’t want to check value or state of x2 based on change on x1 because it may possible that x2 follows all transaction on x1 but there are also unexpected transaction x2 that are not there on x1 those transition also needs to be reported as error.
Seems interesting topic. Is there any simple way to check signal pipeline variable delay. let’s consider 2 signals x1 and x2. Here x2 is delayed version on x1 and this delay is programmable with some variable. I don’t want to check value or state of x2 based on change on x1 because it may possible that x2 follows all transaction on x1 but there are also unexpected transaction x2 that are not there on x1 those transition also needs to be reported as error.
You need to first clarify your requirements about the relationships between x1 and x2.
x2 always follows x1 // Normal behavior
2 occurrences of x2 after x1 // Error behavior
Other relationships
Once this is done, you can easily write assertions. Understand your requirements!
:)
Ben Cohen SystemVerilog.us
In reply to Digesh:
You need to first clarify your requirements about the relationships between x1 and x2.
x2 always follows x1 // Normal behavior
2 occurrences of x2 after x1 // Error behavior
Other relationships
Once this is done, you can easily write assertions. Understand your requirements!
:)
Ben Cohen SystemVerilog.us
x2 always follows x1 is normal condition. 2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2. Now if you think of error behavior it can be like you said 2 occurrences of x2 after x1 other error condition I think of are :
transition on x2 only
transition on x1 only
n number of transition on x1 but m transition on x2 where (m !== n)
Please let me know if you are having hard time understanding my point. I can draw some diagram that way you it will be easy for you to understand me.
In reply to ben@SystemVerilog.us:
x2 always follows x1 is normal condition. 2 transition on x1 before they reach x2 is also normal condition in such condition you should expect same 2 transition on x2. Now if you think of error behavior it can be like you said 2 occurrences of x2 after x1 other error condition I think of are :
transition on x2 only
transition on x1 only
n number of transition on x1 but m transition on x2 where (m !== n)
I’ll give you guidelines in writing the needed assertions.
FOR “n number of transition on x1 but m transition on x2 where (m !== n)”, you can use the module variables int ticket, now_serving as the difference should be zero at the end of simulation, or at times determined by you.
FOR “2 occurrences of x2 after x1 // Error behavior”. Use something like rose(x1) |-> strong(x2[->1] ##1 !x2[*0:] ##1 $rose(x1));
BTW, this is in conflict with your first requirement “2 transition on x1 before they reach x2”
FOR “n number of transition on x1 but m transition on x2 where (m !== n)”, you can use the module variables int ticket, now_serving as the difference should be zero at the end of simulation, or at times determined by you.
FOR “2 occurrences of x2 after x1 // Error behavior”. Use something like rose(x1) |-> strong(x2[->1] ##1 !x2[*0:] ##1 $rose(x1));
BTW, this is in conflict with your first requirement “2 transition on x1 before they reach x2”
Ben Cohen
Hi Ben ,
Thanks for reply I have already implemented this check as per below.
always @(signal1)begin
sig1_cnt = sig1_cnt + 1;
end
always @(signal2)begin
sig2_cnt = sig2_cnt + 1;
end
final begin
if(enable_condition)begin
CNT_CHK: assert (sig1_cnt == sig2_cnt) else $display(“sig1_cnt:%d and sig2_cnt:%d count mismatch”,sig1_cnt,sig2_cnt);
end
end
Let me know if you think of any better solution than this.
You need to build a testbench for the assertions and see if it meets your requirements.
As you may have noticed, I typically use the randomize with weighted distributions to generate the test signals. For example:
import uvm_pkg::*; `include "uvm_macros.svh"
module m;
bit clk, a, din;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, din) with
{ a dist {1'b1:=1, 1'b0:=3};
din dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error")
end
$finish;
end
endmodule
In my 4th edition of the SVA book, I have a chapter thta addresses building a testbench for assertions, and explain the use of typical constraints.
