Hello Dave,
I have referred the above paper and found what I have been looking for, but I couldn't quite get what is being done. Here is the property:
property connect_dly_p (clk, rst, inA, inB,delayC);
@(posedge clk) disable iff (rst)
1’b1 ##delayC 1’b1 |-> (inB == $past(inA,delayC));
endproperty:connect_dly_p
I get that its passing a signal for a delay and checking if the past value of inA and the delayC is equal to inB. Could you tell me how this works and also how do you verify if the signal is getting reflected on inB by using a waveform. also instead of using a fixed delay I want to use a range of delays so could you tell me if that would work here. also I found that
this property would work on only bit type data when I try to pass a stimulus to it so could you tell me how I can use logic or any other data type. This is the stimulus which I'm passing:
module top();
import connection_check::*;
parameter inA_width = 2;
parameter inB_width = 2;
bit [inA_width-1:0]inA = 2'b01;
bit [inB_width-1:0]inB = 2'b01;
parameter min_delay = 0;
parameter max_delay = 8;
logic [min_delay:max_delay] delayC = 1;
bit clk;
bit rst_n = 0;
always
#1 clk= !clk;
sys_conn_check: assert property (connector(clk,rst_n,inA,inB,2))
$display("Assertion Passed at =%0t",$time);
else
$error("connection failed");
initial #50 $finish;
endmodule
The assertions pass when I run them in EDA but when I try to include the waveform I can't see the property being fulfilled. Please let me know if I'm doing it right.
Thank You
