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