Lesson 4.2 · Formal Property Verification (FPV) Basics

The example: a periodic timer

Our device under test (DUT) is a periodic timer, the kind found in every microcontroller. Software loads a period; the timer counts down and raises a one-cycle interrupt pulse each time a period ends, then reloads automatically.

Specification

load starts the timer with a new period. A period of 0 stops the timer. Software must never load a period of 1 (minimum period is 2).
While running and not stopped, count decreases by one each cycle.
When count is 1, the next cycle reloads count with the stored period and irq pulses for exactly one cycle.
While stop is high the timer holds its value.
load has priority over everything else.

periodic_timer.sv

// periodic_timer.sv — auto-reloading down-counter with interrupt pulse
module periodic_timer #(
  parameter int W = 8
) (
  input  logic         clk,
  input  logic         rst,       // synchronous, active-high
  input  logic         load,      // start / restart with a new period
  input  logic [W-1:0] period,    // spec: 0 = off, otherwise must be >= 2
  input  logic         stop,      // pause while high
  output logic [W-1:0] count,     // cycles left in the current period
  output logic [W-1:0] period_q,  // stored period
  output logic         running,
  output logic         irq        // one-cycle pulse at the end of each period
);
  always_ff @(posedge clk) begin
    if (rst) begin
      count    <= '0;
      period_q <= '0;
      running  <= 1'b0;
      irq      <= 1'b0;
    end else begin
      irq <= 1'b0;
      if (load) begin
        count    <= period;
        period_q <= period;
        running  <= (period != '0);
      end else if (running && !stop) begin
        if (count == W'(1)) begin
          count <= period_q;           // auto-reload
          irq   <= 1'b1;
        end else begin
          count <= count - W'(1);
        end
      end
    end
  end
endmodule

Load period 3 at cycle 1. stop at cycle 3 freezes the count for one cycle; irq pulses whenever a period completes.