// SVA form of the properties (used by commercial formal tools):
//   a_onehot: assert property (@(posedge clk) disable iff (rst) $onehot0(gnt));
//   a_subset: assert property (@(posedge clk) disable iff (rst) ##1 (gnt & ~$past(req)) == 4'b0000);
//   a_some:   assert property (@(posedge clk) disable iff (rst) (req != 4'b0000) |=> (gnt != 4'b0000));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module prio_arb (input clk, input rst, input [3:0] req, output reg [3:0] gnt);
  // fixed priority: req[0] highest, req[3] lowest, grant registered
  wire [3:0] nxt;
  assign nxt[0] = req[0];
  assign nxt[1] = req[1] & ~req[0];
  assign nxt[2] = req[2] & ~req[1];               // bug: forgets req[0]
  assign nxt[3] = req[3] & ~(|req[2:0]);
  always @(posedge clk)
    if (rst) gnt <= 4'b0000;
    else     gnt <= nxt;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // at most one grant
  always @(posedge clk) if (!init) assert ($onehot0(gnt));
  // no grant without a request (in the previous cycle)
  always @(posedge clk) if (!init && !$past(rst)) assert ((gnt & ~$past(req)) == 4'b0000);
  // some grant when there was some request
  always @(posedge clk) if (!init && !$past(rst)) assert (($past(req) != 0) == (gnt != 0));
`endif
endmodule