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 and remains valid with the captured data/error through backpressure and acceptance. An old register response may retire on the same edge that a new request is accepted. Reads capture values and successful writes take effect at request acceptance, independently of when their response is accepted.
- 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, select the greatest per-index amount and choose the earliest index on ties; an all-zero water result uses peak_index=0. All 64 retained words remain modeled, but entries beyond LEN do not affect the job.
- A valid job first asserts result_valid on a subsequent sample no later than 3*LEN+12; an invalid LEN first produces error=1,total=peak=index=0 within 12 subsequent samples. Once presented, the complete result stays valid and unchanged until accepted, and backpressure does not extend the first-presentation deadline. A job stays busy through that accepting sample. Every write attempted while the old job is busy, including on its retiring edge, returns a register error and has no effect; reads remain allowed.
- Reset cancels both register and job ownership, clears LEN and permits no old response afterward; preserve every HEIGHT word. Check both exact response timing and job deadlines on every active sampled edge, catch unsolicited responses, and report either unfinished owner at end of test.