Q160FreeSystemVerilog
Verify a retained-memory water accelerator
Question
Complete the supplied retained-memory water checker and both independent oracles. There are 64 HEIGHT words, each 12 bits; the harness supplies their known cold-initialized values before the first observation. Legal LEN is 1..64. Observe all handshakes and outputs immediately before each rising edge, once per edge. Controls are known, accepted addresses are 10-bit byte addresses, and write data is 32 bits. A sampled low reset cancels both pending channels and resets LEN to zero after that edge; it does not require pre-edge outputs to have already cleared. HEIGHT remains unchanged across reset. The environment prevents old canceled work from reappearing; an untagged response interface cannot identify every stale response matching a new job. The register map is LEN at 0x000, START at 0x004, read-only STATUS at 0x008 and HEIGHT[i] at 0x100+4*i for i=0..63. Reads of START return zero. STATUS bit0 captures whether a job was owned before the accepting edge; other bits are zero. START write1 launches, write0 is a no-op and other values error. HEIGHT writes require upper20 data bits zero. Unmapped or unaligned accesses and writes to STATUS error, without state changes. All writes and errors respond with zero read data.
Implementation scaffold
typedef struct packed {
logic rst_n, cfg_valid, cfg_ready, cfg_write;
logic [9:0] cfg_addr;
logic [31:0] cfg_wdata, cfg_rdata;
logic cfg_rsp_valid, cfg_rsp_ready, cfg_rsp_err;
logic result_valid, result_ready, result_error;
logic [19:0] total_water;
logic [11:0] peak_water;
logic [5:0] peak_index;
} rain_observation_t;
typedef struct packed {
int unsigned total, peak, peak_index;
} rain_result_t;
class retained_rain_checker;
logic [11:0] height[64];
logic [31:0] length_register;
bit cfg_owned, job_owned, result_presented;
int unsigned cfg_age, job_age, job_limit;
logic [31:0] expected_cfg_data;
logic expected_cfg_error, expected_job_error;
rain_result_t expected_job;
// Supplied cold initialization; later control resets must retain all 64 words.
function new(input logic [11:0] initial_height[64]);
foreach(height[i])begin
if($isunknown(initial_height[i]))$fatal(1,"Known cold HEIGHT image required");
height[i]=initial_height[i];
end
length_register=0;cfg_owned=0;job_owned=0;result_presented=0;
cfg_age=0;job_age=0;job_limit=0;
endfunction
function automatic rain_result_t scan_oracle(input logic [11:0] values[64],
input int unsigned length);
rain_result_t result='0;
int unsigned left_max,right_max,level,water;
// TODO: implement scan_oracle.
endfunction
function automatic rain_result_t prefix_oracle(input logic [11:0] values[64],
input int unsigned length);
int unsigned left_max[64],right_max[64],level,water;
rain_result_t result='0;
// TODO: implement prefix_oracle.
endfunction
function void start_job();
rain_result_t independent_result;
// TODO: implement start_job.
endfunction
function void accept_register(input rain_observation_t o, input bit busy_before);
int unsigned index;
// TODO: implement accept_register.
endfunction
// Called once per rising edge with pre-edge signal values. Reset cancels
// ownership at this edge; it does not demand pre-edge outputs already clear.
function void observe_cycle(input rain_observation_t o);
bit busy_before;
// TODO: implement observe_cycle.
endfunction
function void check_finished();
// TODO: implement check_finished.
endfunction
endclass
Trace one case
LEN=5 and retained HEIGHT=[0,2,0,2,0]. Accept START at C0 after configuring the memory and LEN.A first result at C1..C27 has error 0,total_water 2,peak_water 2,peak_index 2. If blocked, hold that exact result until its accepting edge.Only the center valley traps water. The register response to START is separately due at C2; result and register backpressure have independent owners.
Requirements
- Accept a register request only on cfg_valid&&cfg_ready, with at most one owner. Its response first appears at the pre-edge sample exactly two cycles later. Hold response validity and the captured data/error through backpressure and acceptance. An old register response may retire on the same edge as a new request is accepted. Capture read values and apply successful writes at request acceptance, independently of response acceptance.
- At an idle START acceptance, freeze the active retained HEIGHT values and LEN by computing the expected result. Implement both the O(N squared) wall scan and independent prefix/suffix maxima, and compare them. Sum per-index water and select the greatest per-index amount, choosing the earliest index on ties. An all-zero water result uses peak_index=0. Model all 64 retained words, but ignore entries beyond LEN when predicting the job.
- For a valid job, require the first result_valid on a subsequent sample no later than 3*LEN+12. For an invalid LEN, require the first error=1,total=peak=index=0 result within 12 subsequent samples. Once presented, hold the complete result valid and unchanged until accepted. Backpressure does not extend the first-presentation deadline, and the job remains busy through the accepting sample. Every write attempted while the old job is busy, including on its retiring edge, must return a register error without effect. Reads remain allowed.
- Reset cancels register and job ownership and clears LEN. Allow no old response afterward, and preserve every HEIGHT word. Check exact response timing and job deadlines on every active sampled edge. Catch unsolicited responses and report either unfinished owner at end of test.