module cyclic(
    input logic clk,
    output logic [4:0] y
);
  logic [4:0] sy;

  subm s(.clk(clk), .x(y), .y(sy));

  initial begin
    y = 1;
    // Base case: Assert P at t=0
    `ifdef AG_CHECK_TOP
    toplevel_guarantee_base: assert(y[0]);
    `endif
  end

  always_ff @(posedge clk) begin
    y <= (sy < 29) ? sy + 2 : sy;
    `ifdef AG_CHECK_TOP
    toplevel_assume: assume($past(sy[0])); // Assume Q held at t-1
    toplevel_guarantee: assert(y[0]);      // Assert P at t
    `endif
    `ifdef MONOLITHIC 
    assert(y[0]);
    `endif
  end
endmodule

module subm (
    input clk,
    input logic [4:0] x,
    output logic [4:0] y
);
  // Base case: Assert Q at t=0
  initial begin
    y = 1;
    `ifdef AG_CHECK_SUBM
    subm_guarantee_base: assert(y[0]);
    `endif
  end

  // Inductive step: Assume P held at t-1, assert Q at t
  always_ff @(posedge clk) begin
    y <= (x < 29) ? x + 2 : x;
    `ifdef AG_CHECK_SUBM
    subm_assume: assume($past(x[0])); // Assume P held at t-1
    subm_guarantee: assert(y[0]);     // Assert Q at t
    `endif
  end
endmodule