800x100 static WP 3
WP_Term Object
(
    [term_id] => 157
    [name] => EDA
    [slug] => eda
    [term_group] => 0
    [term_taxonomy_id] => 157
    [taxonomy] => category
    [description] => Electronic Design Automation
    [parent] => 0
    [count] => 3886
    [filter] => raw
    [cat_ID] => 157
    [category_count] => 3886
    [category_description] => Electronic Design Automation
    [cat_name] => EDA
    [category_nicename] => eda
    [category_parent] => 0
)

Assertion-based Formal Verification

Assertion-based Formal Verification
by Paul McLellan on 08-05-2011 at 5:34 pm

 Formal verification has grown in importance as designs have grown and it has become necessary to face up to the theoretical impossibility of using simulation to get complete coverage along with the practical impossibility of simulating enough to even get close.

There are a number of solvers for what is called satisfiability (SAT) but these work in a rather rarefied theoretical environment different from the way designers work. So it is necessary to add a modeling layer to connect properties in the designer’s world to the types of equations that the solvers can prove. Some properties require additional logic to be added to the design in order to convert, for example, a temporal property into one that an SAT engine can prove.

The modeling layer takes in the design description, the property/properties to be verified, the initial state of the design and any constraints. It then transforms these into the formal equations required by the SAT solver. The solver attempts to find a “witness” for each property. A witness is a sequence of input vectors that make the property true while satisfying all the constraints.

The SAT solver produces one of 3 outcomes:
[LIST=1]

  • Pass, a witness was found
  • Fail, the solver can prove that no witness can exist
  • Undecided, it couldn’t either find a witness nor prove that one is impossible

    As an aside, formal verification products are quite interesting to sell. Typically, to evaluate them, the customer will have an application engineer run an old design through the tool, one that is already in production. It is interesting when the design promptly fails and a sequence is found that causes the design to do something it shouldn’t. Of course, you don’t tell the customer all the problems, they need to buy the tool to find that out.

    Atrenta’s white papers on formal verification, which go into a lot more detail, are available here.

    Share this post via:

  • Comments

    There are no comments yet.

    You must register or log in to view/post comments.