Q028FreeDesign Verification

Verify a RAM-based duplicate-ID detector

Difficulty: Medium
Topic: Memory Systems
Language: SV

Interview prompt

Question

Implement the shadow-memory oracle, completion audit, and core bus properties for a duplicate finder operating on software-programmed random-access memory (RAM) containing N+1 values. N is positive; DW must represent N+1 and may exceed 32. Stored words and observed RAM images retain all DW bits. Program every address 0 through N with a known value before the first START. Legal input has exactly one distinct repeated value; controlled higher multiplicity may omit other legal values, but two distinct repeated values are out of contract. Any zero or value above N takes data_error precedence. Call accepted_write only for an accepted idle write and snapshot_start only for an accepted idle START. A read accepted at C first presents its response at C+1; a previous read may retire on the same edge as a new read or write. Busy blocks all configuration acceptance. The supplied protocol module uses sampled rising-edge reset for control state; retained RAM and shadow contents are an environment policy, not cleared by an oracle reset method.

An immutable START snapshot and separately observed DUT RAM image are compared at every address, alongside an independent duplicate-value oracle. — For N=4, addresses are 0 through 4 and legal values are 1 through 4. The duplicate result is 2; memory preservation requires every observed word to match the START snapshot.

Candidate starting point

Implementation scaffold

class duplicate_ram_oracle #(int N = 15, int DW = $clog2(64'(N)+2));
  typedef logic[DW-1:0] word_t;
  typedef word_t image_t[0:N];
  image_t mirror, start_image;
  function new();
    if(N<1 || DW<$clog2(64'(N)+2))
      $fatal(1,"N must be positive and DW must represent N+1");
  endfunction

  function void accepted_write(int unsigned addr, word_t data);
  // TODO: Implement this oracle or scoreboard method.
endfunction

  function void snapshot_start();
  // TODO: Implement this oracle or scoreboard method.
endfunction

  function void predict(output bit data_error,
                        output int unsigned duplicate_id);
  // TODO: Implement this oracle or scoreboard method.
endfunction

  function bit memory_unchanged(input image_t observed_after);
  // TODO: Implement this oracle or scoreboard method.
endfunction

  function void check_completion(
      input logic got_data_error,
      input word_t got_duplicate_id,
      input image_t observed_after);
  // TODO: Implement this oracle or scoreboard method.
endfunction
endclass

module duplicate_ram_protocol_checker #(int DW=5)(
 input logic clk,rst_n,cfg_valid,cfg_ready,cfg_write,
 input logic cfg_rsp_valid,cfg_rsp_ready,busy,done,
 input logic[DW-1:0]cfg_rdata
);
bit read_pending;
always @(posedge clk) begin : sample_config_transactions
  // TODO: Track reset and accepted transactions; compare/retire old responses first.
end
property p_cfg_response_hold;
  // TODO: Implement this named temporal obligation.
endproperty
property p_done_is_a_pulse;
  // TODO: Implement this named temporal obligation.
endproperty
property p_no_cfg_accept_while_busy;
  // TODO: Implement this named temporal obligation.
endproperty
property p_reset_cancels_read;
  // TODO: Implement this named temporal obligation.
endproperty
assert_cfg_response_hold:assert property(p_cfg_response_hold);
assert_done_is_a_pulse:assert property(p_done_is_a_pulse);
assert_no_cfg_accept_while_busy:assert property(p_no_cfg_accept_while_busy);
assert_reset_cancels_read:assert property(p_reset_cancels_read);
final begin : check_unfinished_config_read
  // TODO: Reject incomplete outstanding work at test end.
end
endmodule

// TODO: Describe legal shuffled/higher-multiplicity images and the reset-retained RAM/shadow policy.

Reviewed example

Trace one case

Input

N=4; programmed RAM image = [1, 2, 3, 2, 4]; then repeat with [1, 0, 3, 2, 4]

Expected output

first run: duplicate_id=2, data_error=0; second run: duplicate_id=0, data_error=1

The first snapshot contains one legal repeated ID, while zero is outside the allowed 1..N data range and takes the error path.

What to cover

Requirements

Model addresses 0 through N and update the Register Abstraction Layer (RAL) shadow only for accepted configuration writes; reads respond one cycle later and hold until consumed.
Use legal shuffled images containing values 1 through N plus one repeated value, including controlled higher multiplicity.
Use a frequency oracle and classify zero or any representable value above N as data_error with duplicate_id zero.
Snapshot memory at accepted start, compare the functional result, and compare an observed post-search image with that snapshot.
Assert read timing, response hold, done pulse shape, and blocked configuration while busy; discuss reset-retained memory as a follow-up environment rule.

Continue practicing

Q113 · Memory SystemsVerify a channel-capacity optimizerMedium Q119 · UVM ComponentsVerify a RAL-programmed grid checkerMedium

class duplicate_ram_oracle #(int N = 15, int DW = $clog2(64'(N)+2)); typedef logic[DW-1:0] word_t; typedef word_t image_t[0:N]; image_t mirror, start_image; function new(); if(N<1 || DW<$clog2(64'(N)+2)) $fatal(1,"N must be positive and DW must represent N+1"); endfunction function void accepted_write(int unsigned addr, word_t data); // TODO: Implement this oracle or scoreboard method. endfunction function void snapshot_start(); // TODO: Implement this oracle or scoreboard method. endfunction function void predict(output bit data_error, output int unsigned duplicate_id); // TODO: Implement this oracle or scoreboard method. endfunction function bit memory_unchanged(input image_t observed_after); // TODO: Implement this oracle or scoreboard method. endfunction function void check_completion( input logic got_data_error, input word_t got_duplicate_id, input image_t observed_after); // TODO: Implement this oracle or scoreboard method. endfunction endclass module duplicate_ram_protocol_checker #(int DW=5)( input logic clk,rst_n,cfg_valid,cfg_ready,cfg_write, input logic cfg_rsp_valid,cfg_rsp_ready,busy,done, input logic[DW-1:0]cfg_rdata ); bit read_pending; always @(posedge clk) begin : sample_config_transactions // TODO: Track reset and accepted transactions; compare/retire old responses first. end property p_cfg_response_hold; // TODO: Implement this named temporal obligation. endproperty property p_done_is_a_pulse; // TODO: Implement this named temporal obligation. endproperty property p_no_cfg_accept_while_busy; // TODO: Implement this named temporal obligation. endproperty property p_reset_cancels_read; // TODO: Implement this named temporal obligation. endproperty assert_cfg_response_hold:assert property(p_cfg_response_hold); assert_done_is_a_pulse:assert property(p_done_is_a_pulse); assert_no_cfg_accept_while_busy:assert property(p_no_cfg_accept_while_busy); assert_reset_cancels_read:assert property(p_reset_cancels_read); final begin : check_unfinished_config_read // TODO: Reject incomplete outstanding work at test end. end endmodule // TODO: Describe legal shuffled/higher-multiplicity images and the reset-retained RAM/shadow policy.

Question

Implementation scaffold

Trace one case

Requirements

Related questions

Question

Implementation scaffold

Trace one case

Requirements

Related questions