verificationspecmane

e HVL (IEEE 1647): expect expression fails unexpectedly


I'm trying to verify a pretty simple handshake between two modules. One module is on a slow clock and raises "req", the faster module should raise "ack" on the next fast clock and hold it until the next slow clock posedge. The end result looks like this:

req-ack wave diagram example

This is how I wrote the expect:

expect expect_ack_when_req_go is
      (@req_rise_e) => @ack_rise_e
      else dut_error("ERROR: ack expected to be asserted when req rises!");

*both @req_rise_e and @ack_rise_e are sampled on slow clock.

Running the simulator yields the error as the first expression seems to succeed but the second one does not. This is despite the fact that when tracing events to the wave, I can see both events occur together (as seen in the wave: event_req, event_ack).


Solution

  • You're trying to do overlapped implication, i.e. both your events happen in the same cycle. What the => operator does is check that the consequent happens on the next sampling event, in this case the next slow clock edge. This is called non-overlapped implication in SystemVerilog assertion parlance.

    You can get your desired behavior by writing the following:

    expect expect_ack_when_req_go is
      (@req_rise_e) => detach({@ack_rise_e; ~[1]})
      else dut_error("ERROR: ack expected to be asserted when req rises!");
    

    Full explanation here.

    On a methodological note, I would recommend against writing the temporal expression in a different way. I'm assuming that you are verifying the module that is driving ack and this module works on both clocks. I would also assume that this module samples req with the fast clock. It would be clearer to formulate your check as:

    expect expect_ack_when_req_go is
      (@req_rise_at_fast_clock_e) => @ack_rise_at_slow_clock_e
      else dut_error("ERROR: ack expected to be asserted when req rises!");
    

    This way you don't have to mess around with detach(...) and the expect more closely matches the natural language description of your desired behavior.