User interface
The use of assertions to verify a design’s functionality is, on the face of things, an obvious next step from pure simulation. But adoption of assertion-based verification (ABV) has progressed slowly and this is at least in part a matter of mindset. In a classic simulation scenario, data and/or test vectors simply flow from inputs to outputs and you either get the result you expect or you do not. ABV requires that the assertions must be written to deliberately test given conditions. To use them effectively, the verification engineer must be comfortable with SystemVerilog Assertions (SVAs), and that isn’t always the case.
Such a situation presents an opportunity for an enterprising EDA vendor, and Jasper Design Automation will attempt to fill this gap with a tool it calls ActiveProp property synthesis. ActiveProp can even help experts in SVAs, because it is intended to jump-start and automate the creation of high-quality assertions, a process that takes time even for experts when undertaken in manual fashion.
ActiveProp offers three modes of operation. It can be used in standalone fashion by all design and verification engineers. RTL designers might prefer to use it with Jasper’s ActiveDesign, with which it teams to produce a design-exploration flow to answer “what-if” questions. Verification engineers may want to hitch it up with JasperGold, Jasper’s formal verification tool. In this mode, users can exhaustively prove the generated assertions.
The tool automatically produces properties from three inputs. First, it needs the design RTL. Second, it needs to know “signals” or “points” of interest within the design; these can be at the perimeter of blocks or internal to the blocks. And lastly, it needs simulation data. The tool can leverage any form of simulation, reusing testbench waveforms. This can be block-level, full-SoC (system-on-a-chip) level, or system-level simulation.
Armed with this information, ActiveProp can be run in one of two modes. If you’re part of an organization that keeps big simulation files around, the tool can be run in batch mode to post-process these files. Or it can be linked directly to a live simulation via a programming-language interface in runtime.
What you get at the tool’s output are SVA properties in the form of constraints, assertions, and covers. Special emphasis is placed on providing this output in human-readable format so you can tell what the properties will be looking for. Once they’re in hand, the properties can be reviewed and classified before they are applied by an ABV tool, simulator, emulator, or formal verification.
At this point it’s fair to ask yourself, “What exactly makes for a high-quality SVA property?” That is exactly what makes some verification engineers a bit squeamish about using properties and assertions. Writing good properties requires a good deal of insight into the design’s functionality. ActiveProp helps in this regard by classifying points of interest in the design (items such as counters, finite state machines, and the like) to extract function-specific properties. It extracts critical expressions from the design RTL to guide, simplify, and merge the resulting properties. The result is fewer but truly functional properties; the low-level, non-essential ones that just clutter things up are weeded out.
Not only are the properties created with insight, but they actually learn and become more effective with multiple simulation runs. Over the course of several runs, ActiveProp refines the properties. Users can take a snapshot of the generated properties and compare them to the refined versions later.
The tool’s user interface (see the figure) displays a full list of points of interest within the design and the properties that have been created. Properties are identified as “candidates;” the user chooses which ones to actually use in verification. Properties that are in red are related to coverage holes.
ActiveProp is useful enough in a standalone flow but it really shines when used in combination with Jasper’s existing JasperGold and ActiveDesign tools. With either of those tools, users can open the waveforms that result from properties. JasperGold can prove the properties’ mettle. If they’re found to be good, they can be published directly as SystemVerilog Assertions for use in simulation.