HOME

    Electronics Directory Articles/ Tutorials eBooks

About Us

FORUM Links Contact Us
   

SystemVerilog Tutorial PART 23: by Abhiram Rao

Assertions in SystemVerilog - Part6

 

        <Previous    TOC      Next>

 

Procedural Assertions

In practice, most sequential assertions are expressed as some form of implication, and thus require the assertion writer to specify the antecedent expression to trigger the assertion. As mentioned previously, one of the key advantages of unifying assertions with the design language is to make it easier for the design engineer to embed assertions in the design. However, declarative assertions, by their very nature, often require additional work by the designer to use them effectively.

Consider a finite state machine design. Assertions in this type of design are often of the form �when in this state, then that should happen,� such as �when in state ACK, if foo is high, then req should be held low for 5 clocks.� This assertion could be coded declaratively as:

P4: assert property(

@(posedge clk) (st == ACK) && (foo == 1) |-> !req[*5]);

Now, consider what the RTL code would look like for the companion state machine:

always @(posedge clk)

case (st)

  ACK:

  if (foo == 1)

        begin // when in this state, req should be low for 5 clocks

               ...

       end

  ...

endcase

It is interesting to note that there are two specific pieces of information that are duplicated in the design and the assertion: the clock and the trigger state. Instead of requiring the designer to duplicate this information, the fact that the assertions are syntactically part of the design language allows them to be embedded procedurally in the RTL code and automatically infer this information from the usage, as in:

always @(posedge clk)

case (st)

  ACK:

  if (foo == 1)

   begin

         P5: assert property (!req[*5]);

         ...

   end

This procedural concurrent assertion (P5) is defined to be semantically equivalent to the declarative concurrent assertion (P4) above, but is much easier to use and maintain. Procedurally embedded assertions use the sampled values of signals to evaluate the inferred trigger condition, just as declarative assertions do. The inferencing rules for the antecedent include both case and if-else statements, allowing arbitrarily complex triggers to be inferred for procedural assertions. The resulting advantage for procedural assertions is simple maintenance. That is, if the finite state machine code is modified, the triggering condition for the assertion is automatically updated, whereas the user would have to modify the code manually to update the trigger of the corresponding declarative assertion, introducing the possibility that the assertion will no longer accurately reflect the design.

Assertion and Testbench Interaction

As stated previously, a significant advantage of unifying assertions with the design and verification language is the ability for the assertions to communicate information to the testbench. In a standalone assertion language there is no such communication mechanism. In SystemVerilog, the pass and fail statements of an assertion may execute any procedural statement, allowing the user to notify the testbench that a sequence occurred, update coverage counters, or anything else that may contribute to the effectiveness of the verification, including setting signal values, calling class object methods, or even calling C code.

Consider a bus protocol that includes the property �a new bus cycle may not start for 2 clock cycles after an abort cycle occurs.� This property could be coded as:

property wait_after_abort;

        @(posedge clk) abort_cycle |=> !cycle_start[*2];

endproperty

P6: assert property (wait_after_abort);

When the abort_cycle sequence is detected, the property dictates that the cycle_start signal will be low for two clocks. The property P6 codifies this behavior, and can be used as a monitor in simulation to check the behavior, or in a formal tool to try to prove that the behavior will never occur.

However, if this property is defining the behavior of a top-level interface, the testbench will be generating the bus transactions that must conform to this behavior. The verification engineer writing the testbench can reuse the assertion information as a constraint to help ensure that the generated stimulus does not violate the behavior. Such a testbench might look something like:

program manual_stimulus_generator;

repeat(1000)

begin

     generate_transaction(addr,data);

     while(wait_cnt > 0)

            @(posedge clk) wait_cnt--;

 end

endprogram

The wait_cnt counter is used to specify the delay between bus transactions generated by the testbench. The abort_cycle sequence can be used to set this counter by using a cover directive:

cover property( abort_cycle ) wait_cnt = 2;

Using the cover directive allows the abort_cycle sequence to be detected, without producing an error if it is not. When the sequence is detected, the wait_cnt counter is set to 2, causing the testbench to wait 2 cycles before generating the next transaction. The scheduling semantics of SystemVerilog ensure that there will not be a race condition between the execution of the pass statement and the testbench, which could not be guaranteed if the assertion were in a different language.

SystemVerilog includes the ability to specify an explicit synchronous interface between the testbench and the design. The clocking domain construct defines when the testbench will sample and drive device-undertest (DUT) signals relative to a clock. By default, the sampling of signals by the testbench is the same as the sampling used by assertions, ensuring that the testbench has access to the same values as the assertions. As mentioned previously, this not only avoids race conditions between the testbench/assertions and the DUT, but it also affords the testbench a �post-synthesis� view of the design behavior, with race conditions resolved according to synthesis rules, during pre-synthesis RTL verification.

 

  <Previous   TOC        Next>

Home   |    About Us   |   Articles/ Tutorials   |   Downloads   |   Feedback   |   Links   |   eBooks   |   Privacy Policy
Copyright � 2005-2007 electroSofts.com.
[email protected]