Applications Interview Questions

Start with apps that need no hand-written properties: connectivity from the integration table and register checks from the register map. Both find real wiring and access-type bugs within days, which earns trust for the harder work. Then add automatic checks and X-propagation, and use unreachability analysis to prune coverage holes for the simulation team. An app proves only the properties it generates, so design rules still need your own.

Checks generated from the RTL only prove that the RTL agrees with itself. A field built with the wrong access type then passes. The map is the independent statement of intent. Each access type in it implies a fixed set of checks. For example, a write of 1 clears a W1C bit and a write of 0 keeps it.

Then the proof passes, because the RTL and the checks agree with the same wrong row. Formal shows that the RTL matches the map, not that the map is right. So the map needs its own review against the spec and the driver code. A firmware test of the field in system simulation catches what that review misses.

The W1C check that a written 0 keeps a set bit fails within a few cycles: plain read-write overwrites the bit with the 0. The subtle part is priority. A hardware event that arrives in the same cycle as the clearing write must still set its bit. The bus protocol is assumed and covered, and the register behaviour is asserted one cycle after the completing write.

Lint reads the text and flags code that could be wrong, such as a width mismatch. It does not know whether the bad case can happen. Formal automatic checks generate covers and assertions from the RTL and show whether the bad state is reachable, with a trace. In the lesson lint warned only about a truncated index, while formal failed the index, a dropped carry and an X default.

Both, about different things. In formal the unreset mode is free at step 0. So the solver picked the value that enables the block before firmware wrote anything. Simulation started mode at one value per run, and a default run never hit the bad one. Either reset the flop, or write the firmware promise as an initial-state assumption and put it on the sign-off list.

Formal models are two-valued, and silicon powers up to some real 0 or 1 in each flop. Leaving the start value free lets the solver try every possibility in one run. Four-state simulation instead carries an X that if statements can silently resolve, so it may never show the bad value.

X-optimism is RTL simulation resolving an unknown too kindly, so a bug hides. For example, an if on X takes the else branch. X-pessimism is gate-level simulation spreading X further than real hardware would, which floods the run with false unknowns. Formal is two-valued and leaves the value free, so it checks both 0 and 1 and reports the one that breaks a property.

A random initial value is one draw per run. If only a few start values break the rule, most seeds pass. Formal treats the start value as free, so one run checks every value. The solver then picks a value that breaks the property, if one exists.

In this flow an explicit x becomes a free value the solver may choose on every cycle. An assertion that the debug output stays low therefore fails, here at step 2. That is useful. A stray x default in a case statement shows up as a real failure, not a silent simulation quirk.

Formal can ask three things of a bin: is it reachable, proven unreachable forever, or merely unreached within N steps. Only the proof supports a waiver; a bounded unreached cover is a hint about depth. In the lesson one bin is unreached at depth 20 and reached at step 26 at depth 30. Run the proof with as few assumptions as possible, since an over-constraint makes a live bin look dead.

Free inputs allow more behaviour than the real environment. So a bin that cannot be reached even with free inputs cannot be reached in the chip. Every assumption you add shrinks the search and can make a live bin look dead. Add an assumption only when a reached trace is clearly illegal, and list it on the waiver.

Replay it as a directed test. SBY writes a small Verilog testbench for every trace. You can port the input values into the simulation environment as a sequence. The simulation team then has a test that hits the bin and keeps hitting it in regression. Every checker and scoreboard watches that test.

Full formal searches every trace from reset, so a few thousand cycles of depth is out of reach. Semiformal starts the solver from a waypoint instead: a simulation or cover trace that has already run close to the event. It then searches exhaustively from there. It finds deep bugs that neither method finds alone. But it proves nothing about the states it skipped, so it counts as bug hunting, not sign-off.

A covergroup bin counts what your tests happened to do. A formal cover asks whether any legal input sequence can reach the condition and returns the shortest trace that does. An unreached formal cover within a bound only says the depth was too short or an assumption blocks it. A proof of the negation is what makes a bin truly unreachable.