Subject: Link between coverage and formal tools
From: Alain Raynaud (alain@tensilica.com)
Date: Thu Aug 29 2002 - 11:01:37 PDT
Regarding the coverage API, there is a flow that I have wanted to
establish for a long time, so please tell me if this falls within the
scope of this standard:
From coverage results (for instance expression coverage results), I'd
like to be able to copy the uncovered conditions into a formal property
checker tool, so that I can ask the question: "is this uncovered case
even possible?"
For instance, let's say a coverage tool tells me that for:
assign a = b & c & d;
The case where c=0 and d=1 never occured (that is, c was never
controlling). As it turns out, d itself is defined as a function of c:
assign d = c & e;
Then, by construction of my design, the uncovered case could not have
happened anyway. I have redundant logic (which may or may not be a good
thing to do). But my point is, would a coverage API allow me to extract
a formal expression that I could then send to a formal tool? Very simply
put, if through the API I can only retrieve a line number for an
expression, but not the expression itself, then I can't manage such a
flow. I guess some kind of link into the Verilog *structure* itself is
what I'm looking for. But as you can see from my simple example above,
the expression "c==0 && d==1" does not actually appear in the Verilog
code anywhere.
Thoughts anyone?
Alain Raynaud
Tensilica, Inc.
This archive was generated by hypermail 2b28 : Thu Aug 29 2002 - 11:07:39 PDT