Creating, Simulating, and Debugging SVA Code Outside of the Traditional Design/Verification Environment

By Eric Deal, Robert Biczek (Zocalo Tech)

Overview:

Adding assertions early and throughout the ASIC design cycle is the best way to independently check that design code reflects the intended behavior as specified in design specifications and the verification plan. However, there still exist barriers of limiting Assertion Based Verification (ABV) adoption due to assertion debug and the complexity of the System-Verilog Assertion (SVA) language. As a result the industry hasn't come close to realizing the full benefits of ABV. Zocalo Tech believes the more effective approach is to create an independent environment to debug SVAs before placing them in RTL code. This paper illustrates the design flow and benefits of debugging SVAs outside the RTL environment.

Background:

Adding assertions early and throughout the ASIC design cycle is the best way to independently check that design code reflects intended behavior while dramatically reducing debug time. Assertions accomplish this by

• Pinpointing both the time and location of the root cause of the problem, saving time normally spent tracing a failing scenario backwards through time.
• Identifying failures early during test environment development, allowing verification engineers to bypass consultations with a the designer and saving time normally spent identifying testbench issues.
• Documenting design behavior, so that incompatible changes made to the module or surrounding modules will fire an assertion.
• Capturing the design intent of IP blocks and transferring this knowledge to the integration team to enable successful use of the IP.

Assertions are also useful for verification technologies beyond simulation. Formal verification relies on assertions to provide constraints on inputs to the design and as checks and cover points for internal nodes and outputs of the design. Additionally, some emulation platforms can implement assertions (or subset of assertions) for use in system-level regressions and software testing to extend assertion use to real-world scenarios. In all these cases, assertions must be accurate and debugged in order to gain the maximum benefit.

The challenge with assertions, however, is that the SVA syntax is fairly complicated and implementing assertions requires additional time and effort by both design and verification engineers. The SVA syntax is fairly terse and isn’t obvious to new users, SVA introduces more complicated termporal constructs, and the time spent debugging assertions the traditional way negates many of the benefits.

Solution:

Zazz provides an alternative method to creating and debugging high quality assertions before inserting them into the traditional design flow. This allows assertions to be used throughout the design process, maximizing their benefits while greatly reducing the occurrence of false positives (caused by incorrect assertions that trigger on valid behavior) and false negatives (when incorrect or missing assertions do not correctly identify incorrect behavior). The latter case is especially concerning, since the lack of assertion activity may give a false sense of security that the RTL is operating correctly.

SVA Creation

Zazz provides VisualSVA as method of quickly creating assertions using graphical “tiles” that represent the Verilog expressions and temporal operators that make up the SVA syntax. VisualSVA not only enables novice SVA users to create basic assertions, but also provides the capability of creating complex assertions in a manner that allows them to be understood by engineers who are not even familiar with the SVA syntax. Figure 1 shows the visual representation of an assertion that constrains the behavior of an AXI read address bus and Figure 2 shows the corresponding SVA code.

Figure 1: Zazz Visual SVA representation of an assertion checking the AXI Read Address bus

Figure 2: SVA code that corresponds to the VisuaSVA in Figure 1.

SVA Debug

While the VisualSVA features of Zazz improves productivity in the creation of assertions (and greatly aids in the learning of the SVA syntax), this paper will concentrate primarily on the SVA debug features of Zazz and how the Synopsys VCS® and Verdi® products can be used with Zazz to debug assertions outside a traditional verification environment.

To better understand the reasoning behind debugging assertions, consider the underlying purpose of an assertion: to capture the behavior of a group of signals over time. Thus an appropriate way of approaching assertion development should be to capture the rules of the signals in a timing diagram form and/or simply making a list of relationships between the signals. For the ARM APB bus, the basic timing diagram looks something like

Figure 2: Sample APB Waveform

and the relationships are

1. A transaction starts when PSEL goes high,
2. PEANBLE must be high on the following cycle,
3. PSEL and PENABLE must remain high until PREADY is asserted,
4. PWRITE, PADDR and PWDATA must remain stable throughout the transaction

The primary purpose of Zazz Debug is to ensure that the intent of assertions created (the timing diagram and rules) matches the actual behavior allowed by the assertion (what happens in simulation). Zazz does this by creating a constrained-random testbench around the assertion that provides example behaviors allowed (or disallowed) by the assertion. This is even more important in formal verification, since incorrect constraints (assertions used to describe inputs to the design) will cause formal tools to generate stimulus that doesn’t correspond to desired behavior.

Example patterns generated by Zazz are then simulated with the assertion in the Synopsys VCS® simulator in order to exercise the assertion and results are displayed on Synopsys Verdi® waveform viewer. Assertion behavior is annotated directly on the waveforms to help the user identify issues with the assertion that must be addressed. Often the sample waveforms expose additional behaviors that are not addressed by the original assertion(s), prompting the user to either update the assertion code to be more explicit or add additional assertions to properly qualify design behavior. Further iterations can quickly be made to ensure intent and corner cases are correctly implemented so that when the SVA is added into RTL for module and system testing, it has a much higher likelihood of performing correctly.

Example of SVA Debug:

This example will demonstrate the text-based debug mode of Zazz; similar debug features exist within Zazz when creating SVAs via the Visual interface.

To get started, one simply types or pastes an assertion into Zazz’s SVA text box. From our APB example, we might start with a simple assertion that outlines the APB protocol. The assertion triggers on the start of an APB transfer (PSEL active) and then checks that PENABLE is high the 2nd cycle and then terminates when PREADY is asserted. The assertion might look like this:

apb_transfer: assert property ( @(posedge clk) psel |=> penable ##0 pready [->1]);

We have now created the assertion, but do we really know whether it will provide any useful checks on the design? To find out, Zazz will use its internal constraint solver to generate sample waveforms, replay them in VCS®, then view them in Verdi®’s waveform viewer to observe how the assertions behave in various scenarios.

Figure 3: Synopsys Verdi® view of examples generated by Zazz and simulated witih Synopsys VCS®

Before debugging this assertion, let’s examine what is shown in the waveform. In this example, Zazz has generated 6 sample waveforms, which are indicated by the “$$frame$$” signal at the top. Each example stands alone and Zazz forces the signals to an inactive state between examples (where $$frame$$ is X). Below the clock waveform is the assertion itself. VCS®/Verdi® indicate where the assertion triggers by displaying a green dot. A horizontal line then indicates the timeframe where the assertion is active, and the end of the line will either be a green arrow pointing up (indicating assertion completing successfully) or a red arrow pointing down (indicating an assertion failure). Note that it is also very easy to identify when multiple instances of the assertion are currently being checked since multiple horizontal lines are shown at once. This is important, since it often indicates conditions where an assertion is getting triggered too often (and incorrectly) and consuming more simulation resources than necessary.

From the waveforms, it is clear that while we may have captured some of the most basic elements of an APB transaction, our behavioral description captured by the SVA falls far short of ensuring that our APB interface will function correctly since none of the waveforms look anything like our original timing diagram. We must now examine the examples and identify invalid behaviors that are being allowed and modify our assertion accordingly.

The first thing to note is the multiple starts on the assertions. Notice that in Frame 1, the assertion is started at cycles 4 and 5 while waiting for PREADY. Our intention is to only start this check at the beginning of an APB transfer, so we need to modify the trigger to look for the rising edge of PSEL. We can do this by using $rose(psel) instead of just psel before the implication operator. This multiple restart issue can also be seen in several of the other examples as well.

apb_transfer: assert property ( @(posedge clk) $rose(psel) |=> penable ##0 pready [->1]);

Additionally, we note that the PENABLE and PSEL signals do not remain high throughout the transaction (relationship #3). To correct this, we can apply the throughout operator to the “wait for PREADY” portion of the assertion to ensure that both PENABLE and PSEL remain high while waiting for the transaction to complete.

apb_transfer: assert property ( @(posedge clk) $rose(psel) |=>penable ##0 ((penable & psel) throughout pready [->1])) ) ;

When we rerun, the resulting waveform looks like

Figure 4: Synopsys Verdi® view - updated assertion code

Our assertion is making progress, since we have now eliminated the overlapping starts and ensured that PSEL and PENABLE both remain high until the end of the transaction. For instance, Frames 0, 1, 2, and 5 pretty much match our desired behavior . However, our assertion is still allowing too many invalid behaviors:

• Frame 3 allows PENABLE during the first cycle of the transaction (first PSEL cycle), and
• Frame 4 allows PENABLE outside of an APB transaction.

The first issue must be addressed by explicitly requiring that penable be low at the beginning of the transfer. We do this by changing the imply to a “same cycle” implication, adding an expression to check for this condition, then adding a single cycle of delay to transition into the remainder of the assertion:

apb_transfer: assert property ( @(posedge clk) $rose(psel) |->~penable ##1 penable ##0 ( (penable & psel) throughout (pready [->1]))) ;

The second issue is an example of how Zazz can prompt the user to not only further enhance the assertion, but also provide ideas for new assertions. The second case (PENABLE active outside of a transaction) is an implied rule, however nothing is checking this condition. In this case, we would add a second assertion to cover this case:

penable_outside_transfer: assert property ( @(posedge clk) penable |-> psel);

We now include both assertions in Zazz’s SVA text box and after rerunning simulations get the following waveforms:

Figure 5: Synopsys Verdi® view - updated assertion code with two assertions

Note that Zazz now instructs Verdi® to display both assertions and their related signals separately so that the user can inspect each assertion independently (even though PSEL and PENABLE twice in the signal list, they area actually the same signal). Also note that Zazz does not enforce (constrain behavior) assertions during the transition periods, so we now see that the PENABLE outside a transaction is properly flagged as a failure by our new assertion.

At this point, assertion now appears to be accurately describing the APB behavior and covers the stated rules 1-3. We can now add the constraint for rule #4 and end up with the following assertion:

apb_transfer: assert property ( @(posedge clk) $rose(psel) |->
~penable ##1 penable ##0
( ($stable({paddr,pwrite,pwdata})) throughout
( (penable & psel) throughout (pready [->1]) ))) ;

If this is a little intimidating, the VisualSVA view of the assertion is less daunting:

^{Click to enlarge}

Figure 6: Final Zazz Visual SVA representation of APB assertion

Conclusion:

Adding assertions early and throughout the ASIC design cycle is the best way to independently check that design code reflects intended behavior. And today there exists a powerful flow to independently debug and validate SVAs before placing into RTL code. This saves time and ensures the SVAs are performing as intended. The Zocalo Tech flow provides an intuitive and powerful environment to rapidly debug SVAs (and create them visually) for both the verification and RTL designer.

Often subtleties in assertion behavior are not recognized when they are created, so it is important to verify that assertions are operating properly independently of the RTL code they are monitoring. As seen in the debugging example, this debug process often leads not only to more tightly coded assertion constructs, but alerts users to implicit rules that are not being checked. The end result is typically a larger set of assertions that can accurately check the behavior of the circuit.

About the Authors:

Eric Deal; Product Manager at Zocalo-Tech. Eric has 20 years of experience in digital logic design and architecture, and has recognized the benefits of SVAs in his digital design and IP experience. He holds a BSEE degree from Texas A&M University.

Robert Biczek; President and VP Sales at Zocalo Tech. Robert brings over 20 years of selling and management experience to the company. And, he holds a MSEE from University of Illinois, Champaign/Urbana, and a BSEE from Florida Tech.