data/full_repos/permissive/441359809/src/yosys/examples/aiger/demo.v
data/verilator_xmls/9191e18b-d7ff-4f3a-8754-bdd11ab3c522.xml
module demo(input clk, reset, ctrl);
  localparam NBITS = 10;
  reg [NBITS-1:0] counter;
  initial counter[NBITS-2] = 0;
  initial counter[0] = 1;
  always @(posedge clk) begin
    counter <= reset ? 1 : ctrl ? counter + 1 : counter - 1;
    assume(counter != 0);
    assume(counter != 1 << (NBITS-1));
    assert(counter != (1 << NBITS)-1);
  end
endmodule
module demo(input clk, reset, ctrl);

  localparam NBITS = 10;
  reg [NBITS-1:0] counter;
  initial counter[NBITS-2] = 0;
  initial counter[0] = 1;
  always @(posedge clk) begin
    counter <= reset ? 1 : ctrl ? counter + 1 : counter - 1;
    assume(counter != 0);
    assume(counter != 1 << (NBITS-1));
    assert(counter != (1 << NBITS)-1);
  end
endmodule