Goals:
1.  More compact notation

One of our goals was to make the assertion notation more compact.
Consider the following requirement:

     "Signal curr_state is one-hot"

The complete assertion to encode this requirement would be

     a_cstate_oh : assert property (@posedge clk disable iff !reset_n $onehot(curr_state));

Already, the 1800-1995 standard allows the assertion statement to be shortened somewhat by using a default clocking:

     default clocking mclk @(posedge clk);
     endclocking

     a_cstate_oh : assert property (disable iff !reset_n $onehot(curr_state));

The clock can also be inferred from context when the assertion is placed within a procedural block.

Mantis 1648 (approved) adds the capability to set a default disable condition for a block.  This frees the user from writing a disable iff condition in every property in that block.

     default clocking mclk @(posedge clk);
     endclocking
     default disable iff reset_n;

     a_cstate_oh : assert property ($onehot(curr_state));

This makes the assertion much more compact.  If there are a large number of assertions within a block, there can be significant saving, and the resulting code should be much easier to read, as the intent is not obscured by multiple clocking and disable conditions in the assertions.

2.  Encapsulation of more complicated assertion structures

A second goal was to allow better ways of encapsulating assertion structures.  The 1800-1995 standard currently allows at least two ways to encapsulate assertion structures.  The first method is to declare a parameterized named property and use it in multiple places.

     property p_one_hot (input sig);
   $onehot(sig);
     endproperty:p_one_hot

     assert property (p_one_hot(curr_state));
     assert property (p_one_hot(mux_select));

However, this only works when encapsulating a single property.  If we wanted to encapsulate the property checking with coverage, or if some modeling code was required, then we would be forced to use a module to do this.

     module m_one_hot #(Width) (logic clk, reset_n, logic [Width-1:0] sig);
       assert property (@(posedge clk) disable iff reset_n $onehot(sig));
       cover property ( . . .);
     endmodule

This property module would be instantiated as follows:

     m_one_hot  #(.Width(5)) a_sig_x_oh (.clk(clk), .reset_n(reset_n), .sig(x));

Note that we can't use default clocking and default disable iff to make the instantiation more compact.  However, if standard names are used in the design, we could make the instantiation more compact like this:

     m_one_hot  #(.Width(5)) a_sig_x_oh  (.sig(x), .*);

For simple properties like one-hot, it's quicker just to use custom code, rather than the library module!  In addition, module instantiations are not a flexible as assertions in terms of placement.

Our goal for the checker construct was to create a verification unit to encapsulate assertions, coverage, and any necessary modeling logic that had the same flexibility and conciseness as assertions themselves.


3.  Modeling code

It's important for the checker construct to allow modeling code, as not everything is amenable to being described in a temporal language.
I feel that regular always, always_ff, or always_comb procedures would be enough.  I suspect that the special checker variables exist to create an envionment within a checker that restricts the user to a synthesizable subset for formal verification.


4.  Randomization/free variables

Some formal techniques require random variables for a given proof technique.  We had created a new thing called a freevar, but I see no reason why we couldn't simply use a "rand".
NOTE:  I see possible applications of this outside of checkers as well. 
For example, I would like to assign a checker input to a random value in a bind statement.

Currently, most commercial formal tools will randomize any un-driven variable (an unconnected input port, or a signal definition with no driver).  This allows us to essentially create random variables by defining a wire and just not assigning to it, but it usually requires lots of explanatory comments in the code.  This is how we handle this today.

5.  Misc

It might be nice to have a more generic clocking event.  This would allow the same checker to be used in one block with a posedge clock, and in another block with a negedge clock.  In fact, we did this in many of the examples in 1900.  We used an port of type event for the clock port of the checker, and used "@posedge clk"  or "@negedge clk" as the signal connection in the instantiation port list.  The problem is that there are very few examples of events, and I'm not sure if this is even legal.


A side note:  In any current module context, an always block with the following form:

     always @(clk)  q <= d;

Will be synthesized (i.e. formal verification tools will interpret this
) as a combinational assignment (with warnings about missing signals in the sensitivity list), not as a flip-flop clocked on both edges of the clock.  Note that simulators will will simulate this correctly.  But there is no way to describe this currently, and this is part of the motivation for the always_check procedure.  Even the following:

     always_ff @(clk)  q <= d;

generates a compile error in at least one simulator.  This is not just an assertion problem.  Several times I have had to code a model for an exotic library flip flop that was clocked on both edges of the clock, and have always had trouble with it.

-- ErikSeligman - 13 May 2008