Writing Good Properties

A formal tool checks exactly what you write, so the quality of the properties decides the quality of the result. A property that copies the RTL passes on a buggy design. A property that mixes three ideas fails with a counterexample nobody can read. A property with a trigger that never happens passes without checking anything. This article collects the habits that separate useful properties from useless ones, with a real example of a property that hides the bug it was written to find.

9 min read | Intermediate

What You'll Learn

• Write properties from the specification instead of from the RTL
• Keep one idea per assertion and name assertions consistently
• Choose between end-to-end and internal properties
• Review a property set for gaps, vacuity and duplication

Write From the Specification, Not From the RTL

The most common mistake is to read the RTL and turn each line into an assertion. Take the FIFO counter from the reading a counterexample article. Its RTL says full = (count == 3'd5). Copy that into a property:

a_full_rtl: assert property (@(posedge clk) disable iff (rst) full == (count == 3'd5));

It passes. Of course it does: it says the same thing as the code, including the typo. Now write the rule from the specification, which says the FIFO has 4 entries:

a_count: assert property (@(posedge clk) disable iff (rst) count <= 3'd4);

It fails at step 7 and shows the bug.

A property that restates the RTL can only find bugs in the tool, never in the design. Worse, it breaks when the design is fixed: correct the RTL to count == 3'd4 and the copied property fails, because it still expects 5. It tests the code against an old copy of itself.

Good properties describe what the block must do, in terms of its purpose. Ask "what would the person who wrote the specification check?", not "what does this line do?".

One Idea per Assertion

A property that checks several things at once is hard to debug:

// hard to read and to debug
a_all: assert property (@(posedge clk) disable iff (rst)
         $onehot0(gnt) and ##1 ((gnt & ~$past(req)) == 0) and (req != 0 |=> gnt != 0));

When it fails, which part failed? Split it into separate assertions, each with its own name. The counterexample then points straight at the broken rule, and each rule can be switched off or relaxed on its own.

Names and Comments

Use a short prefix for the kind of statement and a name for the rule: a_ for assertions, m_ or asm_ for assumptions, c_ for covers. a_fifo_no_overflow in a report tells the reader what broke without opening the file. A comment above each property with the sentence of the specification it comes from makes reviews quick and keeps the property honest.

End-to-End or Internal?

An end-to-end property talks only about the inputs and outputs of a block: "every word written is read out unchanged". An internal property talks about internal signals: "the write pointer equals the read pointer plus the count".

• End-to-end properties match the specification directly and survive changes to the implementation. They are the ones that matter for sign-off.
• Internal properties are easier for the tool, catch bugs closer to the cause, and are needed later to make full proofs work, as Chapter 6 shows.

Use both. Start with end-to-end rules from the specification, and add internal ones where they help the tool or the debugging.

Keep Assumptions Few and Justified

Each assumption removes input sequences from the search. Write only assumptions that the specification promises, say where each one comes from, and check the same rule as an assertion on the neighbor block where you can. An assumption that "makes the counterexample go away" without a reason in the specification is hiding a bug.

Cover What You Assert

For every implication, add a cover for its trigger, and for every block a cover for its main activity: a FIFO that becomes full, a job that finishes, a grant to each requester. If a cover is unreachable, the assertions that depend on it are passing vacuously. The assert, assume and cover article shows an example.

A Review Checklist

• Does every property come from a sentence of the specification?
• Does any property repeat an expression from the RTL?
• Does each assertion check one idea, with a name that says which?
• Is every assumption justified by the specification, and as weak as possible?
• Does every trigger have a cover, and is every cover reachable?
• Are there data properties, not just control properties?
• Is there a progress rule for every block that must answer requests?
• Is the depth large enough for the interesting states to be reached?

Running It in ChipVerify Lab

The example below is the buggy FIFO counter with both properties: the copied one and the one from the specification. Only the second one fails.

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // restates the RTL: passes, because it repeats the same mistake
  always @(posedge clk) if (!init) assert (full == (count == 3'd5));
  // from the specification: a 4-entry FIFO never holds more than 4
  always @(posedge clk) if (!init) assert (count <= 3'd4);
`endif

Common Mistakes