UART · Module 15
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.
Chapter 15.1 produced a catalogue of sixteen properties. This chapter writes them, binds them to designs this curriculum has already published and verified, and runs them.
The interesting part is not the code. It is that four of the properties were wrong on the first attempt, every one of them fired against a correct design, and each was wrong for a different reason worth knowing.
1. A Checker Watches the Interface
Every input to both checkers is a port of the design. Not a pointer, not a state register, not a memory word.
That is not minimalism. A checker that read the FIFO's write pointer in order to predict its level would be re-deriving the level from the state that produced it, and it would agree with a broken design as readily as a correct one. The same discipline Chapter 14.2 §3 imposed on the monitor applies here for the same reason.
It also makes the checker bindable: any FIFO with this interface can be checked by it, which is what turns a property file into something reusable rather than a one-off.
2. The FIFO Checker
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// uart_fifo_assert_v — the FIFO property checker of Chapter 15.2,
// in Verilog-2001
//
// NOT SYNTHESIZABLE. This is an observer: it is bound alongside a FIFO,
// watches its interface, and reports whenever an invariant is violated.
//
// IT WATCHES THE INTERFACE, NOT THE IMPLEMENTATION. Every input is a port
// of the FIFO, not a pointer or a memory word inside it. That is what makes
// it bindable to any conforming FIFO, and it is what stops it agreeing with
// a broken one -- a checker that read the write pointer to predict the level
// would be re-deriving the level from the same state that produced it.
//
// VERILOG-2001 HAS NO ASSERTIONS AT ALL. There is no `assert`, no
// `property`, no `sequence` and no `cover`. What a SystemVerilog concurrent
// assertion expresses in one line is written here as an explicit comparison
// inside a clocked block with a counter beside it. The properties are the
// same properties; only the notation is poorer, and the poverty is worth
// seeing -- it is why SVA exists.
//
// EACH PROPERTY HAS AN ID. A checker that reports "an assertion failed" has
// told you almost nothing; one that reports P4 has told you the accounting
// is wrong rather than the flags.
//===========================================================================
`timescale 1ns/1ps
module uart_fifo_assert_v #(
parameter DEPTH = 16,
parameter LVL_W = 5 // width of level_i; holds 0..DEPTH
) (
input wire clk,
input wire rst_n,
// the FIFO's interface -- every one of these is a port of the DUT
input wire push_i,
input wire pop_i,
input wire empty_i,
input wire full_i,
input wire [LVL_W-1:0] level_i,
input wire overflow_evt_i,
input wire underflow_evt_i,
output reg [31:0] n_clocks, // clocks on which properties were evaluated
output reg [31:0] n_fail, // total violations
output reg [7:0] fail_mask // bit i set => property i+1 fired
);
// Per-property counters. Named rather than numbered in the source so the
// report reads as English; numbered in fail_mask so a testbench can assert
// on exactly which one fired.
reg [31:0] p1_level_range; // level never exceeds DEPTH
reg [31:0] p2_empty_iff; // empty <-> level == 0
reg [31:0] p3_full_iff; // full <-> level == DEPTH
reg [31:0] p4_accounting; // level advances by accepted pushes/pops
reg [31:0] p5_overflow; // overflow_evt <-> push while full
reg [31:0] p6_underflow; // underflow_evt <-> pop while empty
reg [31:0] p7_not_both; // empty and full never together
reg [31:0] p8_step_one; // level moves by at most one per clock
reg [LVL_W-1:0] level_q;
reg have_prev;
// What the level MUST become, computed from the interface alone.
//
// THE SAMPLING TRAP, and it is worth being explicit because the first
// version of this file got it wrong and fired 3,078 times against a
// correct FIFO.
//
// At a rising edge, `level_i` is still the level from BEFORE that edge --
// the DUT's non-blocking update has not been applied yet. So the level
// observed at edge N must be compared against the level observed at edge
// N-1 plus the operations that were accepted at edge N-1, NOT plus the
// operations being accepted right now. Comparing against the current
// cycle's push and pop is off by exactly one clock, and it is wrong on
// every cycle where anything happens -- which is why it looked like a
// catastrophic DUT failure rather than a checker bug.
// THE ACCEPTANCE RULE, and getting it wrong is how a checker ends up
// arguing with a correct design.
//
// The obvious rule is `push_i && !full_i`. That is NOT what the FIFO of
// Chapter 10.2 implements, and the difference is deliberate: a push into
// a full FIFO is accepted when a pop frees an entry on the SAME cycle,
// because the simpler rule drops a byte at exactly the boundary where a
// consumer is keeping up (10.2 section 5).
//
// The first version of this checker encoded the simpler rule and fired 41
// times during a legal random soak. Nothing was wrong with the FIFO. The
// checker was asserting a specification the design had deliberately not
// been written to.
//
// This is the failure mode to watch for in property work: not a checker
// that is too weak, but one that is confidently checking the wrong thing.
wire pop_ok = pop_i && !empty_i;
wire push_ok = push_i && (!full_i || pop_ok);
// A rejected operation is what raises the event output.
wire ovf_exp = push_i && !push_ok;
wire unf_exp = pop_i && !pop_ok;
reg push_ok_q, pop_ok_q;
reg ovf_exp_q, unf_exp_q;
// Verilog-2001 has no signed arithmetic conveniences worth using here, so
// the expected next level is built by cases rather than as a sum.
reg [LVL_W:0] exp_next;
always @* begin
exp_next = {1'b0, level_q};
if (push_ok_q && !pop_ok_q) exp_next = exp_next + 1'b1;
if (pop_ok_q && !push_ok_q) exp_next = exp_next - 1'b1;
// both accepted in the same cycle leaves the level unchanged
end
task bump;
input [7:0] id;
input [8*40-1:0] name;
begin
n_fail = n_fail + 1;
fail_mask = fail_mask | (8'b1 << (id - 1));
$display(" [assert] P%0d violated at %0t : %0s", id, $time, name);
end
endtask
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
n_clocks <= 32'd0; n_fail <= 32'd0; fail_mask <= 8'd0;
p1_level_range <= 32'd0; p2_empty_iff <= 32'd0;
p3_full_iff <= 32'd0; p4_accounting <= 32'd0;
p5_overflow <= 32'd0; p6_underflow <= 32'd0;
p7_not_both <= 32'd0; p8_step_one <= 32'd0;
level_q <= {LVL_W{1'b0}};
push_ok_q <= 1'b0;
pop_ok_q <= 1'b0;
ovf_exp_q <= 1'b0;
unf_exp_q <= 1'b0;
have_prev <= 1'b0;
end else begin
n_clocks <= n_clocks + 1;
// ---- P1: the level is within range -------------------------
if (level_i > DEPTH) begin
p1_level_range <= p1_level_range + 1; bump(8'd1, "level exceeds DEPTH");
end
// ---- P2 / P3: the flags are functions of the level ----------
// Written as <-> in both directions on purpose. A one-directional
// check ("if empty then level is 0") passes a FIFO that never
// asserts empty at all.
if (empty_i !== (level_i == 0)) begin
p2_empty_iff <= p2_empty_iff + 1; bump(8'd2, "empty does not match level==0");
end
if (full_i !== (level_i == DEPTH)) begin
p3_full_iff <= p3_full_iff + 1; bump(8'd3, "full does not match level==DEPTH");
end
// ---- P7: and they are mutually exclusive --------------------
if (empty_i && full_i) begin
p7_not_both <= p7_not_both + 1; bump(8'd7, "empty and full asserted together");
end
// ---- P4: the accounting property ----------------------------
// THE property of a FIFO. Everything else is a flag; this is the
// claim that nothing is lost or invented.
if (have_prev && (level_i !== exp_next[LVL_W-1:0])) begin
p4_accounting <= p4_accounting + 1; bump(8'd4, "level does not follow push/pop");
end
// ---- P8: and it moves smoothly ------------------------------
if (have_prev && (level_i > level_q + 1 || level_q > level_i + 1)) begin
p8_step_one <= p8_step_one + 1; bump(8'd8, "level moved by more than one");
end
// ---- P5 / P6: the event outputs ------------------------------
// The DUT registers these, so the event observed at this edge
// reports the operation that was rejected at the PREVIOUS one.
// Comparing against the current cycle is the same off-by-one that
// broke P4, arriving from the other direction.
if (overflow_evt_i !== ovf_exp_q) begin
p5_overflow <= p5_overflow + 1; bump(8'd5, "overflow_evt does not match push&&full");
end
if (underflow_evt_i !== unf_exp_q) begin
p6_underflow <= p6_underflow + 1; bump(8'd6, "underflow_evt does not match pop&&empty");
end
level_q <= level_i;
push_ok_q <= push_ok;
pop_ok_q <= pop_ok;
ovf_exp_q <= ovf_exp;
unf_exp_q <= unf_exp;
have_prev <= 1'b1;
end
end
endmoduleThe SystemVerilog version is the same properties with logic, int, and an immediate assertion beside each counter — which is as much as this toolchain will run. §4 has the details.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// uart_fifo_assert — the FIFO property checker of Chapter 15.2,
// in SystemVerilog
//
// NOT SYNTHESIZABLE. This is an observer: it is bound alongside a FIFO,
// watches its interface, and reports whenever an invariant is violated.
//
// IT WATCHES THE INTERFACE, NOT THE IMPLEMENTATION. Every input is a port
// of the FIFO, not a pointer or a memory word inside it. That is what makes
// it bindable to any conforming FIFO, and it is what stops it agreeing with
// a broken one -- a checker that read the write pointer to predict the level
// would be re-deriving the level from the same state that produced it.
//
// SYSTEMSYSTEMVERILOG HAS SVA, AND THIS FILE MOSTLY CANNOT USE IT. There is no `assert`, no
// `property`, no `sequence` and no `cover`. What a SystemVerilog concurrent
// assertion expresses in one line is written here as an explicit comparison
// inside a clocked block with a counter beside it. The properties are the
// same properties; only the notation is poorer, and the poverty is worth
// seeing -- it is why SVA exists.
//
//
// WHAT THIS FILE WOULD LIKE TO SAY, AND WHY IT DOES NOT.
//
// The natural SystemVerilog for P2 is one line:
//
// assert property (@(posedge clk) disable iff (!rst_n)
// empty_i == (level_i == 0));
//
// Icarus Verilog 13.0 rejects it. Not the `disable iff`, not the
// implication -- the whole construct:
//
// sorry: concurrent_assertion_item not supported.
//
// Probed, not assumed: an inline property, a named property, a property
// with no `disable iff` and a purely boolean property were each tried and
// each refused. So the properties here are IMMEDIATE assertions inside a
// clocked block, which Icarus does run, with a counter beside each one.
//
// That is a real loss and worth naming. An immediate assertion cannot
// express a temporal relationship -- `a |=> b` has no equivalent -- so any
// property spanning more than one cycle has to be hand-built out of
// registered history, which is what the `_q` signals below are. The
// properties are the same properties. The notation is poorer, and on this
// toolchain it is the only notation that executes.
// EACH PROPERTY HAS AN ID. A checker that reports "an assertion failed" has
// told you almost nothing; one that reports P4 has told you the accounting
// is wrong rather than the flags.
//===========================================================================
`timescale 1ns/1ps
module uart_fifo_assert #(
parameter DEPTH = 16,
parameter LVL_W = 5 // width of level_i; holds 0..DEPTH
) (
input wire clk,
input wire rst_n,
// the FIFO's interface -- every one of these is a port of the DUT
input wire push_i,
input wire pop_i,
input wire empty_i,
input wire full_i,
input wire [LVL_W-1:0] level_i,
input wire overflow_evt_i,
input wire underflow_evt_i,
output logic [31:0] n_clocks, // clocks on which properties were evaluated
output logic [31:0] n_fail, // total violations
output logic [7:0] fail_mask // bit i set => property i+1 fired
);
// Per-property counters. Named rather than numbered in the source so the
// report reads as English; numbered in fail_mask so a testbench can assert
// on exactly which one fired.
logic [31:0] p1_level_range; // level never exceeds DEPTH
logic [31:0] p2_empty_iff; // empty <-> level == 0
logic [31:0] p3_full_iff; // full <-> level == DEPTH
logic [31:0] p4_accounting; // level advances by accepted pushes/pops
logic [31:0] p5_overflow; // overflow_evt <-> push while full
logic [31:0] p6_underflow; // underflow_evt <-> pop while empty
logic [31:0] p7_not_both; // empty and full never together
logic [31:0] p8_step_one; // level moves by at most one per clock
logic [LVL_W-1:0] level_q;
logic have_prev;
// What the level MUST become, computed from the interface alone.
//
// THE SAMPLING TRAP, and it is worth being explicit because the first
// version of this file got it wrong and fired 3,078 times against a
// correct FIFO.
//
// At a rising edge, `level_i` is still the level from BEFORE that edge --
// the DUT's non-blocking update has not been applied yet. So the level
// observed at edge N must be compared against the level observed at edge
// N-1 plus the operations that were accepted at edge N-1, NOT plus the
// operations being accepted right now. Comparing against the current
// cycle's push and pop is off by exactly one clock, and it is wrong on
// every cycle where anything happens -- which is why it looked like a
// catastrophic DUT failure rather than a checker bug.
// THE ACCEPTANCE RULE, and getting it wrong is how a checker ends up
// arguing with a correct design.
//
// The obvious rule is `push_i && !full_i`. That is NOT what the FIFO of
// Chapter 10.2 implements, and the difference is deliberate: a push into
// a full FIFO is accepted when a pop frees an entry on the SAME cycle,
// because the simpler rule drops a byte at exactly the boundary where a
// consumer is keeping up (10.2 section 5).
//
// The first version of this checker encoded the simpler rule and fired 41
// times during a legal random soak. Nothing was wrong with the FIFO. The
// checker was asserting a specification the design had deliberately not
// been written to.
//
// This is the failure mode to watch for in property work: not a checker
// that is too weak, but one that is confidently checking the wrong thing.
wire pop_ok = pop_i && !empty_i;
wire push_ok = push_i && (!full_i || pop_ok);
// A rejected operation is what raises the event output.
wire ovf_exp = push_i && !push_ok;
wire unf_exp = pop_i && !pop_ok;
logic push_ok_q, pop_ok_q;
logic ovf_exp_q, unf_exp_q;
// Verilog-2001 has no signed arithmetic conveniences worth using here, so
// the expected next level is built by cases rather than as a sum.
logic [LVL_W:0] exp_next;
always @* begin
exp_next = {1'b0, level_q};
if (push_ok_q && !pop_ok_q) exp_next = exp_next + 1'b1;
if (pop_ok_q && !push_ok_q) exp_next = exp_next - 1'b1;
// both accepted in the same cycle leaves the level unchanged
end
task bump;
input [7:0] id;
input [8*40-1:0] name;
begin
n_fail++;
fail_mask = fail_mask | (8'b1 << (id - 1));
// An IMMEDIATE assertion, which Icarus does execute. It reports at
// the instant of the violation; the counter is what a testbench
// can make an arithmetic claim about afterwards.
assert (0) else $error("property %0d violated", id);
$display(" [assert] P%0d violated at %0t : %0s", id, $time, name);
end
endtask
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
n_clocks <= 32'd0; n_fail <= 32'd0; fail_mask <= 8'd0;
p1_level_range <= 32'd0; p2_empty_iff <= 32'd0;
p3_full_iff <= 32'd0; p4_accounting <= 32'd0;
p5_overflow <= 32'd0; p6_underflow <= 32'd0;
p7_not_both <= 32'd0; p8_step_one <= 32'd0;
level_q <= {LVL_W{1'b0}};
push_ok_q <= 1'b0;
pop_ok_q <= 1'b0;
ovf_exp_q <= 1'b0;
unf_exp_q <= 1'b0;
have_prev <= 1'b0;
end else begin
n_clocks <= n_clocks + 1;
// ---- P1: the level is within range -------------------------
if (level_i > DEPTH) begin
p1_level_range <= p1_level_range + 1; bump(8'd1, "level exceeds DEPTH");
end
// ---- P2 / P3: the flags are functions of the level ----------
// Written as <-> in both directions on purpose. A one-directional
// check ("if empty then level is 0") passes a FIFO that never
// asserts empty at all.
if (empty_i !== (level_i == 0)) begin
p2_empty_iff <= p2_empty_iff + 1; bump(8'd2, "empty does not match level==0");
end
if (full_i !== (level_i == DEPTH)) begin
p3_full_iff <= p3_full_iff + 1; bump(8'd3, "full does not match level==DEPTH");
end
// ---- P7: and they are mutually exclusive --------------------
if (empty_i && full_i) begin
p7_not_both <= p7_not_both + 1; bump(8'd7, "empty and full asserted together");
end
// ---- P4: the accounting property ----------------------------
// THE property of a FIFO. Everything else is a flag; this is the
// claim that nothing is lost or invented.
if (have_prev && (level_i !== exp_next[LVL_W-1:0])) begin
p4_accounting <= p4_accounting + 1; bump(8'd4, "level does not follow push/pop");
end
// ---- P8: and it moves smoothly ------------------------------
if (have_prev && (level_i > level_q + 1 || level_q > level_i + 1)) begin
p8_step_one <= p8_step_one + 1; bump(8'd8, "level moved by more than one");
end
// ---- P5 / P6: the event outputs ------------------------------
// The DUT registers these, so the event observed at this edge
// reports the operation that was rejected at the PREVIOUS one.
// Comparing against the current cycle is the same off-by-one that
// broke P4, arriving from the other direction.
if (overflow_evt_i !== ovf_exp_q) begin
p5_overflow <= p5_overflow + 1; bump(8'd5, "overflow_evt does not match push&&full");
end
if (underflow_evt_i !== unf_exp_q) begin
p6_underflow <= p6_underflow + 1; bump(8'd6, "underflow_evt does not match pop&&empty");
end
level_q <= level_i;
push_ok_q <= push_ok;
pop_ok_q <= pop_ok;
ovf_exp_q <= ovf_exp;
unf_exp_q <= unf_exp;
have_prev <= 1'b1;
end
end
endmodule3. The Transmitter Checker
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// uart_tx_assert_v — the transmitter property checker of Chapter 15.2,
// in Verilog-2001
//
// NOT SYNTHESIZABLE. Bound alongside a UART transmitter, it watches the
// interface and reports whenever a protocol invariant is violated.
//
// WHAT BELONGS HERE AND WHAT DOES NOT (Chapter 15.1).
//
// A property earns its place when it holds CONTINUOUSLY and a scoreboard
// would not notice it being broken. "The byte 0xA5 came out as 0xA5" is a
// scoreboard's job -- it is a fact about one transaction, checked once, at
// the end. "The line is at MARK whenever the transmitter is idle" is a
// property: it must be true on every clock of the entire run, there is no
// transaction to attach it to, and a scoreboard comparing delivered bytes
// would never see it fail.
//
// The eight below are all of the second kind. Not one of them checks a data
// value, and that is deliberate -- the data path already has a reference
// model in Chapter 14.5.
//
// VERILOG-2001 HAS NO ASSERTIONS. What SystemVerilog writes as
//
// assert property (@(posedge clk) disable iff (!rst_n)
// !tx_busy_o |-> tx_o == 1'b1);
//
// is written here as an `if` and a counter. The property is identical; the
// notation is poorer, and the difference is the whole argument for SVA.
//===========================================================================
`timescale 1ns/1ps
module uart_tx_assert_v #(
parameter DATA_W = 8
) (
input wire clk,
input wire rst_n,
// the transmitter's interface -- all ports of the DUT
input wire baud_tick_i,
input wire tx_valid_i,
input wire tx_ready_i,
input wire tx_busy_i,
input wire tx_line_i,
input wire [1:0] parity_mode_i, // 0 none, 1 even, 2 odd, 3 mark
output reg [31:0] n_clocks,
output reg [31:0] n_frames, // frames seen start to finish
output reg [31:0] n_fail,
output reg [7:0] fail_mask // bit i set => property i+1 fired
);
localparam P_NONE = 2'd0;
// Expected bit intervals in a frame: start + data + optional parity + stop
wire [5:0] exp_bits = 6'd1 + DATA_W[5:0]
+ ((parity_mode_i != P_NONE) ? 6'd1 : 6'd0) + 6'd1;
reg busy_q, ready_q, line_q;
reg have_prev;
reg [5:0] tick_cnt; // baud ticks elapsed in this frame
reg in_frame;
reg hs_q; // a handshake happened last cycle
reg tick_q; // a baud tick happened last cycle
wire handshake = tx_valid_i && tx_ready_i;
task bump;
input [7:0] id;
input [8*46-1:0] name;
begin
n_fail = n_fail + 1;
fail_mask = fail_mask | (8'b1 << (id - 1));
$display(" [assert] T%0d violated at %0t : %0s", id, $time, name);
end
endtask
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
n_clocks <= 32'd0; n_frames <= 32'd0; n_fail <= 32'd0;
fail_mask <= 8'd0;
busy_q <= 1'b0; ready_q <= 1'b0; line_q <= 1'b1;
have_prev <= 1'b0; tick_cnt <= 6'd0; in_frame <= 1'b0;
hs_q <= 1'b0;
end else begin
n_clocks <= n_clocks + 1;
// ---- T1: the idle line is MARK ------------------------------
// The single most valuable property in the file. A transmitter
// that leaves the line low when idle looks like a permanent break
// to the far end, and no scoreboard comparing delivered bytes
// would ever notice -- because nothing is delivered.
// `in_frame` is excluded as well as busy: between the handshake
// and busy rising there is a cycle in which the transmitter has
// accepted a byte but has not started driving it, and the line is
// legitimately still at MARK-or-transitioning.
if (!tx_busy_i && !hs_q && !in_frame && tx_line_i !== 1'b1)
bump(8'd1, "line is not MARK while idle");
// ---- T2: no two acceptances back to back ---------------------
//
// NOT "ready and busy are mutually exclusive". That was the first
// draft and it fired 189 times against a correct transmitter,
// because this transmitter asserts ready during the STOP interval
// ON PURPOSE -- that is what lets frames follow each other with no
// gap (Chapter 7.4). Ready and busy overlap by design.
//
// The real interface contract is narrower: having accepted a byte,
// the transmitter must not accept another on the next cycle.
if (hs_q && tx_ready_i)
bump(8'd2, "ready still high the cycle after an acceptance");
// ---- T3: a handshake is followed by busy --------------------
if (hs_q && !tx_busy_i)
bump(8'd3, "busy did not rise after an accepted handshake");
// ---- T4: ready comes back only near the END of a frame -------
//
// Also not "ready stays low for the whole frame". The useful
// version states WHEN it may return: not before the frame has
// reached its final bit interval. That permits the back-to-back
// handoff and still catches a transmitter that offers capacity
// it does not have.
if (in_frame && tx_busy_i && tx_ready_i && (tick_cnt + 1 < exp_bits))
bump(8'd4, "ready returned before the final bit interval");
// ---- T5: the frame is exactly exp_bits baud intervals --------
// The property a scoreboard cannot see at all: it compares bytes,
// and a frame one bit too long delivers the right byte.
if (in_frame && tx_busy_i && baud_tick_i && tick_cnt > exp_bits)
bump(8'd5, "frame ran past its expected bit count");
// ---- T6: the frame opens with SPACE --------------------------
//
// Checked at the FIRST BAUD TICK of the frame, not on the cycle
// after the handshake. The transmitter is a baud-paced state
// machine and registers its output: the line does not move until
// the next tick. Checking one clock after the handshake fired 41
// times against a correct design and was measuring the clock
// rather than the protocol.
// Measured, not assumed: the transmitter transitions out of IDLE
// at tick 0 and its registered output follows, so the start bit
// is on the wire at tick 1. Checking at tick 0 fired 40 times
// against a correct design.
if (in_frame && tx_busy_i && baud_tick_i && tick_cnt == 1
&& tx_line_i !== 1'b0)
bump(8'd6, "start bit is not SPACE at the first driven tick");
// ---- T7: the line only moves on a baud tick ------------------
// Strictly: on the cycle AFTER a tick, since the DUT registers.
if (have_prev && tx_busy_i && (tx_line_i !== line_q) && !tick_q)
bump(8'd7, "line changed without a baud tick");
// ---- T8: busy does not drop mid-frame ------------------------
if (busy_q && !tx_busy_i && in_frame && tick_cnt < exp_bits - 1)
bump(8'd8, "busy dropped before the frame finished");
// ---- frame bookkeeping ---------------------------------------
if (handshake) begin
in_frame <= 1'b1;
tick_cnt <= 6'd0;
end else if (in_frame && baud_tick_i && tx_busy_i) begin
tick_cnt <= tick_cnt + 1'b1;
end
if (busy_q && !tx_busy_i && in_frame) begin
in_frame <= 1'b0;
n_frames <= n_frames + 1;
end
busy_q <= tx_busy_i;
ready_q <= tx_ready_i;
line_q <= tx_line_i;
tick_q <= baud_tick_i;
hs_q <= handshake;
have_prev <= 1'b1;
end
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// uart_tx_assert — the transmitter property checker of Chapter 15.2,
// in SystemVerilog
//
// NOT SYNTHESIZABLE. Bound alongside a UART transmitter, it watches the
// interface and reports whenever a protocol invariant is violated.
//
// WHAT BELONGS HERE AND WHAT DOES NOT (Chapter 15.1).
//
// A property earns its place when it holds CONTINUOUSLY and a scoreboard
// would not notice it being broken. "The byte 0xA5 came out as 0xA5" is a
// scoreboard's job -- it is a fact about one transaction, checked once, at
// the end. "The line is at MARK whenever the transmitter is idle" is a
// property: it must be true on every clock of the entire run, there is no
// transaction to attach it to, and a scoreboard comparing delivered bytes
// would never see it fail.
//
// The eight below are all of the second kind. Not one of them checks a data
// value, and that is deliberate -- the data path already has a reference
// model in Chapter 14.5.
//
// SYSTEMSYSTEMVERILOG HAS SVA, AND THIS FILE MOSTLY CANNOT USE IT. What SystemVerilog writes as
//
// assert property (@(posedge clk) disable iff (!rst_n)
// !tx_busy_o |-> tx_o == 1'b1);
//
// is written here as an `if` and a counter. The property is identical; the
// notation is poorer, and the difference is the whole argument for SVA.
//===========================================================================
`timescale 1ns/1ps
module uart_tx_assert #(
parameter DATA_W = 8
) (
input wire clk,
input wire rst_n,
// the transmitter's interface -- all ports of the DUT
input wire baud_tick_i,
input wire tx_valid_i,
input wire tx_ready_i,
input wire tx_busy_i,
input wire tx_line_i,
input wire [1:0] parity_mode_i, // 0 none, 1 even, 2 odd, 3 mark
output logic [31:0] n_clocks,
output logic [31:0] n_frames, // frames seen start to finish
output logic [31:0] n_fail,
output logic [7:0] fail_mask // bit i set => property i+1 fired
);
localparam P_NONE = 2'd0;
// Expected bit intervals in a frame: start + data + optional parity + stop
wire [5:0] exp_bits = 6'd1 + DATA_W[5:0]
+ ((parity_mode_i != P_NONE) ? 6'd1 : 6'd0) + 6'd1;
logic busy_q, ready_q, line_q;
logic have_prev;
logic [5:0] tick_cnt; // baud ticks elapsed in this frame
logic in_frame;
logic hs_q; // a handshake happened last cycle
logic tick_q; // a baud tick happened last cycle
wire handshake = tx_valid_i && tx_ready_i;
task bump;
input [7:0] id;
input [8*46-1:0] name;
begin
n_fail++;
fail_mask = fail_mask | (8'b1 << (id - 1));
// An IMMEDIATE assertion, which Icarus does execute. It reports at
// the instant of the violation; the counter is what a testbench
// can make an arithmetic claim about afterwards.
assert (0) else $error("property %0d violated", id);
$display(" [assert] T%0d violated at %0t : %0s", id, $time, name);
end
endtask
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin
n_clocks <= 32'd0; n_frames <= 32'd0; n_fail <= 32'd0;
fail_mask <= 8'd0;
busy_q <= 1'b0; ready_q <= 1'b0; line_q <= 1'b1;
have_prev <= 1'b0; tick_cnt <= 6'd0; in_frame <= 1'b0;
hs_q <= 1'b0;
end else begin
n_clocks <= n_clocks + 1;
// ---- T1: the idle line is MARK ------------------------------
// The single most valuable property in the file. A transmitter
// that leaves the line low when idle looks like a permanent break
// to the far end, and no scoreboard comparing delivered bytes
// would ever notice -- because nothing is delivered.
// `in_frame` is excluded as well as busy: between the handshake
// and busy rising there is a cycle in which the transmitter has
// accepted a byte but has not started driving it, and the line is
// legitimately still at MARK-or-transitioning.
if (!tx_busy_i && !hs_q && !in_frame && tx_line_i !== 1'b1)
bump(8'd1, "line is not MARK while idle");
// ---- T2: no two acceptances back to back ---------------------
//
// NOT "ready and busy are mutually exclusive". That was the first
// draft and it fired 189 times against a correct transmitter,
// because this transmitter asserts ready during the STOP interval
// ON PURPOSE -- that is what lets frames follow each other with no
// gap (Chapter 7.4). Ready and busy overlap by design.
//
// The real interface contract is narrower: having accepted a byte,
// the transmitter must not accept another on the next cycle.
if (hs_q && tx_ready_i)
bump(8'd2, "ready still high the cycle after an acceptance");
// ---- T3: a handshake is followed by busy --------------------
if (hs_q && !tx_busy_i)
bump(8'd3, "busy did not rise after an accepted handshake");
// ---- T4: ready comes back only near the END of a frame -------
//
// Also not "ready stays low for the whole frame". The useful
// version states WHEN it may return: not before the frame has
// reached its final bit interval. That permits the back-to-back
// handoff and still catches a transmitter that offers capacity
// it does not have.
if (in_frame && tx_busy_i && tx_ready_i && (tick_cnt + 1 < exp_bits))
bump(8'd4, "ready returned before the final bit interval");
// ---- T5: the frame is exactly exp_bits baud intervals --------
// The property a scoreboard cannot see at all: it compares bytes,
// and a frame one bit too long delivers the right byte.
if (in_frame && tx_busy_i && baud_tick_i && tick_cnt > exp_bits)
bump(8'd5, "frame ran past its expected bit count");
// ---- T6: the frame opens with SPACE --------------------------
//
// Checked at the FIRST BAUD TICK of the frame, not on the cycle
// after the handshake. The transmitter is a baud-paced state
// machine and registers its output: the line does not move until
// the next tick. Checking one clock after the handshake fired 41
// times against a correct design and was measuring the clock
// rather than the protocol.
// Measured, not assumed: the transmitter transitions out of IDLE
// at tick 0 and its registered output follows, so the start bit
// is on the wire at tick 1. Checking at tick 0 fired 40 times
// against a correct design.
if (in_frame && tx_busy_i && baud_tick_i && tick_cnt == 1
&& tx_line_i !== 1'b0)
bump(8'd6, "start bit is not SPACE at the first driven tick");
// ---- T7: the line only moves on a baud tick ------------------
// Strictly: on the cycle AFTER a tick, since the DUT registers.
if (have_prev && tx_busy_i && (tx_line_i !== line_q) && !tick_q)
bump(8'd7, "line changed without a baud tick");
// ---- T8: busy does not drop mid-frame ------------------------
if (busy_q && !tx_busy_i && in_frame && tick_cnt < exp_bits - 1)
bump(8'd8, "busy dropped before the frame finished");
// ---- frame bookkeeping ---------------------------------------
if (handshake) begin
in_frame <= 1'b1;
tick_cnt <= 6'd0;
end else if (in_frame && baud_tick_i && tx_busy_i) begin
tick_cnt <= tick_cnt + 1'b1;
end
if (busy_q && !tx_busy_i && in_frame) begin
in_frame <= 1'b0;
n_frames <= n_frames + 1;
end
busy_q <= tx_busy_i;
ready_q <= tx_ready_i;
line_q <= tx_line_i;
tick_q <= baud_tick_i;
hs_q <= handshake;
have_prev <= 1'b1;
end
end
endmodule4. What Each Toolchain Will Actually Run
This is where the three languages stop being notations for the same thing.
Verilog-2001 has no assertion construct at all. No assert, no property, no sequence, no cover. Every property above is an if and a counter. That is not a stylistic choice; it is the entire language.
SystemVerilog has SVA and cannot use it here. Icarus Verilog 13.0 rejects concurrent assertions outright:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
sva.sv:4: error: Error in property_spec of concurrent assertion item.
sva4.sv:4: sorry: concurrent_assertion_item not supported.
Try -gno-assertions or -gsupported-assertions to turn this message off.Probed rather than assumed — an inline property, a named property, one without disable iff, and a purely boolean one were each tried and each refused. So the SystemVerilog checker uses immediate assertions inside a clocked block, which do run. The loss is real: an immediate assertion cannot express a temporal relationship, so a |=> b has no equivalent and any multi-cycle property has to be hand-built from registered history. That is what the _q signals are.
VHDL, through PSL, has all of it — and NVC 1.23.0 runs it.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
-- psl default clock is rising_edge(clk);
-- psl p4_accounting : assert always (rst_n = '1' -> not v4)
-- report "P4: level does not follow push/pop";
-- psl p7_not_both : assert never (rst_n = '1' and v7)
-- report "P7: empty and full asserted together";
--
-- A temporal property, which no immediate assertion can express:
-- psl t3_temporal : assert always ((rst_n = '1' and handshake = '1')
-- -> next (tx_busy_i = '1'))
-- report "T3(temporal): busy did not follow the handshake";
--
-- And a SEQUENCE being covered -- functional coverage in the assertion
-- language rather than in a separate model:
-- psl c_fill_drain : cover {full_i = '1'; (full_i = '0')[*]; empty_i = '1'}
-- report "COVER: the FIFO went from full to empty";always, never, next, until, sequences and cover were each written and each executed. On this toolchain the oldest of the three languages has by far the most expressive assertion support, which is not a sentence anyone expects to write.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
--===========================================================================
-- uart_fifo_assert — the FIFO property checker of Chapter 15.2,
-- in VHDL-2008 with PSL
--
-- NOT SYNTHESIZABLE. Bound alongside a FIFO, it watches the interface and
-- reports whenever an invariant is violated.
--
-- AND THIS IS THE VERSION THAT GETS TO SAY WHAT IT MEANS.
--
-- The Verilog-2001 file has no assertion construct at all. The SystemVerilog
-- file has SVA in the language and cannot use it, because Icarus Verilog
-- 13.0 answers every concurrent assertion with
--
-- sorry: concurrent_assertion_item not supported.
--
-- VHDL, through PSL, has the lot -- and NVC 1.23.0 runs it. `always`,
-- implication, `never`, `next`, `until`, sequences and `cover` all work,
-- which was verified by running each one rather than by reading a manual.
-- The oldest of the three languages ends up with the most expressive
-- assertion support on this toolchain, which is not the result anyone
-- expects.
--
-- So this file states each property TWICE, on purpose:
-- - as a PSL directive, which is what the property actually is; and
-- - as a counter in a process, so a testbench has a number to make an
-- arithmetic claim about. PSL reports to the simulator's log; it does
-- not hand a count back to the design.
--===========================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity uart_fifo_assert is
generic (
DEPTH : positive := 16;
LVL_W : positive := 5
);
port (
clk : in std_logic;
rst_n : in std_logic;
-- the FIFO's interface -- every one of these is a port of the DUT
push_i : in std_logic;
pop_i : in std_logic;
empty_i : in std_logic;
full_i : in std_logic;
level_i : in std_logic_vector(LVL_W-1 downto 0);
overflow_evt_i : in std_logic;
underflow_evt_i : in std_logic;
n_clocks : out natural;
n_fail : out natural;
fail_mask : out std_logic_vector(7 downto 0)
);
end entity uart_fifo_assert;
architecture checker of uart_fifo_assert is
signal lvl : natural;
signal lvl_q : natural := 0;
signal have_prev: boolean := false;
-- THE ACCEPTANCE RULE. The obvious one is `push and not full`. That is
-- NOT what the FIFO of Chapter 10.2 implements: a push into a full FIFO
-- is accepted when a pop frees an entry on the SAME cycle, because the
-- simpler rule drops a byte exactly where a consumer is keeping up.
-- The first version of this checker encoded the simpler rule and argued
-- with a correct design 41 times.
signal pop_ok, push_ok : std_logic;
signal ovf_exp, unf_exp : std_logic;
signal push_ok_q, pop_ok_q : std_logic := '0';
signal ovf_exp_q, unf_exp_q : std_logic := '0';
signal exp_next : natural := 0;
signal fails : natural := 0;
signal mask : std_logic_vector(7 downto 0) := (others => '0');
signal clks : natural := 0;
-- Boolean forms of each property, so PSL and the counting process are
-- looking at exactly the same expression rather than two paraphrases.
signal v1, v2, v3, v4, v5, v6, v7, v8 : boolean;
begin
lvl <= to_integer(unsigned(level_i));
pop_ok <= pop_i and (not empty_i);
push_ok <= push_i and ((not full_i) or pop_ok);
ovf_exp <= push_i and (not push_ok);
unf_exp <= pop_i and (not pop_ok);
-- What the level must become, from the PREVIOUS cycle's accepted
-- operations. At a rising edge `level_i` is still the pre-edge value, so
-- comparing it against this cycle's push and pop is off by one clock --
-- the first version did exactly that and fired 3,078 times.
exp_next <= lvl_q + 1 when (push_ok_q = '1' and pop_ok_q = '0') and lvl_q < DEPTH else
lvl_q - 1 when (pop_ok_q = '1' and push_ok_q = '0') and lvl_q > 0 else
lvl_q;
v1 <= lvl > DEPTH;
v2 <= (empty_i = '1') /= (lvl = 0);
v3 <= (full_i = '1') /= (lvl = DEPTH);
v4 <= have_prev and (lvl /= exp_next);
v5 <= overflow_evt_i /= ovf_exp_q;
v6 <= underflow_evt_i /= unf_exp_q;
v7 <= (empty_i = '1') and (full_i = '1');
v8 <= have_prev and (lvl > lvl_q + 1 or lvl_q > lvl + 1);
-----------------------------------------------------------------------
-- The properties, as PSL. This is what they ARE.
-----------------------------------------------------------------------
-- psl default clock is rising_edge(clk);
-- psl p1_level_range : assert always (rst_n = '1' -> not v1)
-- report "P1: level exceeds DEPTH";
-- psl p2_empty_iff : assert always (rst_n = '1' -> not v2)
-- report "P2: empty does not match level=0";
-- psl p3_full_iff : assert always (rst_n = '1' -> not v3)
-- report "P3: full does not match level=DEPTH";
-- psl p4_accounting : assert always (rst_n = '1' -> not v4)
-- report "P4: level does not follow push/pop";
-- psl p5_overflow : assert always (rst_n = '1' -> not v5)
-- report "P5: overflow_evt does not match a rejected push";
-- psl p6_underflow : assert always (rst_n = '1' -> not v6)
-- report "P6: underflow_evt does not match a rejected pop";
-- psl p7_not_both : assert never (rst_n = '1' and v7)
-- report "P7: empty and full asserted together";
-- psl p8_step_one : assert always (rst_n = '1' -> not v8)
-- report "P8: level moved by more than one";
--
-- And a coverage directive, which is functional coverage expressed in the
-- assertion language rather than in a separate model. Icarus has no
-- equivalent that runs.
-- psl c_fill_drain : cover {full_i = '1'; (full_i = '0')[*]; empty_i = '1'}
-- report "COVER: the FIFO went from full to empty";
-----------------------------------------------------------------------
-- The same properties as counters, so the testbench has numbers.
-----------------------------------------------------------------------
count_proc : process (clk, rst_n)
procedure bump(id : natural; name : string) is
begin
fails <= fails + 1;
mask(id-1) <= '1';
report " [assert] P" & integer'image(id) & " violated : " & name
severity warning;
end procedure bump;
begin
if rst_n = '0' then
clks <= 0; fails <= 0; mask <= (others => '0');
lvl_q <= 0; push_ok_q <= '0'; pop_ok_q <= '0';
ovf_exp_q <= '0'; unf_exp_q <= '0';
have_prev <= false;
elsif rising_edge(clk) then
clks <= clks + 1;
if v1 then bump(1, "level exceeds DEPTH"); end if;
if v2 then bump(2, "empty does not match level=0"); end if;
if v3 then bump(3, "full does not match level=DEPTH"); end if;
if v4 then bump(4, "level does not follow push/pop"); end if;
if v5 then bump(5, "overflow_evt does not match a rejected push"); end if;
if v6 then bump(6, "underflow_evt does not match a rejected pop"); end if;
if v7 then bump(7, "empty and full asserted together"); end if;
if v8 then bump(8, "level moved by more than one"); end if;
lvl_q <= lvl;
push_ok_q <= push_ok;
pop_ok_q <= pop_ok;
ovf_exp_q <= ovf_exp;
unf_exp_q <= unf_exp;
have_prev <= true;
end if;
end process count_proc;
n_clocks <= clks;
n_fail <= fails;
fail_mask <= mask;
end architecture checker;Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
--===========================================================================
-- uart_tx_assert — the transmitter property checker of Chapter 15.2,
-- in VHDL-2008 with PSL
--
-- NOT SYNTHESIZABLE. Bound alongside a UART transmitter, it watches the
-- interface and reports protocol violations.
--
-- WHAT BELONGS HERE (Chapter 15.1). A property earns its place when it
-- holds CONTINUOUSLY and a scoreboard would not notice it breaking. "The
-- byte 0xA5 came out as 0xA5" is a scoreboard's job. "The line is at MARK
-- whenever the transmitter is idle" is a property: true on every clock,
-- attached to no transaction, and invisible to a scoreboard comparing
-- delivered bytes -- because when it fails, nothing is delivered.
--
-- THREE OF THESE EIGHT WERE WRONG IN THEIR FIRST DRAFT, and each was wrong
-- in the same way: it asserted folklore instead of the contract.
--
-- T2 said ready and busy are mutually exclusive. 189 false failures.
-- T4 said ready stays low for a whole frame. 187 false failures.
-- T6 checked the start bit one tick too early. 40 false failures.
--
-- The transmitter of Chapter 7.1 asserts ready DURING the stop interval on
-- purpose -- that is what lets frames follow each other with no gap -- and
-- it registers its output, so the start bit is on the wire at the second
-- tick rather than the first. Both behaviours are documented. The checker
-- simply had not read the documentation.
--===========================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity uart_tx_assert is
generic (
DATA_W : positive := 8
);
port (
clk : in std_logic;
rst_n : in std_logic;
baud_tick_i : in std_logic;
tx_valid_i : in std_logic;
tx_ready_i : in std_logic;
tx_busy_i : in std_logic;
tx_line_i : in std_logic;
parity_mode_i : in std_logic_vector(1 downto 0);
n_clocks : out natural;
n_frames : out natural;
n_fail : out natural;
fail_mask : out std_logic_vector(7 downto 0)
);
end entity uart_tx_assert;
architecture checker of uart_tx_assert is
signal exp_bits : natural;
signal handshake : std_logic;
signal busy_q, line_q, tick_q, hs_q : std_logic := '0';
signal have_prev : boolean := false;
signal tick_cnt : natural := 0;
signal in_frame : boolean := false;
signal frames, fails, clks : natural := 0;
signal mask : std_logic_vector(7 downto 0) := (others => '0');
signal t1, t2, t3, t4, t5, t6, t7, t8 : boolean;
begin
-- A conditional SIGNAL ASSIGNMENT, not a conditional expression.
-- `a + (1 when c else 0)` is VHDL-2019; in VHDL-2008 the condition has to
-- select the whole right-hand side. The same restriction bit Chapter 11.4.
exp_bits <= 1 + DATA_W + 1 + 1 when parity_mode_i /= "00"
else 1 + DATA_W + 1;
handshake <= tx_valid_i and tx_ready_i;
t1 <= (tx_busy_i = '0') and (hs_q = '0') and (not in_frame)
and (tx_line_i /= '1');
t2 <= (hs_q = '1') and (tx_ready_i = '1');
t3 <= (hs_q = '1') and (tx_busy_i = '0');
t4 <= in_frame and (tx_busy_i = '1') and (tx_ready_i = '1')
and (tick_cnt + 1 < exp_bits);
t5 <= in_frame and (tx_busy_i = '1') and (baud_tick_i = '1')
and (tick_cnt > exp_bits);
t6 <= in_frame and (tx_busy_i = '1') and (baud_tick_i = '1')
and (tick_cnt = 1) and (tx_line_i /= '0');
t7 <= have_prev and (tx_busy_i = '1') and (tx_line_i /= line_q)
and (tick_q = '0');
t8 <= (busy_q = '1') and (tx_busy_i = '0') and in_frame
and (tick_cnt + 1 < exp_bits);
-----------------------------------------------------------------------
-- The properties, as PSL.
-----------------------------------------------------------------------
-- psl default clock is rising_edge(clk);
-- psl t1_idle_mark : assert always (rst_n = '1' -> not t1)
-- report "T1: line is not MARK while idle";
-- psl t2_no_double : assert always (rst_n = '1' -> not t2)
-- report "T2: ready still high the cycle after an acceptance";
-- psl t3_busy_rises : assert always (rst_n = '1' -> not t3)
-- report "T3: busy did not rise after an accepted handshake";
-- psl t4_ready_late : assert always (rst_n = '1' -> not t4)
-- report "T4: ready returned before the final bit interval";
-- psl t5_frame_len : assert always (rst_n = '1' -> not t5)
-- report "T5: frame ran past its expected bit count";
-- psl t6_start_space: assert always (rst_n = '1' -> not t6)
-- report "T6: start bit is not SPACE at the first driven tick";
-- psl t7_tick_moves : assert always (rst_n = '1' -> not t7)
-- report "T7: line changed without a baud tick";
-- psl t8_no_abort : assert always (rst_n = '1' -> not t8)
-- report "T8: busy dropped before the frame finished";
--
-- A temporal property that no immediate assertion can express, and which
-- Icarus cannot run in any notation: an accepted handshake must be
-- followed, on the very next cycle, by busy.
-- psl t3_temporal : assert always ((rst_n = '1' and handshake = '1')
-- -> next (tx_busy_i = '1'))
-- report "T3(temporal): busy did not follow the handshake";
--
-- And a cover directive: did a frame ever actually start?
-- psl c_frame : cover {handshake = '1'; tx_busy_i = '1'}
-- report "COVER: a frame was accepted and started";
-----------------------------------------------------------------------
-- The same properties as counters.
-----------------------------------------------------------------------
count_proc : process (clk, rst_n)
procedure bump(id : natural; name : string) is
begin
fails <= fails + 1;
mask(id-1) <= '1';
report " [assert] T" & integer'image(id) & " violated : " & name
severity warning;
end procedure bump;
begin
if rst_n = '0' then
clks <= 0; frames <= 0; fails <= 0; mask <= (others => '0');
busy_q <= '0'; line_q <= '1'; tick_q <= '0'; hs_q <= '0';
have_prev <= false; tick_cnt <= 0; in_frame <= false;
elsif rising_edge(clk) then
clks <= clks + 1;
if t1 then bump(1, "line is not MARK while idle"); end if;
if t2 then bump(2, "ready still high the cycle after an acceptance"); end if;
if t3 then bump(3, "busy did not rise after an accepted handshake"); end if;
if t4 then bump(4, "ready returned before the final bit interval"); end if;
if t5 then bump(5, "frame ran past its expected bit count"); end if;
if t6 then bump(6, "start bit is not SPACE at the first driven tick"); end if;
if t7 then bump(7, "line changed without a baud tick"); end if;
if t8 then bump(8, "busy dropped before the frame finished"); end if;
if handshake = '1' then
in_frame <= true;
tick_cnt <= 0;
elsif in_frame and baud_tick_i = '1' and tx_busy_i = '1' then
tick_cnt <= tick_cnt + 1;
end if;
if busy_q = '1' and tx_busy_i = '0' and in_frame then
in_frame <= false;
frames <= frames + 1;
end if;
busy_q <= tx_busy_i;
line_q <= tx_line_i;
tick_q <= baud_tick_i;
hs_q <= handshake;
have_prev <= true;
end if;
end process count_proc;
n_clocks <= clks;
n_frames <= frames;
n_fail <= fails;
fail_mask <= mask;
end architecture checker;5. Four Properties That Were Wrong
Every one of these fired against a published, already-verified design. None of them was a design bug.
| # | What the property said | False failures | What was actually true |
|---|---|---|---|
| P4 | level = previous level + this cycle's accepted ops | 3,078 | at a rising edge level_i is still the pre-edge value |
| P4/P5/P6 | a push is accepted when push && !full | 41 | a push into a full FIFO is accepted if a pop frees an entry the same cycle |
| T2 | ready and busy are mutually exclusive | 189 | they overlap during the stop interval, on purpose |
| T6 | the start bit is SPACE at the first baud tick | 40 | the output is registered; the start bit is on the wire at the second |
The sampling trap
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// WRONG -- and it fires on every cycle where anything happens.
wire push_ok = push_i && !full_i;
if (level_i !== level_q + push_ok - pop_ok) ...
// RIGHT -- the level observed at edge N must be compared against the level
// at edge N-1 plus the operations accepted at edge N-1.
reg push_ok_q, pop_ok_q;
if (level_i !== exp_next) ... // exp_next built from the _q versionsAt a rising edge, a registered output still holds its pre-edge value; the non-blocking update has not been applied. Comparing it against the current cycle's inputs is off by exactly one clock. It produced 3,078 failures against a correct FIFO, which looked like catastrophe and was arithmetic.
The same trap caught P5 and P6 from the other direction: the FIFO's event outputs are registered, so the event observed at an edge reports the operation rejected at the previous one.
The specification trap, which is worse
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// The obvious acceptance rule.
wire push_ok = push_i && !full_i;
// The rule this FIFO actually implements -- Chapter 10.2 section 5.
wire pop_ok = pop_i && !empty_i;
wire push_ok = push_i && (!full_i || pop_ok);A push into a full FIFO is accepted when a pop frees an entry on the same cycle, because the simpler rule drops a byte at exactly the boundary where a consumer is keeping up. That is documented, deliberate, and was argued for two modules earlier.
The checker asserted the simpler rule and disagreed with the design 41 times. Nothing was broken. The checker was confidently checking the wrong specification, which is the failure mode Chapter 15.1 §3 warns about — and the one most likely to end with the assertion on a waiver list instead of the bug in a tracker.
The folklore trap
ready and busy mutually exclusive is a rule that is true of many transmitters. It is not true of this one:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// uart_tx, Chapter 7.1:
// Ready only where shreg_q is free: IDLE, or STOP (payload already shifted
// out). Asserting it during DATA would promise capacity that does not exist.
assign tx_ready_o = ((state_q == S_IDLE) || (state_q == S_STOP)) && !pending_q;
assign tx_busy_o = (state_q != S_IDLE) || pending_q;ready is asserted during S_STOP so that frames can follow each other with no gap (Chapter 7.4). The overlap is the feature.
The useful properties are narrower, and both are checkable from the interface:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
// T2: having accepted a byte, do not accept another on the next cycle.
if (hs_q && tx_ready_i) bump(2, "ready still high the cycle after an acceptance");
// T4: ready may return, but not before the final bit interval.
if (in_frame && tx_busy_i && tx_ready_i && (tick_cnt + 1 < exp_bits))
bump(4, "ready returned before the final bit interval");6. Testing the Checkers
A property checker has two failure modes and a suite has to cover both:
- it fails to fire — the property is violated and nothing is reported;
- it fires anyway — the design is correct and the checker complains.
The second is worse in practice, because the response is to stop reading it.
So each suite has two halves. Half one binds the checker to the real published design and drives thousands of legal operations, requiring zero violations. Half two drives a second checker instance directly with synthetic interface traffic that breaks one named property at a time, requiring that the right one fires.
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// tb_uart_fifo_assert_v — self-checking Verilog-2001 testbench
//
// A property checker has TWO failure modes and a test has to cover both:
//
// IT FAILS TO FIRE. The property is violated and nothing is reported.
// The regression stays green and the bug ships.
// IT FIRES ANYWAY. The design is correct and the checker complains.
// Worse in practice: the team learns to ignore it, and
// then it might as well not exist.
//
// So the suite has two halves, and neither is optional.
//
// HALF ONE binds the checker to the REAL published FIFO of Chapter 10.2 and
// drives thousands of legal operations. The requirement is ZERO violations.
// This is the half that proves the checker is not noisy.
//
// HALF TWO drives a SECOND checker instance directly with synthetic
// interface traffic that violates one named property at a time. The
// requirement is that the right property fires. This is the half that
// proves the checker is not blind.
//
// A checker tested only against a correct design has been shown to be
// quiet. Quiet is not the same as correct.
//===========================================================================
`timescale 1ns/1ps
module tb_uart_fifo_assert_v;
localparam DEPTH = 16;
localparam LVL_W = 5;
reg clk = 1'b0;
always #5 clk = ~clk;
reg rst_n = 1'b0;
//====================================================================
// HALF ONE — the checker bound to the real FIFO
//====================================================================
reg push = 1'b0, pop = 1'b0;
reg [7:0] push_data = 8'h00;
wire [7:0] pop_data;
wire empty, full, ovf, unf;
wire [LVL_W-1:0] level;
uart_sync_fifo_v #(.WIDTH(8), .DEPTH(DEPTH)) dut (
.clk(clk), .rst_n(rst_n),
.push_i(push), .push_data_i(push_data),
.pop_i(pop), .pop_data_o(pop_data),
.empty_o(empty), .full_o(full), .level_o(level),
.overflow_evt_o(ovf), .underflow_evt_o(unf));
wire [31:0] r_clocks, r_fail;
wire [7:0] r_mask;
uart_fifo_assert_v #(.DEPTH(DEPTH), .LVL_W(LVL_W)) chk_real (
.clk(clk), .rst_n(rst_n),
.push_i(push), .pop_i(pop), .empty_i(empty), .full_i(full),
.level_i(level), .overflow_evt_i(ovf), .underflow_evt_i(unf),
.n_clocks(r_clocks), .n_fail(r_fail), .fail_mask(r_mask));
//====================================================================
// HALF TWO — a checker driven directly with illegal interface traffic
//====================================================================
reg s_rst_n = 1'b0;
reg s_push = 1'b0, s_pop = 1'b0, s_empty = 1'b1, s_full = 1'b0;
reg [LVL_W-1:0] s_level = 5'd0;
reg s_ovf = 1'b0, s_unf = 1'b0;
wire [31:0] s_clocks, s_fail;
wire [7:0] s_mask;
uart_fifo_assert_v #(.DEPTH(DEPTH), .LVL_W(LVL_W)) chk_synth (
.clk(clk), .rst_n(s_rst_n),
.push_i(s_push), .pop_i(s_pop), .empty_i(s_empty), .full_i(s_full),
.level_i(s_level), .overflow_evt_i(s_ovf), .underflow_evt_i(s_unf),
.n_clocks(s_clocks), .n_fail(s_fail), .fail_mask(s_mask));
integer checks = 0, failures = 0;
task check;
input cond;
input [8*80-1:0] name;
begin
checks = checks + 1;
if (cond) $display(" PASS %0s", name);
else begin failures = failures + 1; $display(" FAIL %0s", name); end
end
endtask
integer i;
reg [15:0] lfsr = 16'hF00D;
// Put the synthetic checker into a known, legal, empty state.
task s_reset;
begin
@(negedge clk);
s_rst_n = 1'b0; s_push = 1'b0; s_pop = 1'b0;
s_empty = 1'b1; s_full = 1'b0; s_level = 5'd0;
s_ovf = 1'b0; s_unf = 1'b0;
repeat (2) @(negedge clk);
s_rst_n = 1'b1;
repeat (2) @(negedge clk);
end
endtask
// Hold a legal, self-consistent interface state for one clock, with the
// push/pop that JUSTIFIES the next level.
//
// The first version of this task set the level without asserting push or
// pop, and then "walked" it from 0 to DEPTH. That walk is not legal
// traffic -- a level that moves with no accepted operation is exactly
// what P4 exists to catch -- so the checker was right and the test was
// wrong. Worth recording: the first instinct on seeing P4 fire here was
// to suspect P4.
task s_step;
input [LVL_W-1:0] lvl;
input do_push;
input do_pop;
begin
@(negedge clk);
s_level = lvl; s_empty = (lvl == 0); s_full = (lvl == DEPTH);
s_push = do_push; s_pop = do_pop;
s_ovf = 1'b0; s_unf = 1'b0;
end
endtask
// A quiet, self-consistent cycle: no operation, so no level change.
task s_legal;
input [LVL_W-1:0] lvl;
begin s_step(lvl, 1'b0, 1'b0); end
endtask
initial begin
#20_000_000;
$display(" FAIL watchdog: simulation did not finish");
$display("== %0d checks, %0d failures ==", checks+1, failures+1);
$display(" RESULT: VERILOG FIFO-ASSERT TESTS FAILED (timeout)");
$finish;
end
initial begin
$display("== uart_fifo_assert_v : self-checking Verilog testbench ==");
rst_n = 1'b0; s_rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (2) @(negedge clk);
//================================================================
// HALF ONE: legal traffic against the real FIFO
//================================================================
// fill, drain, and a long random soak -- every operation legal
for (i = 0; i < DEPTH; i = i + 1) begin
@(negedge clk) push = 1'b1; push_data = i[7:0];
end
@(negedge clk) push = 1'b0;
check(full === 1'b1 && level == DEPTH, "the real FIFO filled to DEPTH");
check(r_fail == 0, "checker silent while the FIFO filled legally");
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
check(empty === 1'b1 && level == 0, "and drained to empty");
check(r_fail == 0, "checker still silent after a legal drain");
// push while full and pop while empty are LEGAL operations -- the
// FIFO is required to reject them and say so, not to be spared them.
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) push = 1'b1;
@(negedge clk);
check(full === 1'b1, "full again");
@(negedge clk) push = 1'b1; // push into a full FIFO
@(negedge clk) push = 1'b0;
check(r_fail == 0, "an overflow event is not a property violation");
for (i = 0; i < DEPTH + 2; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
check(r_fail == 0, "nor is an underflow event");
// a long random soak
for (i = 0; i < 4000; i = i + 1) begin
@(negedge clk);
lfsr = {lfsr[14:0], lfsr[15]^lfsr[13]^lfsr[12]^lfsr[10]};
push = lfsr[0];
pop = lfsr[1];
push_data = lfsr[9:2];
end
@(negedge clk) push = 1'b0; pop = 1'b0;
repeat (4) @(negedge clk);
check(r_clocks > 4000, "the checker evaluated over 4000 clocks of traffic");
check(r_fail == 0,
"ZERO violations across the whole legal soak -- the checker is not noisy");
check(r_mask == 8'h00, "and not one property ever fired");
//=== THE boundary the random soak never reached =====================
// Push and pop asserted together while the FIFO is FULL. This is the
// single cycle on which the two candidate acceptance rules disagree:
// push && !full rejects it (and would raise overflow)
// push && (!full || pop) accepts it (Chapter 10.2 section 5)
//
// 4,079 clocks of random push/pop reached it ZERO times, and a mutant
// carrying the wrong rule survived the entire suite because of it.
// Directed stimulus, because randomisation had no reason to find it.
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) push = 1'b1;
@(negedge clk) push = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) push = 1'b1; pop = 1'b1; // both, while full
@(negedge clk) push = 1'b0; pop = 1'b0;
repeat (3) @(negedge clk);
check(r_fail == 0,
"push and pop together while FULL is accepted, not an overflow");
for (i = 0; i < DEPTH + 2; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
repeat (2) @(negedge clk);
//================================================================
// HALF TWO: each property, violated deliberately
//================================================================
// P1 -- a level beyond DEPTH
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd20; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[0] === 1'b1, "P1 fires when the level exceeds DEPTH");
// P2 -- empty asserted while the level is not zero
s_reset; s_legal(5'd4);
@(negedge clk) s_empty = 1'b1; // level is still 4
@(negedge clk);
check(s_mask[1] === 1'b1, "P2 fires when empty disagrees with level==0");
// P3 -- full deasserted at DEPTH
s_reset; s_legal(5'd16);
@(negedge clk) s_full = 1'b0; // level is DEPTH
@(negedge clk);
check(s_mask[2] === 1'b1, "P3 fires when full disagrees with level==DEPTH");
// P4 -- the level moves with no push and no pop
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd5; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[3] === 1'b1,
"P4 fires when the level changes without an accepted push or pop");
// P5 -- an overflow event with no push
s_reset; s_legal(5'd8);
@(negedge clk) s_ovf = 1'b1;
@(negedge clk);
check(s_mask[4] === 1'b1, "P5 fires on an overflow event that had no push");
// P6 -- an underflow event with no pop
s_reset; s_legal(5'd0);
@(negedge clk) s_unf = 1'b1;
@(negedge clk);
check(s_mask[5] === 1'b1, "P6 fires on an underflow event that had no pop");
// P7 -- empty and full at once
s_reset; s_legal(5'd0);
@(negedge clk) s_full = 1'b1; // empty is already 1, level 0
@(negedge clk);
check(s_mask[6] === 1'b1, "P7 fires when empty and full assert together");
// P8 -- the level jumps by more than one
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd9; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[7] === 1'b1, "P8 fires when the level jumps by more than one");
//================================================================
// and the checker stays quiet on legal synthetic traffic
//================================================================
s_reset;
// Up: assert push on the cycle BEFORE each increment.
for (i = 0; i < DEPTH; i = i + 1) s_step(i[LVL_W-1:0], 1'b1, 1'b0);
s_step(DEPTH[LVL_W-1:0], 1'b0, 1'b0);
// Down: assert pop on the cycle before each decrement.
for (i = DEPTH; i > 0; i = i - 1) s_step(i[LVL_W-1:0], 1'b0, 1'b1);
s_step(5'd0, 1'b0, 1'b0);
repeat (2) @(negedge clk);
check(s_fail == 0 && s_mask == 8'h00,
"walking the level legally from 0 to DEPTH and back fires nothing");
$display("== %0d checks, %0d failures ==", checks, failures);
if (failures == 0) $display(" RESULT: ALL VERILOG FIFO-ASSERT TESTS PASSED");
else $display(" RESULT: VERILOG FIFO-ASSERT TESTS FAILED");
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// tb_uart_fifo_assert — self-checking SystemVerilog testbench
//
// A property checker has TWO failure modes and a test has to cover both:
//
// IT FAILS TO FIRE. The property is violated and nothing is reported.
// The regression stays green and the bug ships.
// IT FIRES ANYWAY. The design is correct and the checker complains.
// Worse in practice: the team learns to ignore it, and
// then it might as well not exist.
//
// So the suite has two halves, and neither is optional.
//
// HALF ONE binds the checker to the REAL published FIFO of Chapter 10.2 and
// drives thousands of legal operations. The requirement is ZERO violations.
// This is the half that proves the checker is not noisy.
//
// HALF TWO drives a SECOND checker instance directly with synthetic
// interface traffic that violates one named property at a time. The
// requirement is that the right property fires. This is the half that
// proves the checker is not blind.
//
// A checker tested only against a correct design has been shown to be
// quiet. Quiet is not the same as correct.
//===========================================================================
`timescale 1ns/1ps
module tb_uart_fifo_assert;
localparam DEPTH = 16;
localparam LVL_W = 5;
logic clk = 1'b0;
always #5 clk = ~clk;
logic rst_n = 1'b0;
//====================================================================
// HALF ONE — the checker bound to the real FIFO
//====================================================================
logic push = 1'b0, pop = 1'b0;
logic [7:0] push_data = 8'h00;
wire [7:0] pop_data;
wire empty, full, ovf, unf;
wire [LVL_W-1:0] level;
uart_sync_fifo #(.WIDTH(8), .DEPTH(DEPTH)) dut (
.clk(clk), .rst_n(rst_n),
.push_i(push), .push_data_i(push_data),
.pop_i(pop), .pop_data_o(pop_data),
.empty_o(empty), .full_o(full), .level_o(level),
.overflow_evt_o(ovf), .underflow_evt_o(unf));
wire [31:0] r_clocks, r_fail;
wire [7:0] r_mask;
uart_fifo_assert #(.DEPTH(DEPTH), .LVL_W(LVL_W)) chk_real (
.clk(clk), .rst_n(rst_n),
.push_i(push), .pop_i(pop), .empty_i(empty), .full_i(full),
.level_i(level), .overflow_evt_i(ovf), .underflow_evt_i(unf),
.n_clocks(r_clocks), .n_fail(r_fail), .fail_mask(r_mask));
//====================================================================
// HALF TWO — a checker driven directly with illegal interface traffic
//====================================================================
logic s_rst_n = 1'b0;
logic s_push = 1'b0, s_pop = 1'b0, s_empty = 1'b1, s_full = 1'b0;
logic [LVL_W-1:0] s_level = 5'd0;
logic s_ovf = 1'b0, s_unf = 1'b0;
wire [31:0] s_clocks, s_fail;
wire [7:0] s_mask;
uart_fifo_assert #(.DEPTH(DEPTH), .LVL_W(LVL_W)) chk_synth (
.clk(clk), .rst_n(s_rst_n),
.push_i(s_push), .pop_i(s_pop), .empty_i(s_empty), .full_i(s_full),
.level_i(s_level), .overflow_evt_i(s_ovf), .underflow_evt_i(s_unf),
.n_clocks(s_clocks), .n_fail(s_fail), .fail_mask(s_mask));
int checks = 0, failures = 0;
task automatic check(input logic cond, input string name);
checks++;
if (cond) $display(" PASS %0s", name);
else begin failures++; $display(" FAIL %0s", name); end
endtask
int i;
logic [15:0] lfsr = 16'hF00D;
// Put the synthetic checker into a known, legal, empty state.
task s_reset;
begin
@(negedge clk);
s_rst_n = 1'b0; s_push = 1'b0; s_pop = 1'b0;
s_empty = 1'b1; s_full = 1'b0; s_level = 5'd0;
s_ovf = 1'b0; s_unf = 1'b0;
repeat (2) @(negedge clk);
s_rst_n = 1'b1;
repeat (2) @(negedge clk);
end
endtask
// Hold a legal, self-consistent interface state for one clock, with the
// push/pop that JUSTIFIES the next level.
//
// The first version of this task set the level without asserting push or
// pop, and then "walked" it from 0 to DEPTH. That walk is not legal
// traffic -- a level that moves with no accepted operation is exactly
// what P4 exists to catch -- so the checker was right and the test was
// wrong. Worth recording: the first instinct on seeing P4 fire here was
// to suspect P4.
task s_step;
input [LVL_W-1:0] lvl;
input do_push;
input do_pop;
begin
@(negedge clk);
s_level = lvl; s_empty = (lvl == 0); s_full = (lvl == DEPTH);
s_push = do_push; s_pop = do_pop;
s_ovf = 1'b0; s_unf = 1'b0;
end
endtask
// A quiet, self-consistent cycle: no operation, so no level change.
task s_legal;
input [LVL_W-1:0] lvl;
begin s_step(lvl, 1'b0, 1'b0); end
endtask
initial begin
#20_000_000;
$display(" FAIL watchdog: simulation did not finish");
$display("== %0d checks, %0d failures ==", checks+1, failures+1);
$display(" RESULT: SYSTEMVERILOG FIFO-ASSERT TESTS FAILED (timeout)");
$finish;
end
initial begin
$display("== uart_fifo_assert : self-checking Verilog testbench ==");
rst_n = 1'b0; s_rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (2) @(negedge clk);
//================================================================
// HALF ONE: legal traffic against the real FIFO
//================================================================
// fill, drain, and a long random soak -- every operation legal
for (i = 0; i < DEPTH; i = i + 1) begin
@(negedge clk) push = 1'b1; push_data = i[7:0];
end
@(negedge clk) push = 1'b0;
check(full === 1'b1 && level == DEPTH, "the real FIFO filled to DEPTH");
check(r_fail == 0, "checker silent while the FIFO filled legally");
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
check(empty === 1'b1 && level == 0, "and drained to empty");
check(r_fail == 0, "checker still silent after a legal drain");
// push while full and pop while empty are LEGAL operations -- the
// FIFO is required to reject them and say so, not to be spared them.
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) push = 1'b1;
@(negedge clk);
check(full === 1'b1, "full again");
@(negedge clk) push = 1'b1; // push into a full FIFO
@(negedge clk) push = 1'b0;
check(r_fail == 0, "an overflow event is not a property violation");
for (i = 0; i < DEPTH + 2; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
check(r_fail == 0, "nor is an underflow event");
// a long random soak
for (i = 0; i < 4000; i = i + 1) begin
@(negedge clk);
lfsr = {lfsr[14:0], lfsr[15]^lfsr[13]^lfsr[12]^lfsr[10]};
push = lfsr[0];
pop = lfsr[1];
push_data = lfsr[9:2];
end
@(negedge clk) push = 1'b0; pop = 1'b0;
repeat (4) @(negedge clk);
check(r_clocks > 4000, "the checker evaluated over 4000 clocks of traffic");
check(r_fail == 0,
"ZERO violations across the whole legal soak -- the checker is not noisy");
check(r_mask == 8'h00, "and not one property ever fired");
//=== THE boundary the random soak never reached =====================
// Push and pop asserted together while the FIFO is FULL. This is the
// single cycle on which the two candidate acceptance rules disagree:
// push && !full rejects it (and would raise overflow)
// push && (!full || pop) accepts it (Chapter 10.2 section 5)
//
// 4,079 clocks of random push/pop reached it ZERO times, and a mutant
// carrying the wrong rule survived the entire suite because of it.
// Directed stimulus, because randomisation had no reason to find it.
for (i = 0; i < DEPTH; i = i + 1) @(negedge clk) push = 1'b1;
@(negedge clk) push = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) push = 1'b1; pop = 1'b1; // both, while full
@(negedge clk) push = 1'b0; pop = 1'b0;
repeat (3) @(negedge clk);
check(r_fail == 0,
"push and pop together while FULL is accepted, not an overflow");
for (i = 0; i < DEPTH + 2; i = i + 1) @(negedge clk) pop = 1'b1;
@(negedge clk) pop = 1'b0;
repeat (2) @(negedge clk);
//================================================================
// HALF TWO: each property, violated deliberately
//================================================================
// P1 -- a level beyond DEPTH
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd20; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[0] === 1'b1, "P1 fires when the level exceeds DEPTH");
// P2 -- empty asserted while the level is not zero
s_reset; s_legal(5'd4);
@(negedge clk) s_empty = 1'b1; // level is still 4
@(negedge clk);
check(s_mask[1] === 1'b1, "P2 fires when empty disagrees with level==0");
// P3 -- full deasserted at DEPTH
s_reset; s_legal(5'd16);
@(negedge clk) s_full = 1'b0; // level is DEPTH
@(negedge clk);
check(s_mask[2] === 1'b1, "P3 fires when full disagrees with level==DEPTH");
// P4 -- the level moves with no push and no pop
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd5; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[3] === 1'b1,
"P4 fires when the level changes without an accepted push or pop");
// P5 -- an overflow event with no push
s_reset; s_legal(5'd8);
@(negedge clk) s_ovf = 1'b1;
@(negedge clk);
check(s_mask[4] === 1'b1, "P5 fires on an overflow event that had no push");
// P6 -- an underflow event with no pop
s_reset; s_legal(5'd0);
@(negedge clk) s_unf = 1'b1;
@(negedge clk);
check(s_mask[5] === 1'b1, "P6 fires on an underflow event that had no pop");
// P7 -- empty and full at once
s_reset; s_legal(5'd0);
@(negedge clk) s_full = 1'b1; // empty is already 1, level 0
@(negedge clk);
check(s_mask[6] === 1'b1, "P7 fires when empty and full assert together");
// P8 -- the level jumps by more than one
s_reset; s_legal(5'd4);
@(negedge clk) s_level = 5'd9; s_empty = 1'b0; s_full = 1'b0;
@(negedge clk);
check(s_mask[7] === 1'b1, "P8 fires when the level jumps by more than one");
//================================================================
// and the checker stays quiet on legal synthetic traffic
//================================================================
s_reset;
// Up: assert push on the cycle BEFORE each increment.
for (i = 0; i < DEPTH; i = i + 1) s_step(i[LVL_W-1:0], 1'b1, 1'b0);
s_step(DEPTH[LVL_W-1:0], 1'b0, 1'b0);
// Down: assert pop on the cycle before each decrement.
for (i = DEPTH; i > 0; i = i - 1) s_step(i[LVL_W-1:0], 1'b0, 1'b1);
s_step(5'd0, 1'b0, 1'b0);
repeat (2) @(negedge clk);
check(s_fail == 0 && s_mask == 8'h00,
"walking the level legally from 0 to DEPTH and back fires nothing");
$display("== %0d checks, %0d failures ==", checks, failures);
if (failures == 0) $display(" RESULT: ALL SYSTEMVERILOG FIFO-ASSERT TESTS PASSED");
else $display(" RESULT: SYSTEMVERILOG FIFO-ASSERT TESTS FAILED");
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
Snippet
--===========================================================================
-- tb_uart_fifo_assert — self-checking VHDL-2008 testbench
--
-- A property checker has TWO failure modes and a test has to cover both:
--
-- IT FAILS TO FIRE. The property is violated and nothing is reported.
-- IT FIRES ANYWAY. The design is correct and the checker complains --
-- worse in practice, because the team learns to ignore
-- it and then it might as well not exist.
--
-- HALF ONE drives a CONFORMING FIFO and requires ZERO violations.
-- HALF TWO drives a second checker with traffic that violates one named
-- property at a time, and requires that the right one fires.
--
-- A NOTE ON THE FIXTURE. The Verilog and SystemVerilog versions of this
-- suite bind the checker to the real published FIFO of Chapter 10.2. There
-- is no VHDL edition of that block in this curriculum, so half one uses a
-- behavioural model written to the same contract -- including the part that
-- matters most here, that a push into a full FIFO is accepted when a pop
-- frees an entry on the same cycle. It is a testbench fixture, not a design,
-- and it is labelled as one.
--
-- Same 19 counted checks as the Verilog and SystemVerilog twins.
--===========================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity tb_uart_fifo_assert is
end entity tb_uart_fifo_assert;
architecture sim of tb_uart_fifo_assert is
constant DEPTH : positive := 16;
constant LVL_W : positive := 5;
constant TCLK : time := 10 ns;
signal clk : std_logic := '0';
signal rst_n : std_logic := '0';
signal done : boolean := false;
-- HALF ONE: the conforming fixture
signal push, pop : std_logic := '0';
signal empty, full : std_logic;
signal level : std_logic_vector(LVL_W-1 downto 0);
signal ovf, unf : std_logic := '0';
signal lvl_n : natural := 0;
signal r_clocks, r_fail : natural;
signal r_mask : std_logic_vector(7 downto 0);
-- HALF TWO: the synthetic checker
signal s_rst_n : std_logic := '0';
signal s_push, s_pop : std_logic := '0';
signal s_empty : std_logic := '1';
signal s_full : std_logic := '0';
signal s_level : std_logic_vector(LVL_W-1 downto 0) := (others => '0');
signal s_ovf, s_unf : std_logic := '0';
signal s_clocks, s_fail : natural;
signal s_mask : std_logic_vector(7 downto 0);
begin
clk <= not clk after TCLK/2 when not done else '0';
-----------------------------------------------------------------------
-- A CONFORMING FIFO, behavioural. Testbench fixture, not a design.
-----------------------------------------------------------------------
empty <= '1' when lvl_n = 0 else '0';
full <= '1' when lvl_n = DEPTH else '0';
level <= std_logic_vector(to_unsigned(lvl_n, LVL_W));
fixture : process (clk, rst_n)
variable pop_fire, push_fire : boolean;
begin
if rst_n = '0' then
lvl_n <= 0; ovf <= '0'; unf <= '0';
elsif rising_edge(clk) then
pop_fire := (pop = '1') and (lvl_n > 0);
-- The acceptance rule of Chapter 10.2 section 5, in full.
push_fire := (push = '1') and ((lvl_n < DEPTH) or pop_fire);
-- The event outputs are REGISTERED, as in the published FIFO.
if (push = '1') and not push_fire then ovf <= '1'; else ovf <= '0'; end if;
if (pop = '1') and not pop_fire then unf <= '1'; else unf <= '0'; end if;
if push_fire and not pop_fire then lvl_n <= lvl_n + 1;
elsif pop_fire and not push_fire then lvl_n <= lvl_n - 1;
end if;
end if;
end process fixture;
chk_real : entity work.uart_fifo_assert
generic map (DEPTH => DEPTH, LVL_W => LVL_W)
port map (clk => clk, rst_n => rst_n,
push_i => push, pop_i => pop, empty_i => empty, full_i => full,
level_i => level, overflow_evt_i => ovf, underflow_evt_i => unf,
n_clocks => r_clocks, n_fail => r_fail, fail_mask => r_mask);
chk_synth : entity work.uart_fifo_assert
generic map (DEPTH => DEPTH, LVL_W => LVL_W)
port map (clk => clk, rst_n => s_rst_n,
push_i => s_push, pop_i => s_pop, empty_i => s_empty,
full_i => s_full, level_i => s_level,
overflow_evt_i => s_ovf, underflow_evt_i => s_unf,
n_clocks => s_clocks, n_fail => s_fail, fail_mask => s_mask);
watchdog : process
begin
wait for 50 ms;
report "watchdog: simulation did not finish" severity failure;
end process watchdog;
stim : process
variable checks, failures : natural := 0;
variable lfsr : std_logic_vector(15 downto 0) := x"F00D";
procedure check(cond : boolean; name : string) is
begin
checks := checks + 1;
if cond then report " PASS " & name severity note;
else failures := failures + 1; report " FAIL " & name severity error;
end if;
end procedure check;
procedure s_reset is
begin
wait until falling_edge(clk);
s_rst_n <= '0'; s_push <= '0'; s_pop <= '0';
s_empty <= '1'; s_full <= '0'; s_level <= (others => '0');
s_ovf <= '0'; s_unf <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
s_rst_n <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
end procedure s_reset;
-- One clock of self-consistent interface state, with the operation
-- that JUSTIFIES the next level. A level that moves with no accepted
-- operation is exactly what P4 exists to catch.
procedure s_step(lvl : natural; do_push, do_pop : std_logic) is
begin
wait until falling_edge(clk);
s_level <= std_logic_vector(to_unsigned(lvl, LVL_W));
if lvl = 0 then s_empty <= '1'; else s_empty <= '0'; end if;
if lvl = DEPTH then s_full <= '1'; else s_full <= '0'; end if;
s_push <= do_push; s_pop <= do_pop;
s_ovf <= '0'; s_unf <= '0';
end procedure s_step;
procedure s_legal(lvl : natural) is
begin s_step(lvl, '0', '0'); end procedure s_legal;
begin
report "== uart_fifo_assert : self-checking VHDL testbench ==" severity note;
rst_n <= '0'; s_rst_n <= '0';
for i in 1 to 4 loop wait until falling_edge(clk); end loop;
rst_n <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
--=== HALF ONE: legal traffic ========================================
for i in 1 to DEPTH loop
wait until falling_edge(clk); push <= '1';
end loop;
wait until falling_edge(clk); push <= '0';
check(full = '1' and lvl_n = DEPTH, "the FIFO fixture filled to DEPTH");
check(r_fail = 0, "checker silent while the FIFO filled legally");
for i in 1 to DEPTH loop
wait until falling_edge(clk); pop <= '1';
end loop;
wait until falling_edge(clk); pop <= '0';
check(empty = '1' and lvl_n = 0, "and drained to empty");
check(r_fail = 0, "checker still silent after a legal drain");
for i in 1 to DEPTH loop wait until falling_edge(clk); push <= '1'; end loop;
wait until falling_edge(clk);
check(full = '1', "full again");
wait until falling_edge(clk); push <= '1';
wait until falling_edge(clk); push <= '0';
check(r_fail = 0, "an overflow event is not a property violation");
for i in 1 to DEPTH + 2 loop wait until falling_edge(clk); pop <= '1'; end loop;
wait until falling_edge(clk); pop <= '0';
check(r_fail = 0, "nor is an underflow event");
for i in 1 to 4000 loop
wait until falling_edge(clk);
lfsr := lfsr(14 downto 0)
& (lfsr(15) xor lfsr(13) xor lfsr(12) xor lfsr(10));
push <= lfsr(0);
pop <= lfsr(1);
end loop;
wait until falling_edge(clk); push <= '0'; pop <= '0';
for i in 1 to 4 loop wait until falling_edge(clk); end loop;
check(r_clocks > 4000, "the checker evaluated over 4000 clocks of traffic");
check(r_fail = 0,
"ZERO violations across the whole legal soak -- the checker is not noisy");
check(r_mask = x"00", "and not one property ever fired");
--=== THE boundary the random soak never reached =====================
-- Push and pop asserted together while the FIFO is FULL. This is the
-- single cycle on which the two candidate acceptance rules disagree:
-- push and not full rejects it (and would raise overflow)
-- push and (not full or pop) accepts it (Chapter 10.2 section 5)
--
-- 4,079 clocks of random push/pop reached it ZERO times, and a mutant
-- carrying the wrong rule survived the whole suite because of it.
for i in 1 to DEPTH loop wait until falling_edge(clk); push <= '1'; end loop;
wait until falling_edge(clk); push <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
wait until falling_edge(clk); push <= '1'; pop <= '1';
wait until falling_edge(clk); push <= '0'; pop <= '0';
for i in 1 to 3 loop wait until falling_edge(clk); end loop;
check(r_fail = 0,
"push and pop together while FULL is accepted, not an overflow");
for i in 1 to DEPTH + 2 loop wait until falling_edge(clk); pop <= '1'; end loop;
wait until falling_edge(clk); pop <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
--=== HALF TWO: each property, violated deliberately =================
s_reset; s_legal(4);
wait until falling_edge(clk);
s_level <= std_logic_vector(to_unsigned(20, LVL_W));
s_empty <= '0'; s_full <= '0';
wait until falling_edge(clk);
check(s_mask(0) = '1', "P1 fires when the level exceeds DEPTH");
s_reset; s_legal(4);
wait until falling_edge(clk); s_empty <= '1';
wait until falling_edge(clk);
check(s_mask(1) = '1', "P2 fires when empty disagrees with level=0");
s_reset; s_legal(DEPTH);
wait until falling_edge(clk); s_full <= '0';
wait until falling_edge(clk);
check(s_mask(2) = '1', "P3 fires when full disagrees with level=DEPTH");
s_reset; s_legal(4);
wait until falling_edge(clk);
s_level <= std_logic_vector(to_unsigned(5, LVL_W));
s_empty <= '0'; s_full <= '0';
wait until falling_edge(clk);
check(s_mask(3) = '1',
"P4 fires when the level changes without an accepted push or pop");
s_reset; s_legal(8);
wait until falling_edge(clk); s_ovf <= '1';
wait until falling_edge(clk);
check(s_mask(4) = '1', "P5 fires on an overflow event that had no push");
s_reset; s_legal(0);
wait until falling_edge(clk); s_unf <= '1';
wait until falling_edge(clk);
check(s_mask(5) = '1', "P6 fires on an underflow event that had no pop");
s_reset; s_legal(0);
wait until falling_edge(clk); s_full <= '1';
wait until falling_edge(clk);
check(s_mask(6) = '1', "P7 fires when empty and full assert together");
s_reset; s_legal(4);
wait until falling_edge(clk);
s_level <= std_logic_vector(to_unsigned(9, LVL_W));
s_empty <= '0'; s_full <= '0';
wait until falling_edge(clk);
check(s_mask(7) = '1', "P8 fires when the level jumps by more than one");
--=== and the checker stays quiet on legal synthetic traffic =========
s_reset;
for i in 0 to DEPTH-1 loop s_step(i, '1', '0'); end loop;
s_step(DEPTH, '0', '0');
for i in DEPTH downto 1 loop s_step(i, '0', '1'); end loop;
s_step(0, '0', '0');
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_fail = 0 and s_mask = x"00",
"walking the level legally from 0 to DEPTH and back fires nothing");
report "== " & integer'image(checks) & " checks, "
& integer'image(failures) & " failures ==" severity note;
if failures = 0 then
report " RESULT: ALL VHDL FIFO-ASSERT TESTS PASSED" severity note;
else
report " RESULT: VHDL FIFO-ASSERT TESTS FAILED" severity error;
end if;
done <= true;
wait;
end process stim;
end architecture sim;Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// tb_uart_tx_assert_v — self-checking Verilog-2001 testbench
//
// Same two halves as the FIFO checker's suite, for the same reason: a
// property checker can fail by staying silent and it can fail by crying
// wolf, and only one of those is caught by pointing it at a correct design.
//
// HALF ONE binds the checker to the REAL published transmitter of Chapter
// 7.1 and sends frames in every parity mode. The requirement is ZERO
// violations over thousands of clocks.
//
// HALF TWO drives a SECOND checker instance with synthetic interface
// traffic that breaks one named property at a time, and requires that the
// right one fires.
//===========================================================================
`timescale 1ns/1ps
module tb_uart_tx_assert_v;
localparam DATA_W = 8;
localparam DIV = 8; // clocks per bit interval
localparam P_NONE = 2'd0, P_EVEN = 2'd1, P_ODD = 2'd2, P_MARK = 2'd3;
reg clk = 1'b0;
always #5 clk = ~clk;
reg rst_n = 1'b0;
//================================================================
// a baud tick: one pulse every DIV clocks
//================================================================
reg [7:0] divcnt = 8'd0;
reg baud_tick = 1'b0;
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin divcnt <= 8'd0; baud_tick <= 1'b0; end
else if (divcnt == DIV-1) begin divcnt <= 8'd0; baud_tick <= 1'b1; end
else begin divcnt <= divcnt + 1'b1; baud_tick <= 1'b0; end
end
//================================================================
// HALF ONE — the checker bound to the real transmitter
//================================================================
reg [DATA_W-1:0] tx_data = 8'h00;
reg [1:0] parity = P_NONE;
reg tx_valid = 1'b0;
wire tx_ready, tx_line, tx_busy;
uart_tx_v #(.DATA_W(DATA_W)) dut (
.clk(clk), .rst_n(rst_n), .baud_tick_i(baud_tick),
.tx_data_i(tx_data), .parity_mode_i(parity), .tx_valid_i(tx_valid),
.tx_ready_o(tx_ready), .tx_o(tx_line), .tx_busy_o(tx_busy));
wire [31:0] r_clocks, r_frames, r_fail;
wire [7:0] r_mask;
uart_tx_assert_v #(.DATA_W(DATA_W)) chk_real (
.clk(clk), .rst_n(rst_n), .baud_tick_i(baud_tick),
.tx_valid_i(tx_valid), .tx_ready_i(tx_ready), .tx_busy_i(tx_busy),
.tx_line_i(tx_line), .parity_mode_i(parity),
.n_clocks(r_clocks), .n_frames(r_frames), .n_fail(r_fail),
.fail_mask(r_mask));
//================================================================
// HALF TWO — a checker driven directly with illegal traffic
//================================================================
reg s_rst_n = 1'b0;
reg s_tick = 1'b0, s_valid = 1'b0, s_ready = 1'b1, s_busy = 1'b0, s_line = 1'b1;
reg [1:0] s_par = P_NONE;
wire [31:0] s_clocks, s_frames, s_fail;
wire [7:0] s_mask;
uart_tx_assert_v #(.DATA_W(DATA_W)) chk_synth (
.clk(clk), .rst_n(s_rst_n), .baud_tick_i(s_tick),
.tx_valid_i(s_valid), .tx_ready_i(s_ready), .tx_busy_i(s_busy),
.tx_line_i(s_line), .parity_mode_i(s_par),
.n_clocks(s_clocks), .n_frames(s_frames), .n_fail(s_fail),
.fail_mask(s_mask));
integer checks = 0, failures = 0;
task check;
input cond;
input [8*80-1:0] name;
begin
checks = checks + 1;
if (cond) $display(" PASS %0s", name);
else begin failures = failures + 1; $display(" FAIL %0s", name); end
end
endtask
integer i, pm, base_frames;
// Send one frame through the real transmitter and wait for it to finish.
task send;
input [DATA_W-1:0] d;
begin
@(negedge clk);
while (!tx_ready) @(negedge clk);
tx_data = d; tx_valid = 1'b1;
@(negedge clk);
while (!(tx_valid && tx_ready)) @(negedge clk);
@(negedge clk) tx_valid = 1'b0;
while (tx_busy) @(negedge clk);
repeat (2) @(negedge clk);
end
endtask
task s_reset;
begin
@(negedge clk);
s_rst_n = 1'b0;
s_tick = 1'b0; s_valid = 1'b0; s_ready = 1'b1;
s_busy = 1'b0; s_line = 1'b1; s_par = P_NONE;
repeat (2) @(negedge clk);
s_rst_n = 1'b1;
repeat (2) @(negedge clk);
end
endtask
initial begin
#50_000_000;
$display(" FAIL watchdog: simulation did not finish");
$display("== %0d checks, %0d failures ==", checks+1, failures+1);
$display(" RESULT: VERILOG TX-ASSERT TESTS FAILED (timeout)");
$finish;
end
initial begin
$display("== uart_tx_assert_v : self-checking Verilog testbench ==");
rst_n = 1'b0; s_rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (4) @(negedge clk);
//================================================================
// HALF ONE: legal frames in every parity mode
//================================================================
check(tx_line === 1'b1, "the real transmitter idles at MARK");
check(tx_ready === 1'b1 && tx_busy === 1'b0,
"and comes out of reset ready, not busy");
for (pm = 0; pm <= 3; pm = pm + 1) begin
@(negedge clk) parity = pm[1:0];
base_frames = r_frames;
send(8'h00); send(8'hFF); send(8'hA5); send(8'h55); send(8'h01);
check(r_frames - base_frames == 5,
(pm==0) ? "5 frames completed at parity NONE" :
(pm==1) ? "5 frames completed at parity EVEN" :
(pm==2) ? "5 frames completed at parity ODD" :
"5 frames completed at parity MARK");
end
check(r_clocks > 3000, "the checker evaluated over 3000 clocks");
check(r_fail == 0,
"ZERO violations across every parity mode -- the checker is not noisy");
check(r_mask == 8'h00, "and not one property ever fired");
//================================================================
// HALF TWO: each property, violated deliberately
//================================================================
// T1 -- idle line at SPACE
s_reset;
@(negedge clk) s_line = 1'b0; // idle, not busy, line low
repeat (2) @(negedge clk);
check(s_mask[0] === 1'b1, "T1 fires when the idle line is not MARK");
// T2 -- ready still high the cycle after an acceptance
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_busy = 1'b1; // ready left high
repeat (2) @(negedge clk);
check(s_mask[1] === 1'b1,
"T2 fires when ready is still high the cycle after an acceptance");
// T3 -- a handshake that is not followed by busy
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_busy = 1'b0; // busy never rose
repeat (2) @(negedge clk);
check(s_mask[2] === 1'b1, "T3 fires when busy does not follow a handshake");
// T4 -- ready returning long before the final bit interval
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0; s_line = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_ready = 1'b1; // one tick in, nine to go
repeat (2) @(negedge clk);
check(s_mask[3] === 1'b1,
"T4 fires when ready returns before the final bit interval");
// T6 -- the line is still MARK at the first DRIVEN tick
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1; // tick 0
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_tick = 1'b1; // tick 1: still MARK
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
check(s_mask[5] === 1'b1,
"T6 fires when the line is still MARK at the first driven tick");
// T7 -- the line moves with no baud tick
s_reset;
@(negedge clk) s_busy = 1'b1; s_ready = 1'b0; s_line = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_line = 1'b1; // moved, and s_tick is low
repeat (2) @(negedge clk);
check(s_mask[6] === 1'b1, "T7 fires when the line moves without a baud tick");
// T5 / T8 -- a frame that runs long, and one that ends early
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
for (i = 0; i < 20; i = i + 1) begin // far more than 10 bits
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
end
check(s_mask[4] === 1'b1, "T5 fires when a frame runs past its bit count");
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
@(negedge clk) s_busy = 1'b0; s_line = 1'b1; // one tick in, done
repeat (2) @(negedge clk);
check(s_mask[7] === 1'b1, "T8 fires when busy drops before the frame ends");
//================================================================
// and a legal synthetic frame fires nothing
//================================================================
// Built to the timing MEASURED from the real transmitter above:
// tick 0 is the transition (line still MARK), tick 1 carries the
// start bit, ticks 2..9 the data, and ready returns on the last.
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
for (i = 0; i < 10; i = i + 1) begin
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
if (i == 0) s_line = 1'b0; // start bit, from tick 1
else if (i < 9) s_line = ~s_line; // data
else s_line = 1'b1; // stop
if (i == 9) s_ready = 1'b1; // the back-to-back handoff
repeat (2) @(negedge clk);
end
@(negedge clk) s_line = 1'b1; s_busy = 1'b0; s_ready = 1'b1;
repeat (3) @(negedge clk);
check(s_fail == 0 && s_mask == 8'h00,
"a legal synthetic frame fires nothing at all");
$display("== %0d checks, %0d failures ==", checks, failures);
if (failures == 0) $display(" RESULT: ALL VERILOG TX-ASSERT TESTS PASSED");
else $display(" RESULT: VERILOG TX-ASSERT TESTS FAILED");
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
Snippet
//===========================================================================
// tb_uart_tx_assert — self-checking SystemVerilog testbench
//
// Same two halves as the FIFO checker's suite, for the same reason: a
// property checker can fail by staying silent and it can fail by crying
// wolf, and only one of those is caught by pointing it at a correct design.
//
// HALF ONE binds the checker to the REAL published transmitter of Chapter
// 7.1 and sends frames in every parity mode. The requirement is ZERO
// violations over thousands of clocks.
//
// HALF TWO drives a SECOND checker instance with synthetic interface
// traffic that breaks one named property at a time, and requires that the
// right one fires.
//===========================================================================
`timescale 1ns/1ps
module tb_uart_tx_assert;
localparam DATA_W = 8;
localparam DIV = 8; // clocks per bit interval
localparam P_NONE = 2'd0, P_EVEN = 2'd1, P_ODD = 2'd2, P_MARK = 2'd3;
logic clk = 1'b0;
always #5 clk = ~clk;
logic rst_n = 1'b0;
//================================================================
// a baud tick: one pulse every DIV clocks
//================================================================
logic [7:0] divcnt = 8'd0;
logic baud_tick = 1'b0;
always @(posedge clk or negedge rst_n) begin
if (!rst_n) begin divcnt <= 8'd0; baud_tick <= 1'b0; end
else if (divcnt == DIV-1) begin divcnt <= 8'd0; baud_tick <= 1'b1; end
else begin divcnt <= divcnt + 1'b1; baud_tick <= 1'b0; end
end
//================================================================
// HALF ONE — the checker bound to the real transmitter
//================================================================
logic [DATA_W-1:0] tx_data = 8'h00;
logic [1:0] parity = P_NONE;
logic tx_valid = 1'b0;
wire tx_ready, tx_line, tx_busy;
uart_tx #(.DATA_W(DATA_W)) dut (
.clk(clk), .rst_n(rst_n), .baud_tick_i(baud_tick),
.tx_data_i(tx_data), .parity_mode_i(parity), .tx_valid_i(tx_valid),
.tx_ready_o(tx_ready), .tx_o(tx_line), .tx_busy_o(tx_busy));
wire [31:0] r_clocks, r_frames, r_fail;
wire [7:0] r_mask;
uart_tx_assert #(.DATA_W(DATA_W)) chk_real (
.clk(clk), .rst_n(rst_n), .baud_tick_i(baud_tick),
.tx_valid_i(tx_valid), .tx_ready_i(tx_ready), .tx_busy_i(tx_busy),
.tx_line_i(tx_line), .parity_mode_i(parity),
.n_clocks(r_clocks), .n_frames(r_frames), .n_fail(r_fail),
.fail_mask(r_mask));
//================================================================
// HALF TWO — a checker driven directly with illegal traffic
//================================================================
logic s_rst_n = 1'b0;
logic s_tick = 1'b0, s_valid = 1'b0, s_ready = 1'b1, s_busy = 1'b0, s_line = 1'b1;
logic [1:0] s_par = P_NONE;
wire [31:0] s_clocks, s_frames, s_fail;
wire [7:0] s_mask;
uart_tx_assert #(.DATA_W(DATA_W)) chk_synth (
.clk(clk), .rst_n(s_rst_n), .baud_tick_i(s_tick),
.tx_valid_i(s_valid), .tx_ready_i(s_ready), .tx_busy_i(s_busy),
.tx_line_i(s_line), .parity_mode_i(s_par),
.n_clocks(s_clocks), .n_frames(s_frames), .n_fail(s_fail),
.fail_mask(s_mask));
int checks = 0, failures = 0;
task automatic check(input logic cond, input string name);
checks++;
if (cond) $display(" PASS %0s", name);
else begin failures++; $display(" FAIL %0s", name); end
endtask
int i, pm, base_frames;
// Send one frame through the real transmitter and wait for it to finish.
task send;
input [DATA_W-1:0] d;
begin
@(negedge clk);
while (!tx_ready) @(negedge clk);
tx_data = d; tx_valid = 1'b1;
@(negedge clk);
while (!(tx_valid && tx_ready)) @(negedge clk);
@(negedge clk) tx_valid = 1'b0;
while (tx_busy) @(negedge clk);
repeat (2) @(negedge clk);
end
endtask
task s_reset;
begin
@(negedge clk);
s_rst_n = 1'b0;
s_tick = 1'b0; s_valid = 1'b0; s_ready = 1'b1;
s_busy = 1'b0; s_line = 1'b1; s_par = P_NONE;
repeat (2) @(negedge clk);
s_rst_n = 1'b1;
repeat (2) @(negedge clk);
end
endtask
initial begin
#50_000_000;
$display(" FAIL watchdog: simulation did not finish");
$display("== %0d checks, %0d failures ==", checks+1, failures+1);
$display(" RESULT: SYSTEMVERILOG TX-ASSERT TESTS FAILED (timeout)");
$finish;
end
initial begin
$display("== uart_tx_assert : self-checking Verilog testbench ==");
rst_n = 1'b0; s_rst_n = 1'b0;
repeat (4) @(negedge clk);
rst_n = 1'b1;
repeat (4) @(negedge clk);
//================================================================
// HALF ONE: legal frames in every parity mode
//================================================================
check(tx_line === 1'b1, "the real transmitter idles at MARK");
check(tx_ready === 1'b1 && tx_busy === 1'b0,
"and comes out of reset ready, not busy");
for (pm = 0; pm <= 3; pm = pm + 1) begin
@(negedge clk) parity = pm[1:0];
base_frames = r_frames;
send(8'h00); send(8'hFF); send(8'hA5); send(8'h55); send(8'h01);
check(r_frames - base_frames == 5,
(pm==0) ? "5 frames completed at parity NONE" :
(pm==1) ? "5 frames completed at parity EVEN" :
(pm==2) ? "5 frames completed at parity ODD" :
"5 frames completed at parity MARK");
end
check(r_clocks > 3000, "the checker evaluated over 3000 clocks");
check(r_fail == 0,
"ZERO violations across every parity mode -- the checker is not noisy");
check(r_mask == 8'h00, "and not one property ever fired");
//================================================================
// HALF TWO: each property, violated deliberately
//================================================================
// T1 -- idle line at SPACE
s_reset;
@(negedge clk) s_line = 1'b0; // idle, not busy, line low
repeat (2) @(negedge clk);
check(s_mask[0] === 1'b1, "T1 fires when the idle line is not MARK");
// T2 -- ready still high the cycle after an acceptance
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_busy = 1'b1; // ready left high
repeat (2) @(negedge clk);
check(s_mask[1] === 1'b1,
"T2 fires when ready is still high the cycle after an acceptance");
// T3 -- a handshake that is not followed by busy
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_busy = 1'b0; // busy never rose
repeat (2) @(negedge clk);
check(s_mask[2] === 1'b1, "T3 fires when busy does not follow a handshake");
// T4 -- ready returning long before the final bit interval
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0; s_line = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_ready = 1'b1; // one tick in, nine to go
repeat (2) @(negedge clk);
check(s_mask[3] === 1'b1,
"T4 fires when ready returns before the final bit interval");
// T6 -- the line is still MARK at the first DRIVEN tick
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1; // tick 0
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_tick = 1'b1; // tick 1: still MARK
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
check(s_mask[5] === 1'b1,
"T6 fires when the line is still MARK at the first driven tick");
// T7 -- the line moves with no baud tick
s_reset;
@(negedge clk) s_busy = 1'b1; s_ready = 1'b0; s_line = 1'b0;
repeat (2) @(negedge clk);
@(negedge clk) s_line = 1'b1; // moved, and s_tick is low
repeat (2) @(negedge clk);
check(s_mask[6] === 1'b1, "T7 fires when the line moves without a baud tick");
// T5 / T8 -- a frame that runs long, and one that ends early
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
for (i = 0; i < 20; i = i + 1) begin // far more than 10 bits
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
repeat (2) @(negedge clk);
end
check(s_mask[4] === 1'b1, "T5 fires when a frame runs past its bit count");
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1; s_line = 1'b0;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
@(negedge clk) s_busy = 1'b0; s_line = 1'b1; // one tick in, done
repeat (2) @(negedge clk);
check(s_mask[7] === 1'b1, "T8 fires when busy drops before the frame ends");
//================================================================
// and a legal synthetic frame fires nothing
//================================================================
// Built to the timing MEASURED from the real transmitter above:
// tick 0 is the transition (line still MARK), tick 1 carries the
// start bit, ticks 2..9 the data, and ready returns on the last.
s_reset;
@(negedge clk) s_valid = 1'b1; s_ready = 1'b1;
@(negedge clk) s_valid = 1'b0; s_ready = 1'b0; s_busy = 1'b1;
for (i = 0; i < 10; i = i + 1) begin
@(negedge clk) s_tick = 1'b1;
@(negedge clk) s_tick = 1'b0;
if (i == 0) s_line = 1'b0; // start bit, from tick 1
else if (i < 9) s_line = ~s_line; // data
else s_line = 1'b1; // stop
if (i == 9) s_ready = 1'b1; // the back-to-back handoff
repeat (2) @(negedge clk);
end
@(negedge clk) s_line = 1'b1; s_busy = 1'b0; s_ready = 1'b1;
repeat (3) @(negedge clk);
check(s_fail == 0 && s_mask == 8'h00,
"a legal synthetic frame fires nothing at all");
$display("== %0d checks, %0d failures ==", checks, failures);
if (failures == 0) $display(" RESULT: ALL SYSTEMVERILOG TX-ASSERT TESTS PASSED");
else $display(" RESULT: SYSTEMVERILOG TX-ASSERT TESTS FAILED");
$finish;
end
endmoduleAzvya Education Pvt. Ltd.VLSI Mentor
Snippet
--===========================================================================
-- tb_uart_tx_assert — self-checking VHDL-2008 testbench
--
-- Same two halves as the FIFO checker's suite: a conforming transmitter
-- that must produce ZERO violations, and synthetic traffic that must make
-- each named property fire.
--
-- A NOTE ON THE FIXTURE. The Verilog and SystemVerilog versions bind the
-- checker to the real published transmitter of Chapter 7.1. There is no
-- VHDL edition of that block in this curriculum, so half one uses a
-- behavioural model built to the timing MEASURED from the real one:
--
-- tick 0 : the FSM leaves IDLE, the registered line is still MARK
-- tick 1 : the start bit is on the wire
-- ticks 2..9 : the data bits, least significant first
-- tick 9 : ready returns, so the next byte can be handed over with no
-- gap -- ready and busy overlap ON PURPOSE (Chapter 7.4)
--
-- Those last two lines are the ones that broke three properties in their
-- first draft. The fixture reproduces them because a fixture that behaved
-- the way the checker's author ASSUMED would have hidden the bug.
--
-- Same 18 counted checks as the Verilog and SystemVerilog twins.
--===========================================================================
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity tb_uart_tx_assert is
end entity tb_uart_tx_assert;
architecture sim of tb_uart_tx_assert is
constant DATA_W : positive := 8;
constant DIV : positive := 8;
constant TCLK : time := 10 ns;
signal clk : std_logic := '0';
signal rst_n : std_logic := '0';
signal done : boolean := false;
signal baud_tick : std_logic := '0';
-- HALF ONE: the conforming transmitter fixture
signal tx_data : std_logic_vector(DATA_W-1 downto 0) := (others => '0');
signal parity : std_logic_vector(1 downto 0) := "00";
signal tx_valid : std_logic := '0';
signal tx_ready : std_logic := '1';
signal tx_busy : std_logic := '0';
signal tx_line : std_logic := '1';
signal r_clocks, r_frames, r_fail : natural;
signal r_mask : std_logic_vector(7 downto 0);
-- HALF TWO: the synthetic checker
signal s_rst_n : std_logic := '0';
signal s_tick, s_valid : std_logic := '0';
signal s_ready : std_logic := '1';
signal s_busy : std_logic := '0';
signal s_line : std_logic := '1';
signal s_par : std_logic_vector(1 downto 0) := "00";
signal s_clocks, s_frames, s_fail : natural;
signal s_mask : std_logic_vector(7 downto 0);
begin
clk <= not clk after TCLK/2 when not done else '0';
tickgen : process (clk, rst_n)
variable dc : natural := 0;
begin
if rst_n = '0' then dc := 0; baud_tick <= '0';
elsif rising_edge(clk) then
if dc = DIV-1 then dc := 0; baud_tick <= '1';
else dc := dc + 1; baud_tick <= '0'; end if;
end if;
end process tickgen;
-----------------------------------------------------------------------
-- A CONFORMING TRANSMITTER, behavioural. Testbench fixture.
-----------------------------------------------------------------------
fixture : process (clk, rst_n)
variable cnt : natural := 0;
variable shr : std_logic_vector(DATA_W-1 downto 0);
variable busy : boolean := false;
begin
if rst_n = '0' then
cnt := 0; busy := false;
tx_ready <= '1'; tx_busy <= '0'; tx_line <= '1';
elsif rising_edge(clk) then
if (tx_valid = '1') and (tx_ready = '1') then
shr := tx_data;
cnt := 0;
busy := true;
tx_busy <= '1';
tx_ready <= '0';
elsif busy and baud_tick = '1' then
if cnt = 0 then tx_line <= '0'; -- start
elsif cnt <= DATA_W then tx_line <= shr(cnt-1); -- data, LSB first
elsif cnt = DATA_W + 1 then
tx_line <= '1'; -- stop
tx_ready <= '1'; -- back-to-back handoff
end if;
if cnt = DATA_W + 1 then
busy := false;
tx_busy <= '0';
end if;
cnt := cnt + 1;
end if;
end if;
end process fixture;
chk_real : entity work.uart_tx_assert
generic map (DATA_W => DATA_W)
port map (clk => clk, rst_n => rst_n, baud_tick_i => baud_tick,
tx_valid_i => tx_valid, tx_ready_i => tx_ready,
tx_busy_i => tx_busy, tx_line_i => tx_line,
parity_mode_i => parity,
n_clocks => r_clocks, n_frames => r_frames,
n_fail => r_fail, fail_mask => r_mask);
chk_synth : entity work.uart_tx_assert
generic map (DATA_W => DATA_W)
port map (clk => clk, rst_n => s_rst_n, baud_tick_i => s_tick,
tx_valid_i => s_valid, tx_ready_i => s_ready,
tx_busy_i => s_busy, tx_line_i => s_line,
parity_mode_i => s_par,
n_clocks => s_clocks, n_frames => s_frames,
n_fail => s_fail, fail_mask => s_mask);
watchdog : process
begin
wait for 50 ms;
report "watchdog: simulation did not finish" severity failure;
end process watchdog;
stim : process
variable checks, failures : natural := 0;
variable base_frames : natural;
procedure check(cond : boolean; name : string) is
begin
checks := checks + 1;
if cond then report " PASS " & name severity note;
else failures := failures + 1; report " FAIL " & name severity error;
end if;
end procedure check;
procedure send(d : std_logic_vector(DATA_W-1 downto 0)) is
begin
wait until falling_edge(clk);
while tx_ready /= '1' loop wait until falling_edge(clk); end loop;
tx_data <= d; tx_valid <= '1';
wait until falling_edge(clk);
while not (tx_valid = '1' and tx_ready = '1') loop
wait until falling_edge(clk);
end loop;
wait until falling_edge(clk); tx_valid <= '0';
while tx_busy = '1' loop wait until falling_edge(clk); end loop;
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
end procedure send;
procedure s_reset is
begin
wait until falling_edge(clk);
s_rst_n <= '0'; s_tick <= '0'; s_valid <= '0'; s_ready <= '1';
s_busy <= '0'; s_line <= '1'; s_par <= "00";
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
s_rst_n <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
end procedure s_reset;
procedure s_pulse_tick is
begin
wait until falling_edge(clk); s_tick <= '1';
wait until falling_edge(clk); s_tick <= '0';
end procedure s_pulse_tick;
begin
report "== uart_tx_assert : self-checking VHDL testbench ==" severity note;
rst_n <= '0'; s_rst_n <= '0';
for i in 1 to 4 loop wait until falling_edge(clk); end loop;
rst_n <= '1';
for i in 1 to 4 loop wait until falling_edge(clk); end loop;
--=== HALF ONE: legal frames ========================================
check(tx_line = '1', "the transmitter fixture idles at MARK");
check(tx_ready = '1' and tx_busy = '0',
"and comes out of reset ready, not busy");
for pm in 0 to 3 loop
wait until falling_edge(clk);
parity <= std_logic_vector(to_unsigned(pm, 2));
base_frames := r_frames;
send(x"00"); send(x"FF"); send(x"A5"); send(x"55"); send(x"01");
if pm = 0 then
check(r_frames - base_frames = 5, "5 frames completed at parity NONE");
elsif pm = 1 then
check(r_frames - base_frames = 5, "5 frames completed at parity EVEN");
elsif pm = 2 then
check(r_frames - base_frames = 5, "5 frames completed at parity ODD");
else
check(r_frames - base_frames = 5, "5 frames completed at parity MARK");
end if;
end loop;
check(r_clocks > 3000, "the checker evaluated over 3000 clocks");
check(r_fail = 0,
"ZERO violations across every parity mode -- the checker is not noisy");
check(r_mask = x"00", "and not one property ever fired");
--=== HALF TWO: each property, violated deliberately ================
s_reset;
wait until falling_edge(clk); s_line <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(0) = '1', "T1 fires when the idle line is not MARK");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1'; s_line <= '0';
wait until falling_edge(clk); s_valid <= '0'; s_busy <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(1) = '1',
"T2 fires when ready is still high the cycle after an acceptance");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1'; s_line <= '0';
wait until falling_edge(clk); s_valid <= '0'; s_busy <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(2) = '1', "T3 fires when busy does not follow a handshake");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1'; s_line <= '0';
wait until falling_edge(clk); s_valid <= '0'; s_ready <= '0'; s_busy <= '1';
s_pulse_tick;
wait until falling_edge(clk); s_line <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
wait until falling_edge(clk); s_ready <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(3) = '1', "T4 fires when ready returns before the final bit interval");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1';
wait until falling_edge(clk); s_valid <= '0'; s_ready <= '0'; s_busy <= '1';
s_pulse_tick; -- tick 0
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
s_pulse_tick; -- tick 1, line still MARK
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(5) = '1',
"T6 fires when the line is still MARK at the first driven tick");
s_reset;
wait until falling_edge(clk); s_busy <= '1'; s_ready <= '0'; s_line <= '0';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
wait until falling_edge(clk); s_line <= '1'; -- moved with no tick
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(6) = '1', "T7 fires when the line moves without a baud tick");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1'; s_line <= '0';
wait until falling_edge(clk); s_valid <= '0'; s_ready <= '0'; s_busy <= '1';
for i in 1 to 20 loop
s_pulse_tick;
for k in 1 to 2 loop wait until falling_edge(clk); end loop;
end loop;
check(s_mask(4) = '1', "T5 fires when a frame runs past its bit count");
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1'; s_line <= '0';
wait until falling_edge(clk); s_valid <= '0'; s_ready <= '0'; s_busy <= '1';
s_pulse_tick;
wait until falling_edge(clk); s_busy <= '0'; s_line <= '1';
for i in 1 to 2 loop wait until falling_edge(clk); end loop;
check(s_mask(7) = '1', "T8 fires when busy drops before the frame ends");
--=== a legal synthetic frame fires nothing ==========================
s_reset;
wait until falling_edge(clk); s_valid <= '1'; s_ready <= '1';
wait until falling_edge(clk); s_valid <= '0'; s_ready <= '0'; s_busy <= '1';
for i in 0 to 9 loop
s_pulse_tick;
if i = 0 then s_line <= '0';
elsif i < 9 then s_line <= not s_line;
else s_line <= '1'; s_ready <= '1';
end if;
for k in 1 to 2 loop wait until falling_edge(clk); end loop;
end loop;
wait until falling_edge(clk); s_line <= '1'; s_busy <= '0'; s_ready <= '1';
for i in 1 to 3 loop wait until falling_edge(clk); end loop;
check(s_fail = 0 and s_mask = x"00",
"a legal synthetic frame fires nothing at all");
report "== " & integer'image(checks) & " checks, "
& integer'image(failures) & " failures ==" severity note;
if failures = 0 then
report " RESULT: ALL VHDL TX-ASSERT TESTS PASSED" severity note;
else
report " RESULT: VHDL TX-ASSERT TESTS FAILED" severity error;
end if;
done <= true;
wait;
end process stim;
end architecture sim;Twenty checks for the FIFO checker and eighteen for the transmitter, identical across all three languages:
Azvya Education Pvt. Ltd.VLSI Mentor
Snippet
PASS the real FIFO filled to DEPTH
PASS checker silent while the FIFO filled legally
PASS an overflow event is not a property violation
PASS push and pop together while FULL is accepted, not an overflow
PASS the checker evaluated over 4000 clocks of traffic
PASS ZERO violations across the whole legal soak -- the checker is not noisy
PASS P1 fires when the level exceeds DEPTH
PASS P4 fires when the level changes without an accepted push or pop
PASS P7 fires when empty and full assert together
PASS walking the level legally from 0 to DEPTH and back fires nothing
== 20 checks, 0 failures ==
PASS the real transmitter idles at MARK
PASS 5 frames completed at parity NONE / EVEN / ODD / MARK
PASS ZERO violations across every parity mode -- the checker is not noisy
PASS T1 fires when the idle line is not MARK
PASS T6 fires when the line is still MARK at the first driven tick
PASS a legal synthetic frame fires nothing at all
== 18 checks, 0 failures ==
Verilog-2001 : 20 / 0 and 18 / 0
SystemVerilog : 20 / 0 and 18 / 0
VHDL-2008 + PSL : 20 / 0 and 18 / 07. Verification
Bind the checker to a real design and require silence. A checker exercised only against synthetic stimulus has never been shown not to be noisy, and noisy is the failure mode that gets assertions ignored.
Drive every property to fire at least once. An assertion that has never fired has not been shown to work. Half two of each suite exists for this and nothing else.
Give every property an identifier and report it. P4 says the accounting is wrong; "an assertion failed" says nothing. The fail_mask output exists so a testbench can assert on which property fired rather than on how many did.
Check the boolean once. In the VHDL files each property is a named signal used by both the PSL directive and the counter, so the two can never drift into paraphrases of each other — which is a real risk when a property is stated twice in two notations.
Measure timing before asserting it. §5's callout. Four of six property bugs in this chapter were about when, not what.
8. Debugging
9. Understanding Check
10. Summary
A checker watches the interface, never the implementation — which is what makes it bindable and what stops it agreeing with a broken design.
Verilog-2001 has no assertions; Icarus rejects every SystemVerilog concurrent assertion; VHDL with PSL runs always, never, next, until, sequences and cover. On this toolchain the oldest language is the most capable, verified by running each construct rather than by reading a manual.
Four properties out of sixteen were wrong on the first attempt, producing 3,078, 189, 41 and 40 false failures against correct, published designs.
Three distinct traps: sampling a registered value against the current cycle; asserting a simpler specification than the design deliberately implements; and asserting folklore that is true of other transmitters but not this one.
Timing properties should be written from a measurement, not from the specification and certainly not from the RTL.
Every suite has two halves — silence against the real design, and one deliberate violation per property — because a checker that has never fired has not been shown to work.
62 checks per language, 186 in total, 0 failures.
11. What Comes Next
Chapter 15.3 builds the coverage model that says which of these situations were ever reached — and shows a real defect that survived the whole suite because one bin was empty.
Browse the full path on the UART tutorials index. For the property catalogue these implement, read back to Chapter 15.1.
Continue learning
Related tutorials
- Related topic
UART Design Review: The Questions a Reviewer Asks
Twenty-five review questions across RTL, timing, integration, verification and debug, five of them implemented as a synthesisable probe in three HDLs and the same properties written in PSL, where they run as real concurrent assertions.
- Related topic
UART Properties Worth Asserting
Which UART rules deserve a continuous assertion and which a scoreboard already covers, with a test that separates them — and the properties that look valuable until you ask what would notice them failing.
- Related topic
SPI Protocol Assertions
A property attempt has four outcomes, not two, and the two that are not failures are where a suite's silence comes from. Seven SPI properties measured for passes, vacuous evaluations and attempts still open at the end of the test, with the same six obligations run a second time as PSL assertions by a real assertion engine.
- Related topic
USB Assertions
“Eventually” has no failing case, so it cannot be checked in a finite run — every real liveness check is bounded, a window has two edges, and an obligation still outstanding at end of test is a failure, not an unknown.
Where this fits
Part of the UART curriculum.