Most assumptions describe a protocol: the rules that the block on the other side of an interface follows. A memory only responds to requests it received, a sender holds its data until it is taken, a bus master never starts a new burst in the middle of one. This article shows how to turn such rules into assumptions, how they connect to assertions on the neighbor block, and what goes wrong when an assumption models the wrong environment.
9 min read | Intermediate
What You'll Learn
- Turn the protocol rules of a neighbor into assumptions
- Explain assume-guarantee: an assumption here is an assertion there
- Check that a transaction counter cannot wrap, given a well-behaved memory
- Spot an assumption that describes an environment different from the real one
Protocols as Assumptions
An interface specification usually lists rules for each side. When you check one block, the rules for its own side become assertions, and the rules for the other side become assumptions. Together the assumptions form a model of a well-behaved neighbor: the tool may do anything that neighbor could legally do, and nothing else.
The best assumptions are copied from the interface specification, rule by rule. For a valid/ready receiver, the sender rules from the handshake properties article become assumptions: valid is held until ready, and the data is stable while waiting.
m_valid_hold: assume property (@(posedge clk) disable iff (rst) valid && !ready |=> valid);
m_data_hold: assume property (@(posedge clk) disable iff (rst) valid && !ready |=> $stable(data));
The same two lines, with assert instead of assume, check the sender.
Assume-Guarantee
An assumption is a promise that the neighbor makes. If you check the neighbor with the same rule as an assertion, the promise is verified, and the two checks together cover the connection. This is called assume-guarantee reasoning: each block assumes what its neighbors guarantee, and each guarantee is proven on the block that makes it.
An assumption that is never checked on the other side is a gap. It may be right, but nothing confirms it. A verification plan should list every assumption and say where it is checked.
Quick Check
Q: A receiver is checked with the assumption "data is stable while valid and not ready". What should be checked on the sender?
Show Answer
The same rule as an assertion. Then the receiver's assumption is backed by a proof on the sender, and the interface as a whole is covered.
The Design: a Transaction Tracker
This block issues read requests to a memory and counts how many are in flight. It allows at most 3, so req is blocked when the count is 3. A response from the memory lowers the count:
module txn_tracker (input clk, input rst, input go, input resp,
output req, output [1:0] outstanding);
reg [1:0] cnt;
assign outstanding = cnt;
assign req = go && (cnt != 2'd3);
always @(posedge clk)
if (rst) cnt <= 2'd0;
else if (req && !resp) cnt <= cnt + 2'd1;
else if (!req && resp) cnt <= cnt - 2'd1;
endmodule
Two rules for the tracker: no request goes out when 3 are in flight, and a response always lowers the count by one, so the count never wraps.
a_max: assert property (@(posedge clk) disable iff (rst) !(req && cnt == 2'd3));
a_dec: assert property (@(posedge clk) disable iff (rst) resp && !req |=> cnt == $past(cnt) - 2'd1);
The First Run: a Response Nobody Asked For
Without assumptions about the memory, the check fails at step 3:
The tool sends a response in step 1, when nothing is in flight. The count wraps from 0 to 3, and from then on the tracker believes three requests are pending. No real memory sends a response without a request, so this is an impossible input. The interface specification says so: every response belongs to an earlier request.
The Protocol Assumption
m_resp: assume property (@(posedge clk) disable iff (rst) resp |-> cnt != 2'd0);
It reads "the memory only responds while a request is in flight". Note that it uses the internal count of the tracker to describe the memory. That is acceptable here because the count is exactly the number of requests the memory has received. The cleaner alternative is a small model of the memory side, a separate counter in the formal code, which is what larger checks do.
Running It in ChipVerify Lab
`ifdef FORMAL
reg init = 1'b1;
always @(posedge clk) init <= 1'b0;
always @(*) if (init) assume (rst);
// the memory only responds to a request that is in flight
always @(*) if (!init) assume (!resp || cnt != 2'd0);
// never more than 3 in flight, and no request when 3 are in flight
always @(posedge clk) if (!init) assert (!(req && cnt == 2'd3));
// a response always matches a request in flight: cnt never wraps
always @(posedge clk)
if (!init && !$past(rst) && $past(resp) && !$past(req))
assert (cnt == $past(cnt) - 2'd1 && $past(cnt) != 2'd0);
`endif
With the assumption the run passes. Remove the assume line to see the counterexample of this article.
Quick Check
Q: The assumption uses an internal signal, cnt. Why is that not "constraining the design"?
Show Answer
The assumption restricts only resp, an input. It reads cnt to know how many requests the memory has received, but it does not force cnt to any value. Assumptions may read internal signals; they must only constrain inputs.
Common Mistakes
Mistake #1: Writing assumptions from intuition instead of the specification
"The memory responds sensibly" is not an assumption. Copy each rule of the interface specification for the other side into its own assumption, so that each one can be reviewed and checked on the neighbor.
Mistake #2: Leaving assumptions unchecked
An assumption that nobody verifies on the other side is a hole in the verification. Check it as an assertion on the neighbor, or at least in simulation.
Mistake #3: Modelling a different environment
An assumption that looks reasonable can describe a neighbor that does not exist. The exercise shows one: the check passes, but for the wrong environment.
Practice Exercise
Challenge: The Wrong Memory
Open the example and run it. A colleague suggests a simpler assumption: assume (!resp || req), "a response only comes together with a request". Replace the assumption with it and run. Then ask whether a normal response, one that comes in a cycle without a new request, can still happen. In the lab you can ask this with a check that is meant to fail: add always @(posedge clk) if (!init) assert (!(resp && !req));. If it fails, the situation is reachable. Run it with both assumptions. Why is the simpler assumption wrong, even though the real assertions pass?
Hint
When does a real memory send its response: in the same cycle as the request, or later?
Solution
The assertions pass, because with a request and a response in the same cycle the count does not change. But the assumption describes a memory that only answers in a cycle where a new request is issued. A real memory answers later, often when no new request is being sent. The meant-to-fail check passes with the simpler assumption, so a response without a new request is unreachable. With the original assumption it fails at step 3, which shows the normal case is in the search. The simpler assumption removed every normal response, and the check passed for an environment that does not exist. In SVA this question is a cover, cover property (@(posedge clk) resp && !req);, and the cover properties article explains the trick of asserting the negation.
Open the ready-made example in the lab and run the formal check from the formal panel. The free tier allows a depth of up to 10 cycles, and PRO allows up to 100.
Summary
- Protocol rules for the other side of an interface become assumptions; rules for your own side become assertions.
- Assume-guarantee: each assumption should be proven as an assertion on the neighbor that makes the promise.
- Without a protocol assumption, the transaction tracker received a response nobody asked for and its count wrapped.
- Assumptions may read internal signals, but they may only restrict inputs.
- An assumption can pass every check and still describe the wrong environment. Covers for normal behavior catch that.
