AXI4 bresp Assertion

SystemVerilog
,
1

bresp is 3 in below waveform, but why the below assertion isn’t failing ?

Click Here! for Waveform

property bresp_valid;
 @(posedge clk) disable iff(reset==0) 
 	(bvalid) |-> (bresp == 0);
endproperty

VALID_CHK1:assert property(bresp_valid) else $error("Assertion failed: Write Operation on awaddr = %0h isn't successful", awaddr);

Expectation is that whenever bvalid is detected high, bresp should be 0 at same clk.

2

In reply to verif_guy12:

Are you sure that this is the cycle where you think the assertion passes instead of failing?
Retry the simulation with the following code and traces.


int pass, fail; 
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;

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

or Cohen_Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog

3

In reply to ben@SystemVerilog.us:

I am writing on these registers one after another - awaddr = {1C, 30, 34, 44, 48}
and the bresp for all these writes is 3

Observation after adding above pass/fail variable is that the Assertion only fails for awaddr 1C, 30 and doesn’t pass or fail for other invalid writes (assertion inactive?)

Expectation is that it should fail for all above writes. Please check waveform below and suggest.

Click Here! for Waveform

4

In reply to verif_guy12:

You have 3 signals. Is the reset a logical one?
Otherwise, I have no idea why the assertion is not triggering; it should.
Show a closeup for all the signals at address==34.
ake sure you have pass=pass+1; else fail=fail+1;

5

In reply to ben@SystemVerilog.us:

Reset is declared as logic and it is always high.
Yes, pass and fail are added properly.

int pass, fail;   
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;

Waveform for addr 30
Waveform for addr 34

6

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
7

In reply to ben@SystemVerilog.us:

Thank you Ben. I will debug further with tool vendor.