Capturing NBA Region values for concurrent assertions

SystemVerilog
,
1

The expressions in concurrent assertions are captured in the preponed region. How do I use the values which get updated later in NBA region.
For example

If “data” changes on posedge of “ready” and I wish to use the updated value of data in my property, how do i do it ? [Refer image]

property check;
 @(posedge ready) disable iff(0)
   (data == 'h1234);
endproperty

Something on these lines, how do I ensure that “data” from NBA region (i.e D1) is checked in the assertion and not from the preponed region (D0)

Screenshot 2025-02-27 at 12.18.34 PM
Screenshot 2025-02-27 at 12.18.34 PM1404×674 50.3 KB

Thanks

2

@Angadp98
Call a subroutine on non-empty match of a sequence which returns the value of the variable of interest

always @(posedge ready)
   data <= <some_expression> ;

function int unsigned subroutine;
  return data;
enfunction

property check;
  int unsigned val;
 @(posedge ready) 
   (1,val = subroutine() ) ##0 (val == 'h1234);
endproperty

Note that RTL , UVM Tb would sample the NBA updated value at the next clock.

3

Thanks this works :)

4

I presumne taht you are using @(posedge ready) to optimize efficiency since ready may noit ocur too ofetn.
To me, this is bad style, and I am not sure it will work well with formal verification. STick the the clocking event as the clock. SystemVerilog is complex enough; it is better IMHO to stick to a consistent set of rules.

1 Like