OneSpin Solutions presents recent advances in formal assertion-based verification (ABV) that speed-up verification closure. We present a formal verification methodology called Operational ABV, which simplifies verification planning, eases assertion writing working from timing diagrams and enables an exhaustive formal coverage analysis ensuring that no design behavior is missed during verification. The formal coverage analysis automatically uncovers holes in the verification plan, detects unverified design functionality, and identifies errors and omissions in design specifications. The approach is demonstrated using an AHB2Wishbone bus bridge and OneSpin's 360 MV formal verification tool. We also demonstrate how to prevent X-related bugs through new exhaustive 4-state formal analysis techniques. The use of unknown or undefined values (X's) can improve RTL verification and synthesis. But unintended X-propagation in designs can cause data corruption and breaking of control paths. We show recent enhancement of 360 MV for 4-state-logic formal analysis, where signals can explicitly become X and Z — extending the 0/1-models commonly used in formal verification tools. This X-aware formal analysis enables an exhaustive pre-synthesis X-analysis and X-verification, detecting, e.g., unintended X-propagation caused by uninitialized registers, and ensuring safe use of X's for verification and synthesis optimization in general. Both, Operational ABV with formal coverage analysis and 4-state-logic formal X-analysis enable faster verification closure with significantly higher verification confidence. For more information about OneSpin Solutions and 360 MV please visit http://www.onespin-solutions.com.
展开▼
