( ESNUG 440 Item 10 ) ------------------------------------------- [03/03/05]
Subject: ( DAC 04 #24 ) Fishtail On NC-Verilog Support and False Paths
> If you use simulation, you need a comprehensive simulation to ensure
> that all scenarios are exercised. In the past Fishtail relied on
> property checking to verify the assertions, and are just now starting
> to consider the simulation flow. We discovered for example that
> their assertions could not be read into NC-Verilog due to incorrect
> delimiters and name conflicts.
>
> - David Vinke of LSI Logic
From: Ajay Daga <ajay=user domain=fishtail-da spot gone>
Hi, John,
We did have a couple of issues related to the import of our assertions
into NC-Verilog. These have since been fixed and we have tested our
2005.01 release for support of NC-Verilog, VCS and ModelSim and found
no issues.
> The software and technology is relatively new so we are concerned
> about incorrect false paths and multi-cycle paths, and we have found
> examples of both. In some cases these were inconsequential, some
> false paths were not paths at all, and some multi-cycle paths were
> really false paths. But Focus did find 2 false paths that were real
> paths that did need to be timed, and several multi-cycle paths that
> were incorrect.
>
> - David Vinke of LSI Logic
Focus MCP generation can be run in one of two modes. In the unbounded
mode we write out those MCPs that are independent of the number of clock
cycles for which we analyzed the design. We are unequivocally sure about
these MCPs and their corresponding assertions will pass when verified
using functional simulation or property checking tools. In the bounded
MCP generation mode, similar to a bounded proof in property checkers, we
write out what we have identified to be an MCP even if we run into a
computational limit and are unable to analyze a design over a sufficient
number of clock cycles. The MCPs generated with bounded MCP generation
are good as long as their assertions are passed by functional simulation
or property checking tools. Our customers tend to use our bounded MCP
generation capability (it's what Dave was using) because significantly
more MCPs are generated in comparison to the unbounded mode and weeding
out the incorrect ones is simple using an assertion-based verification
methodology.
The verification of the timing exceptions we generate is an important
issue to our customers. The guarantee we provide is that it is impossible
for us to generate a bad timing exception whose corresponding assertion is
proven by the functional verification environment used to sign-off on the
RTL. If a customer or evaluator finds otherwise we fix the issue and give
them a free one-year subscription license to our suite of tools. So far,
we haven't needed to.
- Ajay Daga
Fishtail DA, Inc. Lake Oswego, OR
Index
Next->Item
|
|
