Moreover, 360 MV’s 4-state analysis does not suffer from the X-optimism that plagues 4-state RTL simulation, which results in incorrect coverage information, potential masking of design bugs and mismatches between RTL and netlist simulation – sources of functional errors that are often extremely challenging and time-consuming to find. OneSpin will show 360 MV’s 4-state formal analysis for the first time in public at a free verification tutorial in Booth #1311 at the Design Automation Conference (DAC) in Anaheim, Calif., June 13-18, 2010.
360 MV’s support of 4-state logic extends the 2-state logic (0,1) commonly used in formal analysis to include X and Z (floating values). 360 MV automatically identifies all design signals that can become X, and enables designers to use X-aware constructs – such as “$isunknown” and “===” – to write simple assertions to fully explore the propagation of X’s through their design. Failing assertions are debugged using 360 MV’s RootCauseAnalyzer environment. Its waveform viewer, SVA debugger, fan-in viewer, RTL value annotation, and driver tracing afford full visibility of X’s and full traceability of X propagation in the design, unlike 2-state formal analysis.
“360 MV allows users to fully exploit the use of X’s for RTL verification and synthesis optimization without the pitfalls and risks of X-related bugs,” Michael Siegel, OneSpin’s VP Product Marketing, explained. “For example, designers can now easily determine whether given registers can safely be left uninitialized – to reduce chip area – without breaking their design. 360 MV ensures the X-robustness of designs before synthesis, saving effort in late gate-level simulation.”