How to write an assertion for following case-
There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
clk is same for a, b.
Any alternative to assertion will also be helpful.
In reply to verif4life:
As an educator, I am reluctant to answer what you can easily write yourself and learn something in the process. Thus, I suggest that you look into 1800’2017: 16.13.1 Multiclocked sequences. Your requirements are a simple application of that along with the use of the implication operator (|->).
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Hi Ben,
This is working in my case.
Can you please check this.
Additionally can you give any way to implement this without assertions.For checking signal fell it checks on two consecutive clock edges, for signal ‘a’ in my case it is two consecutive negedge, by the time I get a 2nd negedge my signal b falls at posedge. so I am not getting when to start the check on signal b
// There are 2 signals a, b. Signal a is synchronous to negedge of clk and Signal b synchronous to posedge of clk.
//Whenever signal a falls at a negedge of clk, at the immediate following posedge of clk,signal b should fall.
//clk is same for a, b.
ap_arbiter: assert property(first_match(@(negedge clk) $fell (a)) |-> (@(posedge clk) $fell (b)))
$display ("Assertion passed",$time);
else $display ("Assertion failed",$time);
Thanks for your reply. It is working.
Can you provide a way so that it does not throw an error for the first clock edge??
Here the clock starts after power on reset so cannot use disable iff (rst)… and default value of signal is x and sampled value at first clocking event is 0. So $fell will be true and hence the antecedent…
Also cannot change signal ‘a’ to bit type because it is an internal DUT signal… is it good way to take variable in assertion interface as bit type so that it would be automatically typecast x, z to 0???