Formal verification allows engineers to employ mathematical methods to catch bugs in the RTL description of designs at an early stage in the development process.
Formal verification tools find bugs by taking the RTL description and comparing it with an abstract, formal description of the design behavior, derived from the specification.
SystemVerilog Assertions (SVA) is widely used to create the abstract, formal description of the expected functionality of the design. SVA is a powerful tool to describe the properties of a design. However, wrong usage can lead to inefficiency or false positives. In this post we will present common pitfalls during the assertion creation.
Pitfall No. 1: Implication Chaining
Implication chaining means that a property contains more than one implication operator.
Consider the following example:
request |-> ##1 grant |-> ##1 !grant
It may seem like this property checks at first that the grant is asserted one cycle after the request and secondly checks that when grant is asserted it will be deasserted in the next cycle. However, when we transform the simplified implication sequence to logic, we obtain:
X |-> Y |-> Z = !X || (!Y || Z) = !X || !Y || Z = !(X && Y) || Z = (X && Y) |-> Z
So we get:
request |-> ##1 grant |-> ##1 !grant = request ##1 grant |-> ##1 !grant
This means that there is only one check performed. The recommended example is, therefore:
request ##1 grant |-> ##1 !grant
Pitfall No. 2: Inverted Properties
In an inverted property the antecedent contains primary outputs of the design, and the consequent contains primary inputs of the design.
Consider the following example for an arbiter:
!grant |-> $past(!request)
With this property, the formal tool will check that when the design doesn’t send out a grant, then it cannot have received a request in the previous cycle.
To understand such a property must derive the expected input sequence based on observed output behavior which requires you to traverse backward through the design logic and time.
This is very error-prone for complex properties leading to overlooked verification gaps. The recommended example is:
!request |-> ##1 !grant
Pitfall No. 3: AIP Explosion
AIP (Assertion IP) explosion happens when the number of proofs increase when the parameter in the design changes.
Consider the following example: an array of struct variable is declared as
req_type_t request[PARAM],
and an assertion is added to the property suite as following: verifying that the member variable “mem” for each element in the struct is never assigned value 0.
generate for(i=0;i<PARAM;i++) begin
assert property (request [i].mem != 0)
end
The number of assertions created is dependent upon the value chosen for the “PARAM”, if it is assigned a value 8,16,512….. etc the no. of assertions would also be 8,16,512…etc. The downside is that it creates a lot of performance overhead from a tool perspective.
The work around is to use the free variable as shown in the example below.
Assume property(free_var < PARAM);
Assert property(request [free_var].mem != 0);
Here in the formal tool GUI, we have only one property and the formal tool ensures to check for all the entries by trying out all the possible values for the free variable in the proof to find a trace or counterexample. Of course, the free variable approach increases the complexity of the formal proof, but this increase might be benign. So, the usage of the free variable should be applied with a caution.
Pitfall No. 4: Almighty Property
One of the largest pitfalls in formal verification is to include too many facets of the design behavior in a single property. This can lead to non-convergent, overly complex assertions that are difficult to understand and to maintain.
Let’s consider the following example of a round robin arbiter:
To prove fair arbitration, we define a sequence. This sequence describes unfair arbitration. Requestor 1 is requesting but does not get the grant while requestor 2 gets a grant 2 times that describes an unfair arbitration and negate it. If the property holds it means that unfair arbitration can never occur and thus proves that the arbitration is fair.
property fair_arbitration(en, requestors, requestor_1, requestor_2, grant);
not(
(requestors[requestor_1] && (requestor_1!=requestor_2)) ##0
(((en && !grant[requestor_1])) throughout (((en && grant[requestor_2]))[->2]))
);
endproperty
This is an almighty property which tries to cover the complete functionality of round robin arbitration. Which often increases the run time of the proof and the complexity results in non-convergence.
Any assertion should only check a specific function of the design. Complex functions should be broken down furthermore.
As following,
!request |-> ##1 !grant, which checks if there is no request then there is no grant.
$onehot0(grant), if there is a grant then it should be for only one requestor or none.
And more such proofs could be added which are simple yet collectively covers the complete functionality.
Pitfall No. 5: Design Reimplementation
When formulating properties, the verification engineer may get tempted to either re-implement the design or copy design code into the property. Both approaches can have severe consequences. Reusing design code for verification allows development faults to remain hidden and reimplementing a design functionality is typically time consuming and can introduce faults to the property suite. In addition to that, both approaches increase the maintenance effort when the design is changed.
Let’s consider a buffer implementation that uses a signal that points to the next free slot in the buffer. When data is written to this buffer slot the value of the pointer signal is incremented by one. The verification engineer might be tempted to reuse this simple computation in their property. However, a functionally equivalent implementation of this buffer could have a pointer signal that is decremented by one. The property using incrementation would fail for such a design which could then start a time intensive debug process whose only result is that the design is bug-free.
It is, therefore, advisable to formulate the properties as abstract as possible. In cases where complex logic is necessary to fully verify a certain design functionality the complexity of the required logic can be significantly reduced by dividing the functionality into their parts, e.g., a part for every element of a switch-case statement, and formulate a property for every part
Pitfall No. 6: Power of two
Parameters and defines allow the design to be configured for several application cases. However, formal verification tools do not support the consideration of all parameters and define values in a single check. The verification engineer must, therefore, select a concrete value for every parameter and define for each formal verification run.
Performing multiple verification runs with a different value selection in each run is highly recommended, because some design faults may only activate for specific parameter or define values.
In the world of digital circuits values equal to a power of two, i.e., 2, 4, 8, 16, etc., are the most popular numbers. This popularity opens the pitfall of selecting only parameter values equal to a power of two numbers. Any design fault that requires, for example, an odd parameter value to activate, would remain undetected.
The formal verification plan should, therefore, contain at least some verification runs with numbers that are not a power of two number. Good numbers are for this task are:
A number equal to 2^n -1
A number equal to 2^n +1
A prime number
The pitfalls presented in this post are just an excerpt of the traps in formal verification where both new and experienced formal verification engineers can fall in.
What experience did you have with formal verification pitfalls?