Interview Question · Code Reading

One Arrow or Two: Overlapping Implication

L0 FresherL1 Juniorsvaimplication

The interviewer asks

The spec says gnt is high the cycle after req. Here is the design and its assertion. Does the assertion pass?

systemverilog

// Spec: gnt is high the cycle after req.
always_ff @(posedge clk) gnt <= req;

a_gnt: assert property (@(posedge clk) req |-> gnt);

Reveal the Model Answer

No, it fails on every request. |-> is overlapping implication. The consequent (the right side) starts at the same edge where the antecedent (the left side) matched. So it demands gnt in the same cycle as req. The spec needs |=>, which starts the consequent one edge later and is exactly req |-> ##1 gnt.

A grant one cycle after the request

Same trace, two verdicts. Only the arrow changed.

Self-Check

Tick each key point you covered in your answer.

Key point 1 No, it fails on every request. Key point 2 |-> is overlapping implication. Key point 3 The consequent (the right side) starts at the same edge where the antecedent (the left side) matched. Key point 4 So it demands gnt in the same cycle as req. Key point 5 The spec needs |=>, which starts the consequent one edge later and is exactly req |-> ##1 gnt.

What Interviewers Listen For (Fresher)

A good fresher answer says |-> checks the same edge and |=> checks the next one. It spots the failure straight from the spec sentence.

Cross-Questions

Where the interviewer goes next. Open a node to practise that follow-up.

WhyWhat IfProve ItCompare

One Arrow or Two: Overlapping Implication
WhyWhy the Language Has Both ArrowsL1 Junior
If a |=> b is just a |-> ##1 b, why keep both?

Reveal the Model Answer

Registered outputs, the common case, answer one cycle later, so |=> keeps those rules short and readable. Overlapping implication fits a response in the same cycle. Examples are a combinational output, or a condition checked while a signal is held. Either can express the other with ##, so pick the one that matches the spec sentence.

Self-Check
Tick each key point you covered in your answer.
Key point 1 Registered outputs, the common case, answer one cycle later, so |=> keeps those rules short and readable. Key point 2 Overlapping implication fits a response in the same cycle. Key point 3 Examples are a combinational output, or a condition checked while a signal is held. Key point 4 Either can express the other with ##, so pick the one that matches the spec sentence.

Misconception

"|=> checks the consequent at the falling edge."

Both arrows count ticks of the property's clock; |=> simply starts one tick later.

Source IEEE 1800-2017 §16.12.7
- Lesson A1.3Implication and Vacuous Success
What IfWhere a Longer Antecedent EndsL1 JuniorL2 Mid-Level
What if the antecedent is a sequence, as in req ##1 grant |-> data_valid? Which edge does data_valid belong to?

Reveal the Model Answer

The consequent starts at the end point of the antecedent, the edge where grant matched, one edge after req. So data_valid must be high in the same cycle as grant. With |=> it would be one edge after grant.

Self-Check
Tick each key point you covered in your answer.
Key point 1 The consequent starts at the end point of the antecedent, the edge where grant matched, one edge after req. Key point 2 So data_valid must be high in the same cycle as grant. Key point 3 With |=> it would be one edge after grant.

Misconception

"The consequent is checked at the edge where the antecedent started."

Implication starts the consequent at each end point of the antecedent sequence, not at its start.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §8 (PDF p128-139)
Prove ItSolve 6.6.7: Count the BeatsSimulator-graded

Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
Open Problem 6.6.7
CompareImplication vs a Plain Sequence PropertyL1 JuniorL2 Mid-Level
Compare assert property (req |=> gnt) with assert property (req ##1 gnt).

Reveal the Model Answer

The implication is a conditional rule: on edges without req the attempt succeeds vacuously, and only edges with req check gnt. The plain sequence must match from every attempt, so every edge where req is low fails. A plain sequence fits a cover property that asks whether the scenario ever happened; assertions almost always need the implication.

Edge req |=> gnt req ##1 gnt

req low Vacuous pass Fails
req high, gnt next Pass Pass
req high, no gnt next Fails Fails

The first row is the difference: a plain sequence must match from every edge.

Self-Check
Tick each key point you covered in your answer.
Key point 1 The implication is a conditional rule: on edges without req the attempt succeeds vacuously, and only edges with req check gnt. Key point 2 The plain sequence must match from every attempt, so every edge where req is low fails. Key point 3 A plain sequence fits a cover property that asks whether the scenario ever happened; assertions almost always need the implication.

Half-Truth

"The sequence form is stricter, so it is the safer assertion."

It is not stricter, it is a different claim: that the pattern starts at every single edge. It fails on idle cycles of a correct design.

Source Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.), §17.16 (PDF p285)
- Lesson A1.3Implication and Vacuous Success
WhyWhy Implication Passes When the Antecedent Is FalseL1 Junior
Why does the language make a |-> b succeed when a is false, instead of failing or skipping it?

Reveal the Model Answer

An attempt starts at every clock tick, so one assertion is evaluated thousands of times. The implication says "whenever a holds, b must follow". A tick without a breaks no promise, so it has to succeed. If it failed instead, the assertion would fire on every idle cycle and be useless.

Self-Check
Tick each key point you covered in your answer.
Key point 1 An attempt starts at every clock tick, so one assertion is evaluated thousands of times. Key point 2 The implication says "whenever a holds, b must follow". Key point 3 A tick without a breaks no promise, so it has to succeed. Key point 4 If it failed instead, the assertion would fire on every idle cycle and be useless.

Misconception

"Implication only starts an attempt when the antecedent is true."

An attempt starts at every tick. On ticks without a match, it ends at once as a vacuous success. That is why the pass count can be huge.

Source IEEE 1800-2017 §16.5, §16.14; Mehta, SystemVerilog Assertions and Functional Coverage (3rd ed.) §6.6 p97
- Lesson A1.3Implication and Vacuous Success
What IfAn Antecedent That Starts but Does Not FinishL1 JuniorL2 Mid-Level
What if the antecedent is a ##1 b, and a is seen but b never follows? Is the consequent checked?

Reveal the Model Answer

No. The consequent starts only from an end point of the antecedent. A partial match has no end point, so the attempt ends as a vacuous success. A half-started request therefore counts as a pass. Cover the full antecedent to see whether complete requests happened.

Self-Check
Tick each key point you covered in your answer.
Key point 1 No. Key point 2 The consequent starts only from an end point of the antecedent. Key point 3 A partial match has no end point, so the attempt ends as a vacuous success. Key point 4 A half-started request therefore counts as a pass. Key point 5 Cover the full antecedent to see whether complete requests happened.

Misconception

"Once the antecedent starts, the consequent is checked."

The check waits for the antecedent to match completely. A partial match gives no end point and no check.

Source IEEE 1800-2017 §16.12.7
- Lesson A1.3Implication and Vacuous Success
Prove ItSolve 6.6.8: Answer in TimeSimulator-graded

Show it, don't just say it: this Silicon Lab problem is graded by the simulator.
Open Problem 6.6.8

Edge	`req \|=> gnt`	`req ##1 gnt`
`req` low	Vacuous pass	Fails
`req` high, `gnt` next	Pass	Pass
`req` high, no `gnt` next	Fails	Fails

What People Get Wrong

Common wrong answers and why they fail. Run It shows the wrong belief failing on a real simulator.

Misconception

"|-> checks the consequent in the next cycle."

Overlapping means the consequent starts at the edge where the antecedent ended. The twin's correct design fails twice under |-> and passes under |=>.

Run It

A design that grants one cycle after each request, checked with |->.

RUNVerilator · simulator service

Edit the code, then run it

Expected: failures=2 FAIL: |-> checks gnt at the same edge as req, so a correct design fails

module tb;
  logic clk = 0, req = 0, gnt = 0;
  int fails = 0;
  always #5 clk = ~clk;
  always @(posedge clk) gnt <= req;     // the design: grant one cycle after the request
  // The belief: |-> checks gnt in the next cycle.
  a_gnt: assert property (@(posedge clk) req |-> gnt) else fails++;
  initial begin
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    repeat (2) @(negedge clk);
    $display("failures=%0d", fails);
    if (fails > 0) $display("FAIL: |-> checks gnt at the same edge as req, so a correct design fails");
    $finish;
  end
endmodule

See the Fix

module tb;
  logic clk = 0, req = 0, gnt = 0;
  int fails = 0;
  always #5 clk = ~clk;
  always @(posedge clk) gnt <= req;     // the design: grant one cycle after the request
  // The fix: |=> starts the consequent one edge later.
  a_gnt: assert property (@(posedge clk) req |=> gnt) else fails++;
  initial begin
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    @(negedge clk) req = 1;
    @(negedge clk) req = 0;
    repeat (2) @(negedge clk);
    $display("failures=%0d", fails);
    if (fails == 0) $display("PASS: |=> checks gnt one edge after req");
    $finish;
  end
endmodule

Prints: failures=0 PASS: |=> checks gnt one edge after req

Misconception

"req && gnt is the same rule without the arrow."

Without implication the property must hold at every edge, so it fails on every idle cycle where req is low.

Source IEEE 1800-2017 §16.12.2

Missed Corner

"Use ##1 before gnt and also switch to |=> to be safe."

req |=> ##1 gnt waits two edges. Stacking both is the most common off-by-one in assertion reviews.

Source IEEE 1800-2017 §16.12.7

Find Your Next Track

Put Your Skills to Work

Prepare to Explain Your Thinking

An Idea to Try? Pick a Tool.

One Arrow or Two: Overlapping Implication

Your Answer

Self-Check

What Interviewers Listen For (Fresher)

What Interviewers Listen For (Junior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It

The Question

Your Answer

Self-Check

What Interviewers Listen For (Fresher)

What Interviewers Listen For (Junior)

Cross-Questions

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

Your Answer

Self-Check

What People Get Wrong

Learn It, Then Prove It