Properties Interview Questions

An assumption deletes every input sequence that breaks it. So an assumption stronger than the real environment deletes legal behaviour along with the bug. The proof is then true of a world the chip never sees. Write assumptions only on ports, from the spec, and pair each with a cover of behaviour it should still allow. An unreached cover is the alarm.

The neighbouring block can only promise things it can see, which are the ports. A rule about internal state is a claim about the design itself, so it should be asserted and proven. Assumed instead, it can quietly delete the very states where the bug lives.

Keep the suspect assumption and replace the assertion with three covers. They are the FIFO full, a push while the count is 16, and a pop while empty. The full and pop-on-empty covers are reached, at steps 19 and 2. The push at a count of 16 is unreached, which is exactly the behaviour the assumption deleted.

From that point on no legal trace exists, so every assertion that needs to look past it passes for nothing. Some tools report a conflict when the assumptions are unsatisfiable from reset, but not every case is caught. Covers of normal behaviour after that point are the reliable check.

Add covers of normal behaviour at growing depths, and find where they stop being reached. Then disable assumptions one at a time and rerun the covers. An assumption whose removal brings them back is part of the conflict. Fix it from the spec, and keep the covers as a standing check.

Under-constraint gives false failures: they cost debug time, but every one is visible in a trace. Over-constraint gives false passes, which look exactly like real ones. Over-constraint is the dangerous one, and covers under the full assumption set are the only routine defence against it.

List every assumption with its spec row and a cover showing legal behaviour survives it. Also list where it is checked at system level, usually a bound assertion in simulation. Anything without a spec row is either removed or escalated as a design requirement. The review signs off the list, not the proof.

The inputs are free, so the solver drove a sequence no legal master sends: it changed the address during a stall. The failure is false; the bench is under-constrained. Add one assumption from the spec row and cite the row. It says arvalid stays high and the address stays stable until the handshake. Then cover the stall and the handshake so the assumption did not go too far.

A long list written up front is likely to include rules stronger than the real environment, and nothing tells you which. Starting loose means you add each assumption in answer to a trace that showed an illegal input. So every assumption has a reason and a spec row. The false failures are cheap; a silent over-constraint is not.

The address is now stuck at its starting value, so most legal reads never happen. The pass says nothing about other addresses. A cover of a handshake at address 8'hFF comes back unreached, which shows the assumption removed legal traffic.

Write the spec rule: while arvalid waits for arready, the address holds. In this bench that is arvalid && !arready |=> araddr == araddr_q. Between transfers the address is free again. Then rerun the covers: the stall, the handshake and the handshake at 8'hFF must all be reached.

Not yet: those are glue properties about the mechanism, and they miss bugs that leave the pointers and count intact. Write an end-to-end check at the ports first: every accepted word leaves once, in order and unchanged. In the lesson, this glue set passes depth 10 on a FIFO that reads the wrong slot. The end-to-end check fails at step 3. Keep the glue to localise failures and feed induction.

Glue properties check the mechanism: pointers stay consistent with the count and full and empty agree with them. A bug in what is read, such as the wrong slot or stale data, leaves all of that intact. Only a property that compares what leaves with what entered, the purpose of the block, can see it.

Track one word whose value comes from $anyconst, so the solver picks it once, and let the cycle it enters be free. Count the words ahead of it, then assert that it is never dropped and that it leaves first in line, unchanged. The value and entry time are arbitrary. So a proof for this one word covers every word, as long as the design never inspects the data.

Without helpers the induction step may start with the tracker claiming a word is stored in a slot that holds something else. Helpers tie the tracker to the design. Its distance from the read pointer equals the count of words ahead. Memory at the tracked slot still holds the value. Without them the proof stays UNKNOWN even at k = 8; with them it closes at k = 2.

Track two writes chosen freely by the solver, the first accepted before the second. Assert that the first leaves before the second and both arrive unchanged. Because both choices are free, the check covers every pair of words, which catches reordering that a single tracker cannot see.

The solver may pick any two writes, at any times, as the tracked pair. A proof must hold for every choice it could make. So if any pair could swap, some choice of the two tracked words shows it. Two trackers then stand for all pairs, with only two sets of state.

A reference queue copies every word, so its state grows with depth times width. The solver must reason about all of it. The tracker holds one value, one slot and one count, yet covers every word through the free choice. The queue is closer to a simulation scoreboard and easier to read, so people pick it first. The tracker is what converges.

Track one symbolic packet, tagged at the moment of acceptance. Count how many packets of its flow are owed ahead of it at its output. Assert that it leaves at its turn, on the right port, unchanged. Also assert that no output delivers a packet it does not owe. Fairness is a separate question: a fixed-priority arbiter passes every one of these safety checks.

Anything that needs more than ten steps to reach a port. Examples are a pointer that wraps wrongly only after many writes, or a count that drifts and overflows later. The end-to-end check sees the effect only once the bad word is read. Glue invariants on the count and pointers catch such drift early and also help an induction proof close.

A formal bench has four parts: the DUT, assumptions on inputs, assertions on outputs and state, and covers. There is no driver, clock generator or scoreboard class, because the solver chooses every input. For the slice, assume upstream holds in_valid and its data until accepted. Assert the same rule on the output side. Cover a stall and a back-to-back transfer.

The solver treats every input as free and considers all legal values on every cycle. So writing stimulus would only narrow the search. Assumptions say what is legal. Covers replace the coverage model. Each one asks whether a behaviour is reachable under those assumptions, and returns a trace if it is.

Expect failures that no real neighbour could cause, because every input is free on every cycle. For example, the data changes while valid waits for ready. Triage each one: check the reset state, then each input against the spec. Add one assumption per spec rule, and cover the behaviour you still expect.

Capture the accepted input in modelling code. When the word leaves, assert that the output equals the same function of it, here the captured value plus one. The modelling code only reads design signals; it never drives them.

Write each rule once with its owner, and let a parameter choose assume or assert. Rules owned by the side under test are asserted, and the rest are assumed. A rule that flips from assertion to assumption is no longer checked on the new bench. So review it and cover what it might exclude. Watch for over-strict rules, such as forbidding PREADY high while PENABLE is low, which APB allows.

They check the same rule. The |=> is one flop of delay, and $stable compares with last cycle's sample. So the immediate form registers the stall condition and the data, and asserts on them a cycle later. In the lesson both forms fail the buggy slice at step 4. The immediate form helps where an engine refuses history functions on primary inputs, as this one does.