Lesson 5.4 · Exploring New RTL with Formal

First covers: watching the lift move

The first run contains only covers. Each produces a short waveform — think of them as tests that wrote themselves.

Trace for c_door_at_3: floor 3 is called right after reset. The call is latched into pending one cycle later; the lift then alternates MOVE and IDLE (the arrival check) up to floor 3 and opens the door.

Questions to ask about every trace

Is it plausible? Here: yes — one MOVE per floor, an IDLE "arrival check" on each floor.
Is it what the spec intended? Each floor costs two cycles (MOVE + IDLE). Is that acceptable for the architecture? A cover's trace length is a quick performance estimate.
What did the tool not do? The tool pressed only one button. Try asking for richer traces, for example c_round_trip, which forces a reversal.

Steering with temporary constraints

Sometimes you want a specific kind of trace — say, a round trip where nobody calls floor 1. Add a clearly labelled temporary assumption:

temporary steering assumption

// EXPLORATION ONLY — remove before any signoff use
m_tmp_no_floor1: assume property (!call[1]);

Now c_pass_by shows the lift moving through floor 1 without stopping. Run the covers again without the constraint to confirm the behaviour is not an artefact of it.