Q119FreeDesign Verification
Verify a RAL-programmed grid checker
Question
Write the functional oracle and core bus/interrupt assertions for a memory-mapped 9-by-9 grid checker. A full Universal Verification Methodology Register Abstraction Layer (UVM RAL) environment is a follow-up discussion. Use the supplied decoded bus controls and architectural observation ports; no register-address map is assumed. All accepted control and cell values are known. Decisions use pre-edge controls and busy, while cells, result registers, busy, and done_irq are observed after that edge's nonblocking updates. A cell write changes exactly its selected cell at that edge. An idle START snapshots the existing cells, clears every result field to zero, sets busy, and cannot complete at that same edge. Busy cell or START writes make no architectural change: the bus may stall them or acknowledge and ignore them. A write never creates a read response, but an earlier read may still be pending. A read accepted at C first presents its response at C+1; an old response may retire on the same edge as a new read or write. Reset is sampled at the rising edge and must be observed before programming. Reset clears cells, result fields, busy, done_irq, and read-response validity after that edge. Decode flags for cell and START writes are mutually exclusive; accepted idle cell writes address indices 0 through 80.
Implementation scaffold
typedef enum logic [2:0] {
GRID_OK, BAD_SYMBOL, DUP_ROW, DUP_COLUMN, DUP_REGION
} grid_error_kind_t;
typedef struct packed {
bit legal;
grid_error_kind_t kind;
logic [3:0] row;
logic [3:0] col;
} grid_prediction_t;
function automatic grid_prediction_t predict_grid(input logic [3:0] cells[81]);
// TODO: Implement the row-major precedence oracle.
endfunction
module grid_architectural_checker (
input logic clk,rst_n,cfg_valid,cfg_ready,cfg_write,
input logic cfg_is_cell,cfg_is_start,
input logic[6:0]cfg_cell_index,
input logic[3:0]cfg_cell_data,
input logic cfg_rsp_valid,cfg_rsp_ready,
input logic[31:0]cfg_rdata,
input logic busy,done_irq,result_legal,
input logic[2:0]result_kind,
input logic[3:0]result_row,result_col,
input logic[3:0]cells[81]
);
// Bus decisions are pre-edge. Architectural state is observed after this edge's NBA updates.
clocking monitor_cb @(posedge clk);
input #1step rst_n,cfg_valid,cfg_ready,cfg_write,cfg_is_cell,cfg_is_start;
input #1step cfg_cell_index,cfg_cell_data,cfg_rsp_valid,cfg_rsp_ready;
input #1step pre_busy=busy, accepted_cells=cells;
input #0 observed_cells=cells, observed_busy=busy, observed_irq=done_irq;
input #0 observed_rsp_valid=cfg_rsp_valid;
input #0 result_legal,result_kind,result_row,result_col;
endclocking
bit read_pending,job_pending,initialized;
logic[3:0]previous_cells[81];
logic[11:0]previous_result;
grid_prediction_t expected_result;
always @(monitor_cb)begin
// TODO: Track one pending read and one checking job, validate architectural
// cell/result changes after the edge, and clear all obligations on sampled reset.
end
property p_read_hold;
// TODO: State this named temporal property.
endproperty
property p_irq_is_one_cycle;
// TODO: State this named temporal property.
endproperty
assert_read_hold:assert property(p_read_hold);
assert_irq_is_one_cycle:assert property(p_irq_is_one_cycle);
cover_reset_programming:cover property(
// TODO: Cover this named reset phase.
);
cover_reset_checking:cover property(
// TODO: Cover this named reset phase.
);
cover_reset_read_stall:cover property(
// TODO: Cover this named reset phase.
);
final begin
// TODO: Reject unfinished read or checking work.
end
endmoduleTrace one case
program grid cell(0,0)=12 through RAL, then accept STARTsymbol violation at row0,column0; all result registers update atomically and done_irq pulses onceSymbol values 10..15 have highest same-cell precedence, so row/column/region checks cannot replace this first error.
Requirements
- Scan row-major, ignore zero, reject symbols 10 through 15, and apply same-cell precedence symbol, row, column, then region.
- Model one pending read: an accepted read responds one cycle later and holds data under backpressure; writes produce no read response.
- An idle START clears old status and errors, then completion updates all result registers atomically and pulses done_irq once; busy cell or START writes are rejected while status reads remain legal.
- Reset cancels checking and stalled reads, clears cells and result registers, suppresses interrupts, and is covered during programming, checking, and response stall.
- Explain separately how a RAL predictor would own mirror updates for accepted frontdoor traffic; it is not part of the code requested here.