Viewpoint: Formal verification with constraints - It doesn't have to be like tightrope walking

Krishna Balachandran, Synopsys 
eetimes.com (02/02/2010 8:09 AM EST)

Introduction

The relentless increase in the number of transistors integrated on a single chip continues to take its toll on verification teams. Market pressures squeeze product development times, leaving little room for error.

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.

Click here to read more ...