|
As ASICs continue to grow in size and complexity, traditional verification techniques relying on procedural testbench languages are no longer sufficient. Stimulus generation needs to be further automated to accelerate coverage closure. Checkers and coverage monitors need to be more concisely specified, and bugs need to be more quickly isolated to decrease debugging time. More than fifty percent of the verification effort is spent on debugging errors. Debugging using end-to-end checkers requires tracing the error from the external interface back to the source. In complex designs, debugging is almost impossible without the help of intermediate checkers. Since assertions pinpoint errors at the source, they can be used as intermediate checkers and debug becomes much easier and faster. Figure 1 shows the productivity improvements that can be gained by using assertions.
< i>1. Assertions improve Coverage and Verification productivity. Results with directed testing method are shown in red; coverage driven, directed random results in blue; assertion and coverage driven, directed random in green.
As figure one shows assertions enable productivity improvements and reduce the risk of bugs by concisely specifying temporal behaviors for portable checkers and coverage points, pinpointing bugs closer to their source, and enabling formal model checking techniques to automate stimulus generation.
SystemVerilog Assertions (SVA) is a part of SystemVerilog and is being used in the verification of designs. To deploy SVA, guidelines need to be established which define where assertions should be added. The guidelines should also specify who writes the assertions, how they are controlled and how to ensure there are a sufficient number of assertions for each design.
SVA is a very concise yet expressive language in that each of its constructs can describe complex behaviors. There are subtle semantics of the language, which might not be fully understood, causing the resulting behavior to be different from what was intended. Therefore, it is recommended that coding guidelines be specified for SVA.
Temporal languages are different from procedural languages and thus have a higher learning curve. The key to successfully deploying assertions lies in solid language training from the start. Another key to successful deployment of assertions is to keep things simple, so starting with predefined assertions is easiest. Properties and sequences for custom SVA assertions can be created later. Predefined assertions can be created using assertion checker libraries, which are a predefined set of Verilog checker modules that check common behaviors. Accellera has a standardized set of checker modules known as Open Verification Library (OVL). Most tool vendors also supply checker libraries, which usually extend the OVL functionality adding some proprietary extensions and checkers.
Checker libraries can be used by instantiating the checker module in the RTL. For example, the assert_always checker module from the OVL library can be used to specify a condition that must always be true. The example below shows a counter that uses assert_always to verify that count never exceeds 143. For more details on the OVL checker library, the user should refer to the Accellera Open Verification Library reference manual.
module test_assert_always(reset_n, clk);
input reset_n, clk;
reg [7:0] count;
wire clr;
always @(posedge clk)
count <=(~reset_n || clr) ? 8'b0 : count <= count+8'd1;
assign clr = (count >= 8'd143) ? 1'b1 : 1'b0;
assert_always
#('OVL_ERROR,'OVL_ASSERT,"ERROR: count > 143",'OVL_COVER_ALL)
chk_cnt (clk, reset_n, ((count > 8'd0) && (count <= 8'd143));
endmodule
Checker library modules are a good way to start using assertions; however, they do not cover all of the different checks or coverage points needed for the entire design. A significant number of behaviors in a given design require the user to write custom SVA assertions. Therefore, to ensure a sufficient number of assertions are written for a given design, the user must write custom SVA assertions. In addition, since checker modules are written for generic usage, they contain a lot of additional code to support different configurations, to control different behaviors and to control the various levels of checking and coverage. A custom SVA assertion because it is written for a specific behavior has far less overhead than a checker module so it will provide better performance.
The example below shows a simple SVA based custom assertion that checks for Xs or Zs on control signals. Most SVA assertions will be more complicated but compared to a generic checker library module they will provide less overhead and maybe better suited to describe certain behaviors.
property PnotXorZ (expr);
@(posedge CLK)
disable iff (!reset_done)
!$isunknown (expr);
endproperty
Ap_check_unknown : assert property (PnotXorZ({req1,gnt1,req2,gnt2}));
Effective use of custom SVA assertions requires usage and coding guidelines. A complete discussion of the usage issues and coding guidelines can take up an entire volume; therefore, we have limited ourselves a brief overview of the issues in this article. For more details on these topics, please refer to "The Art of Verification with SystemVerilog Assertions."
Where to Add Assertions
Assertions should be used in both design and testbenches. In design, they should be added in the RTL and used to check design intent, invariants, behaviors of various higher-level logic elements, or to specify interesting coverage points. In testbenches, assertions can be used as temporal checkers as well as to specify coverage points.
Table 1 shows where assertions should be used in RTL to check behaviors and to specify coverage points. Table 2 shows how assertions can be used in testbenches.
Table 1. How to use checker assertions in RTL.
Click here for a larger version.
Table 2. How assertions can be used in testbenches.
Click here for a larger version.
|
