Where the consequent starts

An implication has two halves. The antecedent is a sequence that triggers, and the consequent states the obligation.

Every clock tick starts one attempt. If the antecedent matches, the consequent must hold from each match endpoint.

|-> starts the consequent on the antecedent end tick. |=> starts it one tick later, which is exactly |-> ##1.

1
2
3
4
5
6
7

// snippet
property p_ovl;
  @(posedge clk) req |-> gnt;
endproperty
property p_novl;
  @(posedge clk) req |=> gnt;
endproperty

For a sequence consequent, a |=> s equals a |-> ##1 s. In general, a |=> p equals a ##1 1 |-> p, which also covers a property consequent. Windows need |-> ##[M:N], since no ranged |=> exists. The reverse has no clean form, so |-> is the primitive and |=> is sugar for the one-cycle case.

One stimulus, opposite verdicts

The diagram drives req for one cycle and answers with gnt in the next cycle.

• Slot 0: req 0, gnt 0. The antecedent is low, so the attempt is vacuous.

• Slot 1: req 1. Overlapped samples gnt now (0) and fails, while nonoverlapped waits one tick.

• Slot 2: gnt 1. Nonoverlapped samples 1 and passes.

• Slot 3: both 0. Idle attempt.

• Slot 4: both 0. Idle attempt.

Attempt and failure ticks shift by one with the consequent start. On this stimulus the two forms give opposite verdicts, though with gnt held high both would pass.

Choosing the operator

With (req ##1 ack) |-> done, done is checked on the ack cycle. With |=> it is checked one tick after ack.

Testbench

A registered grant plus the testbench that proves both forms agree on it.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

module tb_impl_ovl;
  timeunit 1ns; timeprecision 1ps;
  logic clk = 0;
  always #5 clk = ~clk;
  logic rst_n = 0;
  logic req = 0;
  logic gnt = 0;
  logic req_q = 0;
  int checks = 0;
  int errors = 0;

  always @(posedge clk) begin
    if (!rst_n) gnt <= 1'b0;
    else gnt <= req;
  end

  a_novl: assert property (@(posedge clk) disable iff (!rst_n) req |=> gnt);
  a_desugar: assert property (@(posedge clk) disable iff (!rst_n) req |-> ##1 gnt);

  always @(posedge clk) begin
    req_q <= req;
    if (rst_n && req_q) begin
      checks <= checks + 1;
      if (gnt !== 1'b1) errors <= errors + 1;
    end
  end

  initial begin
    rst_n = 0;
    req = 0;
    repeat (2) @(negedge clk);
    rst_n = 1;
    @(negedge clk);
    req = 1;
    @(negedge clk);
    req = 0;
    repeat (4) @(negedge clk);
    if (checks == 1 && errors == 0)
      $display("PASS: grant sampled high one cycle after req; both implication forms agreed");
    else
      $fatal(1, "FAIL: grant timing off");
    $finish;
  end
endmodule

PASS: grant sampled high one cycle after req; both implication forms agreed

Related topics

• Vacuous Success

• Sequences