Q130FreeDesign Verification
Verify a shared-memory spiral readout
Question
Write the spiral oracle and transaction checker for the supplied decoded platform adapter. A source tile contains 1..16 rows and 1..16 columns of 32-bit words in row-major order. Source and destination addresses are 32-bit byte addresses, aligned to four bytes. The destination has one guard word immediately before and after its active region. Supplied accessible windows are half-open byte intervals and may end at 2^32. Source and destination words and guards retain logic values; ticks, controls and sampled status are known. The configuration event includes the actual descriptor written to the device. The adapter reports every device access, including activity from stopped generations. Calls and resolved platform events are serialized. A strictly increasing nonzero 64-bit testbench cookie attributes every event to its call; it is adapter ownership, not a hardware register. No cookie wraps. The adapter supplies the concrete cache operations, device publication/acquisition barriers and quiescence, with no outstanding memory access at an event boundary. A faulted access commits no write. Reset is an explicit sampled event which quiesces the old generation before a new call; arbitrary untagged stale activity cannot be identified without that adapter guarantee. Ticks are known unsigned 32-bit values, timeout is 1..2^31-1, and less than 2^32 ticks elapse during an owned operation. Snapshot and check post-event destination memory/status on each observe_step call; source memory can change after START.
Implementation scaffold
typedef enum {SP_OK, SP_BAD_ARG, SP_HW_ERROR, SP_TIMEOUT} spiral_status_t;
typedef enum {SP_CLEAN_SOURCE, SP_CLEAN_DESTINATION, SP_PUBLISH,
SP_CONFIGURE, SP_START, SP_POLL, SP_WRITE, SP_BUSY_START,
SP_DONE, SP_INVALIDATE_DESTINATION, SP_ACQUIRE, SP_CLEAR_DONE,
SP_ABORT_TIMEOUT, SP_RETURN, SP_RESET} spiral_event_t;
typedef struct packed {
logic [31:0] source, destination;
logic [4:0] rows, cols;
logic [31:0] timeout_ticks;
} spiral_descriptor_t;
typedef struct packed {
spiral_event_t kind;
longint unsigned cookie;
logic [31:0] tick, address, data;
bit bus_fault, quiesced, start_rejected;
logic busy, done, irq;
spiral_status_t return_status;
spiral_descriptor_t configuration;
} spiral_observation_t;
class spiral_transaction_checker;
typedef enum {PREPARE, CLEANED_SOURCE, CLEANED_DESTINATION, PUBLISHED,
CONFIGURED, ACTIVE, COMPLETE, INVALIDATED, ACQUIRED, CLEARED,
FAILED, TIMED_OUT, INVALID} phase_t;
phase_t phase;
bit owned;
longint unsigned last_cookie, owner_cookie;
longint unsigned source_lo, source_hi, destination_lo, destination_hi;
spiral_descriptor_t descriptor;
int unsigned total, written;
logic [31:0] started_at;
logic [2:0] terminal_status;
logic [31:0] frozen[256], model_destination[256], saved_guards[2];
logic [31:0] expected[$];
// Supplied windows are accessible byte intervals [lo,hi), with hi <= 2**32.
function new(longint unsigned src_lo=0, src_hi=64'h1_0000_0000,
dst_lo=0, dst_hi=64'h1_0000_0000);
if (src_lo >= src_hi || dst_lo >= dst_hi ||
src_hi > 64'h1_0000_0000 || dst_hi > 64'h1_0000_0000)
$fatal(1,"Invalid accessible windows");
source_lo=src_lo; source_hi=src_hi;
destination_lo=dst_lo; destination_hi=dst_hi;
owned=0; last_cookie=0; owner_cookie=0; total=0; written=0;
endfunction
function automatic bit valid_descriptor(input spiral_descriptor_t d);
longint unsigned bytes, src_end, guarded_lo, guarded_end;
// TODO: implement valid_descriptor.
endfunction
function automatic void spiral_reference(input logic [31:0] image[256],
input int unsigned rows, cols, ref logic [31:0] result[$]);
int top, bottom, left, right;
// TODO: implement spiral_reference.
endfunction
function void begin_call(input spiral_descriptor_t d,
input longint unsigned cookie, input logic [31:0] destination[256],
input logic [31:0] guards[2]);
// TODO: implement begin_call.
endfunction
function void snapshot_start(input logic [31:0] image[256],
input logic [31:0] destination[256], input logic [31:0] guards[2]);
// TODO: implement snapshot_start.
endfunction
function void check_destination(input logic [31:0] destination[256],
input logic [31:0] guards[2]);
// TODO: implement check_destination.
endfunction
function void check_status(input spiral_observation_t o);
// TODO: implement check_status.
endfunction
// One serialized, resolved platform event; status and memory are post-event.
function void observe_step(input spiral_observation_t o,
input logic [31:0] image[256], input logic [31:0] destination[256],
input logic [31:0] guards[2]);
logic [31:0] elapsed;
bit faultable;
// TODO: implement observe_step.
endfunction
function void check_finished();
// TODO: implement check_finished.
endfunction
endclass
Trace one case
A valid frozen 2 by 3 image [[1,2,3],[4,5,6]], source 0x1000, destination 0x2000, timeout 100, and unchanged guards at 0x1ffc and 0x2018.After the required cache/configuration sequence, writes to 0x2000 through 0x2014 contain [1,2,3,6,5,4]. DONE/IRQ persist until clear; return SP_OK after destination invalidation and acquisition.The source snapshot determines all six writes. Neither live-source changes nor a rejected busy START alter the owned traversal.
Requirements
- Before any cache or register event, validate dimensions, timeout, alignment, widened source interval, destination plus both guards, accessible windows and non-overlap of the source with the guarded destination. Invalid calls return only SP_BAD_ARG. For valid calls require source clean, destination clean/invalidate, publication barrier, configuration, then START, in that order.
- At accepted START copy the active source image and predict clockwise traversal. Require exactly rows times columns successful destination writes in order at destination + 4*i, with the predicted value. While active, BUSY is one and DONE/IRQ are zero. Busy START attempts must be rejected without changing the original snapshot, write position or active status. Compare all active destination words with the write model and keep both guards unchanged.
- A resolved bus fault on an event permitted by the current phase takes priority over elapsed-time checks, including at or after the timeout threshold. Validate the event phase and any faulted destination address first; a fault does not excuse an out-of-order or out-of-range access. Stop at that first fault and return SP_HW_ERROR only after adapter quiescence; no later device access, write or completion belongs to that call, and the status observed at the fault must not change before the error return. Reset clears ownership and status and permits no old-generation event afterward. Use unsigned elapsed subtraction across tick wrap. Clean DONE observed no later than the deadline wins; later DONE is a violation. In the absence of a bus fault, at or after the deadline otherwise require a quiescing abort and SP_TIMEOUT, with no further device access and BUSY/DONE/IRQ cleared by the abort.
- Accept DONE only after every expected write. Thereafter BUSY is zero and DONE/IRQ both remain one through polls, destination invalidation and the acquisition barrier. Explicit clear lowers DONE/IRQ. Return SP_OK only after acquisition, clear and quiescence. Report an unfinished owned call at end of test.