Assertion doubt

SystemVerilog
,
1 
bit hresp_count_g;

 property  scrub_fabric_error_for_ecc_read;
 int hresp_count;
 @(posedge clk)   disable iff(!rstb) 
 ((scrub_in_progress===1'b1)&&(boot_done_d1===1'b1))&&
 
( (HADDR<=24'hc007d7 && HADDR>=24'hc007b0) ||(HADDR<=24'hc0067f && HADDR>=24'hc0066c) ) 
&&(HTRANS===2'h2)&&(HREADYOUT===1'h1)&&(HREADY===1'h1)&&((HWRITE===1'b0)||(HWRITE===1'b1)) 
|=> ##[1:$] ((HRESP===1'b1))  ##1  (1,hresp_count=1'b1) ##0 (1,assign_to_global_var(hresp_count));                                   
endproperty 
 SCRUB_FABRIC_ERROR_FOR_ECC_READ: assert property(scrub_fabric_error_for_ecc_read)
                       `uvm_info("scrub_fabric_erro_for_ecc  PASS","SCRUB_FABRIC ERROR WILL COME ONLY, IF HRESP ERROR COMES WHILE READING AND WRITING ECC AND CRC REGIONS OF OTP OR SHADOW REGISTERS ",UVM_LOW)  
                                  else 
 `uvm_error("scrub_fabric_error_for_ecc","SCRUB_FABRIC ERROR  WILL COME ONLY, IF HRESP ERROR COMES WHILE READING AND WRITING ECC AND CRC REGIONS OF OTP OR SHADOW REGISTERS ")  

function void assign_to_global_var(bit temp);
           hresp_count_g =temp;
endfunction

/*
my requirement here is - whenever there is read or write for this address(c0066c to c0067f or c007b0 to c007d7),it should check for hresp===1 or not,if hresp is one ,it should make hresp count variable 1;

but when i look into assertion state in wave diagram it enters the active state, if hddr is in given range and htrans is 2 and hready is one and hreadyout is one ,scrub_in_progress is one and boot_done_d1 is one, hwrite =1’b1 or hwrite=1’b0,even though hresp is becoming high after few cycles of this valid transaction,assertion is not entering finished state or property is not evaluated to true .
please help me with this,

thanks in advance.*/

2

In reply to santosh manur:

An assertion of the form

 
a |-> ##[1:$] b;

Can never fail because if “b” is false, other threads of the consequent will be tested.

An assertion of the form

 
a |-> first_match(##[1:$] b) ##0 c;

Will fail with the sequence b ##0 c occurs.

Rethink the assertion.
Ben

3

In reply to ben@SystemVerilog.us:

Can never fail because if “b” is false, other threads of the consequent will be tested.

An assertion of the form

in reply to above answer:when a is true ,it will keep checking for b==1’b1 from next edge to till the end of simulation ,if b never becomes 1 assertion will fail(is this correct or wrong).

my problem is :when a is one, after few clock cycles delay(take it as ##8) b is also becoming one ,in this scenario also assertion is not passing, it should pass in this scenario.

4

In reply to santosh manur:

For consequent that is a sequence to fail at end of simulation, it needs to be identified as “strong”

 a |-> strong(##[1:$] b);

a |-> ##[1:$] b; 
// if a==1 and b==1 8 cycles later
// assertion should pass

Ben systemverilog.us

5

In reply to ben@SystemVerilog.us:

thanks for the reply.

6

Hi,
I have similar requirement like when a is 1 then I need to check for b should be 2 and next throughout simulation next value b should b3 3. If b is 3 after 2 my assertion should fail.
Ex: assert propert @(posedge clk) ((a==1) |-> (b==2) → ([1:$] (c==3) && (c=!2)));
end property
Is this correct or anyother better solution?

7

In reply to murali405:

  • Too many implication operators.
    with ((a==1) |-> (b==2) → ([1:$] (c==3) && (c=!2)));
    if b!= 2, the assertion is vacuous
  • the expression (c==3) && (c!=2), why the !=2, 3 is !=2

 assert propert @(posedge clk) (a==1 |-> ##1 b==2 ##[1:$] c==3);

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

  1. SVA Alternative for Complex Assertions
    Verification Horizons - March 2018 Issue | Verification Academy
  2. SVA: Package for dynamic and range delays and repeats | Verification Academy
  3. SVA in a UVM Class-based Environment
    SVA in a UVM Class-based Environment | Verification Horizons | Verification Academy