Lesson 5.3 · Exploring New RTL with Formal

Planning an exploration session

Even lightweight work benefits from a ten-minute plan. Write down four things:

Plan item	For the lift controller
Questions — what do you want to see or rule out?	Can the lift reach every floor and open the door there? How long does a full up-and-down trip take? Can it ever move with the door open? Can a call be starved?
Simplifications — what can be reduced to keep runs fast?	Keep DOOR_CYCLES at 3 (could go down to 1 for even faster runs). Four floors is already small.
Staging — what order?	1) covers of basic behaviour, 2) safety assertions, 3) liveness questions.
Exit criteria — when to stop?	All questions answered; every cover hit and its trace reviewed; safety assertions proven; findings shared with the spec owner.

The exploration wrapper

The wrapper starts small and grows during the session. The final version is shown here and built up over the next lessons.

lift_ctrl_fv.sv

// lift_ctrl_fv.sv — exploration wrapper for the lift controller
module lift_ctrl_fv #(
  parameter bit ANTI_STARVE = 1'b1
) (
  input logic       clk,
  input logic       rst,
  input logic [3:0] call
);
  logic [1:0] floor;
  logic       door_open, moving, dir_up;
  logic [3:0] pending;

  lift_ctrl #(.DOOR_CYCLES(3), .ANTI_STARVE(ANTI_STARVE)) dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // ------------------------------------------------ exploration covers
  c_door_at_3:  cover property (door_open && floor == 2'd3);
  c_round_trip: cover property (door_open && floor == 2'd3 ##[1:$] door_open && floor == 2'd0);
  c_pass_by:    cover property (moving && floor == 2'd1 ##1 floor == 2'd2 && !door_open
                                ##1 moving);   // passes floor 2 without stopping
  c_reverse:    cover property (moving && dir_up ##[1:$] moving && !dir_up);

  // ------------------------------------------------ safety
  a_door_not_moving: assert property (moving |-> !door_open);
  a_no_wrap:         assert property (moving |-> (dir_up ? floor != 2'd3 : floor != 2'd0));
  a_one_floor:       assert property (moving |=> floor == ($past(dir_up) ? $past(floor) + 2'd1
                                                                         : $past(floor) - 2'd1));
  a_open_for_call:   assert property ($rose(door_open) |-> $past(pending[floor] || call[floor]));

  for (genvar f = 0; f < 4; f++) begin : g_floor
    // a call is only forgotten when it is served
    a_clear_served: assert property ($fell(pending[f]) |-> door_open && floor == 2'(f));
    // ------------------------------------------------ liveness
    a_served:       assert property (pending[f] |-> s_eventually (door_open && floor == 2'(f)));
  end
endmodule

lift_ctrl.sby

# lift_ctrl.sby — covers and safety (liveness needs a tool with s_eventually support)
[tasks]
cover
prove

[options]
cover: mode cover
prove: mode prove
depth 40

[engines]
cover: smtbmc
prove: abc pdr

[script]
read -formal lift_ctrl.sv lift_ctrl_fv.sv
prep -top lift_ctrl_fv

[files]
lift_ctrl.sv
lift_ctrl_fv.sv