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);