SPI · Module 20
Assertions, Reference Model, and Scoreboard
A reference model derived from the specification rather than the RTL, a scoreboard that predicts frame duration to the cycle, and eight properties of which three fired 21 times against a correct controller.
Chapter 20.3 ran 284 directed checks and passed. This chapter builds the machinery that decides whether a transfer was right, in a form that can be shown to work independently of the thing it is checking.
Three of the eight properties, as first written, reported 21 violations against a correct controller. An assertion that fires on legal behaviour is not strict — it is wrong, and it is the kind that gets switched off rather than fixed.
1. Three Layers, Three Different Kinds Of Claim
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
REFERENCE MODEL predicts, from the SPECIFICATION, what a transaction should
produce. Contains arithmetic. Contains no shift register, no
state machine and no divider.
SCOREBOARD compares prediction against observation, per transaction,
and reports at the transaction level.
PROPERTY MONITORS check invariants EVERY CYCLE, independently of any
transaction. Eight of them, over the pins and the status
outputs.The division matters because the three fail differently. A reference-model mismatch says the wrong data came back. A property violation says the design did something it promised never to do, possibly in a frame whose data was fine. And a property that never fires says nothing at all — which is why §5 counts how often each one was actually exercised.
2. The Reference Model Predicts Time, Not Just Data
Predicting the received word is the obvious half. The model here also predicts how long the frame takes, and that turns out to be the more sensitive check.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
rx_data from mask and reversal alone
edge count 2N
frame duration (cfg_lead + cfg_lag + 2N + 2) x (cfg_div + 1) system clocksThe duration expression comes from Chapter 20.1's timing clauses — the lead, the 2N - 1 half-periods between first and last edge, and the lag — not from reading the state machine. That is what allows it to disagree with the state machine.
Measured across twelve transactions covering all four modes, both bit orders, widths from 4 to 16 and dividers from 0 to 7:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
txn mode ord w div | rx_pred rx_obs edges cycles pred_cyc
0 0 msb 8 1 | 00b9 00b9 16 44 44
1 1 msb 8 1 | 00b9 00b9 16 44 44
2 2 msb 8 1 | 00b9 00b9 16 44 44
3 3 msb 8 1 | 00b9 00b9 16 44 44
4 0 lsb 4 0 | 0005 0005 8 10 10
5 3 lsb 16 3 | 2c48 2c48 32 172 172
6 1 lsb 13 2 | 0b5e 0b5e 26 96 96
7 2 msb 5 7 | 000b 000b 10 128 128
8 0 msb 16 0 | 0001 0001 32 64 64
9 0 msb 4 1 | 000f 000f 8 28 28
10 2 lsb 8 1 | 0001 0001 16 44 44
11 3 msb 12 4 | 0def 0def 24 130 130
12 transactions scored, 0 mismatchesTransaction 7 is the one to look at: a 5-bit transfer at cfg_div = 7 takes 128 cycles, predicted from the specification before the design was run. A duration check like this catches a whole class of fault that a data check cannot — a lead phase one tick short, a lag that expired early, a divider that reloaded with the wrong value. All of those return the correct word.
3. The Eight Properties
Each is a small function of the current and previous pin samples, and each returns three bits.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
bit 0 the guarded REGION was entered reachability evidence
bit 1 the property was VIOLATED
bit 2 a legal EXEMPTION was taken| Property | What bug it stops | |
|---|---|---|
| P1 | At most one chip select is low | two devices driving MISO at once |
| P2 | With nothing selected, SCLK sits at the configured idle level | a device seeing the wrong parked level |
| P3 | With nothing selected, SCLK does not move | a stray edge into a deselected device |
| P4 | MOSI changes only when SCLK changes | a mid-half-period glitch violating device setup |
| P5 | The bit count never exceeds the captured width | a runaway shift corrupting the word |
| P6 | done implies a complete word was transferred | a completion reported early |
| P7 | A chip select is low only while busy | a caller legally starting on top of a live frame |
| P8 | done is emitted inside the frame it completes | a completion attributed to the wrong transfer |
P4 is worth singling out because it is purely pin-level: it needs no knowledge of the controller's state at all, and it is exactly the property a device's setup requirement depends on. A property that can be written from the outside is one that survives a rewrite of the inside.
4. Why Three Of Them Were Wrong
P2, P3 and P4 as first written reported 21 violations against a controller passing all 284 directed checks. Seven each — and seven is exactly the number of times the bench changes cfg_cpol between transactions.
Nothing was wrong with the design. The properties forbade legal behaviour:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
P2 SCLK is a register. When CPOL changes, the pin holds the old level for one
cycle while the configuration already reads the new one. Demanding otherwise
requires a combinational path from a configuration input to a pin.
P3 Re-parking the clock between two devices of different polarity is a legal
and necessary edge on a shared wire. Nothing is selected, so nothing can
see it -- Module 19.4 is about the damage when it lands inside another
device's hold window, and that is a different situation.
P4 CPHA = 0 owes the device a valid first bit BEFORE any edge exists, so MOSI
must change with the chip select. Forbidding that forbids mode 0.Each got an exemption — and an exemption is a hole in a property, so the hole is counted rather than hidden.
Measured, with the corrected properties:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
S2 property monitors: region / exempt / violated
P1 at most one select low 975 0 0
P2 SCLK parked at CPOL when idle 127 7 0
P3 SCLK quiet when nothing selected 127 7 0
P4 MOSI changes only on an edge 848 7 0
P5 bit count never exceeds width 950 0 0
P6 done implies a complete word 12 0 0
P7 a select implies busy 848 0 0
P8 done is emitted inside the frame 12 0 0
8 properties, 0 unreached, 0 violated, 21 exemptions takenEvery region is entered. P6 and P8 have a region of 12 — one per completed transaction — which is correct and is the smallest healthy number here; a region of zero would fail the suite.
5. Every Checker Is Shown Able To Fail
A checker nobody has seen fail is not a checker. Because each property is a function of its arguments, the bench can call the same function with hand-built violating inputs and require a violation. An inline if buried in a monitor cannot be tested that way, and in practice never is.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
S3 every property is shown able to fail
8 of 8 predicates rejected a hand-built violation
3 of 3 exemptions accept the legal case they exist for
reference model separates bit orders (9d vs b9)
reference model is sensitive to lag (44 vs 46 cycles)The second line is the one that is easy to omit. An exemption is checked from both sides: the violating case must be flagged, and the exempted case must be accepted and marked as exempted. Without the second check, an exemption that had quietly widened into "this property no longer fires at all" would still pass the first.
The last two lines test the oracle, not the design. A reference model that returns the same answer for MSB-first and LSB-first cannot detect a bit-order fault, and one insensitive to the lag cannot detect a shortened lag — so both are given inputs that must produce different answers.
6. The Temporal Half, Which Needs A Different Tool
Three of the specification's claims cannot be expressed as a per-cycle predicate at all:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
`done` is exactly one cycle wide needs `next`
`busy` rises with acceptance needs `next`
an accepted request eventually completes needs `eventually!` -- LIVENESSThe third is the important one. A liveness property has no per-cycle form. "Something good happens eventually" cannot be refuted by observing one cycle, because eventually has not run out yet. A controller that accepts a request and then clocks forever violates INV-9 while satisfying every property in §3 indefinitely — the full accounting is in the fourth question below.
assert property is the natural way to write these, and the simulator these examples run in rejects it outright:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
sva.sv:5: syntax error
sva.sv:5: error: Invalid module item.So the SystemVerilog spelling appears below as reviewed code that was not executed, and the same three properties are written as PSL in the VHDL bench, which nvc does execute.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// REVIEWED, NOT EXECUTED — Icarus Verilog rejects concurrent assertions.
// The executed form of all three is the PSL in spi_capstone_check_tb.vhd.
property p_done_is_one_cycle;
@(posedge clk) done |=> !done;
endproperty
property p_busy_rises;
@(posedge clk) (accept && rst_n) |=> busy;
endproperty
property p_accept_completes;
@(posedge clk) (accept && rst_n) |-> s_eventually done;
endproperty
assert property (p_done_is_one_cycle);
assert property (p_busy_rises);
assert property (p_accept_completes);
cover property (@(posedge clk) done);
cover property (@(posedge clk) accept && cfg_width == 5'd16);
cover property (@(posedge clk) accept && cfg_cpol && cfg_cpha);The executed PSL equivalents, which run:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
-- psl default clock is rising_edge(clk);
-- psl DONE_IS_ONE_CYCLE : assert always (done = '1' -> next (done = '0'));
-- psl BUSY_RISES : assert always ((accept_r = '1' and rst_n = '1')
-- -> next (busy = '1'));
-- psl ACCEPT_COMPLETES : assert always ((accept_r = '1' and rst_n = '1')
-- -> eventually! (done = '1'));These were confirmed able to fail before being trusted. With the completion suppressed in an isolated probe, nvc reports:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
** Error: 410ns+0: PSL assertion failed ... eventually! (dn = '1')7. UVM, And Where It Would Go
UVM is not installed in this toolchain, so nothing below was executed. What is worth stating is the mapping, because the components in this chapter are a UVM environment with the ceremony removed.
| This chapter | UVM component | Same job? |
|---|---|---|
| the transaction table in §2 | spi_seq_item + spi_sequence | yes |
fire and set_cfg | spi_driver | yes |
| the pin monitors in §3 | spi_monitor with an analysis port | yes |
| the specification arithmetic | spi_reference_model (predictor) | yes |
| the comparison in §2 | spi_scoreboard | yes, in-order |
| the hit arrays in 20.6 | spi_coverage subscriber + covergroup | yes |
| the bench module | spi_env + spi_test | structurally |
| the device model | a passive agent, or a real slave BFM | yes |
RAL — intentional absence. A register abstraction layer models a software-visible register map, and this controller does not have one: its configuration arrives on wires, not through an address decoder. Chapter 19.3 wraps a controller behind APB and is the place a RAL model belongs, with RW configuration, a WO command, W1C status bits and a derived BUSY that RAL must treat as volatile or mirror() will report a stale value. Adding RAL here would add ceremony and produce no finding.
What UVM would genuinely buy at this scale is the factory and the configuration database — the ability to swap the device model for a different one, or to run the same environment against a slave-mode DUT, without editing the bench. What it would cost is roughly 400 lines of infrastructure around 200 lines of actual checking, which for a single-agent, single-protocol capstone is a poor trade. At the point a second protocol or a second agent appears, the trade inverts.
8. The Checking Layer
Azvya Education Pvt. Ltd.VLSI Mentor
spi_capstone_check_tb.sv — reference model, scoreboard, and eight properties that can each be shown to fail
// spi_capstone_check_tb.sv
//
// Chapter 20.5 -- the checking layer: reference model, scoreboard, property monitors.
//
// This bench adds no new stimulus worth speaking of. What it adds is the machinery
// that decides whether the controller was RIGHT, built so that each piece can be
// shown to work independently of the thing it is checking.
//
// THREE LAYERS, THREE DIFFERENT KINDS OF CLAIM
//
// REFERENCE MODEL predicts, from the SPECIFICATION alone, what a transaction
// should produce: the received word, the number of SCLK edges,
// and the frame's duration in system clocks. It does not contain
// a shift register, a state machine, or a divider. It contains
// arithmetic. That is the point -- a reference model built by
// copying the RTL's algorithm agrees with the RTL's bugs.
//
// SCOREBOARD compares prediction against observation per transaction and
// reports at the transaction level, not the signal level.
//
// PROPERTY MONITORS check invariants EVERY CYCLE, independently of any transaction.
// Eight of them, each expressed as a small predicate over the
// current and previous pin samples.
//
// WHY THE MONITORS ARE PREDICATES AND NOT INLINE `if` STATEMENTS
//
// Because a checker nobody has ever seen fail is not a checker. Each property is a
// function of its arguments, so group S3 can call the SAME function with
// hand-constructed violating arguments and require it to report a violation. An
// inline `if` buried in a monitor cannot be tested that way, and in practice never
// is.
//
// Each predicate returns two bits, and both matter:
//
// bit 0 the antecedent occurred -- this property was EXERCISED
// bit 1 the property was VIOLATED
//
// The exercise count is the anti-vacuity evidence. A property whose antecedent never
// occurs reports zero failures forever, and reads exactly like a property that
// passed. This bench FAILS if any property finishes with an exercise count of zero.
//
// WHAT IS NOT HERE, AND WHY
//
// `assert property (...)` is the natural way to write the temporal half of this, and
// the simulator these examples run in rejects it outright:
//
// sva.sv:5: syntax error
// sva.sv:5: error: Invalid module item.
//
// So the SVA forms appear in the chapter as reviewed code that was NOT executed, and
// said so; the eight properties below are executed instead. The VHDL sibling of this
// file carries the same eight as PSL directives, which `nvc` does execute -- so every
// property in this module has a form that actually ran, in at least one language.
`timescale 1ns/1ps
module spi_capstone_check_tb;
reg clk, rst_n;
reg cfg_cpol, cfg_cpha, cfg_lsb;
reg [4:0] cfg_width;
reg [7:0] cfg_div;
reg [1:0] cfg_dev;
reg [3:0] cfg_lead, cfg_lag, cfg_idle;
reg start, abort;
reg [15:0] tx_data;
wire busy, done, cfg_err;
wire [15:0] rx_data;
wire [4:0] bits_done;
wire sclk, mosi;
wire [3:0] cs_n;
wire miso;
integer n_chk, n_err, n_neg;
spi_capstone_ctrl #(.DATA_W(16), .MIN_WIDTH(4), .NDEV(4)) dut (
.clk(clk), .rst_n(rst_n),
.cfg_cpol(cfg_cpol), .cfg_cpha(cfg_cpha), .cfg_lsb_first(cfg_lsb),
.cfg_width(cfg_width), .cfg_div(cfg_div), .cfg_dev(cfg_dev),
.cfg_lead(cfg_lead), .cfg_lag(cfg_lag), .cfg_idle(cfg_idle),
.start(start), .tx_data(tx_data), .abort(abort),
.busy(busy), .done(done), .cfg_err(cfg_err),
.rx_data(rx_data), .bits_done(bits_done),
.sclk(sclk), .mosi(mosi), .cs_n(cs_n), .miso(miso)
);
always #5 clk = ~clk;
// =====================================================================
// REFERENCE MODEL -- specification arithmetic, no hardware structure
// =====================================================================
function [15:0] mask;
input [4:0] w;
reg [16:0] one;
begin one = 17'd1; mask = ((one << w) - 17'd1); end
endfunction
function [15:0] revw;
input [15:0] v; input [4:0] w;
integer b;
begin
revw = 16'd0;
for (b = 0; b < 16; b = b + 1) if (b < w) revw[w-1-b] = v[b];
end
endfunction
function [15:0] ref_rx; // what the master must receive
input [15:0] sw; input [4:0] w; input lsb;
begin ref_rx = lsb ? revw(sw & mask(w), w) : (sw & mask(w)); end
endfunction
function [15:0] ref_slave_rx; // what the device must receive
input [15:0] tx; input [4:0] w; input lsb;
begin ref_slave_rx = lsb ? revw(tx & mask(w), w) : (tx & mask(w)); end
endfunction
function integer ref_edges; // SCLK transitions per frame
input [4:0] w;
begin ref_edges = 2 * w; end
endfunction
// Frame duration, CS falling to CS rising, in system clocks.
//
// t_half = div + 1
// CS fall -> first edge (lead + 2) half-periods
// first -> last edge (2N - 1) half-periods
// last edge-> CS rise (lag + 1) half-periods
//
// so the whole frame is (lead + lag + 2N + 2) half-periods. This is derived from
// the specification's timing clauses, NOT read off the state machine, which is why
// it is able to disagree with it.
function integer ref_frame_cycles;
input [4:0] w; input [7:0] dv; input [3:0] ld; input [3:0] lg;
begin
ref_frame_cycles = (ld + lg + 2 * w + 2) * (dv + 1);
end
endfunction
// =====================================================================
// PIN-LEVEL DEVICE MODEL (same as 20.3 -- unchanged, deliberately)
// =====================================================================
reg slv_cpol, slv_cpha;
reg [15:0] slv_word, slv_sr, slv_rx;
reg [4:0] slv_w, slv_idx, slv_nrx;
reg slv_miso, lead_s;
wire cs_any = ~(&cs_n);
assign miso = slv_miso;
always @(posedge cs_any) begin
slv_sr = slv_word << (16 - slv_w);
slv_rx = 16'd0;
slv_nrx = 5'd0;
if (!slv_cpha) begin
slv_miso = slv_sr[15]; slv_sr = slv_sr << 1; slv_idx = 5'd1;
end else begin
slv_miso = 1'b0; slv_idx = 5'd0;
end
end
always @(sclk) begin
if (cs_any === 1'b1) begin
lead_s = (sclk !== slv_cpol);
if (slv_cpha ? !lead_s : lead_s) begin
if (slv_nrx < slv_w) begin
slv_rx = {slv_rx[14:0], mosi}; slv_nrx = slv_nrx + 5'd1;
end
end
if (slv_cpha ? lead_s : !lead_s) begin
if (slv_idx < slv_w) begin
slv_miso = slv_sr[15]; slv_sr = slv_sr << 1;
slv_idx = slv_idx + 5'd1;
end
end
end
end
// =====================================================================
// THE EIGHT PROPERTIES, as predicates.
//
// return[0] the guarded REGION was entered -- reachability evidence
// return[1] the property was VIOLATED
// return[2] a legal EXEMPTION was taken
//
// THREE BITS, NOT TWO, AND THE THIRD ONE IS THE INTERESTING ONE.
//
// Written with two bits, P2, P3 and P4 reported 21 violations against a
// correct controller -- seven each, which is exactly how many times this bench
// changes CPOL between transactions. The properties were too strong. An
// assertion that fires on legal behaviour is not strict, it is WRONG, and it is
// the kind that gets switched off instead of fixed.
//
// Adding an exemption fixes the false failure and opens a hole, so the hole is
// COUNTED. When P3's exemption was first added it fired on every single one of
// its seven antecedent occurrences -- the property passed, reported no
// violations, and had never once tested anything. That is a worse kind of
// vacuity than an antecedent that never occurs, because the exercise count
// looks healthy.
//
// So each property separates the REGION it guards (reachable, and checked to be
// non-zero) from the exemptions taken inside it (reported, so a reviewer can ask
// whether the hole is too wide).
// =====================================================================
// P1 At most one chip select may be low. Structural here -- one index through one
// decoder -- so this is a regression guard. A property that is true by
// construction today is the first casualty of tomorrow's edit.
function [2:0] p1_one_select;
input [3:0] csn;
integer n;
begin
n = (csn[0] ? 0 : 1) + (csn[1] ? 0 : 1) + (csn[2] ? 0 : 1) + (csn[3] ? 0 : 1);
p1_one_select[0] = 1'b1;
p1_one_select[1] = (n > 1) ? 1'b1 : 1'b0;
p1_one_select[2] = 1'b0;
end
endfunction
// P2 With no device selected, SCLK sits at the configured idle polarity.
// EXEMPT: the cycle CPOL itself changes. SCLK is a register and follows one
// clock later, so for one cycle the pin holds the old level while the
// configuration reads the new one. Nothing is selected, so no device can see
// it, and demanding otherwise would require a combinational path from a
// configuration input straight to a pin.
function [2:0] p2_parked_level;
input csany; input sclk_v; input cpol_v; input cpol_d1;
reg region; reg stable;
begin
region = ~csany;
stable = (cpol_v === cpol_d1);
p2_parked_level[0] = region;
p2_parked_level[1] = (region && stable && (sclk_v !== cpol_v)) ? 1'b1 : 1'b0;
p2_parked_level[2] = (region && !stable) ? 1'b1 : 1'b0;
end
endfunction
// P3 With no device selected, SCLK does not move.
// EXEMPT: a move that FOLLOWS a change of CPOL. Re-parking the clock between
// two devices of different polarity is a legal and necessary edge on a shared
// wire -- Module 19.4 is about the damage it does when it lands inside another
// device's hold window. Here nothing is selected, so it is safe, and the
// property has to say so rather than forbid it.
function [2:0] p3_quiet_when_idle;
input csany; input sclk_v; input sclk_prev; input cpol_d1; input cpol_d2;
reg region; reg moved; reg cpol_moved;
begin
region = ~csany;
moved = (sclk_v !== sclk_prev);
cpol_moved = (cpol_d1 !== cpol_d2);
p3_quiet_when_idle[0] = region;
p3_quiet_when_idle[1] = (region && moved && !cpol_moved) ? 1'b1 : 1'b0;
p3_quiet_when_idle[2] = (region && moved && cpol_moved) ? 1'b1 : 1'b0;
end
endfunction
// P4 MOSI changes only when SCLK changes -- the property a device's setup time
// actually depends on, and checkable entirely at the pins.
// EXEMPT: the cycle a chip select is asserted. CPHA=0 owes the device a valid
// first bit BEFORE any edge exists, so MOSI must change with CS. Forbidding
// that would forbid mode 0.
function [2:0] p4_mosi_only_on_edges;
input csany; input cs_prev; input mosi_v; input mosi_prev;
input sclk_v; input sclk_prev;
reg region; reg moved; reg cs_asserting;
begin
region = csany;
moved = (mosi_v !== mosi_prev);
cs_asserting = csany & ~cs_prev;
p4_mosi_only_on_edges[0] = region;
p4_mosi_only_on_edges[1] =
(region && moved && !cs_asserting && (sclk_v === sclk_prev))
? 1'b1 : 1'b0;
p4_mosi_only_on_edges[2] = (region && moved && cs_asserting) ? 1'b1 : 1'b0;
end
endfunction
// P5 The bit counter never passes the configured width.
function [2:0] p5_bits_bounded;
input [4:0] bits; input [4:0] w; input bsy;
begin
p5_bits_bounded[0] = bsy;
p5_bits_bounded[1] = (bsy && (bits > w)) ? 1'b1 : 1'b0;
p5_bits_bounded[2] = 1'b0;
end
endfunction
// P6 `done` implies a whole word was transferred.
function [2:0] p6_done_means_complete;
input dn; input [4:0] bits; input [4:0] w;
begin
p6_done_means_complete[0] = dn;
p6_done_means_complete[1] = (dn && (bits !== w)) ? 1'b1 : 1'b0;
p6_done_means_complete[2] = 1'b0;
end
endfunction
// P7 A device is selected only while the controller reports itself busy. This is
// what makes `busy` meaningful to software: if a select could be low while
// busy was clear, a caller could legally start a transfer on top of a live one.
function [2:0] p7_select_implies_busy;
input csany; input bsy;
begin
p7_select_implies_busy[0] = csany;
p7_select_implies_busy[1] = (csany && !bsy) ? 1'b1 : 1'b0;
p7_select_implies_busy[2] = 1'b0;
end
endfunction
// P8 `done` is emitted inside the frame it completes, never while idle.
function [2:0] p8_done_inside_frame;
input dn; input bsy;
begin
p8_done_inside_frame[0] = dn;
p8_done_inside_frame[1] = (dn && !bsy) ? 1'b1 : 1'b0;
p8_done_inside_frame[2] = 1'b0;
end
endfunction
// =====================================================================
// LIVE MONITOR
// =====================================================================
integer ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8;
integer fv1, fv2, fv3, fv4, fv5, fv6, fv7, fv8;
integer xm1, xm2, xm3, xm4, xm5, xm6, xm7, xm8;
reg sclk_d, mosi_d;
reg cpol_d1, cpol_d2;
reg [2:0] r;
integer cyc, n_edge, t_cs_fall, t_frame, frames;
reg cs_d;
// WHICH select went low, not merely that one did. Added because bug injection
// found this gap: the device model responds to ANY select, so with this field
// absent a controller that asserted cs_n[1] when asked for cs_n[0] transferred
// the right data to the right model and every check passed.
integer dev_seen;
always @(posedge clk) begin
if (!rst_n) begin
ex1<=0; ex2<=0; ex3<=0; ex4<=0; ex5<=0; ex6<=0; ex7<=0; ex8<=0;
fv1<=0; fv2<=0; fv3<=0; fv4<=0; fv5<=0; fv6<=0; fv7<=0; fv8<=0;
xm1<=0; xm2<=0; xm3<=0; xm4<=0; xm5<=0; xm6<=0; xm7<=0; xm8<=0;
cyc<=0; n_edge<=0; frames<=0; cs_d<=1'b0;
sclk_d<=1'b0; mosi_d<=1'b0; cpol_d1<=1'b0; cpol_d2<=1'b0;
end else begin
cyc <= cyc + 1;
r = p1_one_select(cs_n);
ex1<=ex1+r[0]; fv1<=fv1+r[1]; xm1<=xm1+r[2];
r = p2_parked_level(cs_any, sclk, cfg_cpol, cpol_d1);
ex2<=ex2+r[0]; fv2<=fv2+r[1]; xm2<=xm2+r[2];
r = p3_quiet_when_idle(cs_any, sclk, sclk_d, cpol_d1, cpol_d2);
ex3<=ex3+r[0]; fv3<=fv3+r[1]; xm3<=xm3+r[2];
r = p4_mosi_only_on_edges(cs_any, cs_d, mosi, mosi_d, sclk, sclk_d);
ex4<=ex4+r[0]; fv4<=fv4+r[1]; xm4<=xm4+r[2];
r = p5_bits_bounded(bits_done, cfg_width, busy);
ex5<=ex5+r[0]; fv5<=fv5+r[1]; xm5<=xm5+r[2];
r = p6_done_means_complete(done, bits_done, cfg_width);
ex6<=ex6+r[0]; fv6<=fv6+r[1]; xm6<=xm6+r[2];
r = p7_select_implies_busy(cs_any, busy);
ex7<=ex7+r[0]; fv7<=fv7+r[1]; xm7<=xm7+r[2];
r = p8_done_inside_frame(done, busy);
ex8<=ex8+r[0]; fv8<=fv8+r[1]; xm8<=xm8+r[2];
if (cs_any && !cs_d) begin
t_cs_fall <= cyc;
n_edge <= 0;
dev_seen <= cs_n[0] ? (cs_n[1] ? (cs_n[2] ? 3 : 2) : 1) : 0;
end
if (!cs_any && cs_d) begin t_frame <= cyc - t_cs_fall; frames <= frames + 1; end
// `cs_d` as well as `cs_any`: an edge is only a FRAME edge if a device
// was ALREADY selected last cycle. A transition in the very cycle the
// select falls is SCLK reaching its new idle level, not a clocking
// edge -- the controller parks SCLK and asserts CS together, so when
// the previous idle level differed the two coincide.
//
// Measured cost of omitting `cs_d`: the first transaction after reset
// with CPOL=1 counted 17 edges instead of 16 in VHDL and 16 in
// SystemVerilog, because a one-cycle difference in reset-release
// timing decided whether the re-park landed inside the window. The
// received data was correct in both. With the gate the measurement no
// longer depends on that phase at all.
if (cs_any && cs_d && (sclk !== sclk_d)) n_edge <= n_edge + 1;
cs_d <= cs_any; sclk_d <= sclk; mosi_d <= mosi;
cpol_d1 <= cfg_cpol; cpol_d2 <= cpol_d1;
end
end
// =====================================================================
// Stimulus and scoreboard
// =====================================================================
task set_cfg;
input cpol_i; input cpha_i; input lsb_i; input [4:0] w;
input [7:0] dv; input [1:0] dv_n;
input [3:0] ld; input [3:0] lg; input [3:0] id;
begin
cfg_cpol=cpol_i; cfg_cpha=cpha_i; cfg_lsb=lsb_i;
cfg_width=w; cfg_div=dv; cfg_dev=dv_n;
cfg_lead=ld; cfg_lag=lg; cfg_idle=id;
slv_cpol=cpol_i; slv_cpha=cpha_i; slv_w=w;
end
endtask
task fire;
input [15:0] d;
begin
@(negedge clk); tx_data = d; start = 1'b1;
@(negedge clk); start = 1'b0;
end
endtask
task wait_idle;
input integer maxc; output gotd;
integer g; reg seen;
begin
g=0; seen=1'b0;
while (g < maxc) begin
@(negedge clk); g=g+1;
if (done) seen=1'b1;
if (!busy && seen) g=maxc;
else if (!busy && g>4) g=maxc;
end
gotd = seen;
end
endtask
task chk16;
input [8*24-1:0] nm; input [15:0] got; input [15:0] exp;
begin
n_chk=n_chk+1;
if (got !== exp) begin
n_err=n_err+1;
$display(" FAIL %0s: got %04h expected %04h", nm, got, exp);
end
end
endtask
task chki;
input [8*24-1:0] nm; input integer got; input integer exp;
begin
n_chk=n_chk+1;
if (got !== exp) begin
n_err=n_err+1;
$display(" FAIL %0s: got %0d expected %0d", nm, got, exp);
end
end
endtask
// Transaction table. Chosen to exercise every property's antecedent, not to be
// exhaustive -- exhaustiveness is Chapter 20.6's job.
integer t;
reg [4:0] T_W [0:11];
reg [7:0] T_DIV [0:11];
reg [1:0] T_DEV [0:11];
reg [3:0] T_LD [0:11];
reg [3:0] T_LG [0:11];
reg T_POL [0:11];
reg T_PHA [0:11];
reg T_LSB [0:11];
reg [15:0] T_TX [0:11];
reg [15:0] T_SW [0:11];
reg gd;
integer mism, vac;
initial begin
clk=1'b0; rst_n=1'b0; start=1'b0; abort=1'b0; tx_data=16'd0;
cfg_cpol=1'b0; cfg_cpha=1'b0; cfg_lsb=1'b0; cfg_width=5'd8;
cfg_div=8'd1; cfg_dev=2'd0; cfg_lead=4'd2; cfg_lag=4'd2; cfg_idle=4'd2;
slv_cpol=1'b0; slv_cpha=1'b0; slv_w=5'd8; slv_word=16'd0;
slv_miso=1'b0; slv_sr=16'd0; slv_rx=16'd0; slv_idx=5'd0; slv_nrx=5'd0;
n_chk=0; n_err=0; n_neg=0; mism=0; vac=0;
cyc=0; n_edge=0; frames=0; t_cs_fall=0; t_frame=0; dev_seen=0;
ex1=0; ex2=0; ex3=0; ex4=0; ex5=0; ex6=0; ex7=0; ex8=0;
fv1=0; fv2=0; fv3=0; fv4=0; fv5=0; fv6=0; fv7=0; fv8=0;
xm1=0; xm2=0; xm3=0; xm4=0; xm5=0; xm6=0; xm7=0; xm8=0;
sclk_d=1'b0; mosi_d=1'b0; cs_d=1'b0; cpol_d1=1'b0; cpol_d2=1'b0;
// w div dev ld lg pol pha lsb tx sw
T_W[ 0]=5'd8; T_DIV[ 0]=8'd1; T_DEV[ 0]=2'd0; T_LD[ 0]=4'd2; T_LG[ 0]=4'd2;
T_POL[ 0]=0; T_PHA[ 0]=0; T_LSB[ 0]=0; T_TX[ 0]=16'h9D; T_SW[ 0]=16'hB9;
T_W[ 1]=5'd8; T_DIV[ 1]=8'd1; T_DEV[ 1]=2'd1; T_LD[ 1]=4'd2; T_LG[ 1]=4'd2;
T_POL[ 1]=0; T_PHA[ 1]=1; T_LSB[ 1]=0; T_TX[ 1]=16'h9D; T_SW[ 1]=16'hB9;
T_W[ 2]=5'd8; T_DIV[ 2]=8'd1; T_DEV[ 2]=2'd2; T_LD[ 2]=4'd2; T_LG[ 2]=4'd2;
T_POL[ 2]=1; T_PHA[ 2]=0; T_LSB[ 2]=0; T_TX[ 2]=16'h9D; T_SW[ 2]=16'hB9;
T_W[ 3]=5'd8; T_DIV[ 3]=8'd1; T_DEV[ 3]=2'd3; T_LD[ 3]=4'd2; T_LG[ 3]=4'd2;
T_POL[ 3]=1; T_PHA[ 3]=1; T_LSB[ 3]=0; T_TX[ 3]=16'h9D; T_SW[ 3]=16'hB9;
T_W[ 4]=5'd4; T_DIV[ 4]=8'd0; T_DEV[ 4]=2'd0; T_LD[ 4]=4'd0; T_LG[ 4]=4'd0;
T_POL[ 4]=0; T_PHA[ 4]=0; T_LSB[ 4]=1; T_TX[ 4]=16'h0D; T_SW[ 4]=16'h0A;
T_W[ 5]=5'd16; T_DIV[ 5]=8'd3; T_DEV[ 5]=2'd1; T_LD[ 5]=4'd5; T_LG[ 5]=4'd4;
T_POL[ 5]=1; T_PHA[ 5]=1; T_LSB[ 5]=1; T_TX[ 5]=16'hBEEF; T_SW[ 5]=16'h1234;
T_W[ 6]=5'd13; T_DIV[ 6]=8'd2; T_DEV[ 6]=2'd2; T_LD[ 6]=4'd1; T_LG[ 6]=4'd3;
T_POL[ 6]=0; T_PHA[ 6]=1; T_LSB[ 6]=1; T_TX[ 6]=16'h1ACE; T_SW[ 6]=16'h0F5A;
T_W[ 7]=5'd5; T_DIV[ 7]=8'd7; T_DEV[ 7]=2'd3; T_LD[ 7]=4'd3; T_LG[ 7]=4'd1;
T_POL[ 7]=1; T_PHA[ 7]=0; T_LSB[ 7]=0; T_TX[ 7]=16'h15; T_SW[ 7]=16'h0B;
T_W[ 8]=5'd16; T_DIV[ 8]=8'd0; T_DEV[ 8]=2'd0; T_LD[ 8]=4'd15; T_LG[ 8]=4'd15;
T_POL[ 8]=0; T_PHA[ 8]=0; T_LSB[ 8]=0; T_TX[ 8]=16'hFFFF; T_SW[ 8]=16'h0001;
T_W[ 9]=5'd4; T_DIV[ 9]=8'd1; T_DEV[ 9]=2'd1; T_LD[ 9]=4'd2; T_LG[ 9]=4'd2;
T_POL[ 9]=0; T_PHA[ 9]=0; T_LSB[ 9]=0; T_TX[ 9]=16'h0000; T_SW[ 9]=16'h000F;
T_W[10]=5'd8; T_DIV[10]=8'd1; T_DEV[10]=2'd2; T_LD[10]=4'd2; T_LG[10]=4'd2;
T_POL[10]=1; T_PHA[10]=0; T_LSB[10]=1; T_TX[10]=16'h01; T_SW[10]=16'h80;
T_W[11]=5'd12; T_DIV[11]=8'd4; T_DEV[11]=2'd3; T_LD[11]=4'd0; T_LG[11]=4'd0;
T_POL[11]=1; T_PHA[11]=1; T_LSB[11]=0; T_TX[11]=16'h0ABC; T_SW[11]=16'h0DEF;
$display("=== Chapter 20.5 -- reference model, scoreboard and assertions ===");
// Reset is RELEASED ON A NEGEDGE, for the same reason `start` is driven on one.
// Releasing it on a posedge puts the assignment in the same region as every
// clocked block that tests it, and the order is undefined: the monitor may see
// the old value or the new one. Measured cost of getting this wrong -- the
// monitor held its reset one cycle longer in VHDL than in SystemVerilog, so the
// idle re-park of SCLK to CPOL=1 was counted as a frame edge in one language
// and not the other, and the first transaction of the run reported 17 edges
// instead of 16 in exactly one of the three.
repeat (4) @(posedge clk);
@(negedge clk); rst_n = 1'b1;
repeat (2) @(posedge clk);
// ---------------------------------------------------------------
$display(" S1 scoreboard: predicted vs observed, per transaction");
$display(" txn mode ord w div | rx_pred rx_obs edges cycles pred_cyc");
for (t = 0; t < 12; t = t + 1) begin
set_cfg(T_POL[t], T_PHA[t], T_LSB[t], T_W[t], T_DIV[t], T_DEV[t],
T_LD[t], T_LG[t], 4'd2);
slv_word = T_SW[t] & mask(T_W[t]);
fire(T_TX[t]);
wait_idle(20000, gd);
chki ("done pulsed", gd ? 1 : 0, 1);
chk16("rx_data", rx_data,
ref_rx(T_SW[t] & mask(T_W[t]), T_W[t], T_LSB[t]));
chk16("device rx", slv_rx & mask(T_W[t]),
ref_slave_rx(T_TX[t], T_W[t], T_LSB[t]));
chki ("sclk edges", n_edge, ref_edges(T_W[t]));
chki ("frame cycles", t_frame,
ref_frame_cycles(T_W[t], T_DIV[t], T_LD[t], T_LG[t]));
chki ("device selected", dev_seen, T_DEV[t]);
$display(" %3d %4d %0s %3d %3d | %7h %6h %5d %6d %8d",
t, {T_POL[t], T_PHA[t]}, T_LSB[t] ? "lsb" : "msb",
T_W[t], T_DIV[t],
ref_rx(T_SW[t] & mask(T_W[t]), T_W[t], T_LSB[t]), rx_data,
n_edge, t_frame,
ref_frame_cycles(T_W[t], T_DIV[t], T_LD[t], T_LG[t]));
end
$display(" 12 transactions scored, %0d mismatches", n_err);
// ---------------------------------------------------------------
$display(" S2 property monitors: region / exempt / violated");
$display(" P1 at most one select low %6d %6d %3d", ex1, xm1, fv1);
$display(" P2 SCLK parked at CPOL when idle %6d %6d %3d", ex2, xm2, fv2);
$display(" P3 SCLK quiet when nothing selected %6d %6d %3d", ex3, xm3, fv3);
$display(" P4 MOSI changes only on an edge %6d %6d %3d", ex4, xm4, fv4);
$display(" P5 bit count never exceeds width %6d %6d %3d", ex5, xm5, fv5);
$display(" P6 done implies a complete word %6d %6d %3d", ex6, xm6, fv6);
$display(" P7 a select implies busy %6d %6d %3d", ex7, xm7, fv7);
$display(" P8 done is emitted inside the frame %6d %6d %3d", ex8, xm8, fv8);
vac = 0;
if (ex1 == 0) vac = vac + 1;
if (ex2 == 0) vac = vac + 1;
if (ex3 == 0) vac = vac + 1;
if (ex4 == 0) vac = vac + 1;
if (ex5 == 0) vac = vac + 1;
if (ex6 == 0) vac = vac + 1;
if (ex7 == 0) vac = vac + 1;
if (ex8 == 0) vac = vac + 1;
n_chk = n_chk + 1;
if (vac != 0) begin
n_err = n_err + 1;
$display(" FAIL %0d propert(y/ies) never entered their region", vac);
end
n_chk = n_chk + 1;
if ((fv1|fv2|fv3|fv4|fv5|fv6|fv7|fv8) != 0) begin
n_err = n_err + 1;
$display(" FAIL a property was violated");
end
$display(" 8 properties, %0d unreached, %0d violated, %0d exemptions taken",
vac, fv1+fv2+fv3+fv4+fv5+fv6+fv7+fv8,
xm1+xm2+xm3+xm4+xm5+xm6+xm7+xm8);
// ---------------------------------------------------------------
// Each predicate is called with arguments that VIOLATE it. A monitor that
// cannot be made to fire is decoration, and this is the cheapest possible
// proof that these eight can.
$display(" S3 every property is shown able to fail");
n_neg = 0;
// Each call supplies arguments that VIOLATE the property: region entered,
// violation flagged, exemption NOT taken -> 3'b011.
if (p1_one_select(4'b1100) == 3'b011) n_neg = n_neg + 1;
if (p2_parked_level(1'b0, 1'b1, 1'b0, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p3_quiet_when_idle(1'b0, 1'b1, 1'b0, 1'b0, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p4_mosi_only_on_edges(1'b1, 1'b1, 1'b1, 1'b0, 1'b0, 1'b0)
== 3'b011) n_neg = n_neg + 1;
if (p5_bits_bounded(5'd9, 5'd8, 1'b1) == 3'b011) n_neg = n_neg + 1;
if (p6_done_means_complete(1'b1, 5'd7, 5'd8) == 3'b011) n_neg = n_neg + 1;
if (p7_select_implies_busy(1'b1, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p8_done_inside_frame(1'b1, 1'b0) == 3'b011) n_neg = n_neg + 1;
n_chk = n_chk + 1;
if (n_neg != 8) begin
n_err = n_err + 1;
$display(" FAIL only %0d of 8 predicates rejected a violating input", n_neg);
end
$display(" %0d of 8 predicates rejected a hand-built violation", n_neg);
// An exemption is a hole in a property, so each one is checked from the other
// side too: the exempted case must be ACCEPTED, and must be accepted for the
// stated reason rather than because the property stopped working.
// The exempted case must come back as region entered, NOT violated, exemption
// taken -> 3'b101. Checking this from both sides is what stops an exemption
// from quietly widening into "this property no longer fires at all".
t = 0;
if (p2_parked_level(1'b0, 1'b1, 1'b0, 1'b1) == 3'b101) t = t + 1;
if (p3_quiet_when_idle(1'b0, 1'b1, 1'b0, 1'b1, 1'b0) == 3'b101) t = t + 1;
if (p4_mosi_only_on_edges(1'b1, 1'b0, 1'b1, 1'b0, 1'b0, 1'b0)
== 3'b101) t = t + 1;
n_chk = n_chk + 1;
if (t != 3) begin
n_err = n_err + 1;
$display(" FAIL only %0d of 3 exemptions accepted their legal case", t);
end
$display(" %0d of 3 exemptions accept the legal case they exist for", t);
// And the scoreboard's own oracle must be able to disagree.
n_chk = n_chk + 1;
if (ref_rx(16'h9D, 5'd8, 1'b1) !== ref_rx(16'h9D, 5'd8, 1'b0)) begin
$display(" reference model separates bit orders (9d vs b9)");
end else begin
n_err = n_err + 1;
$display(" FAIL reference model is blind to bit order");
end
n_chk = n_chk + 1;
if (ref_frame_cycles(5'd8, 8'd1, 4'd2, 4'd2) !==
ref_frame_cycles(5'd8, 8'd1, 4'd2, 4'd3)) begin
$display(" reference model is sensitive to lag (44 vs 46 cycles)");
end else begin
n_err = n_err + 1;
$display(" FAIL reference model ignores lag");
end
$display("=== SUMMARY checks=%0d negatives=%0d failures=%0d : %0s ===",
n_chk, n_neg, n_err, (n_err == 0) ? "PASS" : "FAIL");
$finish;
end
initial begin
#8000000;
$display(" FATAL global timeout -- a frame never completed");
$display("=== SUMMARY checks=%0d negatives=%0d failures=%0d : FAIL ===",
n_chk, n_neg, n_err + 1);
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_capstone_check_tb.v — the same checking layer in Verilog-2001 — again, no changes were needed
// spi_capstone_check_tb.sv
//
// Chapter 20.5 -- the checking layer: reference model, scoreboard, property monitors.
//
// This bench adds no new stimulus worth speaking of. What it adds is the machinery
// that decides whether the controller was RIGHT, built so that each piece can be
// shown to work independently of the thing it is checking.
//
// THREE LAYERS, THREE DIFFERENT KINDS OF CLAIM
//
// REFERENCE MODEL predicts, from the SPECIFICATION alone, what a transaction
// should produce: the received word, the number of SCLK edges,
// and the frame's duration in system clocks. It does not contain
// a shift register, a state machine, or a divider. It contains
// arithmetic. That is the point -- a reference model built by
// copying the RTL's algorithm agrees with the RTL's bugs.
//
// SCOREBOARD compares prediction against observation per transaction and
// reports at the transaction level, not the signal level.
//
// PROPERTY MONITORS check invariants EVERY CYCLE, independently of any transaction.
// Eight of them, each expressed as a small predicate over the
// current and previous pin samples.
//
// WHY THE MONITORS ARE PREDICATES AND NOT INLINE `if` STATEMENTS
//
// Because a checker nobody has ever seen fail is not a checker. Each property is a
// function of its arguments, so group S3 can call the SAME function with
// hand-constructed violating arguments and require it to report a violation. An
// inline `if` buried in a monitor cannot be tested that way, and in practice never
// is.
//
// Each predicate returns two bits, and both matter:
//
// bit 0 the antecedent occurred -- this property was EXERCISED
// bit 1 the property was VIOLATED
//
// The exercise count is the anti-vacuity evidence. A property whose antecedent never
// occurs reports zero failures forever, and reads exactly like a property that
// passed. This bench FAILS if any property finishes with an exercise count of zero.
//
// WHAT IS NOT HERE, AND WHY
//
// `assert property (...)` is the natural way to write the temporal half of this, and
// the simulator these examples run in rejects it outright:
//
// sva.sv:5: syntax error
// sva.sv:5: error: Invalid module item.
//
// So the SVA forms appear in the chapter as reviewed code that was NOT executed, and
// said so; the eight properties below are executed instead. The VHDL sibling of this
// file carries the same eight as PSL directives, which `nvc` does execute -- so every
// property in this module has a form that actually ran, in at least one language.
`timescale 1ns/1ps
module spi_capstone_check_tb;
reg clk, rst_n;
reg cfg_cpol, cfg_cpha, cfg_lsb;
reg [4:0] cfg_width;
reg [7:0] cfg_div;
reg [1:0] cfg_dev;
reg [3:0] cfg_lead, cfg_lag, cfg_idle;
reg start, abort;
reg [15:0] tx_data;
wire busy, done, cfg_err;
wire [15:0] rx_data;
wire [4:0] bits_done;
wire sclk, mosi;
wire [3:0] cs_n;
wire miso;
integer n_chk, n_err, n_neg;
spi_capstone_ctrl #(.DATA_W(16), .MIN_WIDTH(4), .NDEV(4)) dut (
.clk(clk), .rst_n(rst_n),
.cfg_cpol(cfg_cpol), .cfg_cpha(cfg_cpha), .cfg_lsb_first(cfg_lsb),
.cfg_width(cfg_width), .cfg_div(cfg_div), .cfg_dev(cfg_dev),
.cfg_lead(cfg_lead), .cfg_lag(cfg_lag), .cfg_idle(cfg_idle),
.start(start), .tx_data(tx_data), .abort(abort),
.busy(busy), .done(done), .cfg_err(cfg_err),
.rx_data(rx_data), .bits_done(bits_done),
.sclk(sclk), .mosi(mosi), .cs_n(cs_n), .miso(miso)
);
always #5 clk = ~clk;
// =====================================================================
// REFERENCE MODEL -- specification arithmetic, no hardware structure
// =====================================================================
function [15:0] mask;
input [4:0] w;
reg [16:0] one;
begin one = 17'd1; mask = ((one << w) - 17'd1); end
endfunction
function [15:0] revw;
input [15:0] v; input [4:0] w;
integer b;
begin
revw = 16'd0;
for (b = 0; b < 16; b = b + 1) if (b < w) revw[w-1-b] = v[b];
end
endfunction
function [15:0] ref_rx; // what the master must receive
input [15:0] sw; input [4:0] w; input lsb;
begin ref_rx = lsb ? revw(sw & mask(w), w) : (sw & mask(w)); end
endfunction
function [15:0] ref_slave_rx; // what the device must receive
input [15:0] tx; input [4:0] w; input lsb;
begin ref_slave_rx = lsb ? revw(tx & mask(w), w) : (tx & mask(w)); end
endfunction
function integer ref_edges; // SCLK transitions per frame
input [4:0] w;
begin ref_edges = 2 * w; end
endfunction
// Frame duration, CS falling to CS rising, in system clocks.
//
// t_half = div + 1
// CS fall -> first edge (lead + 2) half-periods
// first -> last edge (2N - 1) half-periods
// last edge-> CS rise (lag + 1) half-periods
//
// so the whole frame is (lead + lag + 2N + 2) half-periods. This is derived from
// the specification's timing clauses, NOT read off the state machine, which is why
// it is able to disagree with it.
function integer ref_frame_cycles;
input [4:0] w; input [7:0] dv; input [3:0] ld; input [3:0] lg;
begin
ref_frame_cycles = (ld + lg + 2 * w + 2) * (dv + 1);
end
endfunction
// =====================================================================
// PIN-LEVEL DEVICE MODEL (same as 20.3 -- unchanged, deliberately)
// =====================================================================
reg slv_cpol, slv_cpha;
reg [15:0] slv_word, slv_sr, slv_rx;
reg [4:0] slv_w, slv_idx, slv_nrx;
reg slv_miso, lead_s;
wire cs_any = ~(&cs_n);
assign miso = slv_miso;
always @(posedge cs_any) begin
slv_sr = slv_word << (16 - slv_w);
slv_rx = 16'd0;
slv_nrx = 5'd0;
if (!slv_cpha) begin
slv_miso = slv_sr[15]; slv_sr = slv_sr << 1; slv_idx = 5'd1;
end else begin
slv_miso = 1'b0; slv_idx = 5'd0;
end
end
always @(sclk) begin
if (cs_any === 1'b1) begin
lead_s = (sclk !== slv_cpol);
if (slv_cpha ? !lead_s : lead_s) begin
if (slv_nrx < slv_w) begin
slv_rx = {slv_rx[14:0], mosi}; slv_nrx = slv_nrx + 5'd1;
end
end
if (slv_cpha ? lead_s : !lead_s) begin
if (slv_idx < slv_w) begin
slv_miso = slv_sr[15]; slv_sr = slv_sr << 1;
slv_idx = slv_idx + 5'd1;
end
end
end
end
// =====================================================================
// THE EIGHT PROPERTIES, as predicates.
//
// return[0] the guarded REGION was entered -- reachability evidence
// return[1] the property was VIOLATED
// return[2] a legal EXEMPTION was taken
//
// THREE BITS, NOT TWO, AND THE THIRD ONE IS THE INTERESTING ONE.
//
// Written with two bits, P2, P3 and P4 reported 21 violations against a
// correct controller -- seven each, which is exactly how many times this bench
// changes CPOL between transactions. The properties were too strong. An
// assertion that fires on legal behaviour is not strict, it is WRONG, and it is
// the kind that gets switched off instead of fixed.
//
// Adding an exemption fixes the false failure and opens a hole, so the hole is
// COUNTED. When P3's exemption was first added it fired on every single one of
// its seven antecedent occurrences -- the property passed, reported no
// violations, and had never once tested anything. That is a worse kind of
// vacuity than an antecedent that never occurs, because the exercise count
// looks healthy.
//
// So each property separates the REGION it guards (reachable, and checked to be
// non-zero) from the exemptions taken inside it (reported, so a reviewer can ask
// whether the hole is too wide).
// =====================================================================
// P1 At most one chip select may be low. Structural here -- one index through one
// decoder -- so this is a regression guard. A property that is true by
// construction today is the first casualty of tomorrow's edit.
function [2:0] p1_one_select;
input [3:0] csn;
integer n;
begin
n = (csn[0] ? 0 : 1) + (csn[1] ? 0 : 1) + (csn[2] ? 0 : 1) + (csn[3] ? 0 : 1);
p1_one_select[0] = 1'b1;
p1_one_select[1] = (n > 1) ? 1'b1 : 1'b0;
p1_one_select[2] = 1'b0;
end
endfunction
// P2 With no device selected, SCLK sits at the configured idle polarity.
// EXEMPT: the cycle CPOL itself changes. SCLK is a register and follows one
// clock later, so for one cycle the pin holds the old level while the
// configuration reads the new one. Nothing is selected, so no device can see
// it, and demanding otherwise would require a combinational path from a
// configuration input straight to a pin.
function [2:0] p2_parked_level;
input csany; input sclk_v; input cpol_v; input cpol_d1;
reg region; reg stable;
begin
region = ~csany;
stable = (cpol_v === cpol_d1);
p2_parked_level[0] = region;
p2_parked_level[1] = (region && stable && (sclk_v !== cpol_v)) ? 1'b1 : 1'b0;
p2_parked_level[2] = (region && !stable) ? 1'b1 : 1'b0;
end
endfunction
// P3 With no device selected, SCLK does not move.
// EXEMPT: a move that FOLLOWS a change of CPOL. Re-parking the clock between
// two devices of different polarity is a legal and necessary edge on a shared
// wire -- Module 19.4 is about the damage it does when it lands inside another
// device's hold window. Here nothing is selected, so it is safe, and the
// property has to say so rather than forbid it.
function [2:0] p3_quiet_when_idle;
input csany; input sclk_v; input sclk_prev; input cpol_d1; input cpol_d2;
reg region; reg moved; reg cpol_moved;
begin
region = ~csany;
moved = (sclk_v !== sclk_prev);
cpol_moved = (cpol_d1 !== cpol_d2);
p3_quiet_when_idle[0] = region;
p3_quiet_when_idle[1] = (region && moved && !cpol_moved) ? 1'b1 : 1'b0;
p3_quiet_when_idle[2] = (region && moved && cpol_moved) ? 1'b1 : 1'b0;
end
endfunction
// P4 MOSI changes only when SCLK changes -- the property a device's setup time
// actually depends on, and checkable entirely at the pins.
// EXEMPT: the cycle a chip select is asserted. CPHA=0 owes the device a valid
// first bit BEFORE any edge exists, so MOSI must change with CS. Forbidding
// that would forbid mode 0.
function [2:0] p4_mosi_only_on_edges;
input csany; input cs_prev; input mosi_v; input mosi_prev;
input sclk_v; input sclk_prev;
reg region; reg moved; reg cs_asserting;
begin
region = csany;
moved = (mosi_v !== mosi_prev);
cs_asserting = csany & ~cs_prev;
p4_mosi_only_on_edges[0] = region;
p4_mosi_only_on_edges[1] =
(region && moved && !cs_asserting && (sclk_v === sclk_prev))
? 1'b1 : 1'b0;
p4_mosi_only_on_edges[2] = (region && moved && cs_asserting) ? 1'b1 : 1'b0;
end
endfunction
// P5 The bit counter never passes the configured width.
function [2:0] p5_bits_bounded;
input [4:0] bits; input [4:0] w; input bsy;
begin
p5_bits_bounded[0] = bsy;
p5_bits_bounded[1] = (bsy && (bits > w)) ? 1'b1 : 1'b0;
p5_bits_bounded[2] = 1'b0;
end
endfunction
// P6 `done` implies a whole word was transferred.
function [2:0] p6_done_means_complete;
input dn; input [4:0] bits; input [4:0] w;
begin
p6_done_means_complete[0] = dn;
p6_done_means_complete[1] = (dn && (bits !== w)) ? 1'b1 : 1'b0;
p6_done_means_complete[2] = 1'b0;
end
endfunction
// P7 A device is selected only while the controller reports itself busy. This is
// what makes `busy` meaningful to software: if a select could be low while
// busy was clear, a caller could legally start a transfer on top of a live one.
function [2:0] p7_select_implies_busy;
input csany; input bsy;
begin
p7_select_implies_busy[0] = csany;
p7_select_implies_busy[1] = (csany && !bsy) ? 1'b1 : 1'b0;
p7_select_implies_busy[2] = 1'b0;
end
endfunction
// P8 `done` is emitted inside the frame it completes, never while idle.
function [2:0] p8_done_inside_frame;
input dn; input bsy;
begin
p8_done_inside_frame[0] = dn;
p8_done_inside_frame[1] = (dn && !bsy) ? 1'b1 : 1'b0;
p8_done_inside_frame[2] = 1'b0;
end
endfunction
// =====================================================================
// LIVE MONITOR
// =====================================================================
integer ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8;
integer fv1, fv2, fv3, fv4, fv5, fv6, fv7, fv8;
integer xm1, xm2, xm3, xm4, xm5, xm6, xm7, xm8;
reg sclk_d, mosi_d;
reg cpol_d1, cpol_d2;
reg [2:0] r;
integer cyc, n_edge, t_cs_fall, t_frame, frames;
reg cs_d;
// WHICH select went low, not merely that one did. Added because bug injection
// found this gap: the device model responds to ANY select, so with this field
// absent a controller that asserted cs_n[1] when asked for cs_n[0] transferred
// the right data to the right model and every check passed.
integer dev_seen;
always @(posedge clk) begin
if (!rst_n) begin
ex1<=0; ex2<=0; ex3<=0; ex4<=0; ex5<=0; ex6<=0; ex7<=0; ex8<=0;
fv1<=0; fv2<=0; fv3<=0; fv4<=0; fv5<=0; fv6<=0; fv7<=0; fv8<=0;
xm1<=0; xm2<=0; xm3<=0; xm4<=0; xm5<=0; xm6<=0; xm7<=0; xm8<=0;
cyc<=0; n_edge<=0; frames<=0; cs_d<=1'b0;
sclk_d<=1'b0; mosi_d<=1'b0; cpol_d1<=1'b0; cpol_d2<=1'b0;
end else begin
cyc <= cyc + 1;
r = p1_one_select(cs_n);
ex1<=ex1+r[0]; fv1<=fv1+r[1]; xm1<=xm1+r[2];
r = p2_parked_level(cs_any, sclk, cfg_cpol, cpol_d1);
ex2<=ex2+r[0]; fv2<=fv2+r[1]; xm2<=xm2+r[2];
r = p3_quiet_when_idle(cs_any, sclk, sclk_d, cpol_d1, cpol_d2);
ex3<=ex3+r[0]; fv3<=fv3+r[1]; xm3<=xm3+r[2];
r = p4_mosi_only_on_edges(cs_any, cs_d, mosi, mosi_d, sclk, sclk_d);
ex4<=ex4+r[0]; fv4<=fv4+r[1]; xm4<=xm4+r[2];
r = p5_bits_bounded(bits_done, cfg_width, busy);
ex5<=ex5+r[0]; fv5<=fv5+r[1]; xm5<=xm5+r[2];
r = p6_done_means_complete(done, bits_done, cfg_width);
ex6<=ex6+r[0]; fv6<=fv6+r[1]; xm6<=xm6+r[2];
r = p7_select_implies_busy(cs_any, busy);
ex7<=ex7+r[0]; fv7<=fv7+r[1]; xm7<=xm7+r[2];
r = p8_done_inside_frame(done, busy);
ex8<=ex8+r[0]; fv8<=fv8+r[1]; xm8<=xm8+r[2];
if (cs_any && !cs_d) begin
t_cs_fall <= cyc;
n_edge <= 0;
dev_seen <= cs_n[0] ? (cs_n[1] ? (cs_n[2] ? 3 : 2) : 1) : 0;
end
if (!cs_any && cs_d) begin t_frame <= cyc - t_cs_fall; frames <= frames + 1; end
// `cs_d` as well as `cs_any`: an edge is only a FRAME edge if a device
// was ALREADY selected last cycle. A transition in the very cycle the
// select falls is SCLK reaching its new idle level, not a clocking
// edge -- the controller parks SCLK and asserts CS together, so when
// the previous idle level differed the two coincide.
//
// Measured cost of omitting `cs_d`: the first transaction after reset
// with CPOL=1 counted 17 edges instead of 16 in VHDL and 16 in
// SystemVerilog, because a one-cycle difference in reset-release
// timing decided whether the re-park landed inside the window. The
// received data was correct in both. With the gate the measurement no
// longer depends on that phase at all.
if (cs_any && cs_d && (sclk !== sclk_d)) n_edge <= n_edge + 1;
cs_d <= cs_any; sclk_d <= sclk; mosi_d <= mosi;
cpol_d1 <= cfg_cpol; cpol_d2 <= cpol_d1;
end
end
// =====================================================================
// Stimulus and scoreboard
// =====================================================================
task set_cfg;
input cpol_i; input cpha_i; input lsb_i; input [4:0] w;
input [7:0] dv; input [1:0] dv_n;
input [3:0] ld; input [3:0] lg; input [3:0] id;
begin
cfg_cpol=cpol_i; cfg_cpha=cpha_i; cfg_lsb=lsb_i;
cfg_width=w; cfg_div=dv; cfg_dev=dv_n;
cfg_lead=ld; cfg_lag=lg; cfg_idle=id;
slv_cpol=cpol_i; slv_cpha=cpha_i; slv_w=w;
end
endtask
task fire;
input [15:0] d;
begin
@(negedge clk); tx_data = d; start = 1'b1;
@(negedge clk); start = 1'b0;
end
endtask
task wait_idle;
input integer maxc; output gotd;
integer g; reg seen;
begin
g=0; seen=1'b0;
while (g < maxc) begin
@(negedge clk); g=g+1;
if (done) seen=1'b1;
if (!busy && seen) g=maxc;
else if (!busy && g>4) g=maxc;
end
gotd = seen;
end
endtask
task chk16;
input [8*24-1:0] nm; input [15:0] got; input [15:0] exp;
begin
n_chk=n_chk+1;
if (got !== exp) begin
n_err=n_err+1;
$display(" FAIL %0s: got %04h expected %04h", nm, got, exp);
end
end
endtask
task chki;
input [8*24-1:0] nm; input integer got; input integer exp;
begin
n_chk=n_chk+1;
if (got !== exp) begin
n_err=n_err+1;
$display(" FAIL %0s: got %0d expected %0d", nm, got, exp);
end
end
endtask
// Transaction table. Chosen to exercise every property's antecedent, not to be
// exhaustive -- exhaustiveness is Chapter 20.6's job.
integer t;
reg [4:0] T_W [0:11];
reg [7:0] T_DIV [0:11];
reg [1:0] T_DEV [0:11];
reg [3:0] T_LD [0:11];
reg [3:0] T_LG [0:11];
reg T_POL [0:11];
reg T_PHA [0:11];
reg T_LSB [0:11];
reg [15:0] T_TX [0:11];
reg [15:0] T_SW [0:11];
reg gd;
integer mism, vac;
initial begin
clk=1'b0; rst_n=1'b0; start=1'b0; abort=1'b0; tx_data=16'd0;
cfg_cpol=1'b0; cfg_cpha=1'b0; cfg_lsb=1'b0; cfg_width=5'd8;
cfg_div=8'd1; cfg_dev=2'd0; cfg_lead=4'd2; cfg_lag=4'd2; cfg_idle=4'd2;
slv_cpol=1'b0; slv_cpha=1'b0; slv_w=5'd8; slv_word=16'd0;
slv_miso=1'b0; slv_sr=16'd0; slv_rx=16'd0; slv_idx=5'd0; slv_nrx=5'd0;
n_chk=0; n_err=0; n_neg=0; mism=0; vac=0;
cyc=0; n_edge=0; frames=0; t_cs_fall=0; t_frame=0; dev_seen=0;
ex1=0; ex2=0; ex3=0; ex4=0; ex5=0; ex6=0; ex7=0; ex8=0;
fv1=0; fv2=0; fv3=0; fv4=0; fv5=0; fv6=0; fv7=0; fv8=0;
xm1=0; xm2=0; xm3=0; xm4=0; xm5=0; xm6=0; xm7=0; xm8=0;
sclk_d=1'b0; mosi_d=1'b0; cs_d=1'b0; cpol_d1=1'b0; cpol_d2=1'b0;
// w div dev ld lg pol pha lsb tx sw
T_W[ 0]=5'd8; T_DIV[ 0]=8'd1; T_DEV[ 0]=2'd0; T_LD[ 0]=4'd2; T_LG[ 0]=4'd2;
T_POL[ 0]=0; T_PHA[ 0]=0; T_LSB[ 0]=0; T_TX[ 0]=16'h9D; T_SW[ 0]=16'hB9;
T_W[ 1]=5'd8; T_DIV[ 1]=8'd1; T_DEV[ 1]=2'd1; T_LD[ 1]=4'd2; T_LG[ 1]=4'd2;
T_POL[ 1]=0; T_PHA[ 1]=1; T_LSB[ 1]=0; T_TX[ 1]=16'h9D; T_SW[ 1]=16'hB9;
T_W[ 2]=5'd8; T_DIV[ 2]=8'd1; T_DEV[ 2]=2'd2; T_LD[ 2]=4'd2; T_LG[ 2]=4'd2;
T_POL[ 2]=1; T_PHA[ 2]=0; T_LSB[ 2]=0; T_TX[ 2]=16'h9D; T_SW[ 2]=16'hB9;
T_W[ 3]=5'd8; T_DIV[ 3]=8'd1; T_DEV[ 3]=2'd3; T_LD[ 3]=4'd2; T_LG[ 3]=4'd2;
T_POL[ 3]=1; T_PHA[ 3]=1; T_LSB[ 3]=0; T_TX[ 3]=16'h9D; T_SW[ 3]=16'hB9;
T_W[ 4]=5'd4; T_DIV[ 4]=8'd0; T_DEV[ 4]=2'd0; T_LD[ 4]=4'd0; T_LG[ 4]=4'd0;
T_POL[ 4]=0; T_PHA[ 4]=0; T_LSB[ 4]=1; T_TX[ 4]=16'h0D; T_SW[ 4]=16'h0A;
T_W[ 5]=5'd16; T_DIV[ 5]=8'd3; T_DEV[ 5]=2'd1; T_LD[ 5]=4'd5; T_LG[ 5]=4'd4;
T_POL[ 5]=1; T_PHA[ 5]=1; T_LSB[ 5]=1; T_TX[ 5]=16'hBEEF; T_SW[ 5]=16'h1234;
T_W[ 6]=5'd13; T_DIV[ 6]=8'd2; T_DEV[ 6]=2'd2; T_LD[ 6]=4'd1; T_LG[ 6]=4'd3;
T_POL[ 6]=0; T_PHA[ 6]=1; T_LSB[ 6]=1; T_TX[ 6]=16'h1ACE; T_SW[ 6]=16'h0F5A;
T_W[ 7]=5'd5; T_DIV[ 7]=8'd7; T_DEV[ 7]=2'd3; T_LD[ 7]=4'd3; T_LG[ 7]=4'd1;
T_POL[ 7]=1; T_PHA[ 7]=0; T_LSB[ 7]=0; T_TX[ 7]=16'h15; T_SW[ 7]=16'h0B;
T_W[ 8]=5'd16; T_DIV[ 8]=8'd0; T_DEV[ 8]=2'd0; T_LD[ 8]=4'd15; T_LG[ 8]=4'd15;
T_POL[ 8]=0; T_PHA[ 8]=0; T_LSB[ 8]=0; T_TX[ 8]=16'hFFFF; T_SW[ 8]=16'h0001;
T_W[ 9]=5'd4; T_DIV[ 9]=8'd1; T_DEV[ 9]=2'd1; T_LD[ 9]=4'd2; T_LG[ 9]=4'd2;
T_POL[ 9]=0; T_PHA[ 9]=0; T_LSB[ 9]=0; T_TX[ 9]=16'h0000; T_SW[ 9]=16'h000F;
T_W[10]=5'd8; T_DIV[10]=8'd1; T_DEV[10]=2'd2; T_LD[10]=4'd2; T_LG[10]=4'd2;
T_POL[10]=1; T_PHA[10]=0; T_LSB[10]=1; T_TX[10]=16'h01; T_SW[10]=16'h80;
T_W[11]=5'd12; T_DIV[11]=8'd4; T_DEV[11]=2'd3; T_LD[11]=4'd0; T_LG[11]=4'd0;
T_POL[11]=1; T_PHA[11]=1; T_LSB[11]=0; T_TX[11]=16'h0ABC; T_SW[11]=16'h0DEF;
$display("=== Chapter 20.5 -- reference model, scoreboard and assertions ===");
// Reset is RELEASED ON A NEGEDGE, for the same reason `start` is driven on one.
// Releasing it on a posedge puts the assignment in the same region as every
// clocked block that tests it, and the order is undefined: the monitor may see
// the old value or the new one. Measured cost of getting this wrong -- the
// monitor held its reset one cycle longer in VHDL than in SystemVerilog, so the
// idle re-park of SCLK to CPOL=1 was counted as a frame edge in one language
// and not the other, and the first transaction of the run reported 17 edges
// instead of 16 in exactly one of the three.
repeat (4) @(posedge clk);
@(negedge clk); rst_n = 1'b1;
repeat (2) @(posedge clk);
// ---------------------------------------------------------------
$display(" S1 scoreboard: predicted vs observed, per transaction");
$display(" txn mode ord w div | rx_pred rx_obs edges cycles pred_cyc");
for (t = 0; t < 12; t = t + 1) begin
set_cfg(T_POL[t], T_PHA[t], T_LSB[t], T_W[t], T_DIV[t], T_DEV[t],
T_LD[t], T_LG[t], 4'd2);
slv_word = T_SW[t] & mask(T_W[t]);
fire(T_TX[t]);
wait_idle(20000, gd);
chki ("done pulsed", gd ? 1 : 0, 1);
chk16("rx_data", rx_data,
ref_rx(T_SW[t] & mask(T_W[t]), T_W[t], T_LSB[t]));
chk16("device rx", slv_rx & mask(T_W[t]),
ref_slave_rx(T_TX[t], T_W[t], T_LSB[t]));
chki ("sclk edges", n_edge, ref_edges(T_W[t]));
chki ("frame cycles", t_frame,
ref_frame_cycles(T_W[t], T_DIV[t], T_LD[t], T_LG[t]));
chki ("device selected", dev_seen, T_DEV[t]);
$display(" %3d %4d %0s %3d %3d | %7h %6h %5d %6d %8d",
t, {T_POL[t], T_PHA[t]}, T_LSB[t] ? "lsb" : "msb",
T_W[t], T_DIV[t],
ref_rx(T_SW[t] & mask(T_W[t]), T_W[t], T_LSB[t]), rx_data,
n_edge, t_frame,
ref_frame_cycles(T_W[t], T_DIV[t], T_LD[t], T_LG[t]));
end
$display(" 12 transactions scored, %0d mismatches", n_err);
// ---------------------------------------------------------------
$display(" S2 property monitors: region / exempt / violated");
$display(" P1 at most one select low %6d %6d %3d", ex1, xm1, fv1);
$display(" P2 SCLK parked at CPOL when idle %6d %6d %3d", ex2, xm2, fv2);
$display(" P3 SCLK quiet when nothing selected %6d %6d %3d", ex3, xm3, fv3);
$display(" P4 MOSI changes only on an edge %6d %6d %3d", ex4, xm4, fv4);
$display(" P5 bit count never exceeds width %6d %6d %3d", ex5, xm5, fv5);
$display(" P6 done implies a complete word %6d %6d %3d", ex6, xm6, fv6);
$display(" P7 a select implies busy %6d %6d %3d", ex7, xm7, fv7);
$display(" P8 done is emitted inside the frame %6d %6d %3d", ex8, xm8, fv8);
vac = 0;
if (ex1 == 0) vac = vac + 1;
if (ex2 == 0) vac = vac + 1;
if (ex3 == 0) vac = vac + 1;
if (ex4 == 0) vac = vac + 1;
if (ex5 == 0) vac = vac + 1;
if (ex6 == 0) vac = vac + 1;
if (ex7 == 0) vac = vac + 1;
if (ex8 == 0) vac = vac + 1;
n_chk = n_chk + 1;
if (vac != 0) begin
n_err = n_err + 1;
$display(" FAIL %0d propert(y/ies) never entered their region", vac);
end
n_chk = n_chk + 1;
if ((fv1|fv2|fv3|fv4|fv5|fv6|fv7|fv8) != 0) begin
n_err = n_err + 1;
$display(" FAIL a property was violated");
end
$display(" 8 properties, %0d unreached, %0d violated, %0d exemptions taken",
vac, fv1+fv2+fv3+fv4+fv5+fv6+fv7+fv8,
xm1+xm2+xm3+xm4+xm5+xm6+xm7+xm8);
// ---------------------------------------------------------------
// Each predicate is called with arguments that VIOLATE it. A monitor that
// cannot be made to fire is decoration, and this is the cheapest possible
// proof that these eight can.
$display(" S3 every property is shown able to fail");
n_neg = 0;
// Each call supplies arguments that VIOLATE the property: region entered,
// violation flagged, exemption NOT taken -> 3'b011.
if (p1_one_select(4'b1100) == 3'b011) n_neg = n_neg + 1;
if (p2_parked_level(1'b0, 1'b1, 1'b0, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p3_quiet_when_idle(1'b0, 1'b1, 1'b0, 1'b0, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p4_mosi_only_on_edges(1'b1, 1'b1, 1'b1, 1'b0, 1'b0, 1'b0)
== 3'b011) n_neg = n_neg + 1;
if (p5_bits_bounded(5'd9, 5'd8, 1'b1) == 3'b011) n_neg = n_neg + 1;
if (p6_done_means_complete(1'b1, 5'd7, 5'd8) == 3'b011) n_neg = n_neg + 1;
if (p7_select_implies_busy(1'b1, 1'b0) == 3'b011) n_neg = n_neg + 1;
if (p8_done_inside_frame(1'b1, 1'b0) == 3'b011) n_neg = n_neg + 1;
n_chk = n_chk + 1;
if (n_neg != 8) begin
n_err = n_err + 1;
$display(" FAIL only %0d of 8 predicates rejected a violating input", n_neg);
end
$display(" %0d of 8 predicates rejected a hand-built violation", n_neg);
// An exemption is a hole in a property, so each one is checked from the other
// side too: the exempted case must be ACCEPTED, and must be accepted for the
// stated reason rather than because the property stopped working.
// The exempted case must come back as region entered, NOT violated, exemption
// taken -> 3'b101. Checking this from both sides is what stops an exemption
// from quietly widening into "this property no longer fires at all".
t = 0;
if (p2_parked_level(1'b0, 1'b1, 1'b0, 1'b1) == 3'b101) t = t + 1;
if (p3_quiet_when_idle(1'b0, 1'b1, 1'b0, 1'b1, 1'b0) == 3'b101) t = t + 1;
if (p4_mosi_only_on_edges(1'b1, 1'b0, 1'b1, 1'b0, 1'b0, 1'b0)
== 3'b101) t = t + 1;
n_chk = n_chk + 1;
if (t != 3) begin
n_err = n_err + 1;
$display(" FAIL only %0d of 3 exemptions accepted their legal case", t);
end
$display(" %0d of 3 exemptions accept the legal case they exist for", t);
// And the scoreboard's own oracle must be able to disagree.
n_chk = n_chk + 1;
if (ref_rx(16'h9D, 5'd8, 1'b1) !== ref_rx(16'h9D, 5'd8, 1'b0)) begin
$display(" reference model separates bit orders (9d vs b9)");
end else begin
n_err = n_err + 1;
$display(" FAIL reference model is blind to bit order");
end
n_chk = n_chk + 1;
if (ref_frame_cycles(5'd8, 8'd1, 4'd2, 4'd2) !==
ref_frame_cycles(5'd8, 8'd1, 4'd2, 4'd3)) begin
$display(" reference model is sensitive to lag (44 vs 46 cycles)");
end else begin
n_err = n_err + 1;
$display(" FAIL reference model ignores lag");
end
$display("=== SUMMARY checks=%0d negatives=%0d failures=%0d : %0s ===",
n_chk, n_neg, n_err, (n_err == 0) ? "PASS" : "FAIL");
$finish;
end
initial begin
#8000000;
$display(" FATAL global timeout -- a frame never completed");
$display("=== SUMMARY checks=%0d negatives=%0d failures=%0d : FAIL ===",
n_chk, n_neg, n_err + 1);
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_capstone_check_tb.vhd — the same layer in VHDL, plus the three PSL directives that nvc executes
-- spi_capstone_check_tb.vhd
--
-- Chapter 20.5 in VHDL-2008 -- and this is the file where the third language stops
-- being a translation exercise and starts carrying something the other two cannot.
--
-- THE EIGHT PROPERTIES ARE HERE TWICE, ON PURPOSE.
--
-- As PREDICATES, identical to the SystemVerilog and Verilog ones, so the transcript
-- matches line for line and the cross-language comparison still means something.
--
-- As PSL DIRECTIVES, which `nvc` actually executes. That matters because three of
-- the specification's claims are TEMPORAL and a per-cycle predicate cannot state
-- them at all:
--
-- * `done` is exactly one cycle wide next
-- * an accepted request EVENTUALLY completes eventually! (liveness)
-- * `busy` rises with acceptance next
--
-- A liveness property has no per-cycle form. "Something good happens eventually"
-- cannot be checked by looking at one cycle, and a bench that only ever checks
-- single cycles silently has no liveness coverage -- a controller that accepts a
-- request and then sits still forever passes every safety check ever written.
--
-- These PSL directives were confirmed able to fail before being trusted: with the
-- completion suppressed, `nvc` reports
--
-- ** Error: 410ns+0: PSL assertion failed ... eventually! (dn = '1')
--
-- The SystemVerilog spelling of the same three properties is in the chapter text as
-- `assert property`, marked as NOT EXECUTED, because Icarus rejects SVA outright.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use std.textio.all;
use std.env.all;
entity spi_capstone_check_tb is
end entity spi_capstone_check_tb;
architecture tb of spi_capstone_check_tb is
signal clk : std_logic := '0';
signal rst_n : std_logic := '0';
signal cfg_cpol : std_logic := '0';
signal cfg_cpha : std_logic := '0';
signal cfg_lsb : std_logic := '0';
signal cfg_width : std_logic_vector(4 downto 0) := "01000";
signal cfg_div : std_logic_vector(7 downto 0) := x"01";
signal cfg_dev : std_logic_vector(1 downto 0) := "00";
signal cfg_lead : std_logic_vector(3 downto 0) := x"2";
signal cfg_lag : std_logic_vector(3 downto 0) := x"2";
signal cfg_idle : std_logic_vector(3 downto 0) := x"2";
signal start : std_logic := '0';
signal abort : std_logic := '0';
signal tx_data : std_logic_vector(15 downto 0) := (others => '0');
signal busy : std_logic;
signal done : std_logic;
signal cfg_err : std_logic;
signal rx_data : std_logic_vector(15 downto 0);
signal bits_done : std_logic_vector(4 downto 0);
signal sclk : std_logic;
signal mosi : std_logic;
signal cs_n : std_logic_vector(3 downto 0);
signal miso : std_logic;
signal slv_cpol : std_logic := '0';
signal slv_cpha : std_logic := '0';
signal slv_word : std_logic_vector(15 downto 0) := (others => '0');
signal slv_rx : std_logic_vector(15 downto 0) := (others => '0');
signal slv_w : unsigned(4 downto 0) := to_unsigned(8, 5);
signal slv_miso : std_logic := '0';
signal cs_any : std_logic;
-- `accept` is the antecedent the PSL directives below hang off: a request that is
-- actually taken. This bench never sends an illegal width, so acceptance is simply
-- a request while not busy.
signal accept_r : std_logic;
signal cyc : integer := 0;
signal n_edge : integer := 0;
signal t_frame : integer := 0;
signal cs_d, sclk_d, mosi_d, cpol_d1, cpol_d2 : std_logic := '0';
signal t_cs_fall : integer := 0;
-- WHICH select went low, not merely that one did. Added because bug injection
-- found the gap: the device model answers ANY select, so without this a
-- controller that asserted the wrong one passed every check.
signal dev_seen : integer := 0;
signal ex1, ex2, ex3, ex4, ex5, ex6, ex7, ex8 : integer := 0;
signal fv1, fv2, fv3, fv4, fv5, fv6, fv7, fv8 : integer := 0;
signal xm1, xm2, xm3, xm4, xm5, xm6, xm7, xm8 : integer := 0;
-- ---------------- reference model: specification arithmetic --------------------
function maskw (w : integer) return unsigned is
variable m : unsigned(15 downto 0);
begin
m := (others => '0');
for b in 0 to 15 loop
if b < w then m(b) := '1'; end if;
end loop;
return m;
end function maskw;
function revw (v : std_logic_vector(15 downto 0); w : integer)
return std_logic_vector is
variable r : std_logic_vector(15 downto 0);
begin
r := (others => '0');
for b in 0 to 15 loop
if b < w then r(w-1-b) := v(b); end if;
end loop;
return r;
end function revw;
function ref_rx (sw : std_logic_vector(15 downto 0); w : integer; lsb : std_logic)
return std_logic_vector is
variable m : std_logic_vector(15 downto 0);
begin
m := std_logic_vector(unsigned(sw) and maskw(w));
if lsb = '1' then return revw(m, w); else return m; end if;
end function ref_rx;
function ref_slave_rx (tx : std_logic_vector(15 downto 0); w : integer;
lsb : std_logic) return std_logic_vector is
variable m : std_logic_vector(15 downto 0);
begin
m := std_logic_vector(unsigned(tx) and maskw(w));
if lsb = '1' then return revw(m, w); else return m; end if;
end function ref_slave_rx;
function ref_edges (w : integer) return integer is
begin
return 2 * w;
end function ref_edges;
-- (lead + lag + 2N + 2) half-periods, derived from the specification's timing
-- clauses and not from the state machine -- which is what allows it to disagree.
function ref_frame_cycles (w, dv, ld, lg : integer) return integer is
begin
return (ld + lg + 2 * w + 2) * (dv + 1);
end function ref_frame_cycles;
-- ---------------- the eight properties ----------------------------------------
-- bit 0 region entered bit 1 violated bit 2 exemption taken
function p1_one_select (csn : std_logic_vector(3 downto 0))
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
variable n : integer;
begin
n := 0;
for i in 0 to 3 loop
if csn(i) = '0' then n := n + 1; end if;
end loop;
r := (others => '0');
r(0) := '1';
if n > 1 then r(1) := '1'; end if;
return r;
end function p1_one_select;
function p2_parked_level (csany, sclk_v, cpol_v, cpol_1 : std_logic)
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
variable region, stable : boolean;
begin
r := (others => '0');
region := (csany = '0');
stable := (cpol_v = cpol_1);
if region then r(0) := '1'; end if;
if region and stable and (sclk_v /= cpol_v) then r(1) := '1'; end if;
if region and not stable then r(2) := '1'; end if;
return r;
end function p2_parked_level;
function p3_quiet_when_idle (csany, sclk_v, sclk_p, cpol_1, cpol_2 : std_logic)
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
variable region, moved, cpol_moved : boolean;
begin
r := (others => '0');
region := (csany = '0');
moved := (sclk_v /= sclk_p);
cpol_moved := (cpol_1 /= cpol_2);
if region then r(0) := '1'; end if;
if region and moved and not cpol_moved then r(1) := '1'; end if;
if region and moved and cpol_moved then r(2) := '1'; end if;
return r;
end function p3_quiet_when_idle;
function p4_mosi_only_on_edges (csany, cs_p, mosi_v, mosi_p, sclk_v, sclk_p
: std_logic) return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
variable region, moved, cs_asserting : boolean;
begin
r := (others => '0');
region := (csany = '1');
moved := (mosi_v /= mosi_p);
cs_asserting := (csany = '1') and (cs_p = '0');
if region then r(0) := '1'; end if;
if region and moved and not cs_asserting and (sclk_v = sclk_p) then
r(1) := '1';
end if;
if region and moved and cs_asserting then r(2) := '1'; end if;
return r;
end function p4_mosi_only_on_edges;
function p5_bits_bounded (bits, w : unsigned(4 downto 0); bsy : std_logic)
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
begin
r := (others => '0');
if bsy = '1' then
r(0) := '1';
if bits > w then r(1) := '1'; end if;
end if;
return r;
end function p5_bits_bounded;
function p6_done_means_complete (dn : std_logic; bits, w : unsigned(4 downto 0))
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
begin
r := (others => '0');
if dn = '1' then
r(0) := '1';
if bits /= w then r(1) := '1'; end if;
end if;
return r;
end function p6_done_means_complete;
function p7_select_implies_busy (csany, bsy : std_logic)
return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
begin
r := (others => '0');
if csany = '1' then
r(0) := '1';
if bsy /= '1' then r(1) := '1'; end if;
end if;
return r;
end function p7_select_implies_busy;
function p8_done_inside_frame (dn, bsy : std_logic) return std_logic_vector is
variable r : std_logic_vector(2 downto 0);
begin
r := (others => '0');
if dn = '1' then
r(0) := '1';
if bsy /= '1' then r(1) := '1'; end if;
end if;
return r;
end function p8_done_inside_frame;
-- ---------------- formatting --------------------------------------------------
function hex4 (v : std_logic_vector(15 downto 0)) return string is
constant D : string(1 to 16) := "0123456789abcdef";
variable s : string(1 to 4);
variable n : integer;
begin
if is_x(v) then return "xxxx"; end if;
n := to_integer(unsigned(v));
for i in 4 downto 1 loop
s(i) := D((n mod 16) + 1);
n := n / 16;
end loop;
return s;
end function hex4;
function ipad (v : integer; w : integer) return string is
variable s : string(1 to w);
variable t : string(1 to 20);
variable n, len : integer;
begin
t := (others => ' '); n := v; len := 0;
if n = 0 then
len := 1; t(1) := '0';
else
while n > 0 loop
len := len + 1;
t(len) := character'val(character'pos('0') + (n mod 10));
n := n / 10;
end loop;
end if;
s := (others => ' ');
for i in 1 to len loop
s(w - i + 1) := t(i);
end loop;
return s;
end function ipad;
function hpad (v : std_logic_vector(15 downto 0); w : integer) return string is
variable s : string(1 to w);
begin
s := (others => ' ');
s(w - 3 to w) := hex4(v);
return s;
end function hpad;
function i0 (v : integer) return string is
begin
return integer'image(v);
end function i0;
function ord_s (lsb : std_logic) return string is
begin
if lsb = '1' then return "lsb"; else return "msb"; end if;
end function ord_s;
procedure pr (s : string) is
variable l : line;
begin
write(l, s);
writeline(output, l);
end procedure pr;
function sl (b : boolean) return std_logic is
begin
if b then return '1'; else return '0'; end if;
end function sl;
type tv_t is record
w, dv, dev, ld, lg : integer;
pol, pha, lsb : std_logic;
tx, sw : std_logic_vector(15 downto 0);
end record;
type tv_arr is array (0 to 11) of tv_t;
constant TV : tv_arr := (
( 8, 1, 0, 2, 2, '0','0','0', x"009D", x"00B9"),
( 8, 1, 1, 2, 2, '0','1','0', x"009D", x"00B9"),
( 8, 1, 2, 2, 2, '1','0','0', x"009D", x"00B9"),
( 8, 1, 3, 2, 2, '1','1','0', x"009D", x"00B9"),
( 4, 0, 0, 0, 0, '0','0','1', x"000D", x"000A"),
(16, 3, 1, 5, 4, '1','1','1', x"BEEF", x"1234"),
(13, 2, 2, 1, 3, '0','1','1', x"1ACE", x"0F5A"),
( 5, 7, 3, 3, 1, '1','0','0', x"0015", x"000B"),
(16, 0, 0,15,15, '0','0','0', x"FFFF", x"0001"),
( 4, 1, 1, 2, 2, '0','0','0', x"0000", x"000F"),
( 8, 1, 2, 2, 2, '1','0','1', x"0001", x"0080"),
(12, 4, 3, 0, 0, '1','1','0', x"0ABC", x"0DEF")
);
begin
cs_any <= not (cs_n(0) and cs_n(1) and cs_n(2) and cs_n(3));
miso <= slv_miso;
accept_r <= start and (not busy);
dut : entity work.spi_capstone_ctrl
generic map (DATA_W => 16, MIN_WIDTH => 4, NDEV => 4)
port map (
clk => clk, rst_n => rst_n,
cfg_cpol => cfg_cpol, cfg_cpha => cfg_cpha, cfg_lsb_first => cfg_lsb,
cfg_width => cfg_width, cfg_div => cfg_div, cfg_dev => cfg_dev,
cfg_lead => cfg_lead, cfg_lag => cfg_lag, cfg_idle => cfg_idle,
start => start, tx_data => tx_data, abort => abort,
busy => busy, done => done, cfg_err => cfg_err,
rx_data => rx_data, bits_done => bits_done,
sclk => sclk, mosi => mosi, cs_n => cs_n, miso => miso
);
-- ===================== PSL: the temporal half ==============================
-- These three say things no per-cycle predicate can. nvc executes them.
-- psl default clock is rising_edge(clk);
-- psl DONE_IS_ONE_CYCLE : assert always (done = '1' -> next (done = '0'));
-- psl BUSY_RISES : assert always ((accept_r = '1' and rst_n = '1')
-- -> next (busy = '1'));
-- psl ACCEPT_COMPLETES : assert always ((accept_r = '1' and rst_n = '1')
-- -> eventually! (done = '1'));
--
-- The cover directives carry REPORT STRINGS so that being hit is visible. A cover
-- that is never hit is SILENT in nvc, and silence is exactly what a passing
-- assertion looks like -- so without a named report, "no output" would mean both
-- "the property held everywhere" and "the scenario never happened", which are the
-- two things a vacuity review has to tell apart. The runner requires all three
-- strings to appear.
-- psl COVER_DONE : cover {done = '1'} report "psl-cover: a frame completed";
-- psl COVER_W16 : cover {accept_r = '1' and cfg_width = "10000"}
-- report "psl-cover: a 16-bit transfer was accepted";
-- psl COVER_MODE3 : cover {accept_r = '1' and cfg_cpol = '1' and cfg_cpha = '1'}
-- report "psl-cover: mode 3 was accepted";
clkgen : process
begin
clk <= '0'; wait for 5 ns;
clk <= '1'; wait for 5 ns;
end process clkgen;
slave : process (cs_any, sclk)
variable sr : std_logic_vector(15 downto 0);
variable idx : unsigned(4 downto 0);
variable nrx : unsigned(4 downto 0);
variable lead_s : boolean;
begin
if rising_edge(cs_any) then
sr := std_logic_vector(shift_left(unsigned(slv_word),
16 - to_integer(slv_w)));
slv_rx <= (others => '0');
nrx := (others => '0');
if slv_cpha = '0' then
slv_miso <= sr(15);
sr := sr(14 downto 0) & '0';
idx := to_unsigned(1, 5);
else
slv_miso <= '0';
idx := (others => '0');
end if;
elsif sclk'event and cs_any = '1' then
lead_s := (sclk /= slv_cpol);
if (slv_cpha = '1' and not lead_s) or (slv_cpha = '0' and lead_s) then
if nrx < slv_w then
slv_rx <= slv_rx(14 downto 0) & mosi;
nrx := nrx + 1;
end if;
end if;
if (slv_cpha = '1' and lead_s) or (slv_cpha = '0' and not lead_s) then
if idx < slv_w then
slv_miso <= sr(15);
sr := sr(14 downto 0) & '0';
idx := idx + 1;
end if;
end if;
end if;
end process slave;
mon : process (clk)
variable r : std_logic_vector(2 downto 0);
begin
if rising_edge(clk) then
if rst_n = '0' then
cyc <= 0; n_edge <= 0;
cs_d <= '0'; sclk_d <= '0'; mosi_d <= '0';
cpol_d1 <= '0'; cpol_d2 <= '0';
ex1<=0; ex2<=0; ex3<=0; ex4<=0; ex5<=0; ex6<=0; ex7<=0; ex8<=0;
fv1<=0; fv2<=0; fv3<=0; fv4<=0; fv5<=0; fv6<=0; fv7<=0; fv8<=0;
xm1<=0; xm2<=0; xm3<=0; xm4<=0; xm5<=0; xm6<=0; xm7<=0; xm8<=0;
else
cyc <= cyc + 1;
r := p1_one_select(cs_n);
ex1 <= ex1 + to_integer(unsigned'('0' & r(0)));
fv1 <= fv1 + to_integer(unsigned'('0' & r(1)));
xm1 <= xm1 + to_integer(unsigned'('0' & r(2)));
r := p2_parked_level(cs_any, sclk, cfg_cpol, cpol_d1);
ex2 <= ex2 + to_integer(unsigned'('0' & r(0)));
fv2 <= fv2 + to_integer(unsigned'('0' & r(1)));
xm2 <= xm2 + to_integer(unsigned'('0' & r(2)));
r := p3_quiet_when_idle(cs_any, sclk, sclk_d, cpol_d1, cpol_d2);
ex3 <= ex3 + to_integer(unsigned'('0' & r(0)));
fv3 <= fv3 + to_integer(unsigned'('0' & r(1)));
xm3 <= xm3 + to_integer(unsigned'('0' & r(2)));
r := p4_mosi_only_on_edges(cs_any, cs_d, mosi, mosi_d, sclk, sclk_d);
ex4 <= ex4 + to_integer(unsigned'('0' & r(0)));
fv4 <= fv4 + to_integer(unsigned'('0' & r(1)));
xm4 <= xm4 + to_integer(unsigned'('0' & r(2)));
r := p5_bits_bounded(unsigned(bits_done), unsigned(cfg_width), busy);
ex5 <= ex5 + to_integer(unsigned'('0' & r(0)));
fv5 <= fv5 + to_integer(unsigned'('0' & r(1)));
xm5 <= xm5 + to_integer(unsigned'('0' & r(2)));
r := p6_done_means_complete(done, unsigned(bits_done),
unsigned(cfg_width));
ex6 <= ex6 + to_integer(unsigned'('0' & r(0)));
fv6 <= fv6 + to_integer(unsigned'('0' & r(1)));
xm6 <= xm6 + to_integer(unsigned'('0' & r(2)));
r := p7_select_implies_busy(cs_any, busy);
ex7 <= ex7 + to_integer(unsigned'('0' & r(0)));
fv7 <= fv7 + to_integer(unsigned'('0' & r(1)));
xm7 <= xm7 + to_integer(unsigned'('0' & r(2)));
r := p8_done_inside_frame(done, busy);
ex8 <= ex8 + to_integer(unsigned'('0' & r(0)));
fv8 <= fv8 + to_integer(unsigned'('0' & r(1)));
xm8 <= xm8 + to_integer(unsigned'('0' & r(2)));
if cs_any = '1' and cs_d = '0' then
t_cs_fall <= cyc;
n_edge <= 0;
if cs_n(0) = '0' then dev_seen <= 0;
elsif cs_n(1) = '0' then dev_seen <= 1;
elsif cs_n(2) = '0' then dev_seen <= 2;
else dev_seen <= 3;
end if;
end if;
if cs_any = '0' and cs_d = '1' then
t_frame <= cyc - t_cs_fall;
end if;
-- `cs_d` as well as `cs_any`: an edge is only a FRAME edge if a device
-- was ALREADY selected last cycle. A transition in the cycle the
-- select falls is SCLK reaching its new idle level, not a clocking
-- edge. Without this gate the first CPOL=1 transaction counted 17
-- edges here and 16 in SystemVerilog, on identical data.
if cs_any = '1' and cs_d = '1' and sclk /= sclk_d then
n_edge <= n_edge + 1;
end if;
cs_d <= cs_any;
sclk_d <= sclk;
mosi_d <= mosi;
cpol_d1 <= cfg_cpol;
cpol_d2 <= cpol_d1;
end if;
end if;
end process mon;
wd : process
begin
wait for 12 ms;
pr(" FATAL global timeout -- a frame never completed");
pr("=== SUMMARY checks=0 negatives=0 failures=1 : FAIL ===");
finish;
end process wd;
main : process
variable n_chk : integer := 0;
variable n_err : integer := 0;
variable n_neg : integer := 0;
variable vac : integer := 0;
variable t3 : integer := 0;
variable gd : std_logic;
procedure chk16 (nm : string; got, exp : std_logic_vector(15 downto 0)) is
begin
n_chk := n_chk + 1;
if got /= exp then
n_err := n_err + 1;
pr(" FAIL " & nm & ": got " & hex4(got) & " expected " & hex4(exp));
end if;
end procedure chk16;
procedure chki (nm : string; got, exp : integer) is
begin
n_chk := n_chk + 1;
if got /= exp then
n_err := n_err + 1;
pr(" FAIL " & nm & ": got " & i0(got) & " expected " & i0(exp));
end if;
end procedure chki;
procedure set_cfg (cpol_i, cpha_i, lsb_i : std_logic;
wv, dv, dv_n, ld, lg, idl : integer) is
begin
cfg_cpol <= cpol_i;
cfg_cpha <= cpha_i;
cfg_lsb <= lsb_i;
cfg_width <= std_logic_vector(to_unsigned(wv, 5));
cfg_div <= std_logic_vector(to_unsigned(dv, 8));
cfg_dev <= std_logic_vector(to_unsigned(dv_n, 2));
cfg_lead <= std_logic_vector(to_unsigned(ld, 4));
cfg_lag <= std_logic_vector(to_unsigned(lg, 4));
cfg_idle <= std_logic_vector(to_unsigned(idl, 4));
slv_cpol <= cpol_i;
slv_cpha <= cpha_i;
slv_w <= to_unsigned(wv, 5);
end procedure set_cfg;
procedure fire (d : std_logic_vector(15 downto 0)) is
begin
wait until falling_edge(clk);
tx_data <= d;
start <= '1';
wait until falling_edge(clk);
start <= '0';
end procedure fire;
procedure wait_idle (maxc : integer; gotd : out std_logic) is
variable g : integer;
variable seen : std_logic;
begin
g := 0; seen := '0';
while g < maxc loop
wait until falling_edge(clk);
g := g + 1;
if done = '1' then seen := '1'; end if;
if busy = '0' and seen = '1' then g := maxc;
elsif busy = '0' and g > 4 then g := maxc; end if;
end loop;
gotd := seen;
end procedure wait_idle;
begin
pr("=== Chapter 20.5 -- reference model, scoreboard and assertions ===");
-- Reset is RELEASED ON A FALLING EDGE, for the same reason `start` is driven on
-- one: released on a rising edge it races every clocked block that tests it.
-- The measured cost was a one-cycle difference in when the monitor left reset,
-- which counted SCLK's idle re-park as a frame edge in VHDL but not in
-- SystemVerilog -- 17 edges against 16, on the first transaction only.
for i in 1 to 4 loop wait until rising_edge(clk); end loop;
wait until falling_edge(clk);
rst_n <= '1';
for i in 1 to 2 loop wait until rising_edge(clk); end loop;
pr(" S1 scoreboard: predicted vs observed, per transaction");
pr(" txn mode ord w div | rx_pred rx_obs edges cycles pred_cyc");
for t in 0 to 11 loop
set_cfg(TV(t).pol, TV(t).pha, TV(t).lsb, TV(t).w, TV(t).dv, TV(t).dev,
TV(t).ld, TV(t).lg, 2);
slv_word <= std_logic_vector(unsigned(TV(t).sw) and maskw(TV(t).w));
fire(TV(t).tx);
wait_idle(20000, gd);
chki ("done pulsed", to_integer(unsigned'('0' & gd)), 1);
chk16("rx_data", rx_data,
ref_rx(std_logic_vector(unsigned(TV(t).sw) and maskw(TV(t).w)),
TV(t).w, TV(t).lsb));
chk16("device rx",
std_logic_vector(unsigned(slv_rx) and maskw(TV(t).w)),
ref_slave_rx(TV(t).tx, TV(t).w, TV(t).lsb));
chki ("sclk edges", n_edge, ref_edges(TV(t).w));
chki ("frame cycles", t_frame,
ref_frame_cycles(TV(t).w, TV(t).dv, TV(t).ld, TV(t).lg));
chki ("device selected", dev_seen, TV(t).dev);
pr(" " & ipad(t, 3) &
" " & ipad(to_integer(unsigned'(TV(t).pol & TV(t).pha)), 4) &
" " & ord_s(TV(t).lsb) &
" " & ipad(TV(t).w, 3) &
" " & ipad(TV(t).dv, 3) &
" | " & hpad(ref_rx(std_logic_vector(unsigned(TV(t).sw)
and maskw(TV(t).w)), TV(t).w, TV(t).lsb), 7) &
" " & hpad(rx_data, 6) &
" " & ipad(n_edge, 5) &
" " & ipad(t_frame, 6) &
" " & ipad(ref_frame_cycles(TV(t).w, TV(t).dv,
TV(t).ld, TV(t).lg), 8));
end loop;
pr(" 12 transactions scored, " & i0(n_err) & " mismatches");
pr(" S2 property monitors: region / exempt / violated");
pr(" P1 at most one select low " & ipad(ex1,6) & " " & ipad(xm1,6) & " " & ipad(fv1,3));
pr(" P2 SCLK parked at CPOL when idle " & ipad(ex2,6) & " " & ipad(xm2,6) & " " & ipad(fv2,3));
pr(" P3 SCLK quiet when nothing selected " & ipad(ex3,6) & " " & ipad(xm3,6) & " " & ipad(fv3,3));
pr(" P4 MOSI changes only on an edge " & ipad(ex4,6) & " " & ipad(xm4,6) & " " & ipad(fv4,3));
pr(" P5 bit count never exceeds width " & ipad(ex5,6) & " " & ipad(xm5,6) & " " & ipad(fv5,3));
pr(" P6 done implies a complete word " & ipad(ex6,6) & " " & ipad(xm6,6) & " " & ipad(fv6,3));
pr(" P7 a select implies busy " & ipad(ex7,6) & " " & ipad(xm7,6) & " " & ipad(fv7,3));
pr(" P8 done is emitted inside the frame " & ipad(ex8,6) & " " & ipad(xm8,6) & " " & ipad(fv8,3));
vac := 0;
if ex1 = 0 then vac := vac + 1; end if;
if ex2 = 0 then vac := vac + 1; end if;
if ex3 = 0 then vac := vac + 1; end if;
if ex4 = 0 then vac := vac + 1; end if;
if ex5 = 0 then vac := vac + 1; end if;
if ex6 = 0 then vac := vac + 1; end if;
if ex7 = 0 then vac := vac + 1; end if;
if ex8 = 0 then vac := vac + 1; end if;
n_chk := n_chk + 1;
if vac /= 0 then
n_err := n_err + 1;
pr(" FAIL " & i0(vac) & " propert(y/ies) never entered their region");
end if;
n_chk := n_chk + 1;
if (fv1+fv2+fv3+fv4+fv5+fv6+fv7+fv8) /= 0 then
n_err := n_err + 1;
pr(" FAIL a property was violated");
end if;
pr(" 8 properties, " & i0(vac) & " unreached, " &
i0(fv1+fv2+fv3+fv4+fv5+fv6+fv7+fv8) & " violated, " &
i0(xm1+xm2+xm3+xm4+xm5+xm6+xm7+xm8) & " exemptions taken");
pr(" S3 every property is shown able to fail");
n_neg := 0;
if p1_one_select("1100") = "011" then n_neg := n_neg + 1; end if;
if p2_parked_level('0','1','0','0') = "011" then n_neg := n_neg + 1; end if;
if p3_quiet_when_idle('0','1','0','0','0') = "011" then n_neg := n_neg + 1; end if;
if p4_mosi_only_on_edges('1','1','1','0','0','0') = "011" then n_neg := n_neg + 1; end if;
if p5_bits_bounded(to_unsigned(9,5), to_unsigned(8,5), '1') = "011" then n_neg := n_neg + 1; end if;
if p6_done_means_complete('1', to_unsigned(7,5), to_unsigned(8,5)) = "011" then n_neg := n_neg + 1; end if;
if p7_select_implies_busy('1','0') = "011" then n_neg := n_neg + 1; end if;
if p8_done_inside_frame('1','0') = "011" then n_neg := n_neg + 1; end if;
n_chk := n_chk + 1;
if n_neg /= 8 then
n_err := n_err + 1;
pr(" FAIL only " & i0(n_neg) & " of 8 predicates rejected a violating input");
end if;
pr(" " & i0(n_neg) & " of 8 predicates rejected a hand-built violation");
t3 := 0;
if p2_parked_level('0','1','0','1') = "101" then t3 := t3 + 1; end if;
if p3_quiet_when_idle('0','1','0','1','0') = "101" then t3 := t3 + 1; end if;
if p4_mosi_only_on_edges('1','0','1','0','0','0') = "101" then t3 := t3 + 1; end if;
n_chk := n_chk + 1;
if t3 /= 3 then
n_err := n_err + 1;
pr(" FAIL only " & i0(t3) & " of 3 exemptions accepted their legal case");
end if;
pr(" " & i0(t3) & " of 3 exemptions accept the legal case they exist for");
n_chk := n_chk + 1;
if ref_rx(x"009D", 8, '1') /= ref_rx(x"009D", 8, '0') then
pr(" reference model separates bit orders (9d vs b9)");
else
n_err := n_err + 1;
pr(" FAIL reference model is blind to bit order");
end if;
n_chk := n_chk + 1;
if ref_frame_cycles(8,1,2,2) /= ref_frame_cycles(8,1,2,3) then
pr(" reference model is sensitive to lag (44 vs 46 cycles)");
else
n_err := n_err + 1;
pr(" FAIL reference model ignores lag");
end if;
if n_err = 0 then
pr("=== SUMMARY checks=" & i0(n_chk) & " negatives=" & i0(n_neg) &
" failures=" & i0(n_err) & " : PASS ===");
else
pr("=== SUMMARY checks=" & i0(n_chk) & " negatives=" & i0(n_neg) &
" failures=" & i0(n_err) & " : FAIL ===");
end if;
finish;
end process main;
end architecture tb;9. What It Reports
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
=== Chapter 20.5 -- reference model, scoreboard and assertions ===
12 transactions scored, 0 mismatches
8 properties, 0 unreached, 0 violated, 21 exemptions taken
8 of 8 predicates rejected a hand-built violation
3 of 3 exemptions accept the legal case they exist for
=== SUMMARY checks=78 negatives=8 failures=0 : PASS ===78 checks in each of the three languages, with byte-identical transcripts, plus 3 executed PSL assertions and 3 executed cover directives in the VHDL run.
| SystemVerilog | Verilog-2001 | VHDL-2008 | |
|---|---|---|---|
| Checks | 78 | 78 | 78 |
| Failures | 0 | 0 | 0 |
| Properties executed | 8 predicates | 8 predicates | 8 predicates + 3 PSL |
| Cover directives executed | — | — | 3, all hit |
| Concurrent assertions | rejected by the tool | rejected by the tool | 3, executed |
10. Summary
The checking layer has three parts that fail differently. A reference model built from specification arithmetic — a mask, a reversal, and one multiplication — predicts the received word, the edge count, and the frame duration to the cycle, and predicted 128 cycles for a 5-bit transfer at a divider of 7 before the design ran. A scoreboard compares twelve transactions covering all four modes, both bit orders and widths from 4 to 16, with zero mismatches. And eight per-cycle properties watch the pins, of which the most valuable is the one that needs no knowledge of the design's internals at all: MOSI changes only when SCLK changes.
Three of those eight were wrong when first written, and reported 21 violations against a correct controller — seven each, matching exactly the number of times the bench changes CPOL. The repair was not to loosen them but to state the narrow property that is actually true, and then to count the resulting exemptions rather than hide them. That mattered: P3's exemption initially fired on every one of its seven antecedent occurrences, so the property passed, reported nothing, and had never tested anything — a vacuity that a healthy-looking exercise count conceals completely.
Every predicate is unit-tested in both directions: a hand-built violation must be flagged, and the exempted case must be accepted and marked exempt, which is what stops an exemption from quietly widening into a property that no longer fires.
Three of the specification's claims are temporal and have no per-cycle form, and one of them is liveness — a controller that accepts a request and clocks forever satisfies all eight safety properties indefinitely. The SystemVerilog assertions for those three are published as reviewed, unexecuted code because the simulator rejects them; the PSL equivalents run, and the eventually! operator was confirmed able to fail before being trusted.
11. What Comes Next
Chapter 20.6 replaces the hand-written transaction table with a constrained random generator, and starts by reviewing the generator rather than trusting it — where one of the two traps produces a perfectly uniform histogram over a sequence with a period of four.
Continue learning
Related tutorials
- Related topic
Reference Model and Scoreboard
Two predictions of the same traffic through one scoreboard: one computed from the transaction, one produced by a second copy of the design. Both report a clean run on a correct design, and with a fault injected the copy records a pass on every transaction.
- Related topic
SPI Protocol Assertions
A property attempt has four outcomes, not two, and the two that are not failures are where a suite's silence comes from. Seven SPI properties measured for passes, vacuous evaluations and attempts still open at the end of the test, with the same six obligations run a second time as PSL assertions by a real assertion engine.
- Related topic
Full-Duplex Exchange
Every SPI transfer moves a bit in both directions on every edge, whether the software wanted it to or not. Where dummy bytes come from, why bytes received during a command phase exist but mean nothing, and why read and write are interpretations rather than modes.
- Related topic
CS-to-SCLK and SCLK-to-CS Timing
Chip select has timing requirements of its own: the lead before the first clock edge, the lag after the last, and the minimum deselect between transactions. Why violating them breaks a transfer whose every SCLK edge was correct.