SPI · Module 17
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.
Chapter 16.1 extracted eight rules and decided each of them at a single instant: is SCLK at its idle level on this cycle, was this interval long enough, did MOSI move at this edge.
A property is a different kind of statement. It opens at one instant and is settled at another, and between those two instants it is neither true nor false. That difference is the whole content of an assertion language, and it is also where its failure modes live.
An SVA property that is never reached passes, on every clock edge, forever. What distinguishes that from a property that works?
1. Four Outcomes, Not Two
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
PASSED the antecedent matched and the consequent was satisfied
FAILED the antecedent matched and the consequent was not
VACUOUS the property was evaluated and the antecedent did not match, so
nothing was checked. SVA and PSL both report this as a pass.
INCOMPLETE the antecedent matched, the attempt is still open, and the
simulation ended. Neither true nor false, and counted as neither.Most suites collapse all four into "did anything print". The two that are not failures are where the silence comes from:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
vacuous == attempts the property has NEVER been tested. Its zero failure
count is a statement about the STIMULUS, not about
the design.
incomplete > 0 the test ended mid-obligation. A design that was ABOUT
to violate the property is indistinguishable from one
that would have satisfied it.2. An Attempt Has An Extent
EDGE_AFTER_SELECT, settled two ways
18 cyclesThree things in that picture are the chapter. The attempt has duration. It is settled by whichever of two events happens first, so the property needs both written down. And the attempt row is the property's internal state — which is exactly what a waveform viewer cannot display and what a report that shows only pass/fail throws away.
3. Seven Properties, Seven Temporal Shapes
| # | Property | Shape |
|---|---|---|
| P1 | an assert is followed by an SCLK edge, within MAXLEAD and before the release | bounded existence |
| P2 | MOSI does not move in the cycle before, at, or after a capture edge | a stability window |
| P3 | after an edge, SCLK holds for HALF−1 further cycles | a multi-cycle consequent |
| P4 | from the first edge, 2N edges arrive before the release | a count settled by an event |
| P5 | from the release until the next select, SCLK stays at CPOL | an unbounded interval |
| P6 | once the frame is complete, the select is released within MAXLAG | bounded liveness |
| P7 | a one-bit frame behaves | never attempted in this suite |
P1 and P6 are the same shape pointing in opposite directions — one asks that something start, the other that something end — and a suite with only the first kind cannot see a master that never lets go.
4. Legal Traffic, And The Property That Is Never Attempted
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
prop name attempts vacuous passes fails incomplete
P1 EDGE_AFTER_SELECT 2 212 2 0 0
P2 STABLE_AT_CAPTURE 8 48 8 0 0
P3 HALF_STABLE 16 40 16 0 0
P4 FRAME_COMPLETE 2 212 2 0 0
P5 SCLK_PARKED 2 54 2 0 0
P6 RELEASE_AFTER_FRAME 2 0 2 0 0
P7 ONE_BIT_FRAME 0 2 0 0 0Six properties with non-zero passes, no failures, across sixteen transactions in four modes and two widths. And then P7.
P7 was attempted zero times. Its antecedent needs a one-bit frame and this suite sends none. In SVA that property passes vacuously on every clock edge for the life of the project, and a pass/fail report cannot tell it from P1. The only number that separates them is in the attempts column.
Note also P1's vacuous count of 212 against its 2 attempts. That ratio is not a problem — the antecedent is a rare event and should be — but it is the number that tells you the rarity, and a property whose ratio is attempts = 0 is the same object as P7.
5. Six Violations, Six Properties
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
violation expected properties that failed
a select with no SCLK edge P1 0000001
MOSI moving at a capture P2 0000010
a one-cycle half period P3 0000100
a frame two edges short P4 0001000
an SCLK glitch while idle P5 0010000
the select held past MAXLAG P6 0100000A perfect diagonal, and it is a result about the antecedents as much as about the checks.
6. An Attempt Left Open
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
an attempt still open when the test ends:
P1 passes ....... 0
P1 fails ........ 0
P1 incomplete ... 1The select is asserted, nothing follows, and the simulation ends. The attempt appears in neither the pass column nor the fail column.
That is the honest answer. The antecedent matched, the obligation was never settled, and a design that was about to violate the property is indistinguishable here from one that would have satisfied it. PSL does not report this and neither does SVA — an attempt still open when a simulation ends prints nothing at all — which is the one place the verbose procedural version is strictly more informative than the concise declarative one.
7. Building It — Three HDLs, And One Real Assertion Engine
The runnable components are procedural: explicit attempt state, explicit counters, a verdict computed by the bench. The VHDL file carries the same six obligations a second time as PSL directives, and nvc executes them — the only place in this curriculum where an assertion language actually runs. Reading the two side by side is the closest a reader can get to watching an SVA property behave.
Azvya Education Pvt. Ltd.VLSI Mentor
spi_props.sv — seven properties, with attempts, vacuous evaluations, passes, failures and incomplete attempts
// spi_props.sv
//
// Chapter 17.1 -- SPI protocol properties, and the four outcomes of a property attempt.
//
// WHY THIS IS NOT CHAPTER 16.1 AGAIN.
//
// Chapter 16.1's eight rules were decided at single instants: is SCLK at its idle level on
// this cycle, is this interval long enough, did MOSI move at this edge. A property is a
// different kind of statement. It opens at one instant and is settled at another, and
// between those two instants it is OPEN -- neither true nor false yet.
//
// That is what makes an assertion language worth having and it is also where its failure
// modes live. A property attempt has FOUR outcomes, not two:
//
// PASSED the antecedent matched and the consequent was satisfied
// FAILED the antecedent matched and the consequent was not
// VACUOUS the property was evaluated and the antecedent did not match, so
// nothing was checked. SVA reports this as a pass.
// INCOMPLETE the antecedent matched, the attempt is still open, and the
// simulation ended. Neither true nor false, and counted as neither.
//
// Most suites collapse all four into "did anything print". This module counts them
// separately, because the two that are not failures are where the silence comes from:
//
// vacuous == attempts the property has NEVER been tested. Its zero failure count
// is a statement about the stimulus, not about the design.
// incomplete > 0 the test ended mid-obligation. A design that was ABOUT to
// violate the property is indistinguishable from one that
// would have satisfied it, and the report says nothing.
//
// SEVEN PROPERTIES, chosen so that each one needs a different temporal shape.
//
// P1 EDGE_AFTER_SELECT bounded existence: an assert must be followed by an SCLK edge
// within MAXLEAD cycles, and before the deassert.
// P2 STABLE_AT_CAPTURE a stability window: MOSI must not move in the cycle before, at,
// or after a capture edge.
// P3 HALF_STABLE a multi-cycle consequent: after an edge, SCLK holds for HALF-1
// further cycles.
// P4 FRAME_COMPLETE a count settled by a terminating event: from the first edge,
// 2N edges must be seen before the deassert.
// P5 SCLK_PARKED stability over an UNBOUNDED interval, terminated by an event:
// from the deassert until the next assert, SCLK stays at CPOL.
// P6 RELEASE_AFTER_FRAME bounded liveness the other way: once the frame is complete, the
// select must be released within MAXLAG cycles.
// P7 ONE_BIT_FRAME a property whose antecedent this suite never produces. It is
// here to be measured, not to be satisfied.
//
// AND THE ANTECEDENTS ARE CHOSEN SO THE VIOLATION MATRIX CAN BE DIAGONAL.
//
// P4's antecedent is the FIRST EDGE rather than the assert, and that is not cosmetic. With
// the assert as the antecedent, a select pulse carrying no edges at all fails both P1 and
// P4 -- one fault, two reports, and neither of them says "there were no edges". Anchored to
// the first edge, P4 is not attempted at all when there are no edges, and P1's report
// stands alone.
//
// Choosing an antecedent is therefore part of designing a DIAGNOSIS, not just part of
// writing a check.
`timescale 1ns/1ps
module spi_props #(
parameter int HALF = 3, // cycles per SCLK half period
parameter int MAXLEAD = 16, // P1's bound: assert to first edge
parameter int MAXLAG = 8, // P6's bound: frame complete to release
parameter int LEN_W = 6,
parameter int CNT_W = 16,
parameter int NPROPS = 7
) (
input wire clk,
input wire rst_n,
// --- the pins ----------------------------------------------------------
input wire sclk,
input wire cs_n,
input wire mosi,
// --- the configuration -------------------------------------------------
input wire cpol,
input wire cpha,
input wire [LEN_W-1:0] len,
input wire clr,
// Closes every open attempt and books it as INCOMPLETE. A test that does not do
// this at its end is a test whose open attempts vanish, which is the failure this
// whole module exists to make visible.
input wire flush,
output wire [NPROPS*CNT_W-1:0] attempts_flat,
output wire [NPROPS*CNT_W-1:0] vacuous_flat,
output wire [NPROPS*CNT_W-1:0] passes_flat,
output wire [NPROPS*CNT_W-1:0] fails_flat,
output wire [NPROPS*CNT_W-1:0] incomplete_flat
);
localparam int P_EDGE = 0,
P_STABLE = 1,
P_HALF = 2,
P_FRAME = 3,
P_PARKED = 4,
P_REL = 5,
P_ONEBIT = 6;
// --- observed history ---------------------------------------------------
reg sclk_d, cs_n_d, mosi_d, mosi_dd;
wire cs_assert = ~cs_n & cs_n_d;
wire cs_deassert = cs_n & ~cs_n_d;
wire in_txn = ~cs_n | cs_deassert;
wire sclk_edge = sclk ^ sclk_d;
wire leading = sclk_edge & (sclk != cpol);
wire trailing = sclk_edge & (sclk == cpol);
wire capture = cpha ? trailing : leading;
wire [LEN_W:0] edges_per_frame = {1'b0, len} << 1;
reg [CNT_W-1:0] attempts [0:NPROPS-1];
reg [CNT_W-1:0] vacuous [0:NPROPS-1];
reg [CNT_W-1:0] passes [0:NPROPS-1];
reg [CNT_W-1:0] fails [0:NPROPS-1];
reg [CNT_W-1:0] incomplete [0:NPROPS-1];
genvar gi;
generate
for (gi = 0; gi < NPROPS; gi = gi + 1) begin : g_flat
assign attempts_flat [gi*CNT_W +: CNT_W] = attempts[gi];
assign vacuous_flat [gi*CNT_W +: CNT_W] = vacuous[gi];
assign passes_flat [gi*CNT_W +: CNT_W] = passes[gi];
assign fails_flat [gi*CNT_W +: CNT_W] = fails[gi];
assign incomplete_flat[gi*CNT_W +: CNT_W] = incomplete[gi];
end
endgenerate
// --- attempt state, one set per property --------------------------------
// Every property here has at most one attempt open at a time, which is a property of
// these antecedents rather than a limitation: each is anchored to an event that cannot
// recur while its own attempt is open. An antecedent that CAN recur needs a queue of
// attempts, and SVA maintains exactly that -- which is why a property with a level
// antecedent can report hundreds of failures for one fault. Chapter 17.2 measures it.
reg a1_open;
reg [CNT_W-1:0] a1_cnt;
reg seen_edge; // first in-transaction edge seen
reg a2_open;
reg a2_mosi;
reg a3_open;
reg [CNT_W-1:0] a3_cnt;
reg a3_level;
reg a4_open;
reg [LEN_W:0] a4_edges;
reg a5_open; // from a deassert until the next assert
reg a6_open;
reg [CNT_W-1:0] a6_cnt;
integer p;
always_ff @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
sclk_d <= 1'b0;
cs_n_d <= 1'b1;
mosi_d <= 1'b0;
mosi_dd <= 1'b0;
seen_edge <= 1'b0;
a1_open <= 1'b0; a1_cnt <= {CNT_W{1'b0}};
a2_open <= 1'b0; a2_mosi <= 1'b0;
a3_open <= 1'b0; a3_cnt <= {CNT_W{1'b0}}; a3_level <= 1'b0;
a4_open <= 1'b0; a4_edges <= {(LEN_W+1){1'b0}};
a5_open <= 1'b0;
a6_open <= 1'b0; a6_cnt <= {CNT_W{1'b0}};
for (p = 0; p < NPROPS; p = p + 1) begin
attempts[p] <= {CNT_W{1'b0}};
vacuous[p] <= {CNT_W{1'b0}};
passes[p] <= {CNT_W{1'b0}};
fails[p] <= {CNT_W{1'b0}};
incomplete[p] <= {CNT_W{1'b0}};
end
end else begin
sclk_d <= sclk;
cs_n_d <= cs_n;
mosi_dd <= mosi_d;
mosi_d <= mosi;
if (clr) begin
for (p = 0; p < NPROPS; p = p + 1) begin
attempts[p] <= {CNT_W{1'b0}};
vacuous[p] <= {CNT_W{1'b0}};
passes[p] <= {CNT_W{1'b0}};
fails[p] <= {CNT_W{1'b0}};
incomplete[p] <= {CNT_W{1'b0}};
end
end
// =============================================================
// P1 EDGE_AFTER_SELECT -- bounded existence.
//
// cs_assert |-> ##[1:MAXLEAD] (sclk_edge) before cs_deassert
//
// Three ways to settle, and all three have to be written: the edge arrives
// (pass), the select is released first (fail), or the bound expires (fail).
// A version with only the first two never terminates on a master that holds
// the select open forever -- which is exactly the shape that shows up as
// INCOMPLETE rather than as a failure.
// =============================================================
if (cs_assert) begin
attempts[P_EDGE] <= attempts[P_EDGE] + 1'b1;
a1_open <= 1'b1;
a1_cnt <= {CNT_W{1'b0}};
end else if (cs_n & ~cs_deassert) begin
// deselected and not the deassert cycle: the antecedent did not match
vacuous[P_EDGE] <= vacuous[P_EDGE] + 1'b1;
end
if (a1_open && !cs_assert) begin
if (sclk_edge && in_txn) begin
passes[P_EDGE] <= passes[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else if (cs_deassert) begin
fails[P_EDGE] <= fails[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else if (a1_cnt + 1'b1 >= MAXLEAD[CNT_W-1:0]) begin
fails[P_EDGE] <= fails[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else begin
a1_cnt <= a1_cnt + 1'b1;
end
end
// =============================================================
// P2 STABLE_AT_CAPTURE -- a stability WINDOW around an instant.
//
// (capture && in_txn) |-> ($stable(mosi) at -1, 0 and +1)
//
// The cycle BEFORE is checked immediately from the delayed copy; the cycle
// AFTER needs an attempt that stays open for one cycle, which is why even a
// property this small is temporal.
// =============================================================
if (capture && in_txn) begin
attempts[P_STABLE] <= attempts[P_STABLE] + 1'b1;
if (mosi !== mosi_d) begin
fails[P_STABLE] <= fails[P_STABLE] + 1'b1;
end else begin
a2_open <= 1'b1;
a2_mosi <= mosi;
end
end else if (in_txn) begin
vacuous[P_STABLE] <= vacuous[P_STABLE] + 1'b1;
end
if (a2_open && !(capture && in_txn)) begin
if (mosi !== a2_mosi) fails[P_STABLE] <= fails[P_STABLE] + 1'b1;
else passes[P_STABLE] <= passes[P_STABLE] + 1'b1;
a2_open <= 1'b0;
end
// =============================================================
// P3 HALF_STABLE -- a multi-cycle consequent.
//
// (sclk_edge && in_txn) |=> sclk stays put for HALF-1 cycles
//
// Note the non-overlapping implication: the obligation starts on the cycle
// AFTER the edge, because the edge itself is the change. Writing this with an
// overlapping `|->` makes every attempt fail immediately, which looks like a
// catastrophic design bug and is a misplaced operator.
// =============================================================
if (sclk_edge && in_txn) begin
attempts[P_HALF] <= attempts[P_HALF] + 1'b1;
// An edge while an attempt is open IS the failure of that attempt.
if (a3_open) fails[P_HALF] <= fails[P_HALF] + 1'b1;
a3_open <= 1'b1;
a3_cnt <= {CNT_W{1'b0}};
a3_level <= sclk;
end else if (in_txn) begin
vacuous[P_HALF] <= vacuous[P_HALF] + 1'b1;
end
if (a3_open && !(sclk_edge && in_txn)) begin
if (sclk !== a3_level) begin
fails[P_HALF] <= fails[P_HALF] + 1'b1;
a3_open <= 1'b0;
end else if (a3_cnt + 2'd2 >= HALF[CNT_W-1:0]) begin
passes[P_HALF] <= passes[P_HALF] + 1'b1;
a3_open <= 1'b0;
end else begin
a3_cnt <= a3_cnt + 1'b1;
end
end
// =============================================================
// P4 FRAME_COMPLETE -- a count settled by a terminating event.
//
// first_edge |-> (2N edges counted) before cs_deassert
//
// Anchored to the FIRST EDGE, not to the select. See the header: with the
// select as the antecedent, an empty select pulse fails P1 and P4 together
// and neither report names the cause.
// =============================================================
if (sclk_edge && in_txn && !seen_edge) begin
seen_edge <= 1'b1;
attempts[P_FRAME] <= attempts[P_FRAME] + 1'b1;
a4_open <= 1'b1;
a4_edges <= {{LEN_W{1'b0}}, 1'b1};
end else if (sclk_edge && in_txn && a4_open) begin
a4_edges <= a4_edges + 1'b1;
end else if (cs_n & ~cs_deassert) begin
vacuous[P_FRAME] <= vacuous[P_FRAME] + 1'b1;
end
if (cs_deassert) begin
seen_edge <= 1'b0;
if (a4_open) begin
// The count AS IT WILL BE once this cycle's edge is folded in --
// Chapter 16.1's lesson, and it is the difference between a checker
// that works on a prompt master and one that reports a partial frame
// for a master with no fault.
if (((sclk_edge && in_txn) ? a4_edges + 1'b1 : a4_edges) == edges_per_frame)
passes[P_FRAME] <= passes[P_FRAME] + 1'b1;
else
fails[P_FRAME] <= fails[P_FRAME] + 1'b1;
a4_open <= 1'b0;
end
end
// =============================================================
// P5 SCLK_PARKED -- stability over an UNBOUNDED interval.
//
// cs_deassert |-> (sclk == cpol) until_ cs_assert
//
// There is no bound here and there should not be: the obligation lasts as
// long as the bus is idle. Which means this attempt can be OPEN when the
// simulation ends, and `flush` is what makes that visible instead of free.
// =============================================================
if (cs_deassert) begin
attempts[P_PARKED] <= attempts[P_PARKED] + 1'b1;
a5_open <= 1'b1;
if (sclk !== cpol) begin
fails[P_PARKED] <= fails[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end
end else if (~cs_n) begin
vacuous[P_PARKED] <= vacuous[P_PARKED] + 1'b1;
end
if (a5_open && !cs_deassert) begin
if (cs_assert) begin
passes[P_PARKED] <= passes[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end else if (sclk !== cpol) begin
fails[P_PARKED] <= fails[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end
end
// =============================================================
// P6 RELEASE_AFTER_FRAME -- bounded liveness, the other direction.
//
// frame_complete |-> ##[1:MAXLAG] cs_deassert
//
// P1 asks that something start; this asks that something END. The two are
// the same shape and they catch opposite faults, and a suite with only the
// first kind cannot see a master that never lets go.
// =============================================================
if (a4_open && sclk_edge && in_txn &&
(a4_edges + 1'b1 == edges_per_frame) && !cs_deassert) begin
attempts[P_REL] <= attempts[P_REL] + 1'b1;
a6_open <= 1'b1;
a6_cnt <= {CNT_W{1'b0}};
end
if (a6_open) begin
if (cs_deassert) begin
passes[P_REL] <= passes[P_REL] + 1'b1;
a6_open <= 1'b0;
end else if (a6_cnt + 1'b1 >= MAXLAG[CNT_W-1:0]) begin
fails[P_REL] <= fails[P_REL] + 1'b1;
a6_open <= 1'b0;
end else begin
a6_cnt <= a6_cnt + 1'b1;
end
end
// =============================================================
// P7 ONE_BIT_FRAME -- a property this suite never attempts.
//
// (cs_assert && len == 1) |-> ...
//
// It is correct, it is reachable in principle, and no traffic in this bench
// has a one-bit frame. So `attempts` stays at zero while `vacuous` climbs,
// and its zero failure count is a fact about the STIMULUS. A report that
// shows only pass/fail cannot tell this property from P1.
// =============================================================
if (cs_assert && (len == {{(LEN_W-1){1'b0}}, 1'b1})) begin
attempts[P_ONEBIT] <= attempts[P_ONEBIT] + 1'b1;
passes[P_ONEBIT] <= passes[P_ONEBIT] + 1'b1;
end else if (cs_assert) begin
vacuous[P_ONEBIT] <= vacuous[P_ONEBIT] + 1'b1;
end
// =============================================================
// FLUSH -- book every open attempt as INCOMPLETE.
// =============================================================
if (flush) begin
if (a1_open) begin incomplete[P_EDGE] <= incomplete[P_EDGE] + 1'b1; a1_open <= 1'b0; end
if (a2_open) begin incomplete[P_STABLE] <= incomplete[P_STABLE] + 1'b1; a2_open <= 1'b0; end
if (a3_open) begin incomplete[P_HALF] <= incomplete[P_HALF] + 1'b1; a3_open <= 1'b0; end
if (a4_open) begin incomplete[P_FRAME] <= incomplete[P_FRAME] + 1'b1; a4_open <= 1'b0; end
if (a5_open) begin incomplete[P_PARKED] <= incomplete[P_PARKED] + 1'b1; a5_open <= 1'b0; end
if (a6_open) begin incomplete[P_REL] <= incomplete[P_REL] + 1'b1; a6_open <= 1'b0; end
end
end
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_props.v — the same design in Verilog-2001
// spi_props.v
//
// Chapter 17.1 -- SPI protocol properties, and the four outcomes of a property attempt.
//
// WHY THIS IS NOT CHAPTER 16.1 AGAIN.
//
// Chapter 16.1's eight rules were decided at single instants: is SCLK at its idle level on
// this cycle, is this interval long enough, did MOSI move at this edge. A property is a
// different kind of statement. It opens at one instant and is settled at another, and
// between those two instants it is OPEN -- neither true nor false yet.
//
// That is what makes an assertion language worth having and it is also where its failure
// modes live. A property attempt has FOUR outcomes, not two:
//
// PASSED the antecedent matched and the consequent was satisfied
// FAILED the antecedent matched and the consequent was not
// VACUOUS the property was evaluated and the antecedent did not match, so
// nothing was checked. SVA reports this as a pass.
// INCOMPLETE the antecedent matched, the attempt is still open, and the
// simulation ended. Neither true nor false, and counted as neither.
//
// Most suites collapse all four into "did anything print". This module counts them
// separately, because the two that are not failures are where the silence comes from:
//
// vacuous == attempts the property has NEVER been tested. Its zero failure count
// is a statement about the stimulus, not about the design.
// incomplete > 0 the test ended mid-obligation. A design that was ABOUT to
// violate the property is indistinguishable from one that
// would have satisfied it, and the report says nothing.
//
// SEVEN PROPERTIES, chosen so that each one needs a different temporal shape.
//
// P1 EDGE_AFTER_SELECT bounded existence: an assert must be followed by an SCLK edge
// within MAXLEAD cycles, and before the deassert.
// P2 STABLE_AT_CAPTURE a stability window: MOSI must not move in the cycle before, at,
// or after a capture edge.
// P3 HALF_STABLE a multi-cycle consequent: after an edge, SCLK holds for HALF-1
// further cycles.
// P4 FRAME_COMPLETE a count settled by a terminating event: from the first edge,
// 2N edges must be seen before the deassert.
// P5 SCLK_PARKED stability over an UNBOUNDED interval, terminated by an event:
// from the deassert until the next assert, SCLK stays at CPOL.
// P6 RELEASE_AFTER_FRAME bounded liveness the other way: once the frame is complete, the
// select must be released within MAXLAG cycles.
// P7 ONE_BIT_FRAME a property whose antecedent this suite never produces. It is
// here to be measured, not to be satisfied.
//
// AND THE ANTECEDENTS ARE CHOSEN SO THE VIOLATION MATRIX CAN BE DIAGONAL.
//
// P4's antecedent is the FIRST EDGE rather than the assert, and that is not cosmetic. With
// the assert as the antecedent, a select pulse carrying no edges at all fails both P1 and
// P4 -- one fault, two reports, and neither of them says "there were no edges". Anchored to
// the first edge, P4 is not attempted at all when there are no edges, and P1's report
// stands alone.
//
// Choosing an antecedent is therefore part of designing a DIAGNOSIS, not just part of
// writing a check.
`timescale 1ns/1ps
module spi_props #(
parameter HALF = 3, // cycles per SCLK half period
parameter MAXLEAD = 16, // P1's bound: assert to first edge
parameter MAXLAG = 8, // P6's bound: frame complete to release
parameter LEN_W = 6,
parameter CNT_W = 16,
parameter NPROPS = 7
) (
input wire clk,
input wire rst_n,
// --- the pins ----------------------------------------------------------
input wire sclk,
input wire cs_n,
input wire mosi,
// --- the configuration -------------------------------------------------
input wire cpol,
input wire cpha,
input wire [LEN_W-1:0] len,
input wire clr,
// Closes every open attempt and books it as INCOMPLETE. A test that does not do
// this at its end is a test whose open attempts vanish, which is the failure this
// whole module exists to make visible.
input wire flush,
output wire [NPROPS*CNT_W-1:0] attempts_flat,
output wire [NPROPS*CNT_W-1:0] vacuous_flat,
output wire [NPROPS*CNT_W-1:0] passes_flat,
output wire [NPROPS*CNT_W-1:0] fails_flat,
output wire [NPROPS*CNT_W-1:0] incomplete_flat
);
localparam P_EDGE = 0,
P_STABLE = 1,
P_HALF = 2,
P_FRAME = 3,
P_PARKED = 4,
P_REL = 5,
P_ONEBIT = 6;
// --- observed history ---------------------------------------------------
reg sclk_d, cs_n_d, mosi_d, mosi_dd;
wire cs_assert = ~cs_n & cs_n_d;
wire cs_deassert = cs_n & ~cs_n_d;
wire in_txn = ~cs_n | cs_deassert;
wire sclk_edge = sclk ^ sclk_d;
wire leading = sclk_edge & (sclk != cpol);
wire trailing = sclk_edge & (sclk == cpol);
wire capture = cpha ? trailing : leading;
wire [LEN_W:0] edges_per_frame = {1'b0, len} << 1;
reg [CNT_W-1:0] attempts [0:NPROPS-1];
reg [CNT_W-1:0] vacuous [0:NPROPS-1];
reg [CNT_W-1:0] passes [0:NPROPS-1];
reg [CNT_W-1:0] fails [0:NPROPS-1];
reg [CNT_W-1:0] incomplete [0:NPROPS-1];
genvar gi;
generate
for (gi = 0; gi < NPROPS; gi = gi + 1) begin : g_flat
assign attempts_flat [gi*CNT_W +: CNT_W] = attempts[gi];
assign vacuous_flat [gi*CNT_W +: CNT_W] = vacuous[gi];
assign passes_flat [gi*CNT_W +: CNT_W] = passes[gi];
assign fails_flat [gi*CNT_W +: CNT_W] = fails[gi];
assign incomplete_flat[gi*CNT_W +: CNT_W] = incomplete[gi];
end
endgenerate
// --- attempt state, one set per property --------------------------------
// Every property here has at most one attempt open at a time, which is a property of
// these antecedents rather than a limitation: each is anchored to an event that cannot
// recur while its own attempt is open. An antecedent that CAN recur needs a queue of
// attempts, and SVA maintains exactly that -- which is why a property with a level
// antecedent can report hundreds of failures for one fault. Chapter 17.2 measures it.
reg a1_open;
reg [CNT_W-1:0] a1_cnt;
reg seen_edge; // first in-transaction edge seen
reg a2_open;
reg a2_mosi;
reg a3_open;
reg [CNT_W-1:0] a3_cnt;
reg a3_level;
reg a4_open;
reg [LEN_W:0] a4_edges;
reg a5_open; // from a deassert until the next assert
reg a6_open;
reg [CNT_W-1:0] a6_cnt;
integer p;
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
sclk_d <= 1'b0;
cs_n_d <= 1'b1;
mosi_d <= 1'b0;
mosi_dd <= 1'b0;
seen_edge <= 1'b0;
a1_open <= 1'b0; a1_cnt <= {CNT_W{1'b0}};
a2_open <= 1'b0; a2_mosi <= 1'b0;
a3_open <= 1'b0; a3_cnt <= {CNT_W{1'b0}}; a3_level <= 1'b0;
a4_open <= 1'b0; a4_edges <= {(LEN_W+1){1'b0}};
a5_open <= 1'b0;
a6_open <= 1'b0; a6_cnt <= {CNT_W{1'b0}};
for (p = 0; p < NPROPS; p = p + 1) begin
attempts[p] <= {CNT_W{1'b0}};
vacuous[p] <= {CNT_W{1'b0}};
passes[p] <= {CNT_W{1'b0}};
fails[p] <= {CNT_W{1'b0}};
incomplete[p] <= {CNT_W{1'b0}};
end
end else begin
sclk_d <= sclk;
cs_n_d <= cs_n;
mosi_dd <= mosi_d;
mosi_d <= mosi;
if (clr) begin
for (p = 0; p < NPROPS; p = p + 1) begin
attempts[p] <= {CNT_W{1'b0}};
vacuous[p] <= {CNT_W{1'b0}};
passes[p] <= {CNT_W{1'b0}};
fails[p] <= {CNT_W{1'b0}};
incomplete[p] <= {CNT_W{1'b0}};
end
end
// =============================================================
// P1 EDGE_AFTER_SELECT -- bounded existence.
//
// cs_assert |-> ##[1:MAXLEAD] (sclk_edge) before cs_deassert
//
// Three ways to settle, and all three have to be written: the edge arrives
// (pass), the select is released first (fail), or the bound expires (fail).
// A version with only the first two never terminates on a master that holds
// the select open forever -- which is exactly the shape that shows up as
// INCOMPLETE rather than as a failure.
// =============================================================
if (cs_assert) begin
attempts[P_EDGE] <= attempts[P_EDGE] + 1'b1;
a1_open <= 1'b1;
a1_cnt <= {CNT_W{1'b0}};
end else if (cs_n & ~cs_deassert) begin
// deselected and not the deassert cycle: the antecedent did not match
vacuous[P_EDGE] <= vacuous[P_EDGE] + 1'b1;
end
if (a1_open && !cs_assert) begin
if (sclk_edge && in_txn) begin
passes[P_EDGE] <= passes[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else if (cs_deassert) begin
fails[P_EDGE] <= fails[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else if (a1_cnt + 1'b1 >= MAXLEAD[CNT_W-1:0]) begin
fails[P_EDGE] <= fails[P_EDGE] + 1'b1;
a1_open <= 1'b0;
end else begin
a1_cnt <= a1_cnt + 1'b1;
end
end
// =============================================================
// P2 STABLE_AT_CAPTURE -- a stability WINDOW around an instant.
//
// (capture && in_txn) |-> ($stable(mosi) at -1, 0 and +1)
//
// The cycle BEFORE is checked immediately from the delayed copy; the cycle
// AFTER needs an attempt that stays open for one cycle, which is why even a
// property this small is temporal.
// =============================================================
if (capture && in_txn) begin
attempts[P_STABLE] <= attempts[P_STABLE] + 1'b1;
if (mosi !== mosi_d) begin
fails[P_STABLE] <= fails[P_STABLE] + 1'b1;
end else begin
a2_open <= 1'b1;
a2_mosi <= mosi;
end
end else if (in_txn) begin
vacuous[P_STABLE] <= vacuous[P_STABLE] + 1'b1;
end
if (a2_open && !(capture && in_txn)) begin
if (mosi !== a2_mosi) fails[P_STABLE] <= fails[P_STABLE] + 1'b1;
else passes[P_STABLE] <= passes[P_STABLE] + 1'b1;
a2_open <= 1'b0;
end
// =============================================================
// P3 HALF_STABLE -- a multi-cycle consequent.
//
// (sclk_edge && in_txn) |=> sclk stays put for HALF-1 cycles
//
// Note the non-overlapping implication: the obligation starts on the cycle
// AFTER the edge, because the edge itself is the change. Writing this with an
// overlapping `|->` makes every attempt fail immediately, which looks like a
// catastrophic design bug and is a misplaced operator.
// =============================================================
if (sclk_edge && in_txn) begin
attempts[P_HALF] <= attempts[P_HALF] + 1'b1;
// An edge while an attempt is open IS the failure of that attempt.
if (a3_open) fails[P_HALF] <= fails[P_HALF] + 1'b1;
a3_open <= 1'b1;
a3_cnt <= {CNT_W{1'b0}};
a3_level <= sclk;
end else if (in_txn) begin
vacuous[P_HALF] <= vacuous[P_HALF] + 1'b1;
end
if (a3_open && !(sclk_edge && in_txn)) begin
if (sclk !== a3_level) begin
fails[P_HALF] <= fails[P_HALF] + 1'b1;
a3_open <= 1'b0;
end else if (a3_cnt + 2'd2 >= HALF[CNT_W-1:0]) begin
passes[P_HALF] <= passes[P_HALF] + 1'b1;
a3_open <= 1'b0;
end else begin
a3_cnt <= a3_cnt + 1'b1;
end
end
// =============================================================
// P4 FRAME_COMPLETE -- a count settled by a terminating event.
//
// first_edge |-> (2N edges counted) before cs_deassert
//
// Anchored to the FIRST EDGE, not to the select. See the header: with the
// select as the antecedent, an empty select pulse fails P1 and P4 together
// and neither report names the cause.
// =============================================================
if (sclk_edge && in_txn && !seen_edge) begin
seen_edge <= 1'b1;
attempts[P_FRAME] <= attempts[P_FRAME] + 1'b1;
a4_open <= 1'b1;
a4_edges <= {{LEN_W{1'b0}}, 1'b1};
end else if (sclk_edge && in_txn && a4_open) begin
a4_edges <= a4_edges + 1'b1;
end else if (cs_n & ~cs_deassert) begin
vacuous[P_FRAME] <= vacuous[P_FRAME] + 1'b1;
end
if (cs_deassert) begin
seen_edge <= 1'b0;
if (a4_open) begin
// The count AS IT WILL BE once this cycle's edge is folded in --
// Chapter 16.1's lesson, and it is the difference between a checker
// that works on a prompt master and one that reports a partial frame
// for a master with no fault.
if (((sclk_edge && in_txn) ? a4_edges + 1'b1 : a4_edges) == edges_per_frame)
passes[P_FRAME] <= passes[P_FRAME] + 1'b1;
else
fails[P_FRAME] <= fails[P_FRAME] + 1'b1;
a4_open <= 1'b0;
end
end
// =============================================================
// P5 SCLK_PARKED -- stability over an UNBOUNDED interval.
//
// cs_deassert |-> (sclk == cpol) until_ cs_assert
//
// There is no bound here and there should not be: the obligation lasts as
// long as the bus is idle. Which means this attempt can be OPEN when the
// simulation ends, and `flush` is what makes that visible instead of free.
// =============================================================
if (cs_deassert) begin
attempts[P_PARKED] <= attempts[P_PARKED] + 1'b1;
a5_open <= 1'b1;
if (sclk !== cpol) begin
fails[P_PARKED] <= fails[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end
end else if (~cs_n) begin
vacuous[P_PARKED] <= vacuous[P_PARKED] + 1'b1;
end
if (a5_open && !cs_deassert) begin
if (cs_assert) begin
passes[P_PARKED] <= passes[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end else if (sclk !== cpol) begin
fails[P_PARKED] <= fails[P_PARKED] + 1'b1;
a5_open <= 1'b0;
end
end
// =============================================================
// P6 RELEASE_AFTER_FRAME -- bounded liveness, the other direction.
//
// frame_complete |-> ##[1:MAXLAG] cs_deassert
//
// P1 asks that something start; this asks that something END. The two are
// the same shape and they catch opposite faults, and a suite with only the
// first kind cannot see a master that never lets go.
// =============================================================
if (a4_open && sclk_edge && in_txn &&
(a4_edges + 1'b1 == edges_per_frame) && !cs_deassert) begin
attempts[P_REL] <= attempts[P_REL] + 1'b1;
a6_open <= 1'b1;
a6_cnt <= {CNT_W{1'b0}};
end
if (a6_open) begin
if (cs_deassert) begin
passes[P_REL] <= passes[P_REL] + 1'b1;
a6_open <= 1'b0;
end else if (a6_cnt + 1'b1 >= MAXLAG[CNT_W-1:0]) begin
fails[P_REL] <= fails[P_REL] + 1'b1;
a6_open <= 1'b0;
end else begin
a6_cnt <= a6_cnt + 1'b1;
end
end
// =============================================================
// P7 ONE_BIT_FRAME -- a property this suite never attempts.
//
// (cs_assert && len == 1) |-> ...
//
// It is correct, it is reachable in principle, and no traffic in this bench
// has a one-bit frame. So `attempts` stays at zero while `vacuous` climbs,
// and its zero failure count is a fact about the STIMULUS. A report that
// shows only pass/fail cannot tell this property from P1.
// =============================================================
if (cs_assert && (len == {{(LEN_W-1){1'b0}}, 1'b1})) begin
attempts[P_ONEBIT] <= attempts[P_ONEBIT] + 1'b1;
passes[P_ONEBIT] <= passes[P_ONEBIT] + 1'b1;
end else if (cs_assert) begin
vacuous[P_ONEBIT] <= vacuous[P_ONEBIT] + 1'b1;
end
// =============================================================
// FLUSH -- book every open attempt as INCOMPLETE.
// =============================================================
if (flush) begin
if (a1_open) begin incomplete[P_EDGE] <= incomplete[P_EDGE] + 1'b1; a1_open <= 1'b0; end
if (a2_open) begin incomplete[P_STABLE] <= incomplete[P_STABLE] + 1'b1; a2_open <= 1'b0; end
if (a3_open) begin incomplete[P_HALF] <= incomplete[P_HALF] + 1'b1; a3_open <= 1'b0; end
if (a4_open) begin incomplete[P_FRAME] <= incomplete[P_FRAME] + 1'b1; a4_open <= 1'b0; end
if (a5_open) begin incomplete[P_PARKED] <= incomplete[P_PARKED] + 1'b1; a5_open <= 1'b0; end
if (a6_open) begin incomplete[P_REL] <= incomplete[P_REL] + 1'b1; a6_open <= 1'b0; end
end
end
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_props.vhd — the same design in VHDL
-- spi_props.vhd
--
-- Chapter 17.1 -- SPI protocol properties, and the four outcomes of a property attempt.
--
-- THIS FILE CARRIES THE SAME SIX OBLIGATIONS TWICE, IN TWO NOTATIONS.
--
-- `spi_props` a procedural engine that counts attempts, vacuous evaluations,
-- passes, failures and INCOMPLETE attempts. It is the version that
-- exists in all three languages and it is what decides the testbench's
-- verdict.
--
-- `spi_props_psl` the same six obligations written as PSL directives, which nvc
-- EXECUTES. These are real assertions, checked by an assertion engine,
-- and the testbench runs them over its legal phase and requires them to
-- stay silent.
--
-- The second one matters because it is the only place in this whole curriculum where an
-- assertion LANGUAGE actually runs. Icarus Verilog implements no SVA at all, so the
-- SystemVerilog property set in this chapter is published as reviewed code -- and PSL, which
-- is the same idea with different keywords, runs here. Reading the two side by side is the
-- closest a reader can get to watching an SVA property behave.
--
-- A PROPERTY ATTEMPT HAS FOUR OUTCOMES, NOT TWO.
--
-- PASSED the antecedent matched and the consequent was satisfied
-- FAILED the antecedent matched and the consequent was not
-- VACUOUS the property was evaluated and the antecedent did not match, so nothing
-- was checked. SVA and PSL both report this as a pass.
-- INCOMPLETE the antecedent matched, the attempt is still open, and the simulation
-- ended. Neither true nor false, and counted as neither.
--
-- The two that are not failures are where a suite's silence comes from:
--
-- vacuous = attempts the property has NEVER been tested. Its zero failure count is a
-- statement about the stimulus, not about the design.
-- incomplete > 0 the test ended mid-obligation, and a design that was about to
-- violate the property is indistinguishable from one that would
-- have satisfied it.
--
-- SEVEN PROPERTIES, each needing a different temporal shape -- bounded existence, a
-- stability window, a multi-cycle consequent, a count settled by a terminating event,
-- stability over an unbounded interval, bounded liveness, and one whose antecedent this
-- suite never produces.
--
-- AND THE ANTECEDENTS ARE CHOSEN SO THE VIOLATION MATRIX CAN BE DIAGONAL. P4's antecedent is
-- the FIRST EDGE rather than the select: with the select as the antecedent, a pulse carrying
-- no edges fails both P1 and P4, and neither report says "there were no edges". Choosing an
-- antecedent is part of designing a DIAGNOSIS.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
package spi_prop_pkg is
constant NPROPS : natural := 7;
constant P_EDGE : natural := 0;
constant P_STABLE : natural := 1;
constant P_HALF : natural := 2;
constant P_FRAME : natural := 3;
constant P_PARKED : natural := 4;
constant P_REL : natural := 5;
constant P_ONEBIT : natural := 6;
type prop_counts_t is record
attempts : natural;
vacuous : natural;
passes : natural;
fails : natural;
incomplete : natural;
end record;
type prop_array_t is array (0 to NPROPS - 1) of prop_counts_t;
constant COUNTS_ZERO : prop_counts_t := (0, 0, 0, 0, 0);
function prop_name (i : natural) return string;
end package spi_prop_pkg;
package body spi_prop_pkg is
function prop_name (i : natural) return string is
begin
case i is
when P_EDGE => return "EDGE_AFTER_SELECT ";
when P_STABLE => return "STABLE_AT_CAPTURE ";
when P_HALF => return "HALF_STABLE ";
when P_FRAME => return "FRAME_COMPLETE ";
when P_PARKED => return "SCLK_PARKED ";
when P_REL => return "RELEASE_AFTER_FRAME";
when others => return "ONE_BIT_FRAME ";
end case;
end function;
end package body spi_prop_pkg;
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.spi_prop_pkg.all;
entity spi_props is
generic (
HALF : natural := 3; -- cycles per SCLK half period
MAXLEAD : natural := 16; -- P1's bound: assert to first edge
MAXLAG : natural := 8; -- P6's bound: frame complete to release
LEN_W : positive := 6
);
port (
clk : in std_logic;
rst_n : in std_logic;
sclk : in std_logic;
cs_n : in std_logic;
mosi : in std_logic;
cpol : in std_logic;
cpha : in std_logic;
len : in unsigned(LEN_W - 1 downto 0);
clr : in std_logic;
-- Closes every open attempt and books it as INCOMPLETE. A test that does not do
-- this at its end is a test whose open attempts vanish.
flush : in std_logic;
counts : out prop_array_t
);
end entity spi_props;
architecture rtl of spi_props is
signal c : prop_array_t := (others => COUNTS_ZERO);
begin
counts <= c;
process (clk, rst_n) is
variable sclk_d, cs_n_d, mosi_d : std_logic;
variable cs_assert, cs_deassert : boolean;
variable in_txn, sclk_edge : boolean;
variable leading, capture : boolean;
variable epf : natural;
variable seen_edge : boolean := false;
variable a1_open : boolean := false;
variable a1_cnt : natural := 0;
variable a2_open : boolean := false;
variable a2_mosi : std_logic := '0';
variable a3_open : boolean := false;
variable a3_cnt : natural := 0;
variable a3_level : std_logic := '0';
variable a4_open : boolean := false;
variable a4_edges : natural := 0;
variable a5_open : boolean := false;
variable a6_open : boolean := false;
variable a6_cnt : natural := 0;
begin
if rst_n = '0' then
sclk_d := '0'; cs_n_d := '1'; mosi_d := '0';
seen_edge := false;
a1_open := false; a1_cnt := 0;
a2_open := false; a2_mosi := '0';
a3_open := false; a3_cnt := 0; a3_level := '0';
a4_open := false; a4_edges := 0;
a5_open := false;
a6_open := false; a6_cnt := 0;
c <= (others => COUNTS_ZERO);
elsif rising_edge(clk) then
cs_assert := (cs_n = '0') and (cs_n_d = '1');
cs_deassert := (cs_n = '1') and (cs_n_d = '0');
in_txn := (cs_n = '0') or cs_deassert;
sclk_edge := (sclk /= sclk_d);
leading := sclk_edge and (sclk /= cpol);
if cpha = '0' then capture := leading;
else capture := sclk_edge and not leading;
end if;
epf := 2 * to_integer(len);
if clr = '1' then
c <= (others => COUNTS_ZERO);
end if;
-- ==========================================================
-- P1 EDGE_AFTER_SELECT -- bounded existence.
--
-- cs_assert |-> ##[1:MAXLEAD] sclk_edge, before cs_deassert
--
-- Three ways to settle, and all three have to be written: the edge arrives
-- (pass), the select is released first (fail), or the bound expires (fail). A
-- version with only the first two never terminates on a master that holds the
-- select open -- which shows up as INCOMPLETE rather than as a failure.
-- ==========================================================
if cs_assert then
c(P_EDGE).attempts <= c(P_EDGE).attempts + 1;
a1_open := true;
a1_cnt := 0;
elsif (cs_n = '1') and not cs_deassert then
c(P_EDGE).vacuous <= c(P_EDGE).vacuous + 1;
end if;
if a1_open and not cs_assert then
if sclk_edge and in_txn then
c(P_EDGE).passes <= c(P_EDGE).passes + 1;
a1_open := false;
elsif cs_deassert then
c(P_EDGE).fails <= c(P_EDGE).fails + 1;
a1_open := false;
elsif a1_cnt + 1 >= MAXLEAD then
c(P_EDGE).fails <= c(P_EDGE).fails + 1;
a1_open := false;
else
a1_cnt := a1_cnt + 1;
end if;
end if;
-- ==========================================================
-- P2 STABLE_AT_CAPTURE -- a stability WINDOW around an instant.
--
-- The cycle BEFORE is checked immediately from the delayed copy; the cycle
-- AFTER needs an attempt that stays open for one cycle, which is why even a
-- property this small is temporal.
-- ==========================================================
if capture and in_txn then
c(P_STABLE).attempts <= c(P_STABLE).attempts + 1;
if mosi /= mosi_d then
c(P_STABLE).fails <= c(P_STABLE).fails + 1;
else
a2_open := true;
a2_mosi := mosi;
end if;
elsif in_txn then
c(P_STABLE).vacuous <= c(P_STABLE).vacuous + 1;
end if;
if a2_open and not (capture and in_txn) then
if mosi /= a2_mosi then c(P_STABLE).fails <= c(P_STABLE).fails + 1;
else c(P_STABLE).passes <= c(P_STABLE).passes + 1;
end if;
a2_open := false;
end if;
-- ==========================================================
-- P3 HALF_STABLE -- a multi-cycle consequent.
--
-- (sclk_edge && in_txn) |=> sclk stays put for HALF-1 cycles
--
-- Note the NON-OVERLAPPING implication: the obligation starts on the cycle
-- after the edge, because the edge itself is the change. Written with an
-- overlapping implication, every attempt fails immediately -- which looks like
-- a catastrophic design bug and is a misplaced operator.
-- ==========================================================
if sclk_edge and in_txn then
c(P_HALF).attempts <= c(P_HALF).attempts + 1;
if a3_open then
c(P_HALF).fails <= c(P_HALF).fails + 1;
end if;
a3_open := true;
a3_cnt := 0;
a3_level := sclk;
elsif in_txn then
c(P_HALF).vacuous <= c(P_HALF).vacuous + 1;
end if;
if a3_open and not (sclk_edge and in_txn) then
if sclk /= a3_level then
c(P_HALF).fails <= c(P_HALF).fails + 1;
a3_open := false;
elsif a3_cnt + 2 >= HALF then
c(P_HALF).passes <= c(P_HALF).passes + 1;
a3_open := false;
else
a3_cnt := a3_cnt + 1;
end if;
end if;
-- ==========================================================
-- P4 FRAME_COMPLETE -- a count settled by a terminating event.
--
-- Anchored to the FIRST EDGE, not to the select: see the header.
-- ==========================================================
if sclk_edge and in_txn and not seen_edge then
seen_edge := true;
c(P_FRAME).attempts <= c(P_FRAME).attempts + 1;
a4_open := true;
a4_edges := 1;
elsif sclk_edge and in_txn and a4_open then
a4_edges := a4_edges + 1;
elsif (cs_n = '1') and not cs_deassert then
c(P_FRAME).vacuous <= c(P_FRAME).vacuous + 1;
end if;
-- P6's antecedent is "the frame has just become complete", which is evaluated
-- here because it depends on the same count.
if a4_open and sclk_edge and in_txn and (a4_edges = epf) and not cs_deassert then
c(P_REL).attempts <= c(P_REL).attempts + 1;
a6_open := true;
a6_cnt := 0;
end if;
if cs_deassert then
seen_edge := false;
if a4_open then
if a4_edges = epf then
c(P_FRAME).passes <= c(P_FRAME).passes + 1;
else
c(P_FRAME).fails <= c(P_FRAME).fails + 1;
end if;
a4_open := false;
end if;
end if;
-- ==========================================================
-- P5 SCLK_PARKED -- stability over an UNBOUNDED interval.
--
-- cs_deassert |-> (sclk = cpol) until_ cs_assert
--
-- There is no bound and there should not be: the obligation lasts as long as
-- the bus is idle. Which means the attempt can be OPEN when the simulation
-- ends, and `flush` is what makes that visible instead of free.
-- ==========================================================
if cs_deassert then
c(P_PARKED).attempts <= c(P_PARKED).attempts + 1;
a5_open := true;
if sclk /= cpol then
c(P_PARKED).fails <= c(P_PARKED).fails + 1;
a5_open := false;
end if;
elsif cs_n = '0' then
c(P_PARKED).vacuous <= c(P_PARKED).vacuous + 1;
end if;
if a5_open and not cs_deassert then
if cs_assert then
c(P_PARKED).passes <= c(P_PARKED).passes + 1;
a5_open := false;
elsif sclk /= cpol then
c(P_PARKED).fails <= c(P_PARKED).fails + 1;
a5_open := false;
end if;
end if;
-- ==========================================================
-- P6 RELEASE_AFTER_FRAME -- bounded liveness, the other direction.
--
-- P1 asks that something START; this asks that something END. The two are the
-- same shape and catch opposite faults, and a suite with only the first kind
-- cannot see a master that never lets go.
-- ==========================================================
if a6_open then
if cs_deassert then
c(P_REL).passes <= c(P_REL).passes + 1;
a6_open := false;
elsif a6_cnt + 1 >= MAXLAG then
c(P_REL).fails <= c(P_REL).fails + 1;
a6_open := false;
else
a6_cnt := a6_cnt + 1;
end if;
end if;
-- ==========================================================
-- P7 ONE_BIT_FRAME -- a property this suite never attempts.
--
-- It is correct, reachable in principle, and no traffic here has a one-bit
-- frame. So `attempts` stays at zero while `vacuous` climbs, and its zero
-- failure count is a fact about the STIMULUS.
-- ==========================================================
if cs_assert and (len = to_unsigned(1, LEN_W)) then
c(P_ONEBIT).attempts <= c(P_ONEBIT).attempts + 1;
c(P_ONEBIT).passes <= c(P_ONEBIT).passes + 1;
elsif cs_assert then
c(P_ONEBIT).vacuous <= c(P_ONEBIT).vacuous + 1;
end if;
-- ==========================================================
-- FLUSH -- book every open attempt as INCOMPLETE.
-- ==========================================================
if flush = '1' then
if a1_open then c(P_EDGE).incomplete <= c(P_EDGE).incomplete + 1; a1_open := false; end if;
if a2_open then c(P_STABLE).incomplete <= c(P_STABLE).incomplete + 1; a2_open := false; end if;
if a3_open then c(P_HALF).incomplete <= c(P_HALF).incomplete + 1; a3_open := false; end if;
if a4_open then c(P_FRAME).incomplete <= c(P_FRAME).incomplete + 1; a4_open := false; end if;
if a5_open then c(P_PARKED).incomplete <= c(P_PARKED).incomplete + 1; a5_open := false; end if;
if a6_open then c(P_REL).incomplete <= c(P_REL).incomplete + 1; a6_open := false; end if;
end if;
sclk_d := sclk;
cs_n_d := cs_n;
mosi_d := mosi;
end if;
end process;
end architecture rtl;
-- =====================================================================================
-- THE SAME SIX OBLIGATIONS AS PSL, AND THESE ONES ARE EXECUTED BY AN ASSERTION ENGINE.
-- =====================================================================================
--
-- Everything above is procedural: explicit attempt state, explicit counters, and a verdict
-- computed by the testbench. Everything below is DECLARATIVE -- nvc's PSL engine opens and
-- settles the attempts, and a failure prints with a label and a timestamp.
--
-- FOUR THINGS TO NOTICE WHEN READING THEM NEXT TO EACH OTHER.
--
-- 1. THE DERIVED EVENTS STILL HAVE TO BE COMPUTED SOMEWHERE. `cs_assert`, `sclk_edge`,
-- `capture` and `frame_complete` are ordinary VHDL signals below, and the PSL
-- directives reference them. An assertion language removes the attempt bookkeeping; it
-- does not remove the modelling. Where those signals are computed decides what the
-- properties can say, and a property set built on a badly chosen derived signal is
-- wrong in a way no amount of temporal-operator care can fix.
--
-- 2. A DECLARATIVE ASSERTION CANNOT BE SWITCHED OFF FROM OUTSIDE, so it gets its own
-- simulation. The first version of this file gated every property on an `en` signal that
-- the testbench raised over its legal phase and dropped before crafting violations. It
-- did not work, and the reason is worth knowing: an attempt OPENED while the gate was up
-- outlives the gate falling. P5's obligation is unbounded, P4's and P6's SEREs span tens
-- of cycles, and all three were still in flight when the violation phase began -- so they
-- fired on traffic they had been switched off for, at times that looked unrelated to
-- anything.
--
-- Putting the gate in the TERMINATION condition as well as the antecedent fixes P5 and
-- not the SEREs. The honest structure is a separate top level: `spi_psl_tb` in the
-- testbench file drives legal traffic only, and the regression requires it to produce no
-- assertion output before its legal phase ends. Gating a declarative property with a
-- signal is a smell in general -- if a property should not hold, it should not be armed,
-- and "armed" is a property of the simulation rather than of a cycle.
--
-- 3. THE `cover` DIRECTIVES ARE THE `attempts` COUNTERS. PSL `cover` fires a note when
-- its sequence is matched, so a cover directive that never fires is the assertion-
-- language spelling of `attempts = 0`. C_ONEBIT below is expected to stay silent for
-- the whole run, and that silence is the point: it is the same vacuity the procedural
-- engine reports as a number.
--
-- 4. WHAT PSL WILL NOT TELL YOU IS `incomplete`. An attempt still open when the
-- simulation ends prints nothing, in PSL and in SVA alike. The procedural engine's
-- fifth column has no declarative equivalent here, which is the one place the verbose
-- version is strictly more informative than the concise one.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity spi_props_psl is
generic (
HALF : natural := 3;
MAXLEAD : natural := 16;
MAXLAG : natural := 8;
LEN_W : positive := 6
);
port (
clk : in std_logic;
sclk : in std_logic;
cs_n : in std_logic;
mosi : in std_logic;
cpol : in std_logic;
cpha : in std_logic;
len : in unsigned(LEN_W - 1 downto 0)
);
end entity spi_props_psl;
architecture psl of spi_props_psl is
signal sclk_d, cs_n_d, mosi_d : std_logic := '0';
signal cs_assert : std_logic := '0';
signal cs_deassert : std_logic := '0';
signal in_txn : std_logic := '0';
signal sclk_edge : std_logic := '0';
signal edge_in_txn : std_logic := '0';
signal cap_in_txn : std_logic := '0';
signal first_edge : std_logic := '0';
signal frame_done : std_logic := '0'; -- the count has just reached 2N
signal frame_ok : std_logic := '0'; -- ... and it is 2N at this deassert
signal sclk_held : std_logic := '0'; -- sclk equals its previous value
signal seen_edge : std_logic := '0';
signal edge_count : natural := 0;
begin
-- The derived events. Registered copies first, then the combinational events, exactly
-- as the procedural engine computes them -- which is the point of item 1 above.
hist : process (clk) is
begin
if rising_edge(clk) then
sclk_d <= sclk;
cs_n_d <= cs_n;
mosi_d <= mosi;
if cs_n = '1' and cs_n_d = '0' then
seen_edge <= '0';
edge_count <= 0;
elsif (sclk /= sclk_d) and ((cs_n = '0') or (cs_n = '1' and cs_n_d = '0')) then
seen_edge <= '1';
edge_count <= edge_count + 1;
end if;
end if;
end process hist;
cs_assert <= '1' when cs_n = '0' and cs_n_d = '1' else '0';
cs_deassert <= '1' when cs_n = '1' and cs_n_d = '0' else '0';
in_txn <= '1' when cs_n = '0' or cs_deassert = '1' else '0';
sclk_edge <= '1' when sclk /= sclk_d else '0';
edge_in_txn <= sclk_edge and in_txn;
sclk_held <= '1' when sclk = sclk_d else '0';
cap_in_txn <= edge_in_txn when (cpha = '0' and sclk /= cpol) or (cpha = '1' and sclk = cpol)
else '0';
first_edge <= edge_in_txn and not seen_edge;
frame_done <= '1' when edge_in_txn = '1' and (edge_count + 1 = 2 * to_integer(len))
else '0';
frame_ok <= '1' when cs_deassert = '1' and (edge_count = 2 * to_integer(len))
else '0';
-- psl default clock is rising_edge(clk);
--
-- THESE ARE THE DIRECTIVES THAT WERE MEASURED SILENT ON LEGAL TRAFFIC. That sentence is
-- the most useful one in this file, because the first version of this property set was
-- not: it used SERE forms -- `{a} |=> {b[*0 to N]; c}` -- and every one of them fired
-- hundreds of times on traffic the procedural engine passed cleanly. The properties were
-- wrong, not the design, and no amount of reading them made that obvious. An assertion
-- you have not watched stay silent on known-good traffic is an assertion you have not
-- written yet.
--
-- P1 bounded existence, AS TWO DIRECTIVES. `before_!` says "an edge arrives before the
-- release"; `next_e[1 to 16]` says "an edge arrives within the bound".
--
-- THE TRAILING `!` IS THE WHOLE PROPERTY. `before_` is a WEAK operator: it says the edge
-- must not come after the release, and it is satisfied if the edge never comes at all.
-- With it, a select pulse carrying no edges PASSED -- silently, on the exact stimulus the
-- property exists to catch. `before!` is the strong form and requires the edge to occur.
--
-- Weak and strong operators differ by one character and by whether the property means
-- anything, and the weak one is the default spelling. SVA has the same split -- `s_until`
-- and `s_eventually` against `until` and `eventually` -- and the same trap: the weak form
-- of a liveness property is satisfied by a design that simply stops.
--
-- The underscore is a different axis: `before_` includes the terminating cycle and
-- `before` excludes it. The strong-inclusive combination `before_!` is not accepted here,
-- so P1A uses `before!`, which is correct for a FIRST edge -- a first edge coinciding with
-- the release would be a one-edge frame, which this suite never sends. They cannot be
-- combined into one property here -- nvc rejects a boolean ANDed with a temporal operator
-- -- and splitting them is the better shape anyway, because a failure then says WHICH of
-- the two obligations was missed.
-- psl P1A_EDGE_BEFORE_RELEASE : assert always ((cs_assert = '1') -> next ((edge_in_txn = '1') before! (cs_deassert = '1'))) report "P1A EDGE_BEFORE_RELEASE failed";
-- psl P1B_EDGE_WITHIN_BOUND : assert always ((cs_assert = '1') -> next_e[1 to 16] (edge_in_txn = '1')) report "P1B EDGE_WITHIN_BOUND failed";
--
-- P2 the stability window, also as two directives, and for the same reason: written as one
-- property it would read `(mosi = mosi_d) and next (mosi = mosi_d)` -- an immediate
-- obligation ANDed with a temporal one, which nvc rejects outright. The rejection is a
-- useful prompt: a property that mixes the two cannot say WHICH SIDE of the window moved.
--
-- The second directive works because one cycle after the capture, `mosi_d` holds the
-- capture-cycle value -- so `mosi = mosi_d` there says MOSI did not move at the capture.
-- psl P2A_STABLE_BEFORE : assert always ((cap_in_txn = '1') -> (mosi = mosi_d)) report "P2A STABLE_BEFORE failed";
-- psl P2B_STABLE_AFTER : assert always ((cap_in_txn = '1') -> next (mosi = mosi_d)) report "P2B STABLE_AFTER failed";
--
-- P3 the multi-cycle consequent, spelled out one cycle at a time. `next` and `next[2]`
-- cover the HALF-1 = 2 cycles a half period of three owes, and the implication is
-- NON-OVERLAPPING by construction: the edge itself is the change, so the obligation starts
-- on the following cycle. Written as an immediate implication every attempt would fail
-- instantly, which looks like a catastrophic design bug and is a misplaced operator.
-- psl P3A_HALF_STABLE_1 : assert always ((edge_in_txn = '1') -> next (sclk_held = '1')) report "P3A HALF_STABLE_1 failed";
-- psl P3B_HALF_STABLE_2 : assert always ((edge_in_txn = '1') -> next[2] (sclk_held = '1')) report "P3B HALF_STABLE_2 failed";
--
-- P4 a count settled by a terminating event, anchored to the FIRST EDGE rather than to the
-- select: with the select as the antecedent, a pulse carrying no edges fails both P1 and
-- P4 and neither report says "there were no edges".
-- psl P4_FRAME_COMPLETE : assert always ((first_edge = '1') -> next ((frame_done = '1') before! (cs_deassert = '1'))) report "P4 FRAME_COMPLETE failed";
--
-- P6 bounded liveness the other way round: P1 asks that something START, this asks that
-- something END, and a suite with only the first kind cannot see a master that never lets
-- go.
-- psl P6_RELEASE_AFTER_FRAME : assert always ((frame_done = '1') -> next_e[1 to 8] (cs_deassert = '1')) report "P6 RELEASE_AFTER_FRAME failed";
--
-- P5 -- SCLK parked at CPOL for the whole idle interval -- IS NOT HERE, and its absence is
-- a finding rather than an omission. Expressed as `cs_deassert -> next ((sclk = cpol)
-- until_ cs_assert)` it fired repeatedly on traffic the procedural engine passed, and the
-- reason is the mode sweep: this bench reconfigures CPOL between measurement windows, the
-- driver re-parks SCLK a cycle later, and for that one cycle a correct master looks like a
-- violation. Chapter 16.4 hit the same artefact and bracketed it by clearing counters;
-- a declarative assertion has nothing to clear.
--
-- The procedural engine measures P5 because its testbench can bracket the reconfiguration.
-- The declarative one cannot, so it does not claim to -- which is the honest version of a
-- limitation that is usually papered over with a `disable iff` whose real effect nobody
-- checks. Chapter 17.2 is about exactly that operator.
--
-- The cover directives, which are the `attempts` counters in declarative form. The first
-- two must fire; C_ONEBIT must NOT, and its silence is the same vacuity the procedural
-- engine reports as a zero.
-- psl C_SELECT : cover {cs_assert = '1'} report "C_SELECT: a select was seen";
-- psl C_FRAME : cover {frame_done = '1'} report "C_FRAME: a frame completed";
-- psl C_ONEBIT : cover {cs_assert = '1' and len = to_unsigned(1, LEN_W)} report "C_ONEBIT: a one-bit frame was seen";
end architecture psl;The Bench
Azvya Education Pvt. Ltd.VLSI Mentor
spi_props_tb.sv — legal traffic, a property never attempted, a diagonal violation matrix, and an attempt left open
// spi_props_tb.sv
//
// LEGAL TRAFFIC FROM CHAPTER 16.4'S DRIVER, AND SIX CRAFTED VIOLATIONS FROM THE BENCH.
//
// The legal phase uses the real driver, because a property set that has only ever seen
// hand-written stimulus has only ever been tested against the bench author's idea of the
// protocol. The violation phase drives the pins directly, because each violation has to hit
// exactly ONE property and a fault injected into a driver reaches whatever it reaches.
//
// FOUR MEASUREMENTS.
//
// 1. LEGAL TRAFFIC PASSES, AND THE PASS COUNTS ARE NON-ZERO. Six of the seven properties
// report passes and no failures. That pair is the whole of Chapter 16.1's argument
// restated in assertion form: zero failures with zero passes is not a result.
//
// 2. THE SEVENTH PROPERTY IS NEVER ATTEMPTED, and the report says so rather than showing
// a green line. P7's antecedent needs a one-bit frame and this suite sends none, so
// `attempts` stays at zero while `vacuous` climbs. In SVA that property passes
// vacuously on every clock edge for the life of the project.
//
// 3. SIX VIOLATIONS, SIX PROPERTIES, A DIAGONAL. Each crafted violation fails exactly one
// property. The antecedents were chosen to make that possible -- see the note on P4 in
// the property file -- because a fault that trips three properties produces a report
// with three suspects.
//
// 4. AN ATTEMPT LEFT OPEN AT THE END IS NEITHER A PASS NOR A FAIL. The last phase asserts
// the select, produces no edge, and ends. P1's attempt is still open, and the
// measurement is that it is booked as INCOMPLETE and appears in neither the pass
// column nor the fail column. A suite that does not count this has a silent hole
// whose size it cannot state.
`timescale 1ns/1ps
module spi_props_tb;
localparam int LEAD = 4;
localparam int HALF = 3;
localparam int LAG = 2;
localparam int GAP = 3;
localparam int DW = 32;
localparam int LEN_W = 6;
localparam int CNT_W = 16;
localparam int NPROPS = 7;
localparam int MAXLEAD = 16;
localparam int MAXLAG = 8;
localparam int P_EDGE = 0, P_STABLE = 1, P_HALF = 2, P_FRAME = 3,
P_PARKED = 4, P_REL = 5, P_ONEBIT = 6;
reg clk = 1'b0;
always #5 clk = ~clk;
reg rst_n = 1'b1;
// --- the driver, used for the legal phase only --------------------------
reg start = 1'b0;
reg [DW-1:0] tx_data = 32'h0000_1A5C;
reg [LEN_W-1:0] nbits = 6'd8;
reg cpol = 1'b0, cpha = 1'b0, lsb_first = 1'b0;
wire busy, done;
wire [DW-1:0] drv_rx;
wire d_sclk, d_cs_n, d_mosi;
// --- the bench's own pins, used for the violation phase -----------------
reg sel_bench = 1'b0;
reg b_sclk = 1'b0, b_cs_n = 1'b1, b_mosi = 1'b0;
wire sclk = sel_bench ? b_sclk : d_sclk;
wire cs_n = sel_bench ? b_cs_n : d_cs_n;
wire mosi = sel_bench ? b_mosi : d_mosi;
wire miso = ~mosi;
spi_driver #(.LEAD(LEAD), .HALF(HALF), .LAG(LAG), .GAP(GAP),
.DW(DW), .LEN_W(LEN_W), .CNT_W(16)) u_drv (
.clk(clk), .rst_n(rst_n),
.start(start), .tx_data(tx_data), .nbits(nbits),
.cpol(cpol), .cpha(cpha), .lsb_first(lsb_first), .fault(3'd0),
.busy(busy), .done(done), .rx_data(drv_rx),
.sclk(d_sclk), .cs_n(d_cs_n), .mosi(d_mosi), .miso(miso)
);
reg clr = 1'b0, flush = 1'b0;
wire [NPROPS*CNT_W-1:0] at_f, va_f, pa_f, fa_f, ic_f;
spi_props #(.HALF(HALF), .MAXLEAD(MAXLEAD), .MAXLAG(MAXLAG),
.LEN_W(LEN_W), .CNT_W(CNT_W), .NPROPS(NPROPS)) u_p (
.clk(clk), .rst_n(rst_n),
.sclk(sclk), .cs_n(cs_n), .mosi(mosi),
.cpol(cpol), .cpha(cpha), .len(nbits),
.clr(clr), .flush(flush),
.attempts_flat(at_f), .vacuous_flat(va_f), .passes_flat(pa_f),
.fails_flat(fa_f), .incomplete_flat(ic_f)
);
function automatic [CNT_W-1:0] att(input integer i); begin att = at_f[i*CNT_W +: CNT_W]; end endfunction
function automatic [CNT_W-1:0] vac(input integer i); begin vac = va_f[i*CNT_W +: CNT_W]; end endfunction
function automatic [CNT_W-1:0] pas(input integer i); begin pas = pa_f[i*CNT_W +: CNT_W]; end endfunction
function automatic [CNT_W-1:0] fal(input integer i); begin fal = fa_f[i*CNT_W +: CNT_W]; end endfunction
function automatic [CNT_W-1:0] inc(input integer i); begin inc = ic_f[i*CNT_W +: CNT_W]; end endfunction
integer errors = 0;
initial begin
#400_000;
$display("FAIL: the simulation did not finish within its time limit");
$finish;
end
// ------------------------------------------------------------------
// Legal traffic, through the real driver.
// ------------------------------------------------------------------
task automatic set_cfg(input [LEN_W-1:0] n, input integer pol, input integer pha);
begin
@(negedge clk);
nbits = n; cpol = pol[0]; cpha = pha[0];
b_sclk = pol[0]; // keep the bench's idle level in step
repeat (6) @(negedge clk);
end
endtask
task automatic run_burst(input integer ntxn);
integer k;
begin
k = 0;
@(negedge clk);
start = 1'b1;
while (k < ntxn) begin
@(negedge clk);
if (done) begin k = k + 1; if (k == ntxn) start = 1'b0; end
end
repeat (GAP + LAG + 8) @(negedge clk);
end
endtask
task automatic clear_counts;
begin
@(negedge clk);
clr = 1'b1;
@(negedge clk);
clr = 1'b0;
@(negedge clk);
end
endtask
// ------------------------------------------------------------------
// The bench's own pin driving, for the crafted violations.
//
// Every write is on the NEGEDGE -- Chapter 16.3's discipline. A bench that crafts a
// violation on the same edge the checker samples is a bench measuring its own
// evaluation order, and the crafted stimulus is exactly where that is easiest to do
// by accident.
// ------------------------------------------------------------------
task automatic bench_idle(input integer n);
integer i;
begin
for (i = 0; i < n; i = i + 1) @(negedge clk);
end
endtask
// A frame of `n` bits with a half period of `h`, optional MOSI motion at capture edge
// `bad_cap`, and an edge count reduced by `drop`.
task automatic bench_frame(input integer n, input integer h,
input integer bad_cap, input integer drop,
input integer hold_extra, input integer short_half_at);
integer e, i, total;
begin
b_cs_n = 1'b0;
b_mosi = 1'b0;
bench_idle(LEAD);
total = 2*n - drop;
for (e = 0; e < total; e = e + 1) begin
b_sclk = ~b_sclk;
// MOSI moves AT this edge if asked. Capture edges are the leading ones for
// CPHA=0, which is the configuration the violation phase runs in.
if (bad_cap == 1 && e == 2) b_mosi = ~b_mosi;
// A launch that is legal: MOSI moves on trailing edges, away from capture.
if (bad_cap == 0 && (e % 2) == 1) b_mosi = ~b_mosi;
if (short_half_at == e) bench_idle(1);
else bench_idle(h);
end
bench_idle(LAG + hold_extra);
b_cs_n = 1'b1;
bench_idle(GAP + 4);
end
endtask
integer iw, ipol, ipha, p;
reg [LEN_W-1:0] w;
integer legal_txns;
reg [NPROPS-1:0] fired;
integer v, expect_p, other, diag_bad, matrix_bad;
integer inc_before, inc_after;
initial begin
rst_n = 1'b1;
repeat (2) @(negedge clk);
rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (4) @(negedge clk);
// ============================================================
// 1 + 2. LEGAL TRAFFIC.
// ============================================================
sel_bench = 1'b0;
legal_txns = 0;
for (iw = 0; iw < 2; iw = iw + 1) begin
w = (iw == 0) ? 6'd8 : 6'd4;
for (ipol = 0; ipol < 2; ipol = ipol + 1)
for (ipha = 0; ipha < 2; ipha = ipha + 1) begin
set_cfg(w, ipol, ipha);
clear_counts();
run_burst(2);
legal_txns = legal_txns + 2;
for (p = 0; p < NPROPS; p = p + 1)
if (fal(p) != 0) begin
$display(" FAIL: legal traffic failed P%0d %0d time(s) at cpol=%0d cpha=%0d n=%0d",
p + 1, fal(p), ipol, ipha, w);
errors = errors + 1;
end
end
end
$display(" legal traffic, the last measurement window (cpol=1 cpha=1 n=4), 2 transactions:");
$display(" prop name attempts vacuous passes fails incomplete");
$display(" P1 EDGE_AFTER_SELECT %8d %8d %7d %6d %11d", att(0), vac(0), pas(0), fal(0), inc(0));
$display(" P2 STABLE_AT_CAPTURE %8d %8d %7d %6d %11d", att(1), vac(1), pas(1), fal(1), inc(1));
$display(" P3 HALF_STABLE %8d %8d %7d %6d %11d", att(2), vac(2), pas(2), fal(2), inc(2));
$display(" P4 FRAME_COMPLETE %8d %8d %7d %6d %11d", att(3), vac(3), pas(3), fal(3), inc(3));
$display(" P5 SCLK_PARKED %8d %8d %7d %6d %11d", att(4), vac(4), pas(4), fal(4), inc(4));
$display(" P6 RELEASE_AFTER_FRAME %8d %8d %7d %6d %11d", att(5), vac(5), pas(5), fal(5), inc(5));
$display(" P7 ONE_BIT_FRAME %8d %8d %7d %6d %11d", att(6), vac(6), pas(6), fal(6), inc(6));
for (p = 0; p < 6; p = p + 1)
if (pas(p) == 0) begin
$display(" FAIL: P%0d recorded no passes on legal traffic, so its zero failure count is a silence rather than a measurement",
p + 1);
errors = errors + 1;
end
$display(" 1. six of the seven properties passed on legal traffic with NON-ZERO pass counts, across %0d transactions in four modes and two widths. Zero failures with zero passes would have been the same green line and no result at all",
legal_txns);
if (att(P_ONEBIT) != 0) begin
$display(" FAIL: P7 was attempted %0d times; this suite sends no one-bit frames and the vacuity demonstration needs it to be unreachable",
att(P_ONEBIT));
errors = errors + 1;
end
if (vac(P_ONEBIT) == 0) begin
$display(" FAIL: P7 recorded no vacuous evaluations either, so it was never even looked at and the measurement says nothing");
errors = errors + 1;
end
$display(" 2. P7 was attempted ZERO times and evaluated vacuously %0d times. Its antecedent needs a one-bit frame and this suite sends none -- so in SVA it passes on every clock edge, forever, and a pass/fail report cannot tell it from P1",
vac(P_ONEBIT));
// ============================================================
// 3. SIX VIOLATIONS, SIX PROPERTIES.
// ============================================================
set_cfg(6'd4, 0, 0);
sel_bench = 1'b1;
b_cs_n = 1'b1; b_sclk = 1'b0; b_mosi = 1'b0;
bench_idle(8);
diag_bad = 0;
matrix_bad = 0;
$display(" violation expected properties that failed");
for (v = 1; v <= 6; v = v + 1) begin
clear_counts();
case (v)
// A select pulse carrying no SCLK edge at all.
1: begin
expect_p = P_EDGE;
b_cs_n = 1'b0; bench_idle(6); b_cs_n = 1'b1; bench_idle(GAP + 4);
end
// A legal frame in which MOSI moves ON a capture edge.
2: begin expect_p = P_STABLE; bench_frame(4, HALF, 1, 0, 0, -1); end
// A legal frame with one half period of a single cycle.
3: begin expect_p = P_HALF; bench_frame(4, HALF, 0, 0, 0, 3); end
// A frame two edges short -- an even count, so SCLK still parks correctly.
4: begin expect_p = P_FRAME; bench_frame(4, HALF, 0, 2, 0, -1); end
// A glitch on SCLK while the bus is idle.
//
// The phase opens with a COMPLETE, legal frame, and that is not padding:
// SCLK_PARKED's attempt begins at a deassert, so without a transaction
// first there is no attempt for the glitch to fail. An earlier version
// instead appended a short select pulse to close the attempt -- and that
// pulse carried no SCLK edge, so it failed EDGE_AFTER_SELECT too and the
// violation matrix lost its diagonal. A crafted violation has to be
// crafted all the way to its end.
5: begin
expect_p = P_PARKED;
bench_frame(4, HALF, 0, 0, 0, -1);
bench_idle(4);
b_sclk = ~b_sclk; bench_idle(2); b_sclk = ~b_sclk; bench_idle(6);
end
// A complete frame, held selected far longer than MAXLAG.
default: begin expect_p = P_REL; bench_frame(4, HALF, 0, 0, MAXLAG + 4, -1); end
endcase
fired = {NPROPS{1'b0}};
for (p = 0; p < NPROPS; p = p + 1) if (fal(p) != 0) fired[p] = 1'b1;
$display(" %-30s P%0d %b",
(v == 1) ? "a select with no SCLK edge" :
(v == 2) ? "MOSI moving at a capture" :
(v == 3) ? "a one-cycle half period" :
(v == 4) ? "a frame two edges short" :
(v == 5) ? "an SCLK glitch while idle" : "the select held past MAXLAG",
expect_p + 1, fired);
if (fired[expect_p] !== 1'b1) begin
$display(" FAIL: violation %0d did not fail P%0d, so that property is either unreachable or wrong -- and a property that cannot be made to fail has been assumed, not verified",
v, expect_p + 1);
errors = errors + 1;
diag_bad = diag_bad + 1;
end
for (other = 0; other < NPROPS; other = other + 1)
if (other != expect_p && fired[other] === 1'b1) begin
$display(" FAIL: violation %0d also failed P%0d, so the report names more than one suspect for one fault",
v, other + 1);
errors = errors + 1;
matrix_bad = matrix_bad + 1;
end
end
$display(" 3. each of the six crafted violations failed EXACTLY ONE property: %0d expected failures missing, %0d unexpected. The antecedents were chosen to make that possible -- anchoring FRAME_COMPLETE to the first edge rather than to the select is what keeps an empty select pulse from failing two properties and naming neither cause",
diag_bad, matrix_bad);
// ============================================================
// 4. AN ATTEMPT LEFT OPEN.
// ============================================================
clear_counts();
inc_before = inc(P_EDGE);
@(negedge clk);
b_cs_n = 1'b0; // assert, and then produce nothing at all
bench_idle(4); // fewer than MAXLEAD, so the attempt is still open
@(negedge clk);
flush = 1'b1;
@(negedge clk);
flush = 1'b0;
@(negedge clk);
inc_after = inc(P_EDGE);
$display(" an attempt still open when the test ends:");
$display(" P1 passes ....... %0d", pas(P_EDGE));
$display(" P1 fails ........ %0d", fal(P_EDGE));
$display(" P1 incomplete ... %0d", inc_after - inc_before);
if ((inc_after - inc_before) == 0) begin
$display(" FAIL: the open attempt was not booked as incomplete, so an attempt in flight at the end of a test disappears without trace");
errors = errors + 1;
end
if (pas(P_EDGE) != 0 || fal(P_EDGE) != 0) begin
$display(" FAIL: the open attempt was scored as a pass or a fail (%0d/%0d); it is neither",
pas(P_EDGE), fal(P_EDGE));
errors = errors + 1;
end
$display(" 4. the attempt was booked as INCOMPLETE and appears in neither the pass column nor the fail column. That is the honest answer: the antecedent matched, the obligation was never settled, and a design that was about to violate the property is indistinguishable here from one that would have satisfied it. A suite that does not count this cannot state the size of its own blind spot");
if (errors == 0)
$display("PASS: a property is not a rule evaluated at an instant -- it opens at one instant and is settled at another, and between them it is OPEN. So an attempt has FOUR outcomes and not two, and the two that are not failures are where a suite's silence comes from. Across %0d legal transactions in four modes and two widths, six of the seven properties passed with NON-ZERO pass counts, which is what stops the zero failure column from being a silence. The seventh was attempted ZERO times and evaluated vacuously %0d times, because its antecedent needs a one-bit frame and this suite sends none -- in SVA that property passes on every clock edge for the life of the project and a pass/fail report cannot tell it from a property that works. Six crafted violations then failed EXACTLY one property each, which is a result about the ANTECEDENTS as much as about the checks: anchoring FRAME_COMPLETE to the first edge rather than to the select is what stops an empty select pulse from failing two properties while naming neither cause, so choosing an antecedent is part of designing a diagnosis. And an attempt still in flight when the test ended was booked as INCOMPLETE -- in neither the pass column nor the fail column -- because the antecedent matched, the obligation was never settled, and a design that was about to violate it is indistinguishable from one that would have satisfied it",
legal_txns, vac(P_ONEBIT));
else
$display("FAIL: %0d error(s)", errors);
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_props_tb.v — the same bench in Verilog-2001
// spi_props_tb.v
//
// LEGAL TRAFFIC FROM CHAPTER 16.4'S DRIVER, AND SIX CRAFTED VIOLATIONS FROM THE BENCH.
//
// The legal phase uses the real driver, because a property set that has only ever seen
// hand-written stimulus has only ever been tested against the bench author's idea of the
// protocol. The violation phase drives the pins directly, because each violation has to hit
// exactly ONE property and a fault injected into a driver reaches whatever it reaches.
//
// FOUR MEASUREMENTS.
//
// 1. LEGAL TRAFFIC PASSES, AND THE PASS COUNTS ARE NON-ZERO. Six of the seven properties
// report passes and no failures. That pair is the whole of Chapter 16.1's argument
// restated in assertion form: zero failures with zero passes is not a result.
//
// 2. THE SEVENTH PROPERTY IS NEVER ATTEMPTED, and the report says so rather than showing
// a green line. P7's antecedent needs a one-bit frame and this suite sends none, so
// `attempts` stays at zero while `vacuous` climbs. In SVA that property passes
// vacuously on every clock edge for the life of the project.
//
// 3. SIX VIOLATIONS, SIX PROPERTIES, A DIAGONAL. Each crafted violation fails exactly one
// property. The antecedents were chosen to make that possible -- see the note on P4 in
// the property file -- because a fault that trips three properties produces a report
// with three suspects.
//
// 4. AN ATTEMPT LEFT OPEN AT THE END IS NEITHER A PASS NOR A FAIL. The last phase asserts
// the select, produces no edge, and ends. P1's attempt is still open, and the
// measurement is that it is booked as INCOMPLETE and appears in neither the pass
// column nor the fail column. A suite that does not count this has a silent hole
// whose size it cannot state.
`timescale 1ns/1ps
module spi_props_tb;
localparam LEAD = 4;
localparam HALF = 3;
localparam LAG = 2;
localparam GAP = 3;
localparam DW = 32;
localparam LEN_W = 6;
localparam CNT_W = 16;
localparam NPROPS = 7;
localparam MAXLEAD = 16;
localparam MAXLAG = 8;
localparam P_EDGE = 0, P_STABLE = 1, P_HALF = 2, P_FRAME = 3,
P_PARKED = 4, P_REL = 5, P_ONEBIT = 6;
reg clk;
always #5 clk = ~clk;
reg rst_n;
// --- the driver, used for the legal phase only --------------------------
reg start;
reg [DW-1:0] tx_data;
reg [LEN_W-1:0] nbits;
reg cpol, cpha, lsb_first;
wire busy, done;
wire [DW-1:0] drv_rx;
wire d_sclk, d_cs_n, d_mosi;
// --- the bench's own pins, used for the violation phase -----------------
reg sel_bench;
reg b_sclk, b_cs_n, b_mosi;
wire sclk = sel_bench ? b_sclk : d_sclk;
wire cs_n = sel_bench ? b_cs_n : d_cs_n;
wire mosi = sel_bench ? b_mosi : d_mosi;
wire miso = ~mosi;
spi_driver #(.LEAD(LEAD), .HALF(HALF), .LAG(LAG), .GAP(GAP),
.DW(DW), .LEN_W(LEN_W), .CNT_W(16)) u_drv (
.clk(clk), .rst_n(rst_n),
.start(start), .tx_data(tx_data), .nbits(nbits),
.cpol(cpol), .cpha(cpha), .lsb_first(lsb_first), .fault(3'd0),
.busy(busy), .done(done), .rx_data(drv_rx),
.sclk(d_sclk), .cs_n(d_cs_n), .mosi(d_mosi), .miso(miso)
);
reg clr, flush;
wire [NPROPS*CNT_W-1:0] at_f, va_f, pa_f, fa_f, ic_f;
spi_props #(.HALF(HALF), .MAXLEAD(MAXLEAD), .MAXLAG(MAXLAG),
.LEN_W(LEN_W), .CNT_W(CNT_W), .NPROPS(NPROPS)) u_p (
.clk(clk), .rst_n(rst_n),
.sclk(sclk), .cs_n(cs_n), .mosi(mosi),
.cpol(cpol), .cpha(cpha), .len(nbits),
.clr(clr), .flush(flush),
.attempts_flat(at_f), .vacuous_flat(va_f), .passes_flat(pa_f),
.fails_flat(fa_f), .incomplete_flat(ic_f)
);
function [CNT_W-1:0] att;
input integer i; begin att = at_f[i*CNT_W +: CNT_W]; end endfunction
function [CNT_W-1:0] vac;
input integer i; begin vac = va_f[i*CNT_W +: CNT_W]; end endfunction
function [CNT_W-1:0] pas;
input integer i; begin pas = pa_f[i*CNT_W +: CNT_W]; end endfunction
function [CNT_W-1:0] fal;
input integer i; begin fal = fa_f[i*CNT_W +: CNT_W]; end endfunction
function [CNT_W-1:0] inc;
input integer i; begin inc = ic_f[i*CNT_W +: CNT_W]; end endfunction
integer errors;
initial begin
#400_000;
$display("FAIL: the simulation did not finish within its time limit");
$finish;
end
// ------------------------------------------------------------------
// Legal traffic, through the real driver.
// ------------------------------------------------------------------
task set_cfg;
input [LEN_W-1:0] n;
input integer pol;
input integer pha;
begin
@(negedge clk);
nbits = n; cpol = pol[0]; cpha = pha[0];
b_sclk = pol[0]; // keep the bench's idle level in step
repeat (6) @(negedge clk);
end
endtask
task run_burst;
input integer ntxn;
integer k;
begin
k = 0;
@(negedge clk);
start = 1'b1;
while (k < ntxn) begin
@(negedge clk);
if (done) begin k = k + 1; if (k == ntxn) start = 1'b0; end
end
repeat (GAP + LAG + 8) @(negedge clk);
end
endtask
task clear_counts;
begin
@(negedge clk);
clr = 1'b1;
@(negedge clk);
clr = 1'b0;
@(negedge clk);
end
endtask
// ------------------------------------------------------------------
// The bench's own pin driving, for the crafted violations.
//
// Every write is on the NEGEDGE -- Chapter 16.3's discipline. A bench that crafts a
// violation on the same edge the checker samples is a bench measuring its own
// evaluation order, and the crafted stimulus is exactly where that is easiest to do
// by accident.
// ------------------------------------------------------------------
task bench_idle;
input integer n;
integer i;
begin
for (i = 0; i < n; i = i + 1) @(negedge clk);
end
endtask
// A frame of `n` bits with a half period of `h`, optional MOSI motion at capture edge
// `bad_cap`, and an edge count reduced by `drop`.
task bench_frame;
input integer n;
input integer h;
input integer bad_cap;
input integer drop;
input integer hold_extra;
input integer short_half_at;
integer e, i, total;
begin
b_cs_n = 1'b0;
b_mosi = 1'b0;
bench_idle(LEAD);
total = 2*n - drop;
for (e = 0; e < total; e = e + 1) begin
b_sclk = ~b_sclk;
// MOSI moves AT this edge if asked. Capture edges are the leading ones for
// CPHA=0, which is the configuration the violation phase runs in.
if (bad_cap == 1 && e == 2) b_mosi = ~b_mosi;
// A launch that is legal: MOSI moves on trailing edges, away from capture.
if (bad_cap == 0 && (e % 2) == 1) b_mosi = ~b_mosi;
if (short_half_at == e) bench_idle(1);
else bench_idle(h);
end
bench_idle(LAG + hold_extra);
b_cs_n = 1'b1;
bench_idle(GAP + 4);
end
endtask
integer iw, ipol, ipha, p;
reg [LEN_W-1:0] w;
integer legal_txns;
reg [NPROPS-1:0] fired;
integer v, expect_p, other, diag_bad, matrix_bad;
integer inc_before, inc_after;
initial begin
rst_n = 1'b1;
repeat (2) @(negedge clk);
rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (4) @(negedge clk);
// ============================================================
// 1 + 2. LEGAL TRAFFIC.
// ============================================================
sel_bench = 1'b0;
legal_txns = 0;
for (iw = 0; iw < 2; iw = iw + 1) begin
w = (iw == 0) ? 6'd8 : 6'd4;
for (ipol = 0; ipol < 2; ipol = ipol + 1)
for (ipha = 0; ipha < 2; ipha = ipha + 1) begin
set_cfg(w, ipol, ipha);
clear_counts();
run_burst(2);
legal_txns = legal_txns + 2;
for (p = 0; p < NPROPS; p = p + 1)
if (fal(p) != 0) begin
$display(" FAIL: legal traffic failed P%0d %0d time(s) at cpol=%0d cpha=%0d n=%0d",
p + 1, fal(p), ipol, ipha, w);
errors = errors + 1;
end
end
end
$display(" legal traffic, the last measurement window (cpol=1 cpha=1 n=4), 2 transactions:");
$display(" prop name attempts vacuous passes fails incomplete");
$display(" P1 EDGE_AFTER_SELECT %8d %8d %7d %6d %11d", att(0), vac(0), pas(0), fal(0), inc(0));
$display(" P2 STABLE_AT_CAPTURE %8d %8d %7d %6d %11d", att(1), vac(1), pas(1), fal(1), inc(1));
$display(" P3 HALF_STABLE %8d %8d %7d %6d %11d", att(2), vac(2), pas(2), fal(2), inc(2));
$display(" P4 FRAME_COMPLETE %8d %8d %7d %6d %11d", att(3), vac(3), pas(3), fal(3), inc(3));
$display(" P5 SCLK_PARKED %8d %8d %7d %6d %11d", att(4), vac(4), pas(4), fal(4), inc(4));
$display(" P6 RELEASE_AFTER_FRAME %8d %8d %7d %6d %11d", att(5), vac(5), pas(5), fal(5), inc(5));
$display(" P7 ONE_BIT_FRAME %8d %8d %7d %6d %11d", att(6), vac(6), pas(6), fal(6), inc(6));
for (p = 0; p < 6; p = p + 1)
if (pas(p) == 0) begin
$display(" FAIL: P%0d recorded no passes on legal traffic, so its zero failure count is a silence rather than a measurement",
p + 1);
errors = errors + 1;
end
$display(" 1. six of the seven properties passed on legal traffic with NON-ZERO pass counts, across %0d transactions in four modes and two widths. Zero failures with zero passes would have been the same green line and no result at all",
legal_txns);
if (att(P_ONEBIT) != 0) begin
$display(" FAIL: P7 was attempted %0d times; this suite sends no one-bit frames and the vacuity demonstration needs it to be unreachable",
att(P_ONEBIT));
errors = errors + 1;
end
if (vac(P_ONEBIT) == 0) begin
$display(" FAIL: P7 recorded no vacuous evaluations either, so it was never even looked at and the measurement says nothing");
errors = errors + 1;
end
$display(" 2. P7 was attempted ZERO times and evaluated vacuously %0d times. Its antecedent needs a one-bit frame and this suite sends none -- so in SVA it passes on every clock edge, forever, and a pass/fail report cannot tell it from P1",
vac(P_ONEBIT));
// ============================================================
// 3. SIX VIOLATIONS, SIX PROPERTIES.
// ============================================================
set_cfg(6'd4, 0, 0);
sel_bench = 1'b1;
b_cs_n = 1'b1; b_sclk = 1'b0; b_mosi = 1'b0;
bench_idle(8);
diag_bad = 0;
matrix_bad = 0;
$display(" violation expected properties that failed");
for (v = 1; v <= 6; v = v + 1) begin
clear_counts();
case (v)
// A select pulse carrying no SCLK edge at all.
1: begin
expect_p = P_EDGE;
b_cs_n = 1'b0; bench_idle(6); b_cs_n = 1'b1; bench_idle(GAP + 4);
end
// A legal frame in which MOSI moves ON a capture edge.
2: begin expect_p = P_STABLE; bench_frame(4, HALF, 1, 0, 0, -1); end
// A legal frame with one half period of a single cycle.
3: begin expect_p = P_HALF; bench_frame(4, HALF, 0, 0, 0, 3); end
// A frame two edges short -- an even count, so SCLK still parks correctly.
4: begin expect_p = P_FRAME; bench_frame(4, HALF, 0, 2, 0, -1); end
// A glitch on SCLK while the bus is idle.
//
// The phase opens with a COMPLETE, legal frame, and that is not padding:
// SCLK_PARKED's attempt begins at a deassert, so without a transaction
// first there is no attempt for the glitch to fail. An earlier version
// instead appended a short select pulse to close the attempt -- and that
// pulse carried no SCLK edge, so it failed EDGE_AFTER_SELECT too and the
// violation matrix lost its diagonal. A crafted violation has to be
// crafted all the way to its end.
5: begin
expect_p = P_PARKED;
bench_frame(4, HALF, 0, 0, 0, -1);
bench_idle(4);
b_sclk = ~b_sclk; bench_idle(2); b_sclk = ~b_sclk; bench_idle(6);
end
// A complete frame, held selected far longer than MAXLAG.
default: begin expect_p = P_REL; bench_frame(4, HALF, 0, 0, MAXLAG + 4, -1); end
endcase
fired = {NPROPS{1'b0}};
for (p = 0; p < NPROPS; p = p + 1) if (fal(p) != 0) fired[p] = 1'b1;
$display(" %0s P%0d %b",
(v == 1) ? "a select with no SCLK edge" :
(v == 2) ? "MOSI moving at a capture" :
(v == 3) ? "a one-cycle half period" :
(v == 4) ? "a frame two edges short" :
(v == 5) ? "an SCLK glitch while idle" : "the select held past MAXLAG",
expect_p + 1, fired);
if (fired[expect_p] !== 1'b1) begin
$display(" FAIL: violation %0d did not fail P%0d, so that property is either unreachable or wrong -- and a property that cannot be made to fail has been assumed, not verified",
v, expect_p + 1);
errors = errors + 1;
diag_bad = diag_bad + 1;
end
for (other = 0; other < NPROPS; other = other + 1)
if (other != expect_p && fired[other] === 1'b1) begin
$display(" FAIL: violation %0d also failed P%0d, so the report names more than one suspect for one fault",
v, other + 1);
errors = errors + 1;
matrix_bad = matrix_bad + 1;
end
end
$display(" 3. each of the six crafted violations failed EXACTLY ONE property: %0d expected failures missing, %0d unexpected. The antecedents were chosen to make that possible -- anchoring FRAME_COMPLETE to the first edge rather than to the select is what keeps an empty select pulse from failing two properties and naming neither cause",
diag_bad, matrix_bad);
// ============================================================
// 4. AN ATTEMPT LEFT OPEN.
// ============================================================
clear_counts();
inc_before = inc(P_EDGE);
@(negedge clk);
b_cs_n = 1'b0; // assert, and then produce nothing at all
bench_idle(4); // fewer than MAXLEAD, so the attempt is still open
@(negedge clk);
flush = 1'b1;
@(negedge clk);
flush = 1'b0;
@(negedge clk);
inc_after = inc(P_EDGE);
$display(" an attempt still open when the test ends:");
$display(" P1 passes ....... %0d", pas(P_EDGE));
$display(" P1 fails ........ %0d", fal(P_EDGE));
$display(" P1 incomplete ... %0d", inc_after - inc_before);
if ((inc_after - inc_before) == 0) begin
$display(" FAIL: the open attempt was not booked as incomplete, so an attempt in flight at the end of a test disappears without trace");
errors = errors + 1;
end
if (pas(P_EDGE) != 0 || fal(P_EDGE) != 0) begin
$display(" FAIL: the open attempt was scored as a pass or a fail (%0d/%0d); it is neither",
pas(P_EDGE), fal(P_EDGE));
errors = errors + 1;
end
$display(" 4. the attempt was booked as INCOMPLETE and appears in neither the pass column nor the fail column. That is the honest answer: the antecedent matched, the obligation was never settled, and a design that was about to violate the property is indistinguishable here from one that would have satisfied it. A suite that does not count this cannot state the size of its own blind spot");
if (errors == 0)
$display("PASS: a property is not a rule evaluated at an instant -- it opens at one instant and is settled at another, and between them it is OPEN. So an attempt has FOUR outcomes and not two, and the two that are not failures are where a suite's silence comes from. Across %0d legal transactions in four modes and two widths, six of the seven properties passed with NON-ZERO pass counts, which is what stops the zero failure column from being a silence. The seventh was attempted ZERO times and evaluated vacuously %0d times, because its antecedent needs a one-bit frame and this suite sends none -- in SVA that property passes on every clock edge for the life of the project and a pass/fail report cannot tell it from a property that works. Six crafted violations then failed EXACTLY one property each, which is a result about the ANTECEDENTS as much as about the checks: anchoring FRAME_COMPLETE to the first edge rather than to the select is what stops an empty select pulse from failing two properties while naming neither cause, so choosing an antecedent is part of designing a diagnosis. And an attempt still in flight when the test ended was booked as INCOMPLETE -- in neither the pass column nor the fail column -- because the antecedent matched, the obligation was never settled, and a design that was about to violate it is indistinguishable from one that would have satisfied it",
legal_txns, vac(P_ONEBIT));
else
$display("FAIL: %0d error(s)", errors);
$finish;
end
initial begin
cpol = 1'b0;
cpha = 1'b0;
lsb_first = 1'b0;
b_sclk = 1'b0;
b_cs_n = 1'b1;
b_mosi = 1'b0;
clr = 1'b0;
flush = 1'b0;
clk = 1'b0;
rst_n = 1'b1;
start = 1'b0;
tx_data = 32'h0000_1A5C;
nbits = 6'd8;
sel_bench = 1'b0;
errors = 0;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
spi_props_tb.vhd — the same bench in VHDL
-- spi_props_tb.vhd
--
-- LEGAL TRAFFIC FROM CHAPTER 16.4'S DRIVER, AND SIX CRAFTED VIOLATIONS FROM THE BENCH.
--
-- The legal phase uses the real driver, because a property set that has only seen
-- hand-written stimulus has only been tested against the bench author's idea of the protocol.
-- The violation phase drives the pins directly, because each violation has to hit exactly ONE
-- property and a fault injected into a driver reaches whatever it reaches.
--
-- FOUR MEASUREMENTS.
--
-- 1. LEGAL TRAFFIC PASSES, AND THE PASS COUNTS ARE NON-ZERO. Six of the seven properties
-- report passes and no failures. Zero failures with zero passes is not a result.
--
-- 2. THE SEVENTH PROPERTY IS NEVER ATTEMPTED. P7's antecedent needs a one-bit frame and
-- this suite sends none, so `attempts` stays at zero while `vacuous` climbs. In PSL and
-- in SVA alike that property passes vacuously on every clock edge, forever.
--
-- 3. SIX VIOLATIONS, SIX PROPERTIES, A DIAGONAL.
--
-- 4. AN ATTEMPT LEFT OPEN AT THE END IS NEITHER A PASS NOR A FAIL, and is booked as
-- INCOMPLETE.
-- THE DECLARATIVE SET HAS ITS OWN TOP LEVEL, `spi_psl_tb`, AT THE END OF THIS FILE, and the
-- reason is in the property file's header: an assertion that should not hold must not be
-- ARMED, and "armed" is a property of the simulation rather than of a cycle. A first version
-- gated every PSL property on a signal this bench raised over its legal phase; attempts opened
-- while the gate was up outlived the gate falling, and three properties fired on traffic they
-- had been switched off for.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.spi_driver_pkg.all;
use work.spi_prop_pkg.all;
entity spi_props_tb is
end entity spi_props_tb;
architecture tb of spi_props_tb is
constant LEAD_C : natural := 4;
constant HALF_C : natural := 3;
constant LAG_C : natural := 2;
constant GAP_C : natural := 3;
constant MAXLEAD : natural := 16;
constant MAXLAG : natural := 8;
constant HALF_T : time := 5 ns;
signal clk : std_logic := '0';
signal rst_n : std_logic := '1';
signal done_sim : boolean := false;
-- the driver, for the legal phase
signal start : std_logic := '0';
signal req : spi_req_t := (data => x"00001A5C",
nbits => to_unsigned(8, LEN_W),
cpol => '0',
cpha => '0',
lsb_first => '0',
fault => F_NONE);
signal busy, done : std_logic;
signal drv_rx : std_logic_vector(DW - 1 downto 0);
signal d_sclk, d_cs_n, d_mosi : std_logic;
-- the bench's own pins, for the crafted violations
signal sel_bench : boolean := false;
signal b_sclk : std_logic := '0';
signal b_cs_n : std_logic := '1';
signal b_mosi : std_logic := '0';
signal sclk, cs_n, mosi, miso : std_logic;
signal clr, flush : std_logic := '0';
signal c : prop_array_t;
signal errors : integer := 0;
begin
sclk <= b_sclk when sel_bench else d_sclk;
cs_n <= b_cs_n when sel_bench else d_cs_n;
mosi <= b_mosi when sel_bench else d_mosi;
miso <= not mosi;
clk_gen : process is
begin
while not done_sim loop
wait for HALF_T;
clk <= not clk;
end loop;
wait;
end process clk_gen;
u_drv : entity work.spi_driver
generic map (LEAD => LEAD_C, HALF => HALF_C, LAG => LAG_C, GAP => GAP_C)
port map (clk => clk, rst_n => rst_n, start => start, req => req,
busy => busy, done => done, rx_data => drv_rx,
sclk => d_sclk, cs_n => d_cs_n, mosi => d_mosi, miso => miso);
u_p : entity work.spi_props
generic map (HALF => HALF_C, MAXLEAD => MAXLEAD, MAXLAG => MAXLAG, LEN_W => LEN_W)
port map (clk => clk, rst_n => rst_n,
sclk => sclk, cs_n => cs_n, mosi => mosi,
cpol => req.cpol, cpha => req.cpha, len => req.nbits,
clr => clr, flush => flush, counts => c);
main : process is
procedure set_cfg (n : natural; pol : std_logic; pha : std_logic) is
begin
wait until falling_edge(clk);
req.nbits <= to_unsigned(n, LEN_W);
req.cpol <= pol;
req.cpha <= pha;
b_sclk <= pol; -- keep the bench's idle level in step
for i in 0 to 5 loop wait until falling_edge(clk); end loop;
end procedure set_cfg;
procedure run_burst (ntxn : natural) is
variable k : natural := 0;
begin
k := 0;
wait until falling_edge(clk);
start <= '1';
while k < ntxn loop
wait until falling_edge(clk);
if done = '1' then
k := k + 1;
if k = ntxn then start <= '0'; end if;
end if;
end loop;
for i in 0 to GAP_C + LAG_C + 7 loop wait until falling_edge(clk); end loop;
end procedure run_burst;
procedure clear_counts is
begin
wait until falling_edge(clk);
clr <= '1';
wait until falling_edge(clk);
clr <= '0';
wait until falling_edge(clk);
end procedure clear_counts;
procedure bench_idle (n : natural) is
begin
for i in 1 to n loop wait until falling_edge(clk); end loop;
end procedure bench_idle;
-- A frame of `n` bits with a half period of `h`, optional MOSI motion at a capture
-- edge, an edge count reduced by `drop`, extra select hold, and one short half period.
procedure bench_frame (n : natural; h : natural; bad_cap : integer; drop : natural;
hold_extra : natural; short_half_at : integer) is
variable total : natural;
begin
b_cs_n <= '0';
b_mosi <= '0';
bench_idle(LEAD_C);
total := 2 * n - drop;
for e in 0 to total - 1 loop
b_sclk <= not b_sclk;
if bad_cap = 1 and e = 2 then
b_mosi <= not b_mosi;
end if;
if bad_cap = 0 and (e mod 2) = 1 then
b_mosi <= not b_mosi;
end if;
if short_half_at = e then bench_idle(1);
else bench_idle(h);
end if;
end loop;
bench_idle(LAG_C + hold_extra);
b_cs_n <= '1';
bench_idle(GAP_C + 4);
end procedure bench_frame;
type bool_arr_t is array (0 to NPROPS - 1) of boolean;
variable w : natural;
variable legal_txns : natural := 0;
variable legal_fail : natural := 0;
variable fired : bool_arr_t;
variable expect_p : natural;
variable diag_bad, matrix_bad : natural := 0;
variable inc_before : natural;
variable pol, pha : std_logic;
variable fs : string(1 to NPROPS);
variable vlab : string(1 to 30);
begin
rst_n <= '1';
for i in 0 to 1 loop wait until falling_edge(clk); end loop;
rst_n <= '0';
for i in 0 to 3 loop wait until falling_edge(clk); end loop;
rst_n <= '1';
for i in 0 to 3 loop wait until falling_edge(clk); end loop;
-- ==============================================================
-- 1 + 2 + 5. LEGAL TRAFFIC, with the PSL set armed.
-- ==============================================================
sel_bench <= false;
for iw in 0 to 1 loop
if iw = 0 then w := 8; else w := 4; end if;
for ipol in 0 to 1 loop
for ipha in 0 to 1 loop
if ipol = 0 then pol := '0'; else pol := '1'; end if;
if ipha = 0 then pha := '0'; else pha := '1'; end if;
set_cfg(w, pol, pha);
clear_counts;
run_burst(2);
legal_txns := legal_txns + 2;
for p in 0 to NPROPS - 1 loop
if c(p).fails /= 0 then
legal_fail := legal_fail + 1;
end if;
end loop;
end loop;
end loop;
end loop;
if legal_fail /= 0 then
report " FAIL: legal traffic failed a property in " & integer'image(legal_fail) &
" measurement window(s)";
errors <= errors + 1;
wait for 1 ns;
end if;
report " legal traffic, the last measurement window (cpol=1 cpha=1 n=4), 2 transactions:";
report " prop name attempts vacuous passes fails incomplete";
for p in 0 to NPROPS - 1 loop
report " P" & integer'image(p + 1) & " " & prop_name(p) & " " &
integer'image(c(p).attempts) & " " & integer'image(c(p).vacuous) & " " &
integer'image(c(p).passes) & " " & integer'image(c(p).fails) & " " &
integer'image(c(p).incomplete);
end loop;
for p in 0 to 5 loop
if c(p).passes = 0 then
report " FAIL: P" & integer'image(p + 1) &
" recorded no passes on legal traffic, so its zero failure count is a silence rather than a measurement";
errors <= errors + 1;
wait for 1 ns;
end if;
end loop;
report " 1. six of the seven properties passed on legal traffic with NON-ZERO pass counts, across " &
integer'image(legal_txns) &
" transactions in four modes and two widths. Zero failures with zero passes would have been the same green line and no result at all";
if c(P_ONEBIT).attempts /= 0 then
report " FAIL: P7 was attempted " & integer'image(c(P_ONEBIT).attempts) &
" times; this suite sends no one-bit frames and the vacuity demonstration needs it to be unreachable";
errors <= errors + 1;
wait for 1 ns;
end if;
if c(P_ONEBIT).vacuous = 0 then
report " FAIL: P7 recorded no vacuous evaluations either, so it was never even looked at and the measurement says nothing";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 2. P7 was attempted ZERO times and evaluated vacuously " &
integer'image(c(P_ONEBIT).vacuous) &
" times. Its antecedent needs a one-bit frame and this suite sends none -- so in PSL and in SVA alike it passes on every clock edge, forever, and a pass/fail report cannot tell it from P1";
-- ==============================================================
-- 3. SIX VIOLATIONS, SIX PROPERTIES.
-- ==============================================================
set_cfg(4, '0', '0');
sel_bench <= true;
b_cs_n <= '1'; b_sclk <= '0'; b_mosi <= '0';
bench_idle(8);
report " violation expected properties that failed";
for v in 1 to 6 loop
clear_counts;
case v is
-- A select pulse carrying no SCLK edge at all.
when 1 =>
expect_p := P_EDGE;
vlab := "a select with no SCLK edge ";
b_cs_n <= '0'; bench_idle(6); b_cs_n <= '1'; bench_idle(GAP_C + 4);
-- A legal frame in which MOSI moves ON a capture edge.
when 2 =>
expect_p := P_STABLE;
vlab := "MOSI moving at a capture ";
bench_frame(4, HALF_C, 1, 0, 0, -1);
-- A legal frame with one half period of a single cycle.
when 3 =>
expect_p := P_HALF;
vlab := "a one-cycle half period ";
bench_frame(4, HALF_C, 0, 0, 0, 3);
-- A frame two edges short -- an even count, so SCLK still parks correctly.
when 4 =>
expect_p := P_FRAME;
vlab := "a frame two edges short ";
bench_frame(4, HALF_C, 0, 2, 0, -1);
-- A glitch on SCLK while the bus is idle. The phase opens with a COMPLETE
-- legal frame, and that is not padding: SCLK_PARKED's attempt begins at a
-- deassert, so without a transaction first there is no attempt for the
-- glitch to fail. An earlier version instead appended a short select pulse
-- to close the attempt, and that pulse carried no SCLK edge, so it failed
-- EDGE_AFTER_SELECT too and the matrix lost its diagonal.
when 5 =>
expect_p := P_PARKED;
vlab := "an SCLK glitch while idle ";
bench_frame(4, HALF_C, 0, 0, 0, -1);
bench_idle(4);
b_sclk <= not b_sclk; bench_idle(2);
b_sclk <= not b_sclk; bench_idle(6);
-- A complete frame, held selected far longer than MAXLAG.
when others =>
expect_p := P_REL;
vlab := "the select held past MAXLAG ";
bench_frame(4, HALF_C, 0, 0, MAXLAG + 4, -1);
end case;
for p in 0 to NPROPS - 1 loop
fired(p) := (c(p).fails /= 0);
if fired(NPROPS - 1 - p) then fs(p + 1) := '1'; else fs(p + 1) := '0'; end if;
end loop;
for p in 0 to NPROPS - 1 loop
if c(NPROPS - 1 - p).fails /= 0 then fs(p + 1) := '1'; else fs(p + 1) := '0'; end if;
end loop;
report " " & vlab & " P" & integer'image(expect_p + 1) & " " & fs;
for p in 0 to NPROPS - 1 loop
if p = expect_p and not fired(p) then
report " FAIL: violation " & integer'image(v) & " did not fail P" &
integer'image(p + 1) &
", so that property is either unreachable or wrong -- and a property that cannot be made to fail has been assumed, not verified";
errors <= errors + 1;
diag_bad := diag_bad + 1;
wait for 1 ns;
end if;
if p /= expect_p and fired(p) then
report " FAIL: violation " & integer'image(v) & " also failed P" &
integer'image(p + 1) &
", so the report names more than one suspect for one fault";
errors <= errors + 1;
matrix_bad := matrix_bad + 1;
wait for 1 ns;
end if;
end loop;
end loop;
report " 3. each of the six crafted violations failed EXACTLY ONE property: " &
integer'image(diag_bad) & " expected failures missing, " &
integer'image(matrix_bad) &
" unexpected. The antecedents were chosen to make that possible -- anchoring FRAME_COMPLETE to the first edge rather than to the select is what keeps an empty select pulse from failing two properties and naming neither cause";
-- ==============================================================
-- 4. AN ATTEMPT LEFT OPEN.
-- ==============================================================
clear_counts;
inc_before := c(P_EDGE).incomplete;
wait until falling_edge(clk);
b_cs_n <= '0'; -- assert, and then produce nothing at all
bench_idle(4); -- fewer than MAXLEAD, so the attempt is still open
wait until falling_edge(clk);
flush <= '1';
wait until falling_edge(clk);
flush <= '0';
wait until falling_edge(clk);
report " an attempt still open when the test ends:";
report " P1 passes ....... " & integer'image(c(P_EDGE).passes);
report " P1 fails ........ " & integer'image(c(P_EDGE).fails);
report " P1 incomplete ... " & integer'image(c(P_EDGE).incomplete - inc_before);
if (c(P_EDGE).incomplete - inc_before) = 0 then
report " FAIL: the open attempt was not booked as incomplete, so an attempt in flight at the end of a test disappears without trace";
errors <= errors + 1;
wait for 1 ns;
end if;
if c(P_EDGE).passes /= 0 or c(P_EDGE).fails /= 0 then
report " FAIL: the open attempt was scored as a pass or a fail; it is neither";
errors <= errors + 1;
wait for 1 ns;
end if;
report " 4. the attempt was booked as INCOMPLETE and appears in neither the pass column nor the fail column. That is the honest answer: the antecedent matched, the obligation was never settled, and a design that was about to violate the property is indistinguishable here from one that would have satisfied it. PSL does not report this either -- an attempt still open when a simulation ends prints nothing, in PSL and in SVA alike, which is the one place the verbose procedural version is strictly more informative than the concise declarative one";
wait for 1 ns;
if errors = 0 then
report "PASS: a property is not a rule evaluated at an instant -- it opens at one instant and is settled at another, and between them it is OPEN. So an attempt has FOUR outcomes and not two, and the two that are not failures are where a suite's silence comes from. Across " &
integer'image(legal_txns) &
" legal transactions in four modes and two widths, six of the seven properties passed with NON-ZERO pass counts, which is what stops the zero failure column from being a silence. The seventh property was attempted ZERO times and evaluated vacuously " &
integer'image(c(P_ONEBIT).vacuous) &
" times, because its antecedent needs a one-bit frame and this suite sends none; in PSL and in SVA alike that property passes on every clock edge for the life of the project, and in the declarative twin at the end of this file its `cover` directive stays silent for exactly the same reason. Six crafted violations then failed EXACTLY one property each, which is a result about the ANTECEDENTS as much as about the checks: anchoring FRAME_COMPLETE to the first edge rather than to the select is what stops an empty select pulse from failing two properties while naming neither cause, so choosing an antecedent is part of designing a diagnosis. And an attempt still in flight when the test ended was booked as INCOMPLETE -- in neither the pass column nor the fail column -- which is the one thing the declarative notation does not report at all"
severity note;
else
report "FAIL: " & integer'image(errors) & " error(s)" severity error;
end if;
done_sim <= true;
wait for 100 ns;
std.env.stop;
end process main;
end architecture tb;
-- =====================================================================================
-- THE DECLARATIVE SET'S OWN SIMULATION.
-- =====================================================================================
--
-- `spi_props_psl` carries the same six obligations as PSL directives, and nvc executes them.
-- They are not gated, for the reason in that file's header: an assertion that should not hold
-- must not be ARMED, and being armed is a property of a simulation rather than of a cycle.
--
-- So this top level runs the two phases in order and marks the boundary in its log:
--
-- LEGAL PHASE the real driver, four modes, two widths. Every PSL assertion must stay
-- silent, and the C_SELECT and C_FRAME cover directives must fire.
-- C_ONEBIT must NOT fire -- this suite sends no one-bit frames, and that
-- silence is the vacuity the procedural engine reports as `attempts = 0`.
--
-- VIOLATION PHASE two crafted violations, chosen because they exercise the two hardest
-- temporal shapes in the set: a frame two edges short (P4, a count
-- settled by a terminating event) and an SCLK glitch while the bus is
-- idle (P5, stability over an unbounded interval). Both must fire.
--
-- The regression runner checks three things about this run, which is what makes the claim
-- machine-checked rather than described: `PASS:` present, no assertion failure BEFORE the
-- PSL_LEGAL_PHASE_END marker, and at least one AFTER it. An assertion engine that stays quiet
-- on legal traffic and cannot be made to fire is indistinguishable from one that is switched
-- off, which is the same trap the procedural engine's `attempts` column exists to expose.
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
use work.spi_driver_pkg.all;
entity spi_psl_tb is
end entity spi_psl_tb;
architecture tb of spi_psl_tb is
constant LEAD_C : natural := 4;
constant HALF_C : natural := 3;
constant LAG_C : natural := 2;
constant GAP_C : natural := 3;
constant HALF_T : time := 5 ns;
signal clk : std_logic := '0';
signal rst_n : std_logic := '1';
signal done_sim : boolean := false;
signal start : std_logic := '0';
signal req : spi_req_t := (data => x"00001A5C",
nbits => to_unsigned(8, LEN_W),
cpol => '0',
cpha => '0',
lsb_first => '0',
fault => F_NONE);
signal busy, done : std_logic;
signal drv_rx : std_logic_vector(DW - 1 downto 0);
signal d_sclk, d_cs_n, d_mosi : std_logic;
signal sel_bench : boolean := false;
signal b_sclk : std_logic := '0';
signal b_cs_n : std_logic := '1';
signal b_mosi : std_logic := '0';
signal sclk, cs_n, mosi, miso : std_logic;
begin
sclk <= b_sclk when sel_bench else d_sclk;
cs_n <= b_cs_n when sel_bench else d_cs_n;
mosi <= b_mosi when sel_bench else d_mosi;
miso <= not mosi;
clk_gen : process is
begin
while not done_sim loop
wait for HALF_T;
clk <= not clk;
end loop;
wait;
end process clk_gen;
u_drv : entity work.spi_driver
generic map (LEAD => LEAD_C, HALF => HALF_C, LAG => LAG_C, GAP => GAP_C)
port map (clk => clk, rst_n => rst_n, start => start, req => req,
busy => busy, done => done, rx_data => drv_rx,
sclk => d_sclk, cs_n => d_cs_n, mosi => d_mosi, miso => miso);
u_psl : entity work.spi_props_psl
generic map (HALF => HALF_C, MAXLEAD => 16, MAXLAG => 8, LEN_W => LEN_W)
port map (clk => clk,
sclk => sclk, cs_n => cs_n, mosi => mosi,
cpol => req.cpol, cpha => req.cpha, len => req.nbits);
main : process is
procedure set_cfg (n : natural; pol : std_logic; pha : std_logic) is
begin
wait until falling_edge(clk);
req.nbits <= to_unsigned(n, LEN_W);
req.cpol <= pol;
req.cpha <= pha;
b_sclk <= pol;
for i in 0 to 5 loop wait until falling_edge(clk); end loop;
end procedure set_cfg;
procedure run_burst (ntxn : natural) is
variable k : natural := 0;
begin
k := 0;
wait until falling_edge(clk);
start <= '1';
while k < ntxn loop
wait until falling_edge(clk);
if done = '1' then
k := k + 1;
if k = ntxn then start <= '0'; end if;
end if;
end loop;
for i in 0 to GAP_C + LAG_C + 7 loop wait until falling_edge(clk); end loop;
end procedure run_burst;
procedure bench_idle (n : natural) is
begin
for i in 1 to n loop wait until falling_edge(clk); end loop;
end procedure bench_idle;
procedure bench_frame (n : natural; drop : natural) is
variable total : natural;
begin
b_cs_n <= '0';
b_mosi <= '0';
bench_idle(LEAD_C);
total := 2 * n - drop;
for e in 0 to total - 1 loop
b_sclk <= not b_sclk;
if (e mod 2) = 1 then b_mosi <= not b_mosi; end if;
bench_idle(HALF_C);
end loop;
bench_idle(LAG_C);
b_cs_n <= '1';
bench_idle(GAP_C + 4);
end procedure bench_frame;
variable pol, pha : std_logic;
variable txns : natural := 0;
begin
rst_n <= '1';
for i in 0 to 1 loop wait until falling_edge(clk); end loop;
rst_n <= '0';
for i in 0 to 3 loop wait until falling_edge(clk); end loop;
rst_n <= '1';
for i in 0 to 3 loop wait until falling_edge(clk); end loop;
-- ---------------- the legal phase ----------------
sel_bench <= false;
for iw in 0 to 1 loop
for ipol in 0 to 1 loop
for ipha in 0 to 1 loop
if ipol = 0 then pol := '0'; else pol := '1'; end if;
if ipha = 0 then pha := '0'; else pha := '1'; end if;
if iw = 0 then set_cfg(8, pol, pha); else set_cfg(4, pol, pha); end if;
run_burst(2);
txns := txns + 2;
end loop;
end loop;
end loop;
bench_idle(8);
report " PSL_LEGAL_PHASE_END after " & integer'image(txns) &
" legal transactions in four modes and two widths";
-- ---------------- the violation phase ----------------
set_cfg(4, '0', '0');
sel_bench <= true;
b_cs_n <= '1'; b_sclk <= '0'; b_mosi <= '0';
bench_idle(8);
-- A frame two edges short: P4_FRAME_COMPLETE must fire, because the count never
-- reaches 2N before the release.
bench_frame(4, 2);
-- A select pulse carrying no SCLK edge at all: both halves of P1 must fire -- P1A
-- because no edge arrives before the release, and P1B because none arrives inside the
-- bound either.
b_cs_n <= '0'; bench_idle(6); b_cs_n <= '1'; bench_idle(GAP_C + 4);
bench_idle(20);
report " PSL_VIOLATION_PHASE_END";
report "PASS: the declarative set ran as a real assertion engine. Over " &
integer'image(txns) &
" legal transactions in four modes and two widths the eight PSL assertions produced NOTHING, and their C_SELECT and C_FRAME cover directives fired while C_ONEBIT stayed silent -- which is the procedural engine's `attempts = 0` on P7, restated in the assertion language's own terms. Two crafted violations then made three of them fire: a frame two edges short against FRAME_COMPLETE, a count settled by a terminating event; and a select pulse with no SCLK edge against both halves of EDGE_AFTER_SELECT, one bounded by the release and one by a cycle count. Getting there took two corrections worth more than the properties themselves -- SERE forms that fired hundreds of times on known-good traffic, and a WEAK `before_` where the strong `before_!` was needed, which differ by one character and by whether the property means anything. Silence on legal traffic proves nothing on its own -- an assertion engine that cannot be made to fire is indistinguishable from one that is switched off -- which is why this run marks its phase boundary in the log and the regression requires failures after it and none before"
severity note;
done_sim <= true;
wait for 100 ns;
std.env.stop;
end process main;
end architecture tb;8. P5 Is Not In The PSL Set, And That Is A Finding
cs_deassert -> next ((sclk == cpol) until_ cs_assert) fired repeatedly on traffic the procedural engine passed. The reason is the mode sweep: the bench reconfigures CPOL between measurement windows, the driver re-parks SCLK a cycle later, and for that one cycle a correct master looks like a violation. Chapter 16.4 hit the same artefact and bracketed it by clearing counters.
A declarative assertion has nothing to clear. So the procedural engine measures P5 because its testbench can bracket the reconfiguration, and the declarative one does not claim to — which is the honest version of a limitation that is usually papered over with a disable iff whose real effect nobody checks.
9. The Same Properties As SVA
Reviewed code. Icarus implements no SVA at all, which is why the runnable set is procedural and the PSL set exists — see Chapter 16.3's toolchain note.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// Bound to the INTERFACE rather than to a component, so the properties apply to whatever is
// connected -- including the next driver somebody writes. `spi_props_sva` takes the derived
// events as inputs for the same reason the PSL entity does: an assertion language removes the
// attempt bookkeeping, not the modelling, and where the derived events are computed decides
// what the properties can say.
module spi_props_sva #(
parameter int HALF = 3,
parameter int MAXLEAD = 16,
parameter int MAXLAG = 8
) (
input logic clk, rst_n,
input logic cs_assert, cs_deassert, edge_in_txn, cap_in_txn, first_edge, frame_done,
input logic sclk, mosi, cpol, frame_ok
);
default clocking cb @(posedge clk); endclocking
default disable iff (!rst_n);
// P1 -- bounded existence, as TWO properties, for the same reason the PSL version is split:
// one says "before the release" and the other says "within the bound", and a failure then
// names which obligation was missed.
//
// `s_until` is the STRONG form and the choice is the whole property: weak `until` is
// satisfied by a design that simply stops, which is precisely the select-with-no-edges case.
property p1a_edge_before_release;
cs_assert |=> (!cs_deassert) s_until edge_in_txn;
endproperty
property p1b_edge_within_bound;
cs_assert |-> ##[1:MAXLEAD] edge_in_txn;
endproperty
// P2 -- the stability window. Split, so a failure says WHICH side moved.
property p2a_stable_before; cap_in_txn |-> $stable(mosi); endproperty
property p2b_stable_after; cap_in_txn |=> $stable(mosi); endproperty
// P3 -- a multi-cycle consequent, and the implication is NON-OVERLAPPING: the edge itself is
// the change, so the obligation starts on the following cycle. Written with `|->` every
// attempt fails immediately, which looks like a catastrophic design bug and is a misplaced
// operator.
property p3_half_stable;
edge_in_txn |=> ($stable(sclk))[*HALF-1];
endproperty
// P4 -- a count settled by a terminating event, anchored to the FIRST EDGE and not to the
// select. See section 3.
property p4_frame_complete;
first_edge |=> (!cs_deassert) s_until_with frame_ok;
endproperty
// P5 -- an unbounded interval. WEAK `until` is correct here and the difference from P1 is
// worth stating: the obligation is "SCLK stays parked for as long as the bus is idle", and a
// simulation that ends while the bus is still idle has not violated it. This is also the
// property whose attempt can be open at the end of a run -- and neither SVA nor PSL reports
// that, which is why the procedural engine keeps an `incomplete` column.
property p5_sclk_parked;
cs_deassert |=> (sclk == cpol) until cs_assert;
endproperty
// P6 -- bounded liveness the other way round.
property p6_release_after_frame;
frame_done |-> ##[1:MAXLAG] cs_deassert;
endproperty
a_p1a: assert property (p1a_edge_before_release);
a_p1b: assert property (p1b_edge_within_bound);
a_p2a: assert property (p2a_stable_before);
a_p2b: assert property (p2b_stable_after);
a_p3: assert property (p3_half_stable);
a_p4: assert property (p4_frame_complete);
a_p5: assert property (p5_sclk_parked);
a_p6: assert property (p6_release_after_frame);
// THE ANTECEDENT COVERS, which are the `attempts` column in assertion-language form. Without
// these, every assertion above can pass vacuously for the life of the project -- which is
// exactly what P7 does in the table in section 4.
c_select: cover property (cs_assert);
c_first_edge: cover property (first_edge);
c_capture: cover property (cap_in_txn);
c_edge: cover property (edge_in_txn);
c_frame_done: cover property (frame_done);
c_release: cover property (cs_deassert);
// And the one that is expected to stay EMPTY for this suite, declared so that its emptiness
// is a recorded result rather than an absence nobody looked for.
c_one_bit: cover property (cs_assert && (len == 1));
endmodule
// A bind, so nothing in the design or the environment has to know the checker exists.
bind spi_dut spi_props_sva #(.HALF(3), .MAXLEAD(16), .MAXLAG(8)) u_sva (.*);10. Why a Verification Engineer Cares
Because the vacuous pass is the single most common way an assertion-based flow produces false confidence, and it is invisible in every report that shows only pass and fail.
The habit that prevents it is one line per property: cover property on the antecedent. It costs nothing, it is the assertion-language spelling of Chapter 16.1's exercised counter, and a suite with four thousand assertions and no antecedent covers has no idea how many of them are reachable.
The second habit is about operator strength. Weak and strong temporal operators differ by one character, the weak one is the default spelling, and the weak form of a liveness property is satisfied by a design that simply stops. Every until, eventually and before in a property set is a place to ask which one was meant.
11. Why an FPGA or ASIC Engineer Cares
Because these seven properties are the specification of your master's pin behaviour in a form a formal tool can consume, and the shapes matter for that.
P1 and P6 are bounded-liveness properties, and a formal tool will prove or disprove them; P5's unbounded form usually needs a fairness assumption or a bound before it is provable. Knowing which of your requirements is a safety property and which is a liveness property is the difference between a formal run that closes and one that returns inconclusive.
And P2 is a setup-window requirement in disguise — MOSI does not move in the cycle before, at, or after a capture edge is the simulation-level statement of a hold and setup margin. Chapter 16.5 showed that a data monitor is blind to its violation.
12. Failure Signature — Four Thousand Green Assertions
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
Symptom a block has 4,000 assertions and a clean regression. A bug
escapes to the lab on a path an assertion covers.
What happened the assertion's antecedent was never true in this
configuration. It passed vacuously on every clock edge for
eleven months, which is the maximum score SVA can award a
property that was never evaluated.
What would have a `cover property` on the antecedent, and a signoff step
caught it that treats an uncovered antecedent as an unverified
property rather than as a coverage curiosity.
The tell the assertion's antecedent contains a configuration term --
a mode, a width, an enable. Antecedents built only from
protocol events are reached by any traffic; antecedents
qualified by configuration are reached only by the
configurations somebody remembered to run.13. Common Misconceptions
"A passing assertion means the property holds." Only if the antecedent was reached. A property whose antecedent is never true passes on every clock edge, forever, and reports the same green line as one that was tested sixteen thousand times.
"An attempt is either satisfied or violated." It can also be open when the simulation ends. Neither SVA nor PSL reports that, and the design that was one cycle away from violating the property produces exactly the same output as the one that would have satisfied it.
"until and s_until are stylistic variants." The weak form does not require its terminating condition to occur, so a liveness property written with it is satisfied by a design that stops. This chapter's PSL set passed a select-with-no-edges until before_ was changed to before!.
"Assertions replace the modelling." They remove the attempt bookkeeping. The derived events — cs_assert, first_edge, capture, frame_done — still have to be computed somewhere, and a property built on a badly chosen derived signal is wrong in a way no amount of temporal-operator care can fix.
"A property should be written as one expression if possible." Two of the seven here are better as two directives each, and not because of a tool limitation: a property that mixes an immediate obligation with a temporal one cannot say which half failed, and one that combines a bound with an ordering cannot say which was missed.
"disable iff is how you scope a property to when it matters." Sometimes. Chapter 17.2 measures what happens when its condition overlaps the antecedent, and the answer is a property that reports nothing on any stimulus and is indistinguishable in any report from one that works.
14. Reason It Through
P7 reports attempts = 0 and vacuous = 2. What is the difference between those two numbers, and which one would an SVA report show?
attempts counts evaluations where the antecedent matched; vacuous counts evaluations where it did not. SVA shows neither by default — it shows a pass. The vacuous count proves the property was looked at, which distinguishes "the property is in the build and unreachable" from "the property is not in the build at all". Both are failures; they are different failures.
Why is P4 anchored to the first edge rather than to the select?
So that a select pulse carrying no edges fails P1 alone. Anchored to the select, P4 also fails, and a reader of the report sees two broken properties and no statement of the cause. The antecedent is a decision about the shape of a future bug report.
P3 is written with a non-overlapping implication. What happens with an overlapping one?
Every attempt fails immediately, because the edge that forms the antecedent is the change the consequent forbids. The report looks like a catastrophic design failure and the cause is one character.
Why did gating the PSL properties with an enable signal not work?
Because an attempt opened while the gate was up outlives the gate falling. P5's obligation is unbounded and P4's and P6's span tens of cycles, so all three were still in flight when the violation phase began and fired on traffic they had been switched off for. If a property should not hold, it should not be armed — and armed is a property of the simulation, not of a cycle.
The SCLK-glitch violation initially failed two properties. Was the checker wrong?
No — the stimulus was. Closing P5's attempt needed a prior transaction, and the short select pulse used to provide one carried no SCLK edge, so it failed P1 too. An off-diagonal entry in a violation matrix usually means the test is wrong rather than the checker, which is the reason to demand the diagonal in the first place.
15. Understanding Check
16. Summary
A property opens at one instant and is settled at another, so an attempt has four outcomes and not two, and the two that are not failures are where a suite's silence comes from. Seven SPI properties, seven temporal shapes: across sixteen legal transactions in four modes and two widths, six of them passed with non-zero pass counts and the seventh was attempted zero times — its antecedent needs a one-bit frame and this suite sends none, so in SVA it passes on every clock edge forever and a pass/fail report cannot tell it from a property that works. Six crafted violations then failed exactly one property each, which is a result about the antecedents as much as about the checks. An attempt left in flight at the end of a test was booked as incomplete — in neither column — which is the one outcome no assertion language reports. And the same six obligations ran a second time as PSL directives executed by nvc, silent across the whole legal phase with their cover directives firing, after three corrections that were worth more than the properties themselves: SERE forms that fired on known-good traffic, a weak operator where a strong one was needed, and a property that had to be split because it mixed an immediate obligation with a temporal one.
17. What Comes Next
The properties are written. Chapter 17.2 writes one of them five ways, and measures what each version reports on the same faults — because four of the five are defective and a clean regression cannot tell them apart.
Continue learning
Related tutorials
- Related topic
Mode-Aware Checking and Assertion Pitfalls
One obligation written five ways. On legal traffic all five report zero, which is why four of them survive review. A checker clocked on SCLK is unfalsifiable rather than merely under-exercised, and a disable-iff that overlaps its antecedent reports nothing on any stimulus.
- Related topic
UCIe Assertions
Writing SVA that describes UCIe architectural contracts rather than implementation details — triggers that mean the right event, reset and disable scoping that does not sleep through the bug, overlapping transactions that outgrow local variables, liveness with its assumptions written down, and the four wrong properties that pass a regression while checking nothing.
- Related topic
CXL Assertions
An assertion that never fires is indistinguishable from one that cannot. This chapter builds sampling regions, vacuity, gating scope, response windows, implication offsets, evaluation cost, threading, severity, proof depth and the assembled sign-off.
- Related topic
Writing UART Assertions for TX, RX and FIFOs
The transmitter and FIFO property checkers written in three languages and bound to published designs, the sampling pitfalls that make an assertion argue with a correct design, and what each toolchain will actually run.