1,000+ ASIC Interview Questions: SystemVerilog, UVM & RTL

DescriptionQ768

Page ↗

Q768DVMetaASIC interview problem

Formal proof plan for a synchronous FIFO

TechniquesDVFormal verificationFIFOOrdering

DifficultyHard

TopicAssertions and Formal

LanguageSystemVerilog

Requirements4 checkpoints

Problem

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 declarationSystemVerilog

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;

Example input and output

Use this case to check your interpretation

Input

Accepted inputs are A then B; the DUT presents B as its first valid output

Output

a_front_matches fails because ghost_q[0] is A

Explanation

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

Requirements (4)

Constrain only legal reset; leave in_valid, in_data, and out_ready arbitrary and do not assume DUT-driven outputs.
Track accepted writes minus accepted reads in ghost occupancy and assert bounds plus matching empty/full handshakes.
Use a ghost queue to assert every accepted item emerges exactly once in order, with out_data stable while stalled.
Cover empty-to-full, simultaneous input/output, drainage, and enough accepted writes to exercise pointer wraparound.