Formal Verification - An Overview
Formal verification is a technique used in different stages in ASIC project life cycle like front end verification, Logic Synthesis, Post Routing Checks and also for ECOs. But when you go deep into it, the formal verification used for verifying RTLs is entirely different from others. There are different formal techniques available as follows
- Formal Equivalence Checking
- Formal Property Checking.
Formal Equivalence Checking
Formal Equivalence Checking is a method to find the functional equivalence of one design by comparing with the golden design. These are the areas where equivalence checking is commonly used.
- RTL vs Pre-Routed Netlist
- Pre-Routed Netlist vs Post Routed Netlist
- Netlist Vs ECO-Netlist
Another point to note here is, Equivalence Checking is always carried out using two inputs and result comes out by comparing the functionality of these two input designs. Combinational and sequential equivalence checking are the two methods used nowadays. Combination Equivalence checking is done by making one-to-one mapping of flops between golden design and revised design. But Sequential equivalence checkers can verify structurally different implementations which do not have one-to-one flop mapping.
Major EDA providers in this area are Cadence (Conformal LEC) and Synopsys (Formality).
Formal Property Checking Formal property checking is a method to prove the correctness of design or show root cause of an error by rigorous mathematical procedures. It does not require test benches or stimuli and turnaround time is very less.
Property checking can be carried out by using either using property languages (eg: ITL Interval Language) or Assertion languages (SVA,PSL). SVA is the assertions subset of the System Verilog language. Assertions or properties are primarily used to validate the behaviour of a design and can be checked statically by property checker tool and proves whether or not a design meets its specifications.
A holding SVA/ITL/PSL means that the assertion/property has been formally and exhaustively checked and it holds in all possible traces of the design. A failing SVA/ITL/PSL means that a counterexample was found that represents a violation of the intended design behaviour.
Formal Verification compared with Simulation Even if modern test-bench concepts allow for flexible and efficient modeling and sophisticated coverage analysis, Functional verification by simulation is still incomplete, causes high efforts in test-bench design and consumes a deal in simulator run-time.
Formal methods overcome the insufficiencies of simulation in reliability by proving a design’s behavior and its correct functionality instead of observing selected traces and hunting bugs. They are static and give you 100% coverage. In addition, experience has shown that formal techniques not only improve verification quality, but also can reduce the verification effort and time and also a quick and thorough module verification
Limitations of formal property checking- Formal Methods are limited in complexity, time and gates. There are ways to cope with such issues. But, it makes verification cumbersome and leads to loss of efficiency. And, lowering the level of abstraction too much always holds the risk of rewriting RTL by properties.
Verifying complete transactions, transfers For formal property checking, the behaviours that leads to a certain sequential depth being too large to fit into a single proof window.
Verifying Algorithms Algorithms incorporate sources of complexity issues, e.g. multiplications. Moreover, an algorithm will not be verifiable without breaking it down to single operational parts.
Typical Targets The logics which can be easily verified using formal verification are, Decoders, Arbiters, FIFOs, Stacks, Timer, Counters, Interrupt Control Unit, DMA Controller, hand shaking mechanisms, Bit serial protocol circuits, Error-Recovery,-Detection,-Correction, Processor Pipelines (data sequence management, forwarding, write back), Network-On-Chip (Interconnect System, Bus Bridges, cmd Translation), Connectivity proofs (Test logic wiring, Pad control logic) etc.
Conclusion Formal property checking can be used starting from the RTL development Stage and then to IP verification and finally to SoC integration. It is quite easy for the designers to use it while developing RTL, as it does not require any other testbench environment. The same assertions can be used in the later stage for verification engineers as well. For IP verification, this can used to find corner case bugs which cannot be caught in simulation. In SoC level this is used mainly for connectivity verification and pad multiplexing etc.
Major EDA players in this area are OneSpin Solutions (OneSpin), Cadence (Incisive Formal Verifier) and Jasper. The formal technology is extensively used in the industry now and experience from different projects shown that, this helps you to get bug free silicon.