This chapter is entirely devoted to the dynamic Local Variables . Without the dynamic multi-threaded semantics and features of Local Variables, many of the assertions would be impossible to write. The chapter also lays out how operators such as ‘or’ and ‘and’ affect the workings of parallel threads forked off by Local Variables based assertions. There are plenty of examples and applications to help you weed through the semantics.

Local variable is a feature you are likely to use very often. They can be used both in a sequence and a property. They are called local because they are indeed local to a sequence and are not visible or available to other sequences or properties. Of course, there is a solution to this restriction, which we will study further into the section. Figure 9.1 points out key elements of a local var. The most important and useful aspect of a local variable is that it allows multi-threaded application and creates a new copy of the local variable with every instance of the sequence in which it is used. User does not need to worry about creating copies of local variables with each invocation of the sequence. Above application says that whenever ‘RdWr’ is sampled high at a posedge clk, that ‘rData’ is compared with ‘wData’ 5 clocks later. The example shows how to accomplish this specification. Local variable ‘int local_data’ stores the ‘rData’ at posedge of clk and then compares it with wData 5 clocks later. Note that ‘RdWr’ can be sampled true at every posedge clk. Sequence ‘data_check’ will enter every clock; create a new copy of local_data and create a new pipelined thread that will check for local_data+’hff with ‘wData’ 5 clocks later.

Fig. 9.1
figure 1

Local variables—basics

Note that the sampled value of a local variable is defined as the current value.

Moving along, Fig. 9.2 shows other semantics of local variables. Pay close attention to the rule that local variable must be ‘attached’ to an expression while comparison cannot be attached to an expression!!

Fig. 9.2
figure 2

Local variables—do’s and don’ts

As shown in Fig. 9.2, a local variable must be attached to an expression when you store a value into it. But when you compare the value stored in a local variable, it must not be attached to an expression.

In the topmost example, “local_data=rData) is attached to the sequence ‘rdC’. In other words, assignment “local_data=rData” will take place only on completion of sequence ‘rdC’. Continuing with this story of storing a value into a local variable, what if you don’t have anything to attach to the local variable when you are storing a value? Use 1’b1 (always true) as an expression. That will mean whenever you enter a sequence, that the expression is always true and you should store the value in the local variable. Simple!

Note that local variables do not have default initial values. A local variable without an initialization assignment will be unassigned at the beginning of the evaluation attempt. An initialization assignment to a local variable uses the sampled value of its expression in the time slot in which the evaluation attempt begins. The expression of an initialization assignment to a given local variable may refer to a previously declared local variable. In this case the previously declared local variable must itself have an initialization assignment, and the initial value assigned to the previously declared local variable will be used in the evaluation of the expression assigned to the given local variable. More on this later.

Ok, so what if you want to compare a value on an expression being true? As shown in Fig. 9.2, you can indeed accomplish this by ‘detaching’ the expression as shown. The resulting sequence (the last sequence in the Fig. 9.2) will read as “on entering dataCheck, store rData into local_data, wait for 5 clocks and then if ‘b’ (of sequence rdC) is true within 5 clocks, compare wData with stored local_data + ‘hff”.

Figure 9.3 points out a couple of other important features. First, there is no restriction in using a local variable in either a sequence or a property. In addition, you cannot declare a local variable as a formal and pass as an actual from another sequence/property. That makes sense, else why would it be called ‘local’?

Fig. 9.3
figure 3

Local variables—and formal argument

In Fig. 9.4, we see that a local variable in a sequence is not visible to the sequence that instantiates it. The solution is quite straightforward. Instead of poking at the local variable directly, simply pass an argument to the sequence that contains the local variable. When the sequence L_seq updates the argument locally, it will be visible to the calling sequence (H_seq). Note that Ldata is not declared as a local variable in sequence L_seq (else that would be an error as we discussed). L_seq simply updates a formal and passes it to the calling sequence, where the actual is declared as a local variable. This is shown in the bottom of Fig. 9.4.

Fig. 9.4
figure 4

Local variables—visibility

Fig. 9.5
figure 5

Local variable composite sequence with an ‘OR’

Figures 9.5, 9.6, 9.7, 9.8 and 9.9 shows finer rules. Keep them as reference when you embark upon complex assertions. Annotation in the figure explains the situation(s).

Fig. 9.6
figure 6

Local variables—for an ‘OR’ assign local data—before- the composite sequence

Fig. 9.7
figure 7

Local variables—assign local data in both operand sequences of ‘OR’

Fig. 9.8
figure 8

Local variables—‘and’ of composite sequences

Fig. 9.9
figure 9

Local variables—finer nuances III

Fig. 9.10
figure 10

Local variables—further nuances IV

Fig. 9.11
figure 11

Local variable cannot be used in delay range

Fig. 9.12
figure 12

Local variables—cannot use a ‘formal’ to size a local variable

Figure 9.6 describes the semantics governing local variables when they are used in the OR of two sequences. The local variable must be assigned in both the sequences of an OR. However, what if you cannot really do that? There are a couple of solutions presented in Fig. 9.7.

Figure 9.9 describes semantics that govern an ‘and’ of two sequences. In contrast to an ‘or’ of two sequences, a local variable must not be attached to both sequences involved in an ‘and’. The first solution is identical to that for an ‘or’. Assign the local variable outside of the ‘and’ of the two sequences as shown in the figure. Alternatively, simply assign to the local variable in only 1 of two sequences, which is an obvious solution. Figure 9.9 shows solution #2 in addition to the solution #1 in Fig. 9.8.

Figure 9.10 describes further rules governing local variables. First, you can assign to multiple local variables, attached to a single expression. Second, you can also manipulate the assigned local data in the same sequence (as is the case for ldata2). But as before, there are differences in assigning to (storing to) local variables and comparing their stored value. You cannot compare multiple local variable values in a single expression in a sequence as is the case in the line “// (wData == ldata1, wretryData==!ldata2)”. This is illegal. Of course, there is always a solution as shown in the figure. Simply separate comparison of multiple values in two subsequences with no delay between the two. The ‘Solution’ annotation in the figure makes this clear.

Figure 9.11 shows that you cannot use a local variable in the range operator. But, it’s not the local variables fault. It’s the fact that we cannot have variable delay in either #m or #[m:n] delay operators. From software point of view, the delay range operators need to be known at elaboration time. Hence they cannot be ‘variables’. From hardware point of view, this is a bummer!

Figure 9.12 shows that you cannot use a ‘formal’ to size a local variable. Again, ‘size’ of a vector (bus) declaration can only be a constant. Again, there is a software reason and a hardware reason.

Following points out further cases of legal/illegal declarations of local variables.

  • property illegal_legal_declarations;

    • data; // ILLEGAL. ‘data’ needs an explicit data type.

    • logic data = 1’b0; // LEGAL. Note that unlike SystemVerilog variables, local variables have no default initial value. Also, the assignment can be any expression and need not be a constant value

    • byte data []; // ILLEGAL – dynamic array type not allowed.

  • endproperty

Also, you can have multiple local data variable declarations as noted above. And a second data variable can have dependency on the first data variable. But the first data variable must have an initial value assigned. Here’s an example.

  • property legal_data_dependency;

    • logic data = data_in, data_add = data + 16’h FF;

  • endproperty

  • property illegal_data_dependency;

    • logic data, data_add = data + 16’FF;

  • endproperty

  • sequence illegal_declarations (

  • output logic a, // illegal: ‘local’ is not specified with direction.

  • local inout logic b, c = 1’b0, // default actual argument illegal for inout

  • local d = expr, // illegal: type must be specified explicitly

  • local event e, // illegal: ‘event’ type is not allowed

  • local logic f = g // illegal: ‘g’ cannot refer to the local variable declared below. It must be resolved upward from this declaration

  • );

Note one more example of how you can declare a local variable used for initialization directly as an input. First, the sequence with the traditional way of initializing BSize.

  • ONE:

  • sequence burst (logic FRAME_, BurstSize = 4)

  • logic abc = 1’b0, BSize = BurstSize;

  • @(posedge clk)

    • FRAME_ |=>….

  • endsequence

Since, the BurstSize is solely used for sizing the local variable BSize, you can parameterize it as follows, where now the actual will determine the BSize.

  • TWO:

  • sequence burst (logic FRAME_, local input logic BSize)

  • logic abc = 1’b0;

  • @(posedge clk)

    • FRAME_ |=>….

  • endsequence

The keyword ‘local’ specifies that BSize is an ‘argument local variable’ (as LRM puts it) while the direction ‘input’ specifies that BSize will receive its initial value from the actual argument expression.

Note that in the first sequence the BSize initialization takes place @(posedge clk). Here the declaration assignments are performed when the evaluation reaches alignment with @(posedge clk) and at that point the value in the formal argument BurstSize is assigned to BSize as its initial value. In the second sequence, the initialization of BSize takes place when the actual changes its value assigns to formal BSize. Similarly, an ‘output’ ‘argument local variable’ outputs its value to the actual argument whenever the sequence matches. For ‘inout’, it obviously acts both as ‘input’ and ‘output’. So, the rules specified for ‘input’ applies when it acts as an ‘input’ and the rules for ‘output’ apply when it acts as an ‘output’.

Note that ‘argument local variables’ precede the ‘body local variables’. If a sequence or property has both ‘input’ ‘argument local variables’ and the ‘body local variables’ with declaration assignments, the initialization assignment of the ‘input’ ‘argument local variables’ are performed first.

On the similar line of thought, the following rules also apply. See the ‘sequence’ below.

  • sequence local_IO (

    • local byte a;

    • local inout byte b;

    • local input logic c;

    • local output byte d;

  • );

    endsequence

Following rules apply to the local variables of sequence local_IO.

  1. 1.

    If a direction is specified for an argument, then the keyword ‘local’ must also be specified.

  2. 2.

    If the keyword ‘local’ is specified, then the data type must also be explicitly specified.

  3. 3.

    If the keyword ‘local’ is specified without a direction, then a default direction of ‘input’ is understood.

  4. 4.

    An ‘input’ argument local variable may be declared with an optional default actual argument which can be any expression.

  5. 5.

    An ‘output’ or ‘inout’ argument local variable cannot be declared with a default actual argument because the actual argument must specify the local variable that will receive the ‘output’ value.

  6. 6.

    An ‘argument local variable’ can also be declared as ‘output’ or ‘inout’, but only in a sequence declaration. An ‘argument local variable’ of a property must be of direction ‘input’.

  7. 7.

    An ‘output’ ‘argument local variable’ outputs its value to the actual argument whenever the sequence matches.

  8. 8.

    An ‘input’ receives its initial value from the actual argument.

  9. 9.

    For ‘inout’, it obviously acts both as ‘input’ and ‘output’ and the rules for ‘input’ apply when it is of direction ‘input’ and the rules for ‘output’ apply when it is of direction ‘output’.

  10. 10.

    As stated above, it is important to understand that the ‘sampled’ values are used for all terms that are not ‘local’ while the ‘current’ values are used for terms that are ‘local’.

  11. 11.

    The actual argument bound to an ‘argument local variable’ of direction ‘output’ or ‘inout’ must itself be a local variable.

A special note on the use of method ‘.triggered’ with a local variable. A local variable passed into an instance of a named sequence to which sequence method (.triggered) is applied, is not allowed. For example, the following is illegal.

  • sequence check_trdy (cycle_begin);

    • cycle_begin ##2 irdy ##2 trdy;

  • endsequence

  • property illegal_use_of_local_with_triggerd;

    • bit local_var;

    • (1’b1, local_var = CB) |-> check_trdy(local_var).triggered;

  • endproperty

Some more rules on referencing local variables.

A local variable can be referenced in expressions such as:

  • Array indices

  • Arguments of task and function calls

  • Arguments of sequence and property instances

  • Expressions assigned to local variables

  • Boolean expressions

  • Bit-select and part-select expressions

However, a local variable cannot be referenced in following:

  • Clocking event expressions (even though LRM is ambiguous on this)

  • The reset expression of a ‘disable iff’

  • The abort condition of a reset operator (accept_on, sync_accept_on and the reject forms of these expressions. See Sect. 16.16)

  • Expressions that are compile time constants. E.g. [*n], [→ n], ##n, [=n], etc. and the constant expressions of ranged forms of these operators

  • An argument expression to a sampled value function ($rose, $fell, $past, etc.)

9.1 Application: Local Variables

The application in Fig. 9.13 is broken down as follows.

Fig. 9.13
figure 13

Local variables—application

  • ($rose(read),localID=readID

    • On $rose(read), the readID is stored in the localID.

  • not (($rose(read) && readID==localID) [*1:$])

Then we check to see if another read ($rose(read)) occurs and it’s readID is the same as the one we stored for the previous Read in localID. We continue to check this consecutively until

  • ##0 ($rose(readAck) && readAckID == localID) occurs.

If the consecutive check does result in a match, that would mean that we did get another $rose(read) with the same readID with which the previous read was issued. That’s a violation of the specs. This is why we take a ‘not’ of this expression to see that it turns false on a match and the property would end.

If the consecutive check does not result in a match until ##0 ($rose(readAck) && readAckID == localID) arrives then we indeed got a readAck with the same readAckID with which the original read was issued. The property will then pass.

In short we have proven that once a ‘read’ has been issued that another ‘read’ from the same readID cannot be re-issued until a ‘readAck’ with the same ID has returned.

Example: This example shows a simple way to track time. Here, on falling edge of Frame_, rising edge of IRDY cannot arrive for at least MinTime.

Solution:

  • property FrametoIRDY (integer minTime);

  • integer localBaseTime;

    • @(posedge clk) ($fall(Frame_), localBaseTime = $time)

    • |=>

    • $rose(IRDY) && $time >= localBaseTime + minTIme);

  • endproperty

  • measureTime: assert property (FrametoIRDY (.minTIme (MINIMUM_TIME)));

Local variable examples are scattered throughout the book. Some are found in following sections.

  • Section Clock delay range operator: ##[m:n]: multiple threads 6.2.1

  • Section FIFO TESTBENCH AND ASSERTIONS 14.1.2

  • Section Calling subroutines 14.3

  • Section Building a counter 14.7

  • Section Clock Delay : What if you want variable clock delay? 14.8.