I recently met a couple of issues when running formality to check equivalence of RTL vs synthesized netlist. I am a RTL designer and I am not a expert of formality tool. In fact the tool is set up by someone else in backend group. But I was asked to debug why the formal check fails.
First issue is formality flags some mismatches but the mismatches are caused by invalid inputs. In other words, some input combinations are not allowed and won’t occur in real design.
Second issue is some design including registers in it are optimized out during synthesis so formality flags unmatched compare points.
To resolve these issues I found I had to learn some basics about formality first.
Formality is to check if a reference design and an implementation design are equivalent or not. Reference design is gold design and in our case it is the RTL. Implementation is the design to be checked and in our case it is the synthesized netlist.
Formality tries to match compare points in two designs first and then check if each compare point is equivalent. A compare point can be
- primary outputs
- sequential elements
- black box input pins
- nets driven by multiple drivers, where at least one driver is a port or black box
Compare points are primarily matched by object names in the designs. If the object names in the designs are different, Formality uses various methods to match up these compare points automatically. You can also manually match these object names when all automatic methods fail.
Formality uses logic cone concept to verify equivalence of compare point. Logic cone starts with compare point. It is an primary output in below example. Logic cone fans backward and terminates at primary inputs and these that Formality uses to create compare points. It is primary inputs in below example. For all logic cone input combinations, Formality check if logic core output, the compare point, is equivalent or not.
In fact, Formality defines two types of design equivalence: design consistency and design equality.
For every input pattern for which the reference design defines a 1 or 0 response, the implementation design gives the same response. If a don’t care (X) condition exists in the reference design, verification passes if there is a 0 or a 1 at the equivalent point in the implementation design.
Includes design consistency with additional requirements. The functions of the implementation and reference designs must be defined for exactly the same set of input patterns. If a don’t care (X) condition in the reference design, verification passes only when there is an X at the equivalent point in the implementation design.
By default, formality uses design consistency mode.
Armed with above knowledge, let’s revisit our two issues.
For the 1st issue that certain input combinations are not allowed, the solution is to set constraint. There are three cases where setting external constraints is important.
In the most common case, your designs are part of a larger design, and the larger design defines the operating environment for the designs under verification. You want to verify the equivalence of the two designs only within the context of this operating environment. By using external constraints to limit the verification to the restricted operating conditions, you can eliminate the false negatives that can arise out of the functions not exercised.
In the second case, one of the designs you want to verify was optimized under the assumption that some control point conditions cannot occur. The states outside the assumed legal values can be true don’t care conditions during optimization. If the equivalent behavior does not occur under these invalid stimulus conditions, false negatives can arise during verification. Setting the external constraints prevents Formality from marking these control points as false negatives under these conditions.
In the third case, you want to constrain the allowed output states for a black box component within the designs being verified. Using external constraints eliminates the false negatives that can arise if the black box component is not constrained to a subset of output state combinations.
Here is how to define an external constraint.
For the 2nd issue that some logic including FFs are synthesized out in netlist, the solution is to remove FFs from compare points.