A Unified Sequential Equivalence Checking Methodology to Verify RTL Designs with High-Level Functional and Protocol Specification Models

Digital application complexity has steadily made it harder to discover and debug behavioral inconsistencies at register transfer level (RTL). Aiming to bring a solution, several techniques have appeared as alternatives to verify that a circuit description meets the requirements of its corresponding functional specification. Simulation-based verification is still far from reaching high state coverage because of cycle-accurate slowness. Formal approaches are exhaustive in theory, but due to computational limitations, workarounds must always be adopted to check only a portion of the design at a time. Bounded model checking is one of the most popular formal methods; however, a strong disadvantage resides in defining and determining the quality of the set of properties to verify. Sequential equivalence checking is also an effective alternative, but it can only be applied between circuit descriptions where a one-to-one correspondence for states and memory elements is expected. This paper presents a formal methodology to verify RTL descriptions through direct comparison with: 1) a high-level reference model and 2) a protocol reference model. Thus, it is possible to verify behavioral and interface protocol separately. Complete sequences of states are extracted from the reference models and the RTL design, and compared to determine if the design implementation is correct. The natural discrepancies between the models and RTL code are considered, including non-matching interface and memory elements, state mapping, and process concurrency. The validity of the methodology is formally justified and a related tool was developed to show, through examples, that the approach may be applied on real designs.