In reply to ben@SystemVerilog.us:
In reply to MICRO_91:
Comments about the replies:
I see an ambiguity in the requirement sig2 can only be high for one clock cycle while sig1 is high. Does that mean that there ONE sig2 between $rose(sig1) and ($fell(sig1))?
rose(sig1) |-> sig2[->1] ##1 !sig2[*1:] intersect sig1[*1:$];
when the sequence sig2 ##1 !sig2occurs, the consequent is satisfied.
However, it fails to check if sig2 occurs again for one or more cycles when sig1 remains high for more cycles.
How about something like:
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave
module my_module;
bit clk, sig1, sig2;
int pass, fail;
initial forever #1 clk = !clk;
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
#2 @(posedge clk) sig1 <= 1;
repeat(2) @(posedge clk);
sig2 <=1; @(posedge clk) sig2 <= 0;
repeat(2) @(posedge clk);
sig1 <= 0;
#4 $finish;
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
https://rb.gy/f3zhh
Hi Ben.
I think I might miss something with “intersect”. In the below property you gave, Let us say if (sig1 && sig2)[=1] happens at T5 and sig2 drops at T6, !(sig1)[->1] happens at T10. At which point they intersect ?
Thanks
ap_sig1_2: assert property( @(posedge clk)
$rose(sig1) |-> (sig1 && sig2)[=1] intersect
##1 !(sig1)[->1]) pass=pass+1; else fail=fail+1;