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…