Formal verification : The Heartbeat of ASIC Physical Design

 Formal Verification is often referred as "The Heartbeat" of ASIC Physical design. Just as human body, despite having all body parts intact, it cannot function without heartbeat same way   If ASIC design PASSES w.r.t Timing/Physical verification/EMIR checks but Formal verification(Formality) is FAILED , Design is failed to perform as expected ...!!! Hence it is really important to have Formal verification checked at each stages of ASIC Physical design. As Synthesis is the first stage where RTL is converted to synthesized gate-level netlist, it becomes imperative to validate formal verification immediately after   synthesis to ensure design correctness and functionality.

When one design is transformed/optimized, there are some cases when transformed design may not give same functionality as original design due to human errors, improper handling of EDA tool settings, bugs in EDA tools.

Functional verification v/s Formal verification

• Functional verification and Formal verification are two different methodologies in ASIC Physical design.
• Functional verification :
• It verifies if design behaves as intended using wide range of inputs combinations.
• It requires testbench simulation and focuses on Functional correctness of design.
• It generally requires more time as design needs to be verified for all possible combinations of input vectors.
• tools used here : VCS, ModelSim, Questa
• for example, to verify the functionality of 32-bit Multipler ,
• 2^32 * 2^32 = 2^64 combinations are required.
• Lets assume tool takes ~1us for 1 combinations. for 2^64 combinations , it take 2^64 * 1^-6 seconds = ~0.5 million years..!!!!!
• Formal verification : 
• It assumes that reference design (RTL or input gate-level netlist) and mathematically proves that output design (output gate level netlist) have same functionality as input design.
• It doesn't required any testbench simulation as here verification is done using various equivalence techniques. 
• runtime is less compared to Functional verification. also it detects bugs in early in design cycle
• Tools used : Synopsys - Formality, Cadence - Logic equivalence check(LEC) and  JasperGold
• Below are various Formal verification techniques :
• Model checking
• Theorem proving
• equivalence checking
• In this article, will discuss about equivalence checking.

Formal Verification is performed at below stages in ASIC Physical Design cycle:

Logic Equivalence checking 

• Logical equivalence or Formality is used to check the functional equivalence between reference design and modified design. 
• Reference design is also called as Golden design while modified design  is also called as implementation design.
• Below are basic steps involved during Formal verification :

• Design setup :
• tools first collects all the required inputs. below are main inputs required :
• RTL design (Verilog code) -- Reference/Golden design
• gate-level netlist -- modified/implementation design
• Timing libraries 
• Guidance file (optional)
• Guidance file contains the information about optimized registers, registers which got merged or replicated.
• at the end of setup, tool reports the name of black-boxes. it should match in reference and implementation design.
• Concept  of Blackbox...!!
• blackbox is instances whose functionality is unknown. Generally RAM, ROM, Macros or Hard IPs are considered as blockbox.
• input of blockbox are treated as compare points and output of blackbox are treated as primary inputs.
• Mapping :
• In this process, tools automatically maps the elements of reference design to implementation design. 
• Mapping is done based on names, hierarchy and Guidance files.
• user can manually gives the mapping of instance between reference design and implementation design.
• to verify if mapping is done properly or not,  unmatched pointers are checked.
• undriven signals from implementation design  also causes the mapping issues.
• Compare :
• In "Compare" process, tool divides the design into compare points. these compare points are checked in reference and implementation design.
• Concept of Logic Cone ....!!!! : for each compare point, Logic cone is derived. 
• Ideally compare points should be same in reference and implementation design but in some cases it can differ.
• consider below image to understand the compare points and its logic cone.

• In above case, output of FF1/FF2/FF3 are referred as Primary outputs(PO1,PO2,PO3) while input ports are referred as Primary inputs (PI1,PI2)
• Below points are referred as Compare points :
• Primary outputs
• sequential elements
• blackbox input pins
• multi driven nets where at least one driver if part of blackbox
• Primary outputs are compare points of design. and input logic code on each compare points are stops at either Primary inputs or Primary outputs
• for example, for compare point PO2, Logic cone stops at Primary inputs (PI1) and Primary output (PO2)
• for PO3, input is PI2,PO1,PI1
• Once logic cone is identified, some value or vectors are applied at each Primary inputs/Primary outputs and output arrived value is checked at compared point. 
• if same inputs values produces same output value at compare point in reference design and implementation design, verification is PASS.

Techniques to debug Verification Failure

• at the end of Comparison stage, Verification result is reported either as PASS or FAIL.
• I would say, debugging Formal verification is an Art. if you can find the solution instantly while in some case, it required more deep dive analysis,
• If verification is FAIL, below things can be checked first :
• check mapping report for un-matched points.
• verification can also FAIL is design setup is not correct. 
• check if design is linked successfully or not ( missing libraries can cause linking issues) 
• for example, in RTL to Synthesized netlist verification, RTL doesn't contain scan information while netlist contain scan information. 
• In this case, per constant declarations  are required on scan enable signals.
• check if there are any issues reported by tool while loading the "Guidance files". no guidance should be drops.
• if clock gates are replicated in PnR implementation, make sure tool identifies all clock-gates properly. 
• during ECO implementation, like connect/disconnect nets or removing cells, need to be very carful as it can break the Formality. 
• For complex formality failure debugging, it is required to load formality session where both reference design and implementation design is loaded. tools can show the points where values are different between reference design and implementation design. this might give idea for possible cause of failure.
• For design  having combinational loops, in absence of user given cut points tool tries to automatically add cut points in reference and implementation design, if both cut points are not matched, it gates considered as unmatched points and verification might fail.

Please let me know if you have come across any Formal Verification failure and how did you resolved it.