Around 70% of the overall design time and cost is spent on verification and validation. It becomes very important to verify the correctness of the circuits. Modern complex designs contain several hundred million transistors. Verification of such a complex system in a shorter span of time becomes a dominating factor before it goes silicon level. Several Formal Verification methods have been proposed and are under research as an alternative to classical simulation techniques, since it can’t guarantee sufficient coverage of the design. In addition to this simulation is a slow process. Formal Verification (FV) techniques ensure 100% functional correctness and they are more reliable and cost effective, less time consuming. The main concept of FV is not to simulate some vectors, instead prove the functional correctness of a design.
There are different proof methodologies employed, the most common being Equivalence Checking (EC) methodology. The basic methodology used in most of the industry verification tools, known as Binary Decision Diagram (BDD) and Satisfiability (SAT) solvers, come under this category. These traditional methods fail to handle complex circuits efficiently. Hence new trends like SAT based Symbolic Model Checking are emerging which fall under Model Checking (MC) (Also known as Property Checking (PC)) methodology. New techniques like Bounded Model Checking (BMC) based on SAT solvers are promising better efficient methods of Formal Verification. Hybrid Formal Verification methods are under investigation which employs strength of respective Formal Verification models. Each of these methods has their own pros and cons which will be discussed in subsequent articles. The papers I have referred are listed below. For SAT solver related latest developments, [7] is referred and for hybrid Formal Verification methods [6] is referred.
Reference
[2] Rolf Drechsler, Towards Formal Verification on the System Level,
[4] Jawahar Jain, Amit Narayan, M.Fujita, A.Sangiovanni Vincentelli, a survey of techniques for formal verification of combinational circuits, Proceedings of the 1997 International Conference on Computer Design (ICCD '97), IEEE, 1997
No comments:
Post a Comment
Your Comments... (comments are moderated)