Problem:

The problem with error reporting is that the error message does not
directly have access to the signal values and local variables used
in the property to determine a legal sequence of actions or an illegal
sequence.

For example, this property has signals and variables:

property follow_req(a, b, c, address)
  reg [31:0] req_addr;
  @(posedge clk) // Simple example
  (a, (req_addr = address)
     => b ##1 c)
endproperty

assert follow_req(a, b, c, address)
 else
  $error("C (%0d) did not follow b after a with address %0h.\n", c, req_addr);
  // 'c' and req_addr may show the wrong value.

In addition to the difficulty in creating an error message, it will be difficult
to track operation of some sequences and the setting of local variables. 

Motivation:

1. Provide support for error messages using same context of signal values as the property.
2. Provide support for error messages using local variables from the assertion context.
3. Provide debug support for debugging the flow of sequences and local variable settings.



Solution:

[We currently can not define a solution to provide for one error message for the failure
of properties. There are too many questions to be resolved to come up with a full
definition.]

Insert after section 17.8 "Manipulating data in a sequence"

17.9 Messages within sequences.

Messages can be included in sequences to aid in debug of sequences, or to produce
error messages with contextual information. Messages are produced through these
system tasks: $display, $fatal $error, $warning, $info. 

Messages are added within the sequence, after an expression.

  sequence_expr ::=
     ...
    | expression, blocking_assign_or_message

As an example, after 'a' we expect 'b' and we store the value of 'v' into the local
variable 'loc_v'. We then report a message using $display() with the shown string.
We then proceed to expect 'c' one cycle later.

   a ##1 b, (loc_v = v, $display("loc_v is %0h at time %d.", loc_v, $stime))
     ##1 c

These system tasks do not produce a value (a function) they simply execute in the
order they are listed. These messages can be for debug or for error reporting.

[ Not yet. if (b |-> pass_p) and (!b |-> fail_p) then why not
  (first_match(b_p) |-> pass_p) and (!first_match(b_p) |-> fail_p)
 This would make it easier for messages. ]
For error messages, the if() structure allows for checking of the failure of
a sequence or property and subsequent failing of the property and provision
of a correct error message. 


   a |->  if (##[1:10] b) 1 else 0, $error("Did not receive b within 10 cycles.")

Here if the sequence (##[1:10] b) fails then the else branch is taken which yields 0
and executes the $error() routine. This routine shall replace any implicit $error()
routine call (when there is no fail statement in an action block.) If a fail statement
is included in an action block, any $error() (or fatal or warning) calls shall override
the error routine from the property or sequence.

Messages shall not be attached to the success of a sequence. Only a boolean expression
may preceed a message statement. When a sequence is expected to fail, inversion of the
sequence followed by a message will suffice.

    a |->  not ##[1:10] b |-> 0, $error("Did not receive b within 10 cycles.");