In reply to verif_guy12:
The assertion is dependent upon 3 signals and having assertions enabled.
Your signals are
- reset, set to 1. // no issue here as to why assertion is not triggering
- bvalid // Question: Is the value of valid at sampling time ==1?
// It looks like its value is 1, thus antecedent is a match - bresp is !=0 thus expecting a failure
- I assume you do not have an $assertoff or assert control that disables assertions.
If those above conditions are true, then I fail to understand your results.
Maybe the tool you are using has an issue or a limitation as to the number of cycles you can use.
We do not address tools in this forum; talk to you vendor.
Code below works as expected.
module m;
bit clk, reset=1, bvalid;
bit[1:0] bresp=3;
int pass, fail;
initial forever #1 clk = !clk;
property bresp_valid;
@(posedge clk) disable iff(reset==0)
(bvalid) |-> (bresp == 0);
endproperty
VALID_CHK1:assert property(bresp_valid) pass=pass+1; else fail=fail+1;
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) bvalid<=1;
@(posedge clk) bvalid<=0;
repeat(4) @(posedge clk);
@(posedge clk) bvalid<=1;
#2 bvalid<=0;
repeat(4) @(posedge clk);
@(posedge clk) bvalid<=1;
@(posedge clk) bvalid<=0;
repeat(4) @(posedge clk);
$finish;
end
endmodule