[sv-ac] some thoughts on assertions in procedural code

Here is a simplification of Dmitry's example:

    always @(posedge clk) 
    begin
       if (en) 
       begin
          c1 <= c2 || b;
          p: assert property (c2 |=> c1);
       end
    end

Existing inference:

    p: assert property (en |-> c2 |=> c1);

Let's assume that the NBA is the only place that c1 is updated.

Assume first that the value of en when evaluated in the procedural code is the
same as its preponed value.

1. Then the "dispatching" semantics and the existing extracted
   semantics will match.

2. If the value of c2 when evaluated in the RHS of the NBA is the same
   as its preponed value, then the assertion should not fail.
   Otherwise, if the preponed value of c2 is 1 and the value of c2 || b 
   is 0 when evaluated in the RHS of the NBA, then the assertion will fail.
   
Suppose now that the value of en when evaluated in the procedural code is not
the same as its preponed value.  Let's change the example to show how the
enabling might differ from its preponed value due to being computed in the
always procedure.

    always @(posedge clk) 
    begin
       automatic trans_type trans = compute_trans(trans_arg);
       if (trans.en.a) 
       begin
          state.a <= trans.next.a;
          pa: assert property ($current(trans.next.a) iff nexttime state.a);
       end
       if (trans.en.b)
       begin
          state.b <= trans.next.b;
          pb: assert property ($current(trans.next.b) iff nexttime state.b);
       end
    end

Here I've used $current instead of the "const" syntax for kicks.  I guess that
we will need to think about how to make the context aware of information about
use of $current if this syntax is preferred.

I think this example will work as desired with the "dispatching" semantics.  
I don't think that this example will work as desired with the existing 
extracted semantics.

Here is a recoding with property instantiation:

    property p (new_st, next_st);
       new_st iff nexttime next_st;
    endproperty

    always @(posedge clk) 
    begin
       automatic trans_type trans = compute_trans(trans_arg);
       if (trans.en.a) 
       begin
          state.a <= trans.next.a;
          pa: assert property (
             p(.new_st($current(trans.next.a)), .next_st(state.a))
          );
       end
       if (trans.en.b)
       begin
          state.b <= trans.next.b;
          pb: assert property (
             p(.new_st($current(trans.next.b)), .next_st(state.b))
          );
       end
    end

If $current is in the actual arguments, then the local context will be 
aware of its obligation to hook up the current value.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.