Hi,
I have signal a & b. b should be asserted after 64 cycles or more from the time a is asserted. Below is the assertion i had written but its not working accordingly, Please correct me
property p;
disable iff(rst == 1'b1)
@(posedge clk)
$rose(a) |-> ##[64:$] $rose(b);
endproperty : p
assert property (p);
Thanks
In reply to Anudeep J:
This assertion is not checking the state of ‘b’, within the first 64 cycles.
property p;
disable iff(rst == 1'b1)
@(posedge clk)
$rose(a) |-> !b [*64] ##[0:$] $rose(b);
endproperty : p
assert property (p);
In reply to yourcheers:
I have signal a & b. b should be asserted after 64 cycles or more from the time a is asserted.
Clarification: “b” should not be asserted for 64 cycles after “a” is just asserted.
Also, “b” should not be asserted when “a” is just asserted
property p;
disable iff(rst == 1'b1)
@(posedge clk)
$rose(a) |-> !b [*65] ##[1:$] $rose(b); // 64 + 1 for the current cycle of $rose(a)
endproperty : p
assert property (p);
//Note
$rose(a) |-> ##[64:$] $rose(b);
// after rose(a), for 63 cycles later "b" can be anything
// Starting from cyle 64 and thereon, there must be a "b"
// It is equivalent to
$rose(a) |-> 1'b1[*64] ##[1:$] $rose(b);
//Note: Getting the right number of cycles (63? 64?) try smaller numbers
$rose(a) |-> 1'b1[*2] ##[1:$] $rose(b);
// | | | | |
// a 1
// b 0 0 1 // (a) |-> 1'b1[*2] ##1 $rose(b)
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr