I want to write an assertion that when two signals a & b are in sync with each other, that is when both signals rise at the same time then there is a fall of third signal at the same rising edges of former. Moreover all these signals are running at the same single i_clk.
what I have tried is shown below : -
But the problem here is all o_clk_mux_div[a] , o_clk_mux_div[b] rises at the same time and at posedge of i_clk .But I think this is not correct. Can anyone suggest the proper way of writing the above property.
In reply to prashantk:
You will need to explain more how the o_clk’s signals are generated. They will be sampled values from the time before i_clk rises. It would also help if you can explain how you think the results you get from this property to do not match what you want.
But the problem here is all o_clk_mux_div[a] , o_clk_mux_div[b] rises at the same time and at posedge of i_clk .But I think this is not correct.Can anyone suggest the proper way of writing the above property.
Dave is right on the sampling. From what you express, you seem to believe that the PASS or FAILURE should occur in the very time step that @(posedge clk) occurs (i.e., the rose(a); That signal rises after the sampling. Thus, the PASS/FAIL occurs at the next @(posedge clk). Consider this simple example and the results:
import uvm_pkg::*; `include "uvm_macros.svh"
module top;
bit clk, a, b, c, d;
bit clk2;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
always @(clk) #1 clk2=clk;
always @(posedge clk) begin
repeat(2) @(posedge clk);
$display("now= %t", $time);
a <= !a;
b <= !b;
c = !c;
d= !d;
end
ap_abnb: assert property($rose(a) |-> $rose(b)) $display("PASS nb @ %t", $time);
ap_cdb: assert property($rose(c) |-> $rose(d)) $display("PASS b @ %t", $time);
ap_abnb2: assert property(@(posedge clk2) $rose(a) |-> $rose(b)) $display("PASS nb2 @ %t", $time);
ap_cdb2: assert property(@(posedge clk2) $rose(c) |-> $rose(d)) $display("PASS b2 @ %t", $time);
initial begin
repeat(200) @(posedge clk);
$stop;
end
endmodule
// Siumlation results
now= 50
# PASS b2 @ 51 // Notice the clock delay in clk2
# PASS nb2 @ 51
# PASS b @ 70
# PASS nb @ 70
# now= 110
# now= 170
# PASS b2 @ 171
# PASS nb2 @ 171
# PASS b @ 190
# PASS nb @ 190