Skip to question
asic.fyi

Hardware interview practice

Formal proof plan for a synchronous FIFO

HardAssertions and FormalSystemVerilog

A parameterized synchronous FIFO has ready-valid input and output ports. Construct a formal harness that proves no overflow, no underflow, correct ordering, and stable output under backpressure without relying on a directed test sequence.

Starting point

Question code

input logic clk, rst_n;
input logic in_valid, in_ready; input logic [7:0] in_data;
input logic out_valid, out_ready; input logic [7:0] out_data;
Reviewed example

Work through one case

Input
Accepted inputs are A then B; the DUT presents B as its first valid output
Expected output
a_front_matches fails because ghost_q[0] is A

The ghost queue is updated only on accepted handshakes, so its front is an order-independent oracle for the next legal output.

What to cover

Requirements

  1. Constrain only legal reset; leave in_valid, in_data, and out_ready arbitrary and do not assume DUT-driven outputs.
  2. Track accepted writes minus accepted reads in ghost occupancy and assert bounds plus matching empty/full handshakes.
  3. Use a ghost queue to assert every accepted item emerges exactly once in order, with out_data stable while stalled.
  4. Cover empty-to-full, simultaneous input/output, drainage, and enough accepted writes to exercise pointer wraparound.
Continue practicing
Assertions and FormalPlace a formal environment constraintRTL DesignBuild a synchronous FIFO and race-free BFMHardware-Software IntegrationVerify keypad expansion and FIFO draining