Counter abstraction for formal verification

SystemVerilog
, ,
1

hi all,
I’m writing assertions for formal verification environment for an arbiter.
The arbitration is between requests that each have a matching priority.
One of the Arbiter’s features is a starvation counter where each request has a counter counting requests that where granted before it, when this counter reaches a predefined threshold, the request priority is internally updated to a higher value.
What I saw up until now is that all assertions around this counter are taking very long or not ending at all (bounded).
In order to reduce run time I want to abstract the counter, the method of abstraction that I found is the following:

  1. disconnect the original counter (so it is now free)
  2. constraint the counter to specific values that are interesting.

My questions are:

  1. I do not want to “disconnect” the internal counter, is there a different abstraction method?
  2. would building an FSM with the counter values do any good (reduce run time)? or is this saying the same thing differently?
    e.g. FSM:

logic [15:0] threshold;
logic [ALL_REQUEST][1:0] counter_stat;
....
if(starvation_counter[0]==0)
    counter_stat[0] = 0;
 if(starvation_counter[0]==threshold-1)
    counter_stat[0] = 1;
if(starvation_counter[0]>=threshold)
    counter_stat[0] = 2;
....
proprty prio_update;
   counter_stat[0]==2 |-> priority == original_priority+1;
endproperty
...

thanks!

2

In reply to gidon:

  1. General comments: Verilog has strict rules on arithmetic. From my Real Chip book"
    Decimal numbers are signed. Based-numbers (e.g., 4’h21) are unsigned. An UNSIZED value (e.g., 'h5) is 32 bits. Unsized unsigned constants, where the high order bit is unknown (e.g., X or x) or tri-state (Z or z), are extended to the size of the expression containing the constant. If the size of the unsigned number is smaller than the size specified for the constant (e.g. intA32bits = 'hF;), the unsigned number is padded to the left with zeros (e.g., intA32bits = 32’h0000_000F;). If the leftmost bit in the unsigned number is an x or a z, then an x or a z is used to pad to the left respectively. These concepts are demonstrated in Figure 6.2.1.1-1 and 6.2.1.1-2.
    Bottom line: When adding or subtracting a 1, use 1’b1 instead of 1; it’s safer and you don’t have to figure out which arithmetic is needed.
    Thus,
if(starvation_counter[0]==threshold-1'b1) // <<<------
    counter_stat[0] = 1'b1;
if(starvation_counter[0]>=threshold)
    counter_stat[0] = 2'b10;
....
proprty prio_update;
   counter_stat[0]==2'b10 |-> priority == original_priority+1'b1;
endproperty

1000×613 51.8 KB

Contact your formal verification vendor as he may help you figure out your issue. Vendors tend to be very knowledgeable and can be of great help for your particular design.
Do try the 1’b1 instead f 1 first, it may not help, but if the arithmetic is not interpreted correctly, that may solve the issue. Anyway, keep good practices.

Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home

  1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
  2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
  3. “Using SVA for scoreboarding and TB designs”
    http://systemverilog.us/papers/sva4scoreboarding.pdf
  4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
    https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
  5. SVA in a UVM Class-based Environment
    https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
3

In reply to ben@SystemVerilog.us:
hi Ben,
thank you for the comments.
To my understanding abstraction (of counters , memories etc.) is a general methodology and not vendor specific.
I was wondering what is the efficient way to do this?

4

In reply to gidon:

Your formal verification vendor can explain why the analysis is very slow; they can give you guidance on how to speed things up.
Ben systemverilog.us