Chipress

In our book “Crack the Hardware Interview: Verification, Implementation, Synthesis and Power”, we discussed Formal Equivalence Verification (FEV). The goal of FEV is to check if two designs, Specification Model (SPEC design) and Implementation Model (IMP design), are equivalent.

There are 2 major applications of FEV in ASIC / digital design flow: Logical Equivalence Check (LEC) and Sequential Equivalence Check (SEC):

1. LEC looks at the external ports and state elements of the two designs, and decides if the IMP design will exhibit the exact same behavior as SPEC design. If operations like retiming are applied to a design, both designs may no longer match in LEC
2. SEC, however, takes timing into account and examines the equivalency of the SPEC and IMP designs over multiple clock cycles

The most popular SEC tools available in the markets are Synopsys VC Formal’s SEQ app, and Cadence Jasper Gold’s SEC app.

Similar to LEC, there are 3 basic steps in SEC:

1. Setup
2. Mapping
3. Compare

In the Setup phase, designers need to instruct the tool which design is SPEC and which is IMP. In addition, designers may also add necessary assumptions to constrain the undriven input behavior.

Using clock gating FV for example, SPEC design will have free running clock, while IMP design will have clock gated when design is idle. Our goal is to prove that the insertion of clock gaters in IMP design does not alter the design behavior.

In the Mapping phase, by default, mappings are auto-generated per hierarchical paths, and all inputs / outputs / flops / latches are auto-mapped. If the hierarchies differ between the two designs, designers may need to specify how SPEC and IMP designs should map with each other.

In clock gating FV, primary inputs are mapped with assumptions, while primary outputs are mapped with assertions. In addition, sequential elements are mapped using “cutpoint IMP”: in IMP design, “cut” each sequential element’s output, and add a pair of assumption and assertion between SPEC and IMP designs for each “cutpoint”.

It is worth pointing out that FPV (Formal Property Check) and SEC treat black boxes differently:

1. In FPV, the FV tool assumes black box outputs can be any values, and propagates these values downstream
2. In SEC, the FV tool assumes black box outputs always match between SPEC and IMP designs, similar to how it treats primary inputs. It additionally checks black box inputs always match between SPEC and IMP designs, similar to how it treats primary outputs

In the Compare phase, the tool honors the assumptions, and checks that the SPEC and IMP designs behave identically cycle by cycle by evaluating the assertions.

In the next post, we will discuss techniques to get us closer to full proofs in SEC flow.