Monday, May 24, 2010

NextOp's assertion synthesis and our recent FIFO experience

Based on DVCon 2010 paper on SystemVerilog Assertions - 2009 (see --> Publications) we recently got our FIFO model run through NextOp's BugScope tool. It produced some interesting stuff. The main one I liked is

pop |-> full;

This is an eye opener property - as this should never be the case! But BugScope indeed indicated that we are missing this - either as assert or cover. Obviously this is not a good assert, so when we analyzed deep, it turned out to be a "valid coverage" based on the RTL written. Details at:

So essentially we did have a coverage hole - when that hole is analyzed, we get a design error/bug! What an interesting go-around way of detecting bugs - who cares, as long the bug detection is automatic, it is good!


No comments: