This page is a revision map, not a second source. Each answer below is the ten-second version; the solver math and the sequence depth live in the drills topics and the lessons they link to.
If the interviewer asks | Revise in |
|---|---|
Even values, | |
Overlapping versus non-overlapping implication, vacuity, repetition, past values, reset handling | |
What coverage proves and when it closes |
Zero the low bits: addr[0] == 1'b0 for even, addr[1:0] == 2'b00 for multiples of four. Multiples of 2 to the N have N low zeros. See Even/Odd, Alignment & Divisibility.
:= weights each value in the range; :/ shares one weight across the range. Both forms also define the legal set: unlisted values can never generate. See dist: Weighted Distributions.
A soft constraint is a default the solver drops silently whenever a hard constraint contradicts it. See soft Constraints.
Only the distribution, never the legal set. See Implication, if/else and solve...before.
A with block adds one-call hard constraints, and names resolve to the object first, so local:: reaches the test scope. See Inline Constraints. randc permutes through every legal value once per cycle and fits small fields only. See rand vs randc.
// snippet
// rand bit [7:0] addr;
// constraint c_even { addr[0] == 1'b0; }
// constraint c_len { len dist { 1 := 50, [2:9] := 5 }; }
// constraint c_dflt { soft len inside {[1:8]}; }
// constraint c_ord { solve err before code; }
// assert(t.randomize() with { len == local::len; });
// randc bit [1:0] chan; // cycles 0,1,2,3 in a fresh order|-> starts the consequent the same cycle the antecedent completes; |=> waits one cycle, and a |=> b equals a |-> ##1 b. Registered responses need the non-overlapping form. See |-> vs |=>.
An implication passes vacuously whenever its antecedent never matches, checking nothing. Put a cover on every antecedent and audit it at closure. See Vacuous Success.
[*N] needs N back-to-back cycles, [->N] lands exactly on the Nth occurrence, and [=N] has a floating endpoint. See Repetition. Before N ticks of history exist $past returns the type default, so gate the opening cycles. See $past. disable iff aborts in-flight attempts asynchronously.
// snippet
// a_same: assert property (@(posedge clk) req |-> gnt);
// a_next: assert property (@(posedge clk) req |=> gnt);
// c_req: cover property (@(posedge clk) req);
// a_burst: assert property (@(posedge clk) start |-> (beat [->3]) ##1 done);
// a_stable: assert property (@(posedge clk) disable iff (!rst_n)
// (valid && !ready) ##1 valid |-> data == $past(data));Three checkers divide the work: the scoreboard catches data and ordering bugs, assertions catch cycle-accurate protocol violations, and coverage proves what was exercised. Coverage catches nothing by itself, and a cover on every assertion antecedent turns vacuity into a number. See Sign-Off Metrics and Review.
len dist { 1 := 50, [2:9] := 5 }: what weight does each value from 2 to 9 carry, and can 10 generate?Each carries weight 5, and 10 can never generate. The dist defines the legal set as well as the weights.
Nothing. The passes are vacuous, which is why every assert ships with a cover on its antecedent.