Path: EDN Asia >> Design Centre >> IC/Board/Systems Design >> Formal property verification: Grasping constraints
IC/Board/Systems Design Share print

Formal property verification: Grasping constraints

17 Feb 2016  | Anders Nordstrom

Share this page with your friends

Formal coverage analysis
The most effective method to detect an over-constrained environment is to use formal coverage analysis (FCA). FCA uses simulation-type coverage goals such as line, expression, toggle, and FSM coverage to determine which parts of the design are reachable. This is similar to the use of coverage in simulation, where you track and measure which lines and expressions have been executed or reached by the set of test cases. If a line of code is not reached in simulation, it may be because a test has not yet been written, or constrained-random simulation didn't run long enough to reach it. Or, it may simply be impossible to reach a particular line of code.

Some parts of the design may be unreachable regardless of the constraints. The structure of the RTL may prevent some lines from being reached. For example:
if (A && B)

data <= 32'hdeadbeef;

if (!B)

data <=32'h00000000;
The assignment
data <= 32'b00000000;
will never be executed in simulation and is unreachable in formal analysis because it is impossible to reach it. If (A && B) is true, !B cannot be true at the same time. This means that it is necessary to first find the coverage goals that are structurally unreachable so they can be distinguished from goals that are unreachable because of constraints.

If a design is over-constrained, it means part of it is structurally reachable, yet still unreachable because of the constraints. This can be detected by FCA. Any line, expression, toggle, or FSM coverage goal that is unreachable in the presence of constraints but is reachable when no constraints are applied is a potential problem due to over-constraining. The designer needs to determine if the over-constraining in each case is intended or harmless, or if it needs to be addressed and constraints changed.

For example, if we have the constraint and finite-state machine:
assume always @(posedge clk) B <= 4'b5;

case (state)

IDLE: begin if (B == 0) next_state <= ACTIVE;


ACTIVE: begin if (B<= 4'b6) next_state <= ACTIVE;


else next_state <= END;


END: begin next_state <= IDLE;


The state END will never be reached because of the constraint, and we have an over-constrained environment. The FSM coverage and line coverage goal will fail for the state END.

Constraints are needed for FPV since they ensure that only legal input values are used. Care must be taken when creating constraints to avoid over-constraining as this may hide bugs in the design because some parts of the design are not explored. Several methods exist to aid in the detection of this situation, and are an important part of the methodology when adopting FPV on a project. FCA is the most effective method to detect an over-constrained environment. It does not rely on the user to write checks, and hence is straightforward to adopt, and is more complete. Proper and intelligent selection and creation of constraints will ensure that the FPV flow is both effective and efficient.

About the author
Anders Nordstrom is a senior corporate applications engineer in Synopsys' Verification Group working on formal methodology and features on the VC Formal tool. He has 20 years' experience of assertion based verification and formal property verification both from EDA and as a verification engineer.

 First Page Previous Page 1 • 2 • 3

Want to more of this to be delivered to you for FREE?

Subscribe to EDN Asia alerts and receive the latest design ideas and product news in your inbox.

Got to make sure you're not a robot. Please enter the code displayed on the right.

Time to activate your subscription - it's easy!

We have sent an activate request to your registerd e-email. Simply click on the link to activate your subscription.

We're doing this to protect your privacy and ensure you successfully receive your e-mail alerts.

Add New Comment
Visitor (To avoid code verification, simply login or register with us. It is fast and free!)
*Verify code:
Tech Impact

Regional Roundup
Control this smart glass with the blink of an eye
K-Glass 2 detects users' eye movements to point the cursor to recognise computer icons or objects in the Internet, and uses winks for commands. The researchers call this interface the "i-Mouse."

GlobalFoundries extends grants to Singapore students
ARM, Tencent Games team up to improve mobile gaming

News | Products | Design Features | Regional Roundup | Tech Impact