I want to write an assertion that when sig_b is set, sig_a has been asserted 2, 3 clocks before that and it has been kept asserted until now. Note that sig_a can be asserted regardless of sig_b (it can be asserted by the other events). So, it is not preferable here to write assertion like this: $rose(sig_a) |=> #[2:3] $rose(sig_b).
I am wondering using $past can write it in simpler way. I would like the good way to write it.
Thanks.
In reply to tsb_matumoto:
assert property (@(posedge clk) $rose(a) |-> ($past(b,2)[*2:3])) $info("pass");
else $error("fail");
In reply to dave_59:
assert property (@(posedge clk) $rose(b) |-> ($past(a,2)[*2:3]))
This assertion is missing the current cycle, and the last “a” at t1 in my example below.
The pass/fail flag occurs after the rose(b), which makes it a bit difficult to read.
I took a different approach with support logic to count the number of a’s when a==1, and reset the count when a==0. The assertion then checks that count when rose of b
ap_abc: assert property(@ (posedge clk) $rose(b) |->
a and t_counta.acount>=3 && t_counta.acount <=4)
pass=pass+1; else fail=fail+1;
/* I want to write an assertion that when sig_b is set,
sig_a has been asserted 2, 3 clocks before that and
it has been kept asserted until now.
Note that sig_a can be asserted regardless of sig_b
(it can be asserted by the other events).
So, it is not preferable here to write assertion like this:
$rose(sig_a) |=> #[2:3] $rose(sig_b).
-
I am wondering using $past can write it in simpler way. I would like the good way to write it. */
// assert property (@(posedge clk) $rose(b) |-> ($past(a,2)[*2:3])) $info("pass");
// else $error("fail");
// when sig_b is set, sig_a has been asserted 2 or 3 clocks before that and
// it has been kept asserted until now.
// t 0 1 2 3 4 5 6 7
/* | | | | | | | | | | |
a 0 1 1 1 1
b 0 0 0 0 1
| - - $past(a,2)[*1]
| | - $past(a,2)[*2]
| | | $past(a,2)[*3]) */
// b==1 at t4, $past(a,2)[*1] is a at t2,
// $past(a,2)[*2] is a at t2 and t3
// $past(a,2)[*3] is a at t2 and t3 and t4
// ap_ba: assert property (@(posedge clk) $rose(b) |-> ($past(a,2)[*2:3]))
/* $past(a,2)[*2:3] is equivalent to
$past(a,2) ##1 $past(a,2) or $past(a,2) ##1 $past(a,2) ##1 $past(a,2) */
module m;
//`include "uvm_macros.svh" import uvm_pkg::*;
bit a, b, clk, rst_n=1;
int pass, fail;
initial forever clk = #2 !clk;
always @(posedge clk) begin : t_counta
int acount;
if(!rst_n || a==0) acount<=0;
else if(a) acount<= acount+1;
end
ap_abc: assert property(@ (posedge clk) $rose(b) |->
a and t_counta.acount>=3 && t_counta.acount <=4)
pass=pass+1; else fail=fail+1;
ap_ba: assert property (@(posedge clk) $rose(b) |-> a and ($past(a,2)[*2:3]))
pass=pass+8; else fail=fail+8;
initial begin // The test vector generation
$dumpfile("dump.vcd"); $dumpvars;
repeat (20) begin
@(posedge clk); #1;
if (!randomize(a, b) with {
a dist {1'b1 := 4, 1'b0 := 1};
b dist {1'b1 := 4, 1'b0 := 1};
}) $display("error"); // `uvm_error("MYERR", "This is a randomize error");
end
#20;
$finish;
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
Note: Instead of a counter, you could also use a shift register and $countones to determine the number of counts in the last n bits. Indexing that shift register can also be used for then last n bit or n:m.
Like
In reply to ben@SystemVerilog.us:
Thank you very much. I compared two checker implementations and realized that using the support logic can easily and surely checks what I want to check.