Formal as a designer's microscope

A designer has just written new RTL. There is no testbench yet — that may be weeks away. Traditionally the designer would write a quick directed test, tweak stimulus until the waveform looks plausible and move on. With formal, there is a faster and more thorough option: describe the behaviour you want to see, and let the tool construct the stimulus.

We call this design exploration: interactive, question-driven use of FPV during design. Typical questions are:

• Can the FIFO actually become full? (cover)
• What is the fastest way from reset to the first output? (cover, look at the trace length)
• Can these two signals ever be high together? (assertion — or a cover of the bad case)
• If the input never does X, can Y still happen? (cover with a temporary assumption)