Formal methods in verification flow

tblackmore · Posted: Wed Aug 25, 2004 7:40 am **Post subject:**

I fully agree that formally verifying a block does not give 100% confidence that the block is going to function correctly in a system, for the reasons that you give. There are ways to offset these problems, so that the confidence level can approach 100%. However I think that the last three of these issues remain issues for developing block-level testbenches (incompleteness of specs, what to drive and what to check), but now we don't have exhaustivite coverage of the functionality considered.

Formally verifying a chip of 300 blocks would indeed be challenging. But I think the key thing, at least to begin with, is to look among those 300 blocks for likely candidates for formal, or semi-formal, verification. These blocks may be those which have been traditionally problematic, or that are critical to the functioning of the system. In this way the confidence in the correct functioning of these blocks is increased, and hence the confidence in the correct functioning of the chip. This formal or semi-formal verification may augment rather than replace simulation but with a large percentage of chips still needing respins for functional problems it may well be the cheaper option.

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

tblackmore · Posted: Wed Aug 25, 2004 8:57 am **Post subject:**

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

tblackmore · Posted: Wed Aug 25, 2004 10:44 am **Post subject:**

Hi Alexander,

I agree that each block behaving as specified does not on its own ensure correct functionality of a system. However it is necessary to divide a system up into blocks that are manageable by individual designers. It is then necessary to understand the functionality of each of these blocks and how they should communicate. If the block specifications are not correct then it is not only the verification that is meaningless but the whole design process. Of course people have to approach block-level verification intelligently and not just blindly verify to a specification, but satisfy themselves that the specification is sensible. Also, incorrectness in block specifications may be found by verification - for example inconsistencies in two designers' understanding of how their blocks should communicate could be flagged by an assertion (or two) firing during simulation.

In the absence of sufficient specification it may be necessary to extract properties form RTL. In fact for a full formal verification it may be necessary to reverse engineer a complete block into properties, the sum of which describe its functionality (which may be proved by a theorem prover or perhaps just by pencil and paper). If this is necessary then there is all the more need to approach the job intelligently. But working from a good specification is the preferred approach.

I like the idea of formally verifying a high-level model of a system, e.g. to ensure no deadlocks or livelocks exist in the system. Which tools would you recommend for this? What languages do they use? Are you also suggesting that a high-level model could be used to determine suitable places for block boundaries, and which properties these blocks need to satisfy for the correct functioning of the system?

Regards,
Tim.

Editor's note: this topic was split into this topic