SystemVerilog Cover Properties

Prev: More on properties

2. You can use a cover property inside an always block. In such case, if there is a clock specified in the sensitivity list of the always block (e.g., always @(posedge clk)) that must match with the clock specified in the property. If there was no clock specified in the property definition, then the simulation tool assumes that the property has the same clock as the always block where it is located.

always @(posedge clk) begin // {
   cover property fifo_nearly_full_p (
      rst, clk, fifo_nearly_full
   ); // legal 
   cover property fifo_nearly_full_p (
      rst, anotherClk, fifo_nearly_full
   ); // illegal - conflict in clock name
   cover property anotherProperty_p (
      rst, fifo_nearly_full
   ); // legal - uses 'clk' as clock
end 

3. A cover property can also be specified outside of a procedural block (such as, initial or always). In such case, it is equivalent of as if it is inside an always block.

   // 1 and 2 are equivalent
   // 1.
   cover property fifo_nearly_full_p (
      rst, clk, fifo_nearly_full
   ); 
   // 2.
   always cover property fifo_nearly_full_p (
      rst, clk, fifo_nearly_full
   ); 

What about vacuous successes?

If the tool that you are using reports the number of passes of a cover property, how about a vacuous success? Let us consider the following case: suppose there are two additional signals fifo_full that indicates that the FIFO is really full, and new_pkt, that tells us a new packet has arrived that needs to be written to the FIFO. Further assume it takes exactly two clock cycles for a new packet to be written to the FIFO.

property fifo_full_p (reset, clock, fifo_nearly_full, new_pkt, fifo_full) 
   @(posedge clock) (fifo_nearly_full & new_pkt |-> #2 fifo_full) disable iff (reset);
endproperty

cover property (reset, clock, fifo_nearly_full, new_pkt, fifo_full); 

When this looks all good, fifo_full may be asserted without the FIFO being nearly full and then one new packet arriving. It may also happen if the FIFO is empty and a packet large enough to fill up the entire FIFO arrives. Such cases of vacuous success is also reported separately by your tool.

Where is the report?

A typical cover property report looks like as shown below. It is a table that lists the number of attempts, the number of times it is a hit and how many times it can not be decided.

      Name                  Attempts      Matches       Incomplete 
      fifo_nearly_full_p    2147483647    7567          0

Prev: More on properties