Skip to question
asic.fyi

Hardware interview practice

Ready-valid protocol assertions

MediumAssertions and FormalSystemVerilog

A monitor must catch a producer that changes or withdraws an item while the consumer applies backpressure. Write clocked SVA properties for the stated ready-valid rules and one useful coverage sequence.

Starting point

Question code

input logic clk, rst_n, valid, ready;
input logic [31:0] data;
Reviewed example

Work through one case

Input
Cycle 1: valid=1 ready=0 data=32'hAA
Cycle 2: valid=1 ready=0 data=32'hAA
Cycle 3: valid=1 ready=1 data=32'hAA
Expected output
All assertions pass; the two-stalls-then-transfer cover property is hit.

The producer holds both valid and payload across every stalled edge, then completes the transfer without any X or Z values.

What to cover

Requirements

  1. Disable every assertion while rst_n is 0.
  2. If valid is 1 and ready is 0 on one edge, require valid to remain 1 and data to be stable on the next edge.
  3. On every rising edge while reset is inactive, assert that valid is not X or Z. If valid is exactly 1, also assert that every bit of data is known.
  4. Cover a legal sequence with two stalled cycles followed by a cycle on which valid and ready are both 1.
Continue practicing
Assertions and FormalAssert ready-valid stability and responseAssertions and FormalPlace a formal environment constraintUVM ComponentsDrive a ready/valid interface correctly