Formal verification with constraints — It doesn't have to be like tightrope walking

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.