// periodic_timer_fv.sv — formal wrapper for the periodic timer
module periodic_timer_fv #(
  parameter int W = 8
) (
  input logic         clk,
  input logic         rst,
  input logic         load,
  input logic [W-1:0] period,
  input logic         stop
);
  logic [W-1:0] count, period_q;
  logic         running, irq;

  periodic_timer #(.W(W)) dut (.*);

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

  // ------------------------------------------------------------ assumptions
  // Spec 1: software never loads a period of 1
  m_period_legal: assume property (load |-> period != W'(1));

  // ------------------------------------------------------------ assertions
  // Spec 2: count decrements while running
  a_decrement:  assert property (running && !stop && !load && count > W'(1)
                                 |=> count == $past(count) - W'(1));
  // Spec 3: reload and interrupt at the end of a period
  a_reload:     assert property (running && !stop && !load && count == W'(1)
                                 |=> count == period_q && irq);
  a_irq_cause:  assert property (irq |-> $past(running && !stop && !load && count == W'(1)));
  a_irq_pulse:  assert property (irq |=> !irq);
  // Spec 4: stop holds the value
  a_stop_holds: assert property (running && stop && !load |=> $stable(count));
  // Spec 5: load has priority
  a_load:       assert property (load |=> count == $past(period) && irq == 1'b0);
  // Invariant: a running timer always has a count within its period
  a_count_rng:  assert property (running |-> count != '0 && count <= period_q);

  // ------------------------------------------------------------ covers
  c_running:   cover property (running);
  c_irq:       cover property (irq);
  c_two_irqs:  cover property (irq ##[1:$] irq);
  c_stop_hold: cover property (running && stop ##1 running && stop);
  c_reload_while_running: cover property (running && load);
endmodule