// csr_block_fv.sv — register properties (what a CSR app would generate)
module csr_block_fv (
  input logic       clk, rst, wr_en, hw_event,
  input logic [1:0] addr,
  input logic [7:0] wdata
);
  logic [7:0] rdata, ctrl;
  logic       irq;
  csr_block dut (.*);

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

  wire wr_ctrl   = wr_en && addr == 2'd0;
  wire wr_status = wr_en && addr == 2'd1;

  // CTRL: RW
  a_ctrl_write: assert property (wr_ctrl |=> ctrl == $past(wdata));
  a_ctrl_hold:  assert property (!wr_ctrl |=> $stable(ctrl));
  a_ctrl_read:  assert property (addr == 2'd0 |-> rdata == ctrl);

  // STATUS[0]: W1C with hardware priority
  a_evt_set:    assert property (hw_event |=> irq);
  a_evt_clear:  assert property (wr_status && wdata[0] && !hw_event |=> !irq);
  a_evt_sticky: assert property (!hw_event && !(wr_status && wdata[0]) |=> irq == $past(irq));
  a_evt_read:   assert property (addr == 2'd1 |-> rdata == {7'b0, irq});

  // ID: RO constant;  addr 3: reserved
  a_id_read:    assert property (addr == 2'd2 |-> rdata == 8'hA5);
  a_rsvd_read:  assert property (addr == 2'd3 |-> rdata == 8'h00);

  // reset values (checked in the first cycle after reset)
  a_reset_vals: assert property (@(posedge clk) $fell(rst) |-> ctrl == 8'h00 && !irq);

  // covers
  c_set_and_clear_same_cycle: cover property (hw_event && wr_status && wdata[0]);
  c_ctrl_written:             cover property (wr_ctrl ##1 ctrl == 8'hFF);
endmodule