Overview
Compare Point Matching is a step performed during the match phase of an equivalence checking flow used for validating microprocessors and other digital designs. In this step, the equivalence checking tool attempts to map each compare point of a reference (golden) design to its corresponding compare point in the implementation design, so that the two designs can subsequently be checked for logical equivalence at matching boundaries.
A compare point is the output border of a logic cone—a group of logic delimited by registers, ports, or black boxes. For example, in a typical design block the output OUT1 is the compare point of Cone1. After both the reference and implementation versions of the design are read in and segmented into logic cones, compare point matching establishes which cone outputs correspond to one another across the two designs.
Matching Techniques
Two types of compare point matching techniques are used:
- Name-based (non-function) matching – compare points are mapped by matching the names of corresponding signals across the reference and implementation designs. This is the more efficient approach, and the majority of the matching should ideally be completed by name-based methods for good performance.
- Function-based (signature-analysis) matching – compare points are mapped by analyzing the logical signatures (functions) computed by each cone, independent of signal names. This is more computationally expensive and is used as a fallback.
Challenges
The effectiveness of compare point matching depends heavily on the structural similarity between the reference and implementation designs:
- Design transformations can cause significantly fewer cones to be matched by name-based techniques, which slows down match performance. When logic cones are very dissimilar, performance suffers.
- Compare rules can be created to assist name-based techniques, but determining and creating these rules is itself time-consuming.
- Drastically different implementations may not admit any name-based or rule-based mapping at all; in these cases compare points must be manually matched for better performance, or matched using the more costly function-based techniques.
- Certain transformations, such as retiming, can change logic cones so significantly that additional setup is required to successfully verify the designs.
If matching is incomplete or incorrect, downstream equivalence checking may produce false negatives, leading to wasted debug effort on designs that are in reality equivalent. Additional setup—such as manual compare-point mappings or transformation-aware compare rules—is used to guide the tool when automatic matching fails.
Role in Equivalence Checking
Compare point matching is a sub-step of equivalence checking, which is itself used as a formal or semi-formal verification technique for validating that an implementation (e.g., a hand-written RTL design) is functionally equivalent to a golden reference model (e.g., an automatically generated hardware model derived from an Architecture Description Language specification). Other related verification approaches mentioned in the literature include theorem proving for pipelined processors and quantifier-free logic-of-equality-with-uninterpreted-functions techniques for verifying pipelined control circuitry.