Can anyone give some idea on $past use in SVA?

Hi all,

I’m new to System Verilog Assertions concept, so i’m in learning stage of SVA.

I know the functionality of @past(,).
I mean in this case “a|-> ($past(b,2) == 1)” , ‘b’ should be high for 2 clock cycles before assertion of ‘a’.

but still I have one query on $past() operation in SVA.

Here is my code:


module asrt_exmpl();

bit a,b, clk;

initial clk=1;

always
#5 clk = ~ clk;

initial begin
a=0; b=1;
#10 a=0;
#20 a=1;b=1;
#10 a=1;b=0;
#10 b=1;a=1;

end

initial begin
$dumpfile(“dump.vcd”);
$dumpvars;
#100 $finish();
end

property past_p;
@(posedge clk) a|-> ($past(b,2) == 1);
endproperty

past_p_check: assert property (past_p);
endmodule


Simulation Result:

“testbench.sv”, 34: asrt_exmpl.past_p_check: started at 70ns failed at 70ns
Offending ‘($past(b, 2) == 1)’
$finish called from file “testbench.sv”, line 25.

As per the definition of $past(variable/signal, no.of cycles), the simulator is giving correct result only. I Mean the above result is correct, because @70ns assertion is not valid so for this reason it is throwing an assertion failure error .

but my query is @60 ns the value of ‘a’ is high, but ‘b’ is not high for two clock cycles before @60ns(means @40 it is high, @50 it is low). It is high only for one cycle.

@60ns it is not meeting this condition “a|-> ($past(b,2) == 1)”, so simulator should throw an assertion failure error right? but it is not giving such kind of error.

Could anyone of you kindly clarify my question.

Thanks & Regards,
Prathyusha

In reply to prathyushaGadanchi:

The simulator is working correctly for the cycles.
@60ns it IS meeting this condition “a|-> ($past(b,2) == 1)”, and the assertion succeeds.
Your testbench is very poorly written. Many comments:

  1. @(posedge clk) a|-> ($past(b,2) == 1);
    $past of samples before the 2nd cycle are not reliable because the $past(b,1) and $past(b,2) are the initial values of b. In general, if you care about the initial cycles, use
    @(posedge clk) ##2 a|-> ($past(b,2) == 1); //##2 because the past is for 2 cycles
  2. Consider using $rose(a) instead of “a”
  3. For directed tests, use hold times if you insist on using the blocking assignments. Thus,

initial begin
a=0; b=1;
#13 a=0;
#23 a=1;b=1;
#13 a=1;b=0;
#13 b=1;a=1;
end  
  1. In general, it is better (for style) to use clocking delays as nonblocking assignments

initial begin
@(posedge clk)  a<=0; b<=1;
repeat(2) @(posedge clk);
a<=1; b<=1;
@(posedge clk) b <= 0;
@(posedge clk) a<=1; b<=1;
end  
  1. However, I generally DO NOT like directed tests for testbenches as they are very tedious.
    In my book, and in the models I display in this forum, I use constrained-random tests. Here is an example, you need to tune the constraints as needed:

initial begin
bit va, vb;
repeat(200) begin
@(posedge clk);
if (!randomize(va, vb)  with
{ va dist {1'b1:=1, 1'b0:=3};
vb dist {1'b1:=1, 1'b0:=2};
})  `uvm_fatal("RAND", "This is a randomize error")
#1; a <= va;
b <= vb;
end
$stop;
end  

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr


  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy