Hii All,
I am new to assertions based verification and I am confused with where do I need to check the boolean value of a signal at “Antecedent” side when I am using implication operator of any type(overlapping / non-overlapping).
eg.
sequence s1;
@ (posedge clk) a |-> ##b;
endsequence
In the above code snippet, at which clock cycle the assertion should be started.? Current clock or the previous one ???
Please somebody elaborate
Thanks and Regards
Sapna Sharma
In reply to sapsharma19:
Hi sapna,
The assertions will be active throughout the simulation.So, it will be checking at every positive edge of the clock.
In reply to rajan passionate:
Hii,
But as the textbook saying, the sampling of the sequence will be done in the preponed region… Means previous clocking cycle… Isn`t it Rajan
In reply to sapsharma19:
All the systemverilog/verilog events happens in same clock cycles and they are repeated for each clock. Read following paper for better understanding of systemverilog events:
http://www.sunburst-design.com/papers/CummingsSNUG2006Boston_SystemVerilog_Events.pdf
I think it’s better to refresh SV concepts before jumping on to assertions.
Thanks,
Rohit
In reply to rohitk:
@sapna
Preponed region doesn’t mean as previous clock edge.It means the time instant just before the current clock edge.
In reply to sapsharma19:
you can understand better by thinking like this,
before calculations are done for this edge, simulator retains old values in a temp variable internally and those values are used in assertions, not the values updated in this clock.
But, if you use a $display in an assert statement, you would get the updated value not the ones assertions see.
For this reason, you must use $sample(var) in display statements to get the values assertions see…
In reply to ssureshg_:
From my book, I demonstrate the various SV evaluation regions.
In hardware, we have the concept of “setup time”, which is the time needed for the signal to settle after all the delays (that is the FF output delay + all the combinational logic till the D input of the next FF stage). The minimum setup time is a delta time before the clock edge, and that is represented by the Preponed Region.
Those Regions include
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
Hi Ben,
If the sampling of the variables “a” and “c” is done in the preponed region . And the evaluation is done on these sampled values (of “a” and “c”), which are not effected by the changes happening in the current cycle.
Then, why are the concurrent assertions evaluated in Observed region, is there any particular reason.
The assertion evaluation can be done in any region of the current cycle after the preponed region. Am i right in saying so? Please let me know if I am missing something.
In reply to wiki458:
when we are working out of clock we should have some path for the program that we write considering verilog we have stratified event queue so that every condition or evaluation of variables and the results are taken into particular regions so that the execution is perfect.
In the same way we have regions for system verilog assertions also and each regions have its own work like UVM phases,and that too we have two types of assertions one is immediate assertions that are used for combinational circuit evaluations and these are executed based on event regions and the other is concurrent assertions which are based on clock.
I explained upto my knowledge let em know if I am wrong
In reply to wiki458:
Hi Ben,
If the sampling of the variables “a” and “c” is done in the preponed region . And the evaluation is done on these sampled values (of “a” and “c”), which are not effected by the changes happening in the current cycle.
Then, why are the concurrent assertions evaluated in Observed region, is there any particular reason.
The assertion evaluation can be done in any region of the current cycle after the preponed region. Am i right in saying so? Please let me know if I am missing something.
A lot of thoughts went into the processing in the various regions.
If the assertions were evaluated before the NBA, the action block could change the values of variables that are used in the NBA. Consider the following example:
b==1 at initial. Assertion action block changes b to 0. In the always_ff you have a <= b.
What value of “b” should be used? the initial 1’b1’, or the modified 0 by the action block?
bit clk, a, b=1'b1;
default clocking @(posedge clk); endclocking
always_ff @(posedge clk) a <= b;
ap: assert property( 0) else b=1'b0;
http://SystemVerilog.us/fv/tassert.sv
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Thanks for the clarification Ben.
Hi Ben,
“Sampling in preponed region, execution in observed region, action block in reactive region”
Are these scheduling principles obeyed by assertion based formal verification tools as well, or do they have a different mechanism for sampling and evaluation?
Thanks.
In reply to wiki458:
Hi Ben,
“Sampling in preponed region, execution in observed region, action block in reactive region”
Are these scheduling principles obeyed by assertion based formal verification tools as well, or do they have a different mechanism for sampling and evaluation?
Formal verification does not use simulation and works differently. From my SVA 3rd Edition:
7.1.4 More about model checking
In model checking, properties (written in a property language, like SVA) are used to capture the design intent. A formal verifier reads in an RTL design and builds a state transition graph for the system in a manner similar to an FSM. A first and foremost requirement for Model Checking is that designs need to be synthesizable and cycle-based. A natural limitation of such an approach would be that designs that contain
elements such as phase-locked loops (PLLs), behavioral memories, etc. cannot be converted into logic equations, thus they can’t be proven using the formal engines. Typically, a model checker treats non-synthesizable blocks as black-boxes, making the outputs of those blocks free ranging variables (meaning that they can have any random value), unless built-in models are available for those black boxes
The Verifier then reads in the properties and directives. Typically these properties represent the design specification as temporal sequences (such as request to grant protocols, illegal transitions), and they specify whether these properties hold forever or during a finite time. A Model Checker then checks whether the design implementation obeys these properties by searching the entire state space of the design, and produces counterexamples if the design fails to obey the properties.
By definition, FV is a complete proof, and hence is the ultimate verification methodology – if applicable. However, FV suffers heavily from the state space explosion problem for larger designs because it needs to search a very large number of states. An acceptable methodology is to limit the analysis to blocks of manageable size by partitions (i.e., smaller blocks) or by imposing constraints via the restrict operator to limit the scenarios for convergence on a proof (see 4.5.1.3). The assume construct should also be used to specify legal input states; this would avoid a failure due to some sequence of inputs that would not happen in the real world.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
In reply to wiki458:
A lot of thoughts went into the processing in the various regions.
If the assertions were evaluated before the NBA, the action block could change the values of variables that are used in the NBA. Consider the following example:
b==1 at initial. Assertion action block changes b to 0. In the always_ff you have a <= b.
What value of “b” should be used? the initial 1’b1’, or the modified 0 by the action block?
bit clk, a, b=1'b1;
default clocking @(posedge clk); endclocking
always_ff @(posedge clk) a <= b;
ap: assert property( 0) else b=1'b0;
http://SystemVerilog.us/fv/tassert.sv
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Hi, I don’t think this is a good example. The value that a use will for sure be 1 if the assertion is evaluated and updates b just before the NBA region. Since the evaluation of the RHS of a <= b is already done in active region and the value used is 1. Changing b right before the NBA will not affect the outcome. The value used in NBA is determined during the evaluation in active region (it’s not a variable)
Consider running:
initial begin
b = 1;
a <= b;
b = 0;
#1 $display(" a = %0d",a);
end
You will see that the value of a is 1.
In reply to GMZlate:
I an not clear as to what your point is. However, instead of your example with the initial, let me change that to the always_comb.
initial begin
q = 1;
m <= q;
q = 0;
#1 $display(" m = %0d", m);
end
always_comb begin
c= b; // to trigger the always_comb
w = 1;
w = 0;
$display(" at %t in comb: a = %0d", $time, a);
end
always @(posedge clk) begin
$display(" at %t in always: a = %0d", $time, a);
a <= w;
end
// simulation results
at 0 in comb: a = 0
m = 1
at 100 in always: a = 0
at 300 in always: a = 0
at 500 in always: a = 0
at 500 in comb: a = 0
at 700 in always: a = 0
Your comment: “You will see that the value of a is 1.”
Your “a” is my “m”, and it is a 1 in the initial, but using the always, it is a 0, and the combinational logic is re-evaluated, and that is the value taken by the nonblocking assignment.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
In reply to ben@SystemVerilog.us:
Yes, an 0 in the always block is expected. If you want to show that changing w changes the NBA assignment you need to make sure that a <= w happens between the w = 1 and w = 0. However, in your example, the a <= w is scheduled before the always_comb (according to your output) and the value used in evaluating the RHS IS 0. So for sure your always example should output 0.
In reply to ben@SystemVerilog.us:
And my point is once the evaluation of the RHS of a <= w is done, no matter what you do to w, as long as the evaluation of RHS is not triggered again, the assignment to the RHS should not be affected. The evaluation means the RHS is 0,1,x or z, not the RHS is w. Definitely correct me if I’m wrong. Thanks.
In reply to GMZlate:
I believe that what you are saying is true. However the following example should clarify things. Simulation must reflect how harware behaves. Consider the following example where the D output of a D FF is fed back to its input through an AND gate.
always_comb begin
din = dout && enb;
end
always @(posedge clk) begin
dout <= !din;
end
Assumng 0 setup and hold time, andy change to dout or enb re-evaluate din.
@(posedge clk) dout will change its value in the NBA region. The loop through the Active region re-evaluates din (since ther was a change). However, the dout <= !din; will NOT be re-evaluated again, even with zero setup and hold times.
I believe that this is what you were saying. Below is my test code.
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
timeunit 1ns; timeprecision 100ps;
bit clk, din, dout, enb;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
always_comb begin
din = dout && enb;
//$display(" at %t in comb: a = %0d", $time, a);
end
always @(posedge clk) begin
//$display(" at %t in always: a = %0d", $time, a);
dout <= !din;
end
initial begin
bit va;
repeat(20) begin
@(negedge clk);
if (!randomize(va) with
{va dist {1'b1:=6, 1'b0:=1};
}) `uvm_error("MYERR", "This is a randomize error")
enb <= va;
end
$stop;
end
endmodule
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
In reply to ben@SystemVerilog.us:
@ben: I don’t see a reason for the evaluation of concurrent assertions in a specific region as “Observed Region”
The evaluation of concurrent assertion could have been in any of “active region set”, right? Maybe the execution of pass_statement and fail_statement could be in Reactive region.
In reply to Rahul H Iyer:
Why even ask the question after its First appearance in 2005; 11 years ago for sva?
Whether you are correct or not ii really does not matter.
The timing regions were thoroughly analyzed by committees from industry and tool vendors, and unless there are serious issues, I doudt that there would be any changes.
SystemVerilog is the way it is. Next version with minor updates in 3 to 5+ years.
Ben Ben@systemverilog.us