Simulation, with its established methodologies, continues to be the verification engineer's workhorse but is no longer the only choice. Simulation relies on testbenches to generate stimulus that in turn finds bugs, but the absence of a bug in simulation is no evidence of design correctness. It simply means that the stimulus needed to expose the bug has not been applied or correctness checks are missing. Unfortunately, bugs may be still lurking in the design.

Desiring additional measures of design confidence, verification teams are increasingly turning to other verification technologies to augment simulation. Formal model checkers have become a good choice for block-level functional verification because they deliver mathematical proofs of correctness without requiring testbench development. However, there is no free lunch here. In order for formal tools to operate, they require two additional inputs: properties that specify the design's intended behavior; and constraints that specify legal input values for the design.

Properly constraining the design's inputs is the key to getting the most out of formal verification. Both over and under-constraining a design can lead to inaccurate results.

Effect of Input Constraints
Formal model checkers prove or falsify properties. Formal tools exhaustively search the design state space to uncover bugs or prove that they don't exist. When a design is under-constrained, illegal inputs can lead to the formal tool exploring illegal design states. The tool may report false bugs, resulting in the verification team spending time pursuing "wild-goose chases". Under-constrained designs can also lead to a false sense of achieving the desired coverage. Over-constraining a design isn't good either — the proofs obtained are not necessarily valid because all legal values of inputs haven't been considered in the formal analysis, and there may be a combination of legal inputs that negates the proofs. As if this is not enough, constraints can conflict with each other, resulting in invalid results.

When developing constraints for a design, an all important question is whether the constraints are just right. This leads to the next question: will my formal tool let me know if I have over or under-constrained my design? Not so obvious, but also something to consider is whether I can intentionally un-constrain or over-constrain my design to derive some benefits?

Constraint best practices
Like nearly everything else in life, writing proper constraints comes with a great deal of practice. However, there are some basic rules to follow that will give you a jump-start.

Although we have discussed constraints on inputs, internal design constraints can be specified too. The first recommendation is to avoid internal constraints and stick to input constraints only. The internal constraints indirectly restrict the behavior of inputs in ways that may not be obvious, making it difficult to validate and debug them.

Constraints are typically written as properties in SystemVerilog Assertions (SVA), which can also act as checkers. It is tempting to write properties that combine constraints on inputs and checkers on outputs. While this is legal code, our second recommendation is to avoid this because the properties may not be solvable due to a design bug causing the output to not behave as expected.

A third recommendation is to avoid writing constraints that attempt to control past signal values because doing so will make it very difficult for even the most advanced formal tools to detect and debug constraint conflicts.

Finally, if there are constraints that imply an additional constraint, it is better to make explicit the implied constraint. Failure to do so may have unintended consequences because it is not clear what the formal tool will infer from the missing constraint.
Have I fallen off the tightrope?
How much a formal tool can help to ensure you have correct constraints depends on the type of formal tool you deploy. When line, condition, toggle and finite state machine (FSM) coverage are turned on, formal tools will typically report unreachable states. All reported unreachable coverage targets should be carefully examined for signs of over-constraints. Another way to detect over-constraints is to reuse block-level formal constraints as monitors in a system-level simulation environment and let the simulator run. Constraint assertion failures reported by the simulator at the chip-level may point to over-constraints at the block-level.

Under-constrained designs and those with conflicting constraints are much harder to detect. They require the integration of a simulator with a formal engine, something that is not found in pure formal tools. Hybrid formal tools excel at this task because they have a built-in constraint solver that generates stimuli for the built-in simulator. A careful look at resulting assertion failures or unexpected waveforms may point to under-constrained designs.

Hybrid formal tools can also detect conflicting constraints that pure formal tools may not. Acting in concert with the formal engine's built-in integration with the simulator, the constraint solver reports any set of constraints it fails to solve and also points to the cycle in the simulation where the conflict can't be resolved. This is extremely useful in debugging and correcting the constraints. On the other hand, a pure formal tool may make some implicit assumptions to solve the constraints, thereby masking a real problem.

Playing the constraint balancing act
Sometimes un-constraining or over-constraining a design can have its advantages.

Intentionally un-constraining a design to find proofs is a valid methodology because the proof will always hold true. Careful examination of any falsifications resulting from the formal run will determine if these are real design bugs. A falsification not caused by a bug reveals an under-constrained design to which constraints can then be added in an incremental fashion. This method of developing constraints for a design has the advantage of minimizing set-up time for a formal tool.

Intentional over-constraining can also be an effective way to find bugs because these bugs will certainly appear even when the constraints are relaxed. Another benefit of over-constraining is that it reduces the state space for a formal tool, thus improving run-time performance. However, proofs obtained in this way must be carefully qualified because they may not hold true when properly constrained.

Conclusion
Formal model checkers are indispensable, complementing simulation for block-level verification in an ever-challenging design environment. Constraints make a formal tool tick. Too-few, too-many, or incorrect constraints, and your formal verification results can't be relied upon. Following recommended best-practices, constraint writing for formal tools can be reduced to a science. Pure formal tools may fail to detect improperly constrained designs and may mask real design issues. Hybrid formal tools come to the rescue and eliminate the tightrope walking often associated with formal verification with constraints.

About the author:
Krishna Balachandran is director of verification marketing at Synopsys. He holds a master's degree in computer engineering from the University of Louisiana and completed the executive MBA certification program at Stanford University.