Janus: A novel use of Formal Verification for targeted behavioral equivalence

We present a novel way of using a formal verification (FV) framework to establish targeted behavioral equivalence between two similar designs. The new verification framework is generic and can be applied to a wide range of behavioral equivalence problems, such as ensuring late logic changes preserve earlier design intent and do not introduce new flaws. The new framework analyzes two similar designs that may have significant microarchitectural, implementation, or behavioral differences between them. If there is a targeted set of behaviors that are required to be preserved between these two designs, then the verification framework can be used to establish the behavioral equivalence. The new framework combines the strengths of FV and the formal equivalence verification (FEV) flows in a fully automated method to establish the behavioral equivalence. This method was used on one of the next generation Intel^reg microprocessor to verify that design changes for a new microarchitecture feature did not create flaws or unintended behaviors (no-harm) in other parts of the design when that feature was disabled. Three complex design flaws (bugs) were found during the process. After the framework was developed, the verification effort took less than two weeks to complete which was dramatically less effort than if we had used traditional validation methods.