Six quick videos introduce key formal verification concepts
Synopsys has finalised a set of six short (around five minutes each) YouTube videos introducing key concepts in formal verification.
The series, dubbed ‘Casual is the New Formal’, is hosted by Dan Benua and Xiaolin Chen of Synopsys’ verification group.
Introduction
In the first video, the hosts discuss how to plan a formal verification project, developing assertions, debugging failures, and solving difficult properties.
They talk about how to develop formal verification objectives from your design’s structure and specification, and the importance of choosing the right tools and techniques for the particular blocks you are trying to verify. They also offer insights into how to get started with formal verification. Pro tip – start with a small block and use it to understand the whole process, from setting objectives to achieving sign-off.
Bringing up your design
The second video sees Benua and Chen discussing how to bring your design up in formal tools and initialise it properly. They include tips for handling blocks of your simulation code, such as diagnostic monitors, that aren’t intended for implementation and which would therefore not make sense in a formal verification context. They offer insights into configuring clock and reset signals, and why it is important to do this correctly – and go on to discuss some of the challenges of applying formal techniques to large designs with many, truly asynchronous clocks.
They conclude with a discussion about the importance of resetting your design correctly before you start the formal verification process – and the perils of achieving false property proofs if your reset state is too narrowly defined.
Setting constraints
The third video narrows the discussion to formal constraints, which can be used to express assumptions about how a design’s inputs are expected to behave. Setting the correct assumptions, for example by excluding combinations of inputs that would never happen in the real world, can help avoid false property failures during the formal verification process. There’s also advice about how to set correct assumptions, and striking the difficult balance between having too many and too few constraints. You’ll also find out what a ‘vacuous proof’ is, why you should avoid them in your verification strategy – and the value of coverage analysis in developing a clean set of constraints.
Developing properties
In video number four, Benua and Chen talk about developing properties for use in formal verification. They discuss three basic sources of such properties, the use of prepackaged assertion libraries, and introduces the role of SystemVerilog Assertions. There’s also advice on various approaches to debugging assertions, and the use of small test-benches to “check the checkers”. As Chen says: “Your formal results are only valid if your assertions are accurate.”
Interpreting your results
In the penultimate video in the series, the hosts talk about how to interpret the results of a formal verification run, and what to do when the answer isn’t a series of property proofs but a falsified result and a related counter-example waveform. This implies that a set of stimuli met all the constraints you set, but still caused a property check to fail, and leads to a debug cycle in which you must explore whether the issue is an error in your constraints, in the property you were checking – or in the design. Benua and Chen also discuss what a ‘bounded proof’ means, and how you should interpret it, as well as how to respond to an ‘inconclusive’ result.
Knowing when enough is enough
In the last video of the six, the hosts discuss the knotty problem of knowing when a formal verification strategy has been completed. They describe metrics such as ‘cone of influence’ analysis, measurements of the sequential distance between a property and the part of a design where there is an issue, and abstraction coverage. There’s also a discussion of cover properties, which tell you whether certain design states can be reached, and so can help you find bugs either in your design or your formal environment.
