UART Properties Worth Asserting

An assertion is a claim that something is true on every clock, forever, and that is a strong thing to say. Most of what a verification environment checks is not like that at all: a scoreboard compares one transaction against one prediction, once, after the fact. Both are useful. Confusing them produces suites that assert things no design could violate and miss the rules that no scoreboard can see.

This chapter is the sorting exercise. It ends with a catalogue of the properties this UART actually has, and with three that look excellent and are not.

1. The Test: Would Anything Else Notice?

A rule deserves a continuous assertion when both halves of this are true:

1. It holds on every clock, not at the end of a transaction.
2. No scoreboard would see it break.

The second half is the one that does the work, and it is worth applying ruthlessly.

The pattern in the right-hand column is the whole chapter. Every row that earns an assertion is a rule whose violation produces no wrong byte. It produces a link that works and then stops working, or a queue that quietly loses one entry a week, or a transmitter that is fine until someone connects a second master.

2. The Catalogue

These are the properties this UART has. They are grouped by the block they belong to, and each names the interface signals it watches — a property that needs a signal the block does not expose is not a property of that block.

Transmitter

Synchronous FIFO

Receiver and status

R2, R4 and R5 were each checked as counted invariants in Modules 13 and 14 rather than as assertions, and that was the right call there: those suites drove the blocks directly and could make an arithmetic claim at the end. Written as assertions they become reusable — bindable to the block wherever it is instantiated, including inside the assembled IP where no directed suite is driving it.

3. Three Properties Worth Not Writing

Every assertion has a cost: it is read, maintained, and eventually debugged by someone who did not write it. These three look valuable and are not.

"The transmitter never asserts busy without a preceding handshake."

True, and unfalsifiable by any stimulus the environment can produce. busy is driven from a state machine whose only entry is the handshake; there is no input sequence that separates them. An assertion nothing can violate is documentation with a runtime cost — and worse, it inflates an assertion count that someone will quote as evidence.

"The received byte equals the transmitted byte in loopback."

This is a scoreboard check wearing an assertion's clothes. It is a claim about one transaction, it needs the reference model to evaluate, and writing it as a continuous property means evaluating it on every clock in order to be true vacuously on almost all of them.

"The baud tick period is exactly CLK_HZ / BAUD_HZ clocks."

Tempting, and wrong in a way that takes a while to see: with a fractional divider it is deliberately not constant. Chapter 8.3 builds an accumulator whose whole purpose is to alternate between two periods so the average is right. An assertion demanding a constant period fails on the correct design — which is the failure mode Chapter 15.2 spends most of its length on.

4. Where the Three Languages Diverge

The properties are language-independent. Writing them is not, and the differences on this toolchain are larger and stranger than expected.

The middle column is the surprise. SystemVerilog has SVA — it is the language's headline verification feature — and Icarus Verilog 13.0 answers every concurrent assertion with sorry: concurrent_assertion_item not supported. Inline properties, named properties, properties without disable iff, purely boolean properties: each was tried, each refused.

So on this toolchain the oldest of the three languages has the most expressive assertion support, by a distance. Chapter 15.2 §4 shows what that looks like in practice and what the other two have to do instead.

5. Understanding Check

6. Summary

An assertion claims something holds on every clock; a scoreboard compares one transaction once. Both are necessary and they answer different questions.

The test for a property is whether anything else would notice it failing. Every UART rule that earns an assertion is one whose violation produces no wrong byte — a stuck-low line, a frame of the wrong length, a flag that lies, a level that exceeds its depth.

Sixteen properties across the transmitter, the FIFO and the receiver, each named, each watching interface signals only.

P4 — the FIFO accounting property — is the one that would survive a purge, and the other seven exist to localise a failure rather than to detect one.

Three properties are worth not writing: one nothing can violate, one that is a scoreboard check in disguise, and one that is false on a correct fractional baud generator.

And a confidently wrong assertion is more expensive than a missing one, because the usual response to a checker that argues with a correct design is to stop reading it.

7. What Comes Next

Chapter 15.2 writes this catalogue as code, in all three languages, bound to the published transmitter and FIFO — and records the four properties that were wrong on the first attempt, with the number of false failures each one produced.

Browse the full path on the UART tutorials index. For the scoreboard side of the boundary drawn in §1, read back to Chapter 14.5.