Assertion-based emulation
Combining assertion-based verification techniques with emulation makes for easier debug, better coverage and greater functional efficiency.
Today’s SoCs must include ever more features and meet shorter tape-out schedules. Verifying their functional correctness is a growing challenge. Even with more than 70% of the overall design effort spent on verification, research suggests that few designs achieve first-time silicon success.
Design houses are therefore adopting various verification methodologies to reduce cycle time and enhance productivity. Most include the definition and capture of verification closure criteria with progress then measured using key verification coverage metrics. Assertion-based verification (ABV) is one of the most popular examples.
ABV checks the functional correctness of designs, provides valuable coverage feedback and increases debug productivity. ABV is flexible so that all users (be they designers, verification specialists, and/or architects) can write assertions during most stages of design development. RTL designers can write assertions as soon as they start writing code; verification engineers can write assertions as they develop the verification environment; and architects can write assertions during system-level verification.
As ABV has been refined, it has been increasingly used in combination with emulation. This article reviews both techniques and their use together. We look at how Veloce assertion synthesis improves the emulation of SoCs that include assertions and helps reduce the time to verification closure. The Veloce compiler synthesizes logic for the assertions along with the design-under-test (DUT) and then maps them into an emulator, making emulation faster.
Assertion-based verification
ABV uses assertions to capture a design’s functionality. Users then verify that a design correctly implements that functionality through the simulation, formal verification or emulation of those assertions. Assertions provide the following major benefits:
- They detect errors at the source, greatly aiding debug.
- They isolate issues inside the design and at the interfaces (block and system level).
- They are reusable from block to system level, reducing development and debug time.
- They provide coverage feedback so you can monitor verification progress.
- They can be used during formal verification, simulation and emulation.
An ABV methodology establishes a unified flow to uncover IP issues at the IP, subsystem, and system levels. IP sources can be both external and internal. Assertions become an effective means of transferring knowledge between various teams. Assertions that are embedded inside the design improve the controllability and visibility of the RTL and make it easier to debug and isolate software or RTL bugs at the system level.
ABV then plays an important role in low-power verification. The increasing popularity of power formats such as UPF and CPF has resulted in more users realizing power intent schemes and RTL code independently and in parallel. Assertions are a useful means of debugging and isolating issues here such as missing isolation and retention cells, especially when the power scheme is still unproven and in development. Furthermore, assertion-derived coverage information provides a measure of how many power domains are truly being exercised during low-power verification.
Let’s look at the various levels of abstraction at which assertions can be specified, their use at those levels and then as a design progresses.
Design IP level
Assertions can be written during RTL development by design engineers. A good example would be assertions that check FIFO underflow and overflow (Figure 1). The main advantage of assertions here is that they allow design failures to be detected at source: there is then no need for error propagation to an external environment through design ports. IP-level assertions can be delivered and reused with the IP during block, subsystem and SoC level verification. These assertions help save time in debug by isolating verification and design issues even as a design environment becomes larger and more complex.
Figure 1 FIFO underflow and overflow condition checks (Source: Mentor Graphics)
IP interface level
Assertions can be written at the IP or block-level interface. A good example here would be assertions that address communication between two blocks (Figure 2). These can work as checkers and monitors to ensure that the traffic and responses generated by the IP match the specification. They can be developed by engineers who understand the IP and IP interface specifications but who do not have internal development details. Assertions developed at the IP interface are easily migrated from IP to subsystem or SoC levels. Again this saves time isolating and debugging issues that can arise when IPs are integrated within complex SoC environments.
Figure 2 Interface-level communication between two blocks (Source: Mentor Graphics)
Protocol level
Assertions can be written by vendors and standards groups who have expertise in specific domains and then delivered to end-users in the form of libraries. For example, such libraries already exist for standard protocols such as AMBA, USB, SATA, and PCIe. Library development supports the reuse of assertions across various teams, groups, and organizations. It also helps reduce learning and development time. Such assertion libraries (sometimes called ‘protocol monitors’) are easy to use and help isolate issues for complex protocols.
System level
Assertions can be written for system level scenarios. Here an example might user assertions to track specific protocol packet generation by an IP block upon a request from a processor. Such assertions are application-specific and are written to isolate bugs during system-level verification during the latter stages of a project. They are written by system architects who understand the specification and save a lot of effort when application scenarios are being debugged.
Emulation
Emulators allow users to verify multi-million gate designs against real-world scenarios and find bugs that would be impractical to detect using much slower simulator technologies. Their speed advantage over simulators is also extremely useful where a design needs to undergo lengthy and detailed system-level tests.
Here are some important verification activities supported by emulation:
- Functional coverage
- Assertions
- Low power verification
- Peak power numbers
- Average power calculation
- Virtual transaction library
The market-leading emulator is Veloce from Mentor Graphics, and I will use it as an example to now describe the advantages of using ABV in combination with emulation. To do this, we first need to note some specific qualities of the Veloce emulator.
Apart from its capacity and practical value for debug, Veloce’s architecture gives users the flexibility to build testbench verification environments using hardware stimulus, software stimulus, or a combination of the two.
Because Veloce is standards compliant, it fosters interoperability with software simulators. It accurately models the user’s design into the emulator, irrespective of whether it is a single- or a multi-clock domain design.
Finally, its dedicated debug/visibility infrastructure and simulation-like debug environment make Veloce easy-to-use.
Assertions integrated with emulation
The Veloce emulation family includes an integrated compiler that enables emulation’s seamless combination with ABV techniques at all levels: design IP, interfaces, protocols, and system. This integrated use-model (Figure 3) is closely aligned with the simulation use-model. Important features these models share include:
- There is an integrated compiler for the native compilation of assertions – no additional steps are required beyond normal Veloce compilation.
- Assertions are synthesized onto the emulator along with the design.
- Runtime control allows the user to disable or enable assertions, and change the severity of assertions
- There is a runtime assertion report generation for post processing
- Waveform-based assertion debug is available.
- Coverage reports are produced for assessing verification completeness and verification closure.
- Assertions in SVA, PSL, and OVL are all supported.
Figure 3 The assertion-based emulation flow (Source: Mentor Graphics)
Design analysis/compilation
As noted, assertions can be embedded inside blocks. It is also good practice to write assertions in a separate program and then bind them to a specific module or module instance from a testbench. Figure 4 is an example of how an assertion block can be instantiated using a bind statement:
Figure 4 Assertion block instantiated using ‘bind’ (Source: Mentor Graphics)
Once the assertions are inside the design, the user can begin assertion analysis or compilation. In the Veloce emulation environment, you can enable assertion compiles by using a compiler switch. This allows users to maintain one source for running emulation with or without assertions. Similarly users have access to options that allow for the finer control of assertions’ compilation and execution at various stages. Veloce provides useful statistics about assertion metrics after successful compilation of the full design and assertions.
Design run/emulation
After the successful compilation of a design with assertions, the design can be emulated in real-world, long-sequence scenarios. Veloce provides both onscreen messages and text reports with run-time assertion statistics for post processing. Many run-time options are available to handle and control the firing of assertion messages according to the user’s requirements. Finer user-level controls are available to enable and disable various assertions based on module, hierarchy, severity, and other criteria. These run-time controls can be handled directly using command options or various C-APIs provided with the tool.
UCDB generation
The Unified Coverage Interoperability Standard (UCIS) defines a common database — the Unified Coverage Database (UCDB) — for all coverage and assertion data generated by multiple verification tools, including many of those used during simulation, emulation, and formal verification.
Veloce writes assertion coverage information for an emulation run to a UCDB file. This has many advantages. UCDB files can be merged and analyzed using simulation tools. They can also be collected from multiple emulation runs to generate aggregated coverage information. This enables a unified approach to verification in which coverage information from UCDBs generated during various stages of development and using different verification technologies can be merged to generate final coverage statistics and, hence, achieve faster verification closure (Figure 5).
Figure 5 A unified functional coverage environment (Source: Mentor Graphics)
Debug options
Veloce provides various debug options through an assertions GUI (Figure 6) that includes:
- Hierarchy-based assertion tab
- Assertion debug window
- Global assertion table
- Assertion statistics table
- Assertion fire line table
Figure 6 Veloce assertions GUI (Source: Mentor Graphics)
Waveform window
The Veloce waveform GUI allows users to perform any operation on an assertion signal that can be performed on a normal DUT signal. For example, engineers can drag-and-drop assertion signals into the waveform window. This makes debugging more like simulation and easier for verification and design engineers to achieve.
Conclusion
ABV involves the monitoring of activities for functional correctness and provides essential coverage feedback. This approach is proving critical to the success of today’s increasingly complex SoCs. Emulation today can enable the efficient verification of multi-million gate SoCs, and its excellent support of assertions helps design houses quickly realize bug free SoCs.
Veloce specifically also supports UCDB generation, which allows coverage information generated by various teams to be merged, making the entire development flow more productive, more efficient and faster.
About the author
Amit Gupta is a manager at Mentor Graphics, Noida, India.
