A Simple Arbiter Example

The model we use is a simple arbiter design, as shown in Figure 3.1.

This is an arbiter that has four requesting agents, each able to request a shared resource using one bit of the req signal. The gnt signal indicates which agent is currently authorized to use the resource. There is also an opcode input, allowing certain commands that override the normal behavior of the arbiter, such as forcing a particular agent to get priority, or cutting off all access to the resource for a period of time. There is an error output as well, to signify that a bad opcode or illegal sequence of opcodes has been sent. The interface code for a top-level System Verilog (SV) module implementing this design is shown below.

typedef enum logic[2:0] {NOP,FORCE0,FORCE1,FORCE2,

    FORCE3,ACCESS_OFF,ACCESS_ON} t_opcode;

module arbiter(

  input logic [3:0] req,

  input t_opcode opcode,

  input logic clk, rst,

  output logic [3:0] gnt,

  output logic op_error

);

What are Assertions?

At the most basic level, an assertion is a statement about your design that you expect to always be true. In the case of our arbiter, a simple example might be the fact that you never expect a grant to agent 0 when it was not requested:

check_grant: assert property (!(gnt[0] && !req[0])) else $error(“Grant without request for agent 0!”);

As we will see in the discussions below, assertions can get much more complex than the simple Boolean expression above, involving logical implications and potential statements about values changing over time.

When running a simulation on a model, your simulator will usually flag an error when it detects that any SVA assertion in your code is not true. In the above example, if we ever see gnt[0] == 1 and req[0] == 0 in simulation, the message Grant without request for agent 0! will be displayed.

When running a formal property verification (FPV) tool, assertions are treated as proof targets: the goal of the tool is to mathematically prove that your RTL model can never violate this assertion.

There are two other types of properties we should understand before diving into the technical details: assumptions and cover points.

What are Assumptions?

Assumptions are similar to assertions, but rather than specifying the behavior of a device under test, they usually specify conditions that are intended to represent constraints on the verification environment. Often these represent conditions that are externally guaranteed to be true, due to inputs or other environmental factors. For example, perhaps we expect that our arbiter will only see legal non-NOP opcodes arrive at its opcode input:

good_opcode: assume property (opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}) else $error(“Illegal opcode.”);

For simulation, an assumption is treated in exactly the same manner as an assertion: the simulator checks to see whether the current simulation values violate the specified condition, flagging a violation and printing the message if not. But keep in mind that the conceptual meaning is still somewhat different from an assertion failure: a failed assumption usually means something is wrong in the testing environment, testbench code, or a neighboring design module, while a failed assertion usually indicates a problem in the design under test. (This is not strictly required though, as it is legal to have an assumption involving internal design nodes, a situation we will discuss in more detail in future chapters.) In the example good_opcode above, it would indicate that the testbench is incorrectly driving an illegal opcode into the design.

In FV, there is a major difference between assumptions and assertions. Just like its name implies, an assumption is something that the tools assume to be true. An assumption is taken as an axiom and used to prove the truth of the assertions. Without assumptions, FV tools start by allowing any possible values to arrive at the inputs of the model they are analyzing; the assumptions are the primary method by which the user guides these values toward allowable behaviors. In most cases, a good set of assumptions is a requirement in order to eliminate consideration of unrealistic behaviors and correctly prove the assertions on a design.

What are Cover Points?

An SVA cover point is specified in a similar way to assertions and assumptions, but it has a somewhat different meaning. While assertions or assumptions are expected to always be true, a cover point is something that is only occasionally true: it is specifying some kind of interesting condition that we want to make sure we are testing. For example, in our arbiter, we probably want to make sure that we are testing the possibly challenging case where all our agents are requesting the resource at once:

cover_all_at_once: cover property

    (req[0]&&req[1]&&req[2]&&req[3]);

In simulation, most users check cover points collectively: the tool or scripts save information to a database whenever a cover point is hit, and in the end the user can examine the total coverage after running all the simulation tests in their test suite. You usually want to make sure that each of your cover points is hit at least once; if not, this reveals a potential hole in your testing.

For FV, cover points also play an important role. Although FV theoretically covers all possible behaviors of your system, remember that you can specify assumptions or other input requirements that limit the possible traffic considered. This leads to a danger of overconstraint: you may accidentally specify assumptions that rule out interesting classes of traffic to your system. As a result, making sure that your FPV environment is able to reach all your cover points is a critical step in FV. We will discuss this more in the upcoming chapters on FPV.

Clarification on Assertion Statements

As you may have noticed in the examples above, assertions, assumptions, and cover points are all specified with basically the same mechanisms in SVA. Thus, most of the mechanics of defining them are the same for all three types of constructs. For clarity, we concentrate on assertions in the remaining text of this chapter; keep in mind, however, that most of our discussion applies to assumptions and cover points as well. You should be able to use the techniques described in the remainder of this chapter equally for describing all three types of constructs. The term assertion statement, used here the same way it is defined in the LRM [IEE12], can equally refer to assertions, assumptions, or cover points.

SVA Assertion Language Basics

The SVA assertion language can be viewed as several layers of increasing complexity, as shown in Figure 3.2.

gnt_falls: assert property(req[0] ##2 gnt[0] |->

    ##1 !gnt[0]);

We will discuss sequences, properties, and assertion statements in more detail in the remainder of this chapter. But before we move on, there is one more key concept we need to introduce: immediate and concurrent assertions.

    conc1: assert property (!(gnt[0] && !req[0]))

Although concurrent assertion conc1 looks similar to immediate assertion imm1, their evaluations have some important differences. While the immediate assertion is evaluated whenever it is visited in procedural code, the concurrent assertion is only evaluated at edges of a well-defined clock. This will become clearer as we describe the two assertion types in more detail.

Writing Immediate Assertions

While immediate assertions should usually only be used in cases we have described above, it is important that you use them correctly when you do need them. We recommend that you always use the variant of immediate assertions known as final deferred immediate assertions. A final deferred immediate assertion statement is relatively simple to describe: just use assert final followed by any Boolean expression, with an optional label before and failure message after. (If you are working with Electronic Design Automation (EDA) tools that have not yet adopted the latest LRM, you may need to use the observed deferred immediate assertion assert #0 instead, which behaves the same in most common cases. See LRM clause 16.4 for more details on these constructs.) So if we want to write an immediate assertion to check that we are not granting access to agent 0 when they did not request it, we could write this statement:

grant0_ok: assert final (!(gnt[0] && !req[0])) else

  $error(“Grant without request for agent 0.”);

The label grant0_ok is an optional name for the assertion; most EDA tools will auto-generate a name if no label is present, but we recommend always including one.

The action block else $error ... is also optional, with most simulation tools generating default messages for assertion failures if it is not present. But we recommend always including something meaningful here, for aid in simulation debug.

This assertion could be placed within an always block in any module where the gnt and req signals are visible, or inside a function with access to these signals. We could also place it outside an always block within a module; in this case, it is treated as if in an implicit always_comb block. Whenever its procedural code is executed, the assertion will be checked.

Complications of Procedural Code and Motivation for Assert Final

The way that procedural code, mainly always blocks, is executed in SystemVerilog can be a surprise to many users—even some who have been designing in the language for years. What you need to keep in mind are three key concepts:

These can result in some behaviors for immediate assertions that will surprise users without a detailed familiarity with the LRM. This is why the more recent versions of the language introduced the concept of deferred assertions. These are a form of immediate assertion that follows a special rule: if the procedure in which they exist is executed multiple times during a single simulation time step, only the result of the final execution will be reported. (The actual rule is a little more complicated, involving the concept of SystemVerilog “simulation regions,” but rather than getting sidetracked with a full description of SV, we’ll refer you to the LRM for the details.)

To make this clearer, here is an example of a very poorly written fragment of RTL code, which uses non-deferred immediate assertions:

always_comb begin : add_1_to_evens

  if (f_even(i) && i<9) begin

   i=i+1;

   a1: assert (i>=10) else $error(“i is %0d”,i);

  end

end

always_comb begin : add_1_to_odds

  if (f_odd(i) && i<10) begin

   i=i+1;

   a2: assert (i>=10) else $error(“i is %0d”,i);

  end

end

Let’s assume that f_even correctly returns true for even numbers, and f_odd correctly returns true for odd numbers, as their name implies. If i somehow was assigned a value less than 10 somewhere, the above pair of always blocks would together be executed over and over, alternately increasing i by 1 each time, and we would see an assertion failure each time i is incremented but not yet at its maximum:

Assertion failure in myfile.v:40: i is 4

Assertion failure in myfile.v:34: i is 5

Assertion failure in myfile.v:40: i is 6

Assertion failure in myfile.v:34: i is 7

Assertion failure in myfile.v:40: i is 8

Assertion failure in myfile.v:34: i is 9

The user would find the above messages very confusing, since at the end of any time step in their simulator, they would see that i is always at least 10. The intermediate values that were changing during the time step triggered these assertions. This is why deferred assertions were introduced: for a deferred assertion, in any simulation time step, only the result of the final execution of each assertion in a given procedure is reported. In the case of the example above, if each assert were replaced with an assert final, then we would see no violations: at the final execution of each procedure for any given time step, either i would have a legal value, or no assertion would be checked.

For this reason, we recommend that whenever you do use immediate assertions, you use the deferred variety.

Location in Procedural Blocks

There is one more complication of immediate assertions that we should discuss. An immediate assertion operates on whatever values its variables hold at the time its line is executed. This may differ from the values the signals settle upon at the end of the procedure. Here is an example of a procedure with a poorly placed immediate assertion:

always_comb begin

  gnt = 4’b0;

  no_conflict: assert final ($onehot0(gnt));

  if (|req)

   gnt = f_compute_grant (req);

end

In this example, the assertion no_conflict has been written to check that there is always at most one grant. But because it was placed before the f_compute_grant call, it will actually never detect a failure, even if there is an error in the f_compute_grant function: at the time the assertion line is reached, the value of gnt will always be the 0 assigned on the line before. The following version makes much more sense:

always_comb begin

  gnt = 4’b0;

  if (|req)

   gnt = f_compute_grant (req);

  no_conflict: assert final ($onehot0(gnt));

end

You need to keep in mind that the final qualifier for an immediate assertion only signifies the use of the final execution of its enclosing always block during each time step; it does not indicate that it detects the final value for its variables. If you find this confusing, there is no need to worry: you can sidestep the issue in most cases by simply following a rule of thumb to put any immediate assertions at the end of the procedure or function.

Boolean Building Blocks

Before we close our discussion of immediate assertions, we should examine the various Boolean building blocks provided by the SystemVerilog language. These are not strictly for assertions, but are useful shorthand that can enable us to write clearer and more succinct assertions for common situations. They are especially useful in that they can be applied to both immediate and concurrent assertions. In most cases, their meanings are relatively self-explanatory, so rather than explain them in detail here, we will just supply Table 3.1 to summarize the constructs that we have found most useful in assertion contexts.

Concurrent Assertion Basics and Clocking

As we discussed in the last section, most of the assertions that you write for FPV purposes will be concurrent assertions. These assertions support clear specification of clocks and resets, and are capable of examining the behavior of values over time. Before we discuss the more complex sequence and property concepts, which allow us to specify complex behaviors over a period of time, we will begin by introducing concurrent assertions on simple Boolean expressions, so we can discuss the basics of how their timing works. Here is an example of a concurrent assertion for checking that, at any rising edge of the clock clk outside reset, we have an acceptable non-NOP opcode:

safe_opcode: assert property (

  @(posedge clk)

  disable iff (rst)

  (opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))

  else $error(“Illegal opcode.”);

From this example, we can see that the syntax for concurrent assertions differs from immediate assertions in several obvious ways:

In this example, we are checking a simple Boolean formula. Functionally, the key difference between this assertion and a similar immediate assertion is that this one is checked only at the given clock edge, and that this one is ignored during its reset (disable iff) condition.

We should also note that because a concurrent assertion can define its own clocking and reset, concurrent assertions usually make the most sense to use outside procedural code, separate from an always block. You can include them in procedural code as well, but we recommend avoiding this usage, as it can introduce complex relationships between assertion and procedure timing. (See LRM section 16.14.6 if you want to learn the full details of this usage.)

Before we go into greater depth on the many ways to implement more powerful concurrent assertions, we should carefully examine the clock and reset conditions: it is important you understand these in order to fully comprehend what a concurrent assertion is checking.

Sampling and Assertion Clocking

Concurrent assertions operate on what is known as the sampled value of their arguments. Essentially, at any simulation time step, the sampled value of each variable is the value that variable attained at the end of the previous simulation time step.

In Figure 3.3, we see a signal sig1 with values that change at various times, and a concurrent assertion:

sig1_off: assert property (@(posedge clk1) !sig1);

At first glance, the reported values for the assertion might seem strange, because a naïve reader would think that the assertion should simply be true whenever sig1 is false. But actually, the assertion results are only calculated at each positive edge of the clock, and as we stated above, they always examine the value sampled at the end of the previous time step, just before that edge. So we see results indicating:

Although this might be disconcerting at first, a few minutes of reflection will reveal that this will, at worst, lead to off-by-one reporting of assertion failures; as long as this sampling rule is consistent for all values used in the concurrent assertion, any failures defined by its logic should behave as expected, as long as the failing values are visible just before an edge of the relevant clock. We should also note that many EDA tools compensate for this inherent off-by-one behavior in their output, so the particular tool you are using may or may not actually report failures after the signal transitions in this way. But if they are compliant with the rules of the language, they will consistently use these sampled values to calculate assertion results.

The place where this sampling behavior can lead to trouble is if you put concurrent assertions in procedural code or include terms that use unclocked elements, such as software calls, and create situations where sampled and non-sampled values might be combined in one assertion. This is another reason for our earlier tip to put your concurrent assertions outside procedural code.

Sampled Value Functions

As helpful building blocks to construct concurrent assertions, SVA also provides a set of sampled value functions, built-in functions that operate on sampled values in the same way as concurrent assertions. For example, suppose we want to make sure that whenever there is no grant, there was no request on the previous cycle. We could write the assertion like this:

no_grant_ok: assert property (@(posedge clk)

   (|gnt) || !$past(|req));

This assertion checks the desired condition. Both the req and gnt values are sampled just before the positive edge of clk, and the $past function examines the value of its argument one cycle earlier. These functions all inherit the clock of the assertion statement, sequence, or property where they are used, though they may also be passed explicit clock arguments.

The most useful sampled value functions, with summaries and usage examples, are shown in Table 3.2. Here we show the simple forms that are most commonly used: refer to LRM section 16.9.3 for the details and full set of options.

One slight wrinkle to watch for when using these functions is the issue of X or Z values. Many modern simulators support 4-valued runs that include these values, and this feature has been added to some FV tools. According to the LRM, a transition from X to 1 counts as a rise for $rose, and from X to 0 counts as a fall for $fell. If you are targeting a validation environment that allows these values and you do not want transitions from X/Z to count as a rise or fall, you should probably be using sequence notation, as described in the next section, rather than these shorthand functions.

Concurrent Assertion Clock Edges

As you have probably inferred from the discussion in the previous sections, the clock to be used by a concurrent assertion is an important consideration when creating the concurrent assertion. This clock is expressed with a clock specifier such as @(posedge clk1). The clock expression is what determines which values are sampled, and can create unexpected behavior if the wrong clock is used. A common mistake is to omit an edge and use an expression like @(clk1): this makes an assertion act on positive and negative clock edges, effectively examining each phase rather than each cycle. For a latch-based design, this may sometimes be the true user intent, but more commonly, a posedge is really needed. If a slow clock is passed in to an assertion, it may be ignoring short-term values that last only a single phase of a faster clock. If sampled value functions such as $past are used, or sequence delays (which we will describe in the next section) are used, choosing a different clock can actually change the number of cycles that are counted.

In Figure 3.4 we can see the different behaviors of an assertion with the same logical expression, !sig1, but with different clocks passed in.

check_posedge: assert property (@(posedge clk1) !sig1);

check_anyedge: assert property (@(clk1) !sig1);

check_posedge4: assert property (@(posedge clk4) !sig1);

In particular, we see that:

Ultimately, the key lesson here is that you should be sure to understand what clocks you are using for your assertions, and why. Do you want to detect one-phase “glitch” values, or ignore them? Do you want to look for every change relative to your fastest clock or really only care about some slower clock used to sense outputs?

Concurrent Assertion Reset (Disable) Conditions

In addition to clocks, concurrent assertions also allow you to specify reset conditions using disable iff. The main goal here is to shut off assertion checking during reset: on most modern designs, you can expect some level of arbitrary “garbage” values in your design at reset, and you probably do not want to deal with the noise of invalid assertion failures due to these arbitrary values. So an assertion is considered to be trivially passing whenever its disable condition is true.

A complication with assertion resets is that they are an exception to the sampling behavior described in the past few sections: assertion reset is asynchronous, with an assertion being shut off immediately any time its disable condition is met. The consequence of this is that you should not try to be clever and insert miscellaneous logic within your disable clause: because this is timed differently from the rest of the assertion, you are likely to get confusing and unintended results. For example, consider the following two assertions, both trying to state that outside of reset, if you have at least one grant, you should have a request:

bad_assert: assert property (@(posedge clk)

  disable iff

   (real_rst || ($countones(gnt)==0))

  ($countones(req)>0));

good_assert: assert property (@(posedge clk)

  disable iff (real_rst)

  (($countones(req)>0) ||

    ($countones(gnt)==0)));

At first glance, these might look logically equivalent: both are assertions that say you must either not have any grants, or you must have at least one request currently high. But because bad_assert puts the gnt signal in the disable condition, which is not sampled, it will actually be looking at gnt values one cycle earlier than the req values, causing a failure to be missed on the waveform shown in Figure 3.5.

In Figure 3.5, there is clearly a problem in phase 6, where there is a grant with no request. The assertion good_assert will report this failure on phase 8, using the sampled values from just before the relevant rising edge of clk1. The assertion bad_assert is disabled for every phase except 6. The sampled values just before the phase 8 rising edge show |req false, but the current value of gnt (used instead of the sampled value, due to the disable clause) disables the checking of this assertion.

Setting Default Clock and Reset

As we conclude our examination of SVA clocking and reset for concurrent assertions, there is one more important language feature to discuss. You have probably noticed from our examples so far that specifying the clock and reset of an assertion can seem a bit wordy:

good_assert: assert property @(posedge clk)

   disable iff (rst)

   (|req || !(|gnt)) else $error(“Bad gnt.”);

safe_opcode: assert property (

  @(posedge clk)

  disable iff (rst)

  (opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))

  else $error(“Illegal opcode.”);

Fortunately, SVA offers a way to set a global clock and reset for the concurrent assertions in a module, so they can be written once and cover multiple assertions. You declare a default clock with a default clocking statement and a default reset with a default disable iff statement. If these defaults are declared, they apply to all assertion statements in the current module, except those that explicitly include a different clock or reset. Thus, the following code is equivalent to the two assertions above:

default clocking @(posedge clk); endclocking

default disable iff (rst);

good_assert: assert property

   (|req || !(|gnt)) else $error(“Bad gnt.”);

safe_opcode: assert property (

  (opcode inside {FORCE0,FORCE1,FORCE2,FORCE3,ACCESS_OFF,ACCESS_ON}))

  else $error(“Illegal opcode.”);

The asymmetric syntax between the default clocking and default disable iff statements above is not a typo: default clocking requires an endclocking, while default disable iff does not. (Don’t ask us why, it’s a quirk from the initial language design that we’re now stuck with.) In the common case where you have many assertions that use the same clocks and resets, declaring these defaults in each assertion-containing module can significantly improve readability of your assertion code and also prevent the mistakes we have seen in the past few sections from misuse of clock and reset.

By the way—now that we have described the usage of these default constructs, coding examples in this chapter and the following chapters will usually not bother to specify the explicit clock and reset for each assertion. When reading any code fragment in the remainder of this text, you should assume an appropriate default clocking and default disable iff are in effect. This way, we can write our examples much more cleanly, without redundant details of clocking and reset visible in every assertion line.

Sequence Syntax and Examples

A sequence is a specification of a set of values occurring over a period of time. The basic operation used to build a sequence is a delay specifier, in the form ##n (for a specific number of clocks) or ##[a:b] (indicating a variable delay between a and b clocks.) The special symbol $ can be used for the upper bound of a sequence, specifying a potentially unlimited number of cycles. A sequence is said to be matched when its specified values have all occurred. A sequence with a variable delay may have multiple overlapping matches during any execution trace. Figure 3.6 shows a few examples of simple sequences.

Another common sequence operation is the repetition operator [*m:n]. This indicates that a subsequence is to be repeated a certain number of times. Again, the upper bound may be $, indicating a potentially unlimited number of repetitions. Figure 3.7 shows some illustrations of using this operator.

Sequences may be logically combined using the and or or operators. (Note that these are distinct from SystemVerilog’s || and && operators, which provide logical ANDing or ORing for Boolean expressions.) When using the and operator, we are indicating that both sequences are starting at the same time, though their endpoints may mismatch. For the or operator, one of the two sequences must be matched. Also useful are the throughout operator, which checks that some Boolean expression remains true for the whole execution of a sequence, and the within operator, which checks that one sequence occurs within the execution of another. Figure 3.8 shows some examples using these operators.

A final set of sequence operators that is commonly useful are the goto repetition operators, [->n] and [=n]. These indicate that some value occurs exactly n times in the sequence, though these occurrences may be nonconsecutive and have arbitrary other activity in between. The simple goto [->n] matches at the final occurrence of the value, while the nonconsecutive goto [=n] allows an arbitrary amount of additional time after the last occurrence. Figure 3.9 shows some examples of these.

Remember that sequences are not useful unless part of an assertion statement; the simple examples above are technically code fragments, not useful statements. Asserting a sequence as an assertion or assumption is not usually meaningful (we will discuss this more in the next subsection on properties), but sequences are very useful for building a cover property. Here are some examples of cover assertion statements that might be useful in our arbiter example:

// cover case where agent 0 req gets granted in 1 cycle

c1: cover property (req[0] ##1 gnt[0]);

// cover case where agent 0 req waits >5 cycles

c2: cover property ((req[0] && !gnt[0])[*5:$]

   ##1 gnt[0]);

// cover case where we see a FORCE1 arrive sometime

//    while req0 is waiting

c3: cover property (opcode==FORCE1) within

((req[0] && !gnt[0])[*1:$]);

Property Syntax and Examples

The most common types of properties are created using triggered implication constructs, sequence |-> property and sequence |=> property. The left hand side, or antecedent, of an implication must be a sequence. The right hand side, or consequent, can be a sequence or a property. The difference between the two operators is that |-> checks the property on the same clock tick when the sequence is matched, while the |=> operator checks one tick later. Triggered properties are vacuously true (that is, true for trivial reasons) on cycles where their triggering sequence is not matched. Figure 3.10 shows some examples of simple properties and traces where they are true and false at various times.

We should also make an important point here about these triggered implication properties: they provide a very important advantage for validation, as opposed to other ways to write logically equivalent properties. This is because many EDA tools take advantage of the information about the triggering condition. For example, an overlapping |-> operation is often logically equivalent to a simple Boolean operation, as in the example below:

 a1_boolean: assert property (!cat || dog);

 a1_trigger: assert property (cat |-> dog);

However, with the triggered version, EDA tools can provide an advantage in numerous ways, to provide improved debug features.

Thus, we recommend that whenever you have multiple potential ways to write a property, you try to state it as a triggered implication if possible.

Another set of useful tools for constructing properties are the linear temporal logic (LTL) operators. A full discussion of LTL operators is probably more detail than you need at this point, so we will refer you to LRM section 16.12 if you wish to learn the full story. But LTL operators are critical if you want to create “liveness properties”: properties that specify aspects of potentially infinite execution traces. Probably the most useful LTL operators in practice are s_until and s_eventually. For the most part, these operators are exactly what they sound like: s_until specifies that one property must be true until another property (which must occur) is true, and s_eventually specifies that some expression must eventually be true. The s_ prefix on these operators stands for “strong,” indicating that in an infinite trace the specified conditions must happen at some point. (You can omit the s_ prefix to get “weak” versions of these operators, which means that an infinite trace that never hits the condition is not considered a violation.) Infinite traces may sound odd if you are used to simulation, but they can be analyzed by FV tools; we will discuss this issue more in upcoming chapters. Figure 3.11 shows some examples of these LTL operators.

One more very useful class of properties is negated sequences. SVA sequences have a not operator, to enables us to check cases when the sequence is not matched. We did not include this in the sequence section above because technically a negated sequence is a property object, not a sequence object. This means that it cannot be used as the left-hand side of an implication operator. However, a negated sequence is often very useful as a property to check that some unsafe condition never occurs. Here are some examples of negated sequences used as properties. Figure 3.12 shows some examples of these.

Like sequences, properties are not actually meaningful unless included in an assertion statement; once again, the examples above are just fragments at this point. Here are some examples of assertion statements that might be useful in our arbiter model.

// assume after gnt 0, req 0 falls within 5 cycles

req0_fall_within_5: assume property

  ($rose(gnt[0]) |=> ##[1:5] $fell(req[0]));

// assert that any request0 is granted within 20 cycles

gnt0_within_20: assert property

  ($rose(req[0]) |-> ##[1:20] gnt[0])

// assert that any grant on 0 is eventually withdrawn

gnt0_fall: assert property

  ($rose(gnt[0]) |-> s_eventually (!gnt[0]));

Named Sequences and Properties

Until now, we have been using sequences and properties directly in assertion statements, which is the most common mode of use. But sometimes you might want to encapsulate an advanced set of behaviors as a named object for more convenient reuse. SVA provides the ability to create named sequence and property objects for this purpose. These are similar to module declarations, but they take an optional set of untyped arguments. To define a named sequence, you just need the keyword sequence followed by its list of formal arguments, then the expression of the sequence, followed by an endsequence. Similarly for properties, you just need the keyword property followed by its list of formal arguments, then the expression of the property, followed by an endproperty. The property or sequence can then be instantiated in an assertion statement, or in another property/sequence, by using its name and passing in appropriate arguments. Here are some simple examples of a named sequence and property and how they might be used:

sequence within_5_cycles(sig);

 ##[1:5] sig;

endsequence

property b_within_5_after_a(a,b);

 a |-> within_5_cycles(b);

endproperty

// assertions a1 and a2 below are equivalent

a1: assert property (gnt[0] |-> ##[1:5] !req[0]);

a2: assert property (b_within_5_after_a(gnt[0],!req[0]));

Assertions and Implicit Multithreading

Now that you know how to describe complex behaviors that happen over time, a question has probably occurred to you: what happens if multiple behaviors overlap? For example, suppose we implement a version of the arbiter that accepts each request as a one-cycle pulse and expects a grant precisely 10 cycles after any request. Here is an example assertion describing this behavior for agent 0:

delayed_gnt: assert property (req[0] |-> ##10 gnt[0]);

Due to the 10-cycle gap between the request and the grant, though, it is possible that another request will arrive within that window. That second request should also get a grant precisely 10 cycles after it arrived. So in effect, we need two overlapping evaluations of this assertion. Fortunately, SVA assertions provide built-in multithreading: multiple instances of an assertion or sequence may be in progress at any given time, with a new one triggered each time its starting conditions are met. The waveform shown in Figure 3.13 illustrates how this happens.

In Figure 3.13, we can see that the first evaluation thread is launched after the request pulse on req[0] in cycle 1, and completes when the corresponding grant is seen in cycle 11. Similarly, the second thread is launched after the request in cycle 5, and ends after seeing the corresponding grant in cycle 15. Even though these two evaluations of the assertion are happening at the same time, they do not interfere with each other: if the grant had failed to arrive at cycle 11 or at cycle 15, a failure would have been reported.

Of course, like many powerful language features, this implicit multithreading is a double-edged sword: be careful not to create assertions with a triggering condition that happens often, or you risk creating a situation where the system must potentially analyze new threads created every single cycle, significantly impacting both FV and simulation performance. For example, the following assertion would have ended up creating new threads on nearly every cycle (all except cycles 1 and 5) in Figure 3.13:

notreq: assert property (!req[0] |-> ##10 !gnt[0]);

Writing the Properties

At this point, you know enough about the basics of assertions to write a wide variety of useful assertion statements. But in practice, how do you decide when and how to write assertions? In this final section of this chapter, we give you some general guidelines on adding assertions to your RTL models. This initial discussion is fairly general; in future chapters, we will return more specifically to examples of assertions that are especially useful in FV. There are three main project phases when you would typically define assertion statements needed in your code: during design specification, during RTL development, and during validation.

Practical Tips from this Chapter