One-hot state detector

onehot_detector.sby

# To run formal verification call SymbiYosys:
# $ sby -f onehot_detector.sby

[options]
mode prove

[engines]
smtbmc yices

[script]
read -sv2012 -formal onehot_detector.sv
chparam -set WIDTH 21 onehot_detector
chparam -set ATOM_WIDTH 6 onehot_detector
prep -top onehot_detector

[files]
onehot_detector.sv

onehot_detector.sv

`timescale 1ps/1ps
`default_nettype none

module onehot_detector #(parameter WIDTH = 10,
                         parameter ATOM_WIDTH = 4)
    (input wire [WIDTH-1:0] i_data,
     output wire o_have,
     output wire o_many);

    if (WIDTH <= ATOM_WIDTH) begin
        logic have, many;

        assign o_have = have;
        assign o_many = many;

        always_comb begin
            have = 1'b0;
            many = 1'b0;

            for (int n = 0; n < WIDTH; n += 1)
              if (i_data[n])
                if (have) many = 1'b1;
                else      have = 1'b1;
        end
    end
    else begin
        localparam D0_WIDTH = WIDTH >> 1;
        localparam D1_WIDTH = WIDTH - D0_WIDTH;

        logic h0, m0;
        logic h1, m1;

        onehot_detector #(.WIDTH(D0_WIDTH), .ATOM_WIDTH(ATOM_WIDTH))
        d0 (.i_data(i_data[0 +: D0_WIDTH]),
            .o_have(h0),
            .o_many(m0));

        onehot_detector #(.WIDTH(D1_WIDTH), .ATOM_WIDTH(ATOM_WIDTH))
        d1 (.i_data(i_data[D0_WIDTH +: D1_WIDTH]),
            .o_have(h1),
            .o_many(m1));

        assign o_have = h0 | h1;
        assign o_many = m0 | m1 | (h0 & h1);
    end

`ifdef FORMAL
    always_comb
      if (i_data == '0) begin
          assert(o_have == 1'b0);
          assert(o_many == 1'b0);
      end

    always_comb
      if ($onehot(i_data)) begin
          assert(o_have == 1'b1);
          assert(o_many == 1'b0);
      end

    always_comb
      if ((i_data != 0) && !$onehot(i_data)) begin
          assert(o_have == 1'b1);
          assert(o_many == 1'b1);
      end
`endif

endmodule // onehot_detector