Systemverilog Assertion (SVA) 2

Working Assertion Examples:

Normal inline assertion example:

assertStateStartShortFalse:

  assert property (@(posedge clk) disable iff(!reset_n)

  (state==`START) |-> (short==FALSE))

  else $display("Error state START and short is true  ");

Normal Assertion compile with VCS with +assert option
// Assertion example for parity checking
module check_par(clk, parity, data);
input clk, parity;
input [31:0] data;

property p_check_par;
@(posedge clk)  (^(data^parity)) == 1’b0;
endproperty
a_check_par: assert property(p_check_par);
endmodule


binddata_bus check_par u1(clk, parity, data);
bindtop.mid.u1 check_par u2(clk, parity, data);

For OVL, use +define+OVL_ASSERT_ON for OVL.
 
ovl_even_parity

[#(severity_level, width, property_type, msg, coverage_level,

clock_edge, reset_polarity, gating_type)]

instance_name (clock, reset, enable, test_expr, fire);
 
ovl_even_parity top.u1(clk, reset, 1, (^(data^parity)));
 

SVA ( System verilog Assertion)

1.  What are difference between SVA and other assertions?

Answer: Systemverilog Assertions (SVA) are temporal, Declarative and formal friendly.
             Temporal : Design Variables relationship in time
             Declarative: Orthogonal to procedural form in design (describe what instead of how )
             Synthesizable: Good for dynamic and formal verification.
             SVA provides interoperability with RTL, testbench features and functional coverage.

2.  What are the benefits of using assertions?
 
Answer:      1) Improve error detection
                   2) Better observability
                   3) Shortens debug time
 
3. Who writes Assertions?

 Answer:  White box (Designers)  , Black box (DV)

4.  How many ways to connect assertion to RTL?

Answer: There are 3 ways to connect assertion to RTL: inline, Instantiation and Virtual Instantiation (bind).

             Inline Assertion:  Assertion directly put into the RTL by designer. Use compile option for synthesis.

For example: 
// A synchronous D Flip-Flop
moduledff (input logic [7:0] D, input RST_, input CLK, output logic [7:0] Q);
always @(posedge CLK)
if (!RST_) Q<= 8'h0;
else Q <= D;

// assertions

propertyd_q_property_0 (clk, rst_, q);
@(posedge clk) !rst_ |->##1(q == 8'h0);
endproperty
assert_d_q_property_0 : assert property(d_q_property_0(CLK, RST_, Q));

endmodule

Assertion Instantiation: Put assertion into another module and use it again by RTL designers.

For example:

moduledff (input logic [7:0] D, input RST_, input CLK, output logic [7:0] Q);
always @(posedge CLK)
if (!RST_) Q<= 8'h0;
else Q <= D;

// Use assertion module here
dffChecker #(8) Chk0(CLK, RST_, D, Q);

endmodule  

moduledffChecker (clk, rst_, d, q);
parameter WIDTH = 8;
input clk, rst_;
input [WIDTH-1:0] d, q;
propertyd_q_property_0;
@(posedge clk) !rst_ |->##1 (q == 8'h0);
endproperty
assert_d_q_property_0 : assert property(d_q_property_0);
endmodule

Virtual Instantiation (bind): Use bind method to connection both modules together. It's a saftest method for DV because it did not change RTLs. Plus we can use OVL for most of common checkers.

For examples:

binddff dffChecker #(8) Chk0(CLK, RST_, D, Q);