NEWS

360 MV Automated Proof-Based SystemVerilog Assertion Debugger


OneSpin's 360 MV proof-based assertion debugger automatically locates the clause and the time point in a SystemVerilog assertion (SVA) that causes the assertion to fail. By significantly reducing the debug effort – often a laborious manual task in other formal verification tools – 360 MV eases and speeds development of the complex assertions used to verify functional requirements and design operations.

When an assertion proof fails, the new debugger generates diagnostic information in the form of a counter-example that shows design behavior that violates the assertion. The counter-example can then be either debugged within the 360 MV environment, or exported to SpringSoft's Verdi™ Debug System or to any other value change dump (VCD) waveform viewer.

Features

The 360 MV debugging environment consists of a structural SVA debugger (shown on the left side of the graphic), a design viewer with multiple views (top right, featuring a temporal fan-in view), and a waveform viewer (bottom right). Together, they afford the high level of observability essential to fast, accurate debug.

The 360 MV Debugger

OneSpin's 360 MV assertion debugger provides the automation and observability essential for fast debug

  • The structural debugger shows a simple example of a failing SVA assertion. The consequent of the assertion consists of six conditions. The debugger highlights the condition that fails, while conditions satisfied by the DUV are not highlighted. The user can inspect the SVA at multiple levels of hierarchy by expanding or collapsing the assertion's sub-expressions. The user simply traces the highlighted path to the failing sub-expression.
  • The design viewer has several views, including hierarchy, source, temporal fan-in and fan-out views.
  • The temporal fan-in view shows a signal's dependencies on other signals through the design hierarchy. The user can expand and collapse the fan-in of signals to trace back every value that influences the suspect signal, with just a few mouse clicks.
  • Each of the three main windows has a context menu that (for example) opens the source code editor on the assertion definition, or jumps to a signal declaration.
  • The user can drag and drop items between the different views to speed design inspection. For example, a signal in the temporal fan-in view can be dragged to the waveform viewer to analyze its temporal behavior over the whole counter-example
  • The debugger dynamically displays value annotations for signals at selected time points in multiple views, for example in the structural debugger and/or in the temporal fan-in view.