Functional verification of complete sequential behaviors: A formal treatment of discrepancies between system-level and RTL descriptions

Formal techniques allow exhaustive verification on circuit design (at least in theory), but due to actual computational limitations, workarounds must always be adopted to check only a portion of the design at a time. Sequential equivalence checking is an effective approach, but it can only be applied between circuit descriptions where a one-to-one correspondence for states, as well as for memory elements, is expected. This paper presents a formal methodology to verify RTL descriptions through direct comparison with high-level reference models. By doing so, there is no need to specify or analyze formal properties, as the complete behavior is already contained in the reference model. We also consider the natural discrepancies between system level and RTL code, including non-matching interface and memory elements, and state mapping. In this manner, we are able to prove the functional coherence for the overall sequential behavior of the design under verification.