data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v
1: b"%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:548: syntax error, unexpected property, expecting '#' or final\nassume property (~nondetStart | (IMPL_ibuf_io_inst_0_valid_o & ~ IMPL_ctrl_killd_o) );\n       ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:635: syntax error, unexpected property, expecting '#' or final\n    assume property (~( inst_gpr_assert_cond ) | (IMPL_x0 == GM_x0) );\n           ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:679: syntax error, unexpected property, expecting '#' or final\n    assume property ( ~ (GM_step) | (instruction_interested == mem_rdata0 ) );\n           ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:822: syntax error, unexpected property, expecting '#' or final\n    assume property (~CommitPointAll | (~WBisJAL  |(( IMPL_wb_reg_pc_o + WBimmJ ) & 2'b11) == 2'b00 ) );\n           ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:897: syntax error, unexpected property\n    property x1_no_resp_overlap;\n    ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:910: syntax error, unexpected property\n    property x1_resp_overlap ;\n    ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:980: syntax error, unexpected property, expecting '#' or '(' or final\n      assume property ( io_imem_req_valid |-> ##[1:$] io_imem_resp_valid );\n             ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:984: Unsupported: SystemVerilog 2005 reserved word not implemented: 'sequence'\n    sequence dmem_req_VALID;\n    ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:984: syntax error, unexpected ';', expecting IDENTIFIER\n    sequence dmem_req_VALID;\n                           ^\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:986: Unsupported: SystemVerilog 2005 reserved word not implemented: 'endsequence'\n    endsequence\n    ^~~~~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:990: syntax error, unexpected property, expecting '#' or '(' or final\n      assume property (dmem_req_VALID |-> ##[1:$] io_dmem_replay_next_rand );\n             ^~~~~~~~\n%Error: data/full_repos/permissive/437997237/RISC-V-Synth/ILAVerif/Completeness/RocketFV.v:993: syntax error, unexpected ##, expecting TYPE-IDENTIFIER\n    will_finish: assert property ( inst_finished |-> ##[1:$] (before_next_inst_commited && ( IMPL_wb_reg_pc_o == GM_pc) ) );\n                                                     ^~\n%Error: Exiting due to 12 error(s)\n"
module RocketFV(input clock, input reset,

  input io_interrupts_debug,
  input io_dmem_req_ready,
  input io_dmem_replay_next_rand,
  input io_imem_resp_bits_replay,
  input io_imem_resp_valid,
  input io_imem_resp_bits_btb_valid
  );



reg io_interrupts_mtip = 1'b0;
reg io_interrupts_msip = 1'b0;
reg io_interrupts_meip = 1'b0;














wire          io_dmem_req_valid;
wire [31:0]   io_dmem_req_bits_addr;
wire [4:0]    io_dmem_req_bits_cmd;
wire [2:0]    io_dmem_req_bits_typ;
wire [31:0]   io_dmem_req_bits_data;
wire [6:0]    io_dmem_req_bits_tag;
wire [31:0]   io_dmem_s1_data;

wire          io_dmem_s1_kill;
wire          io_dmem_s2_nack;
wire          io_dmem_replay_next; 
wire          io_dmem_resp_valid;
wire          io_dmem_resp_bits_replay;

wire  [31:0]  io_dmem_resp_bits_addr;
wire  [6:0]   io_dmem_resp_bits_tag;
wire  [4:0]   io_dmem_resp_bits_cmd;
wire  [2:0]   io_dmem_resp_bits_typ;
wire  [31:0]  io_dmem_resp_bits_data;
wire          io_dmem_resp_bits_has_data;
wire  [31:0]  io_dmem_resp_bits_data_word_bypass = io_dmem_resp_bits_data;




wire  io_imem_req_valid;
wire [31:0] io_imem_req_bits_pc;

wire  io_imem_resp_ready;
wire  [31:0] io_imem_resp_bits_pc;
wire  [31:0] io_imem_resp_bits_data;











reg ex_monitor=0;
reg mem_monitor=0;

reg inst_begin = 0;
reg inst_issued = 0;
reg inst_finished = 0;
reg inst_finished_delay = 0;
reg inst_finished_delay2= 0;
reg inst_finished_delay3= 0;

reg second_finished = 0;
wire this_inst_finished = inst_finished & ~second_finished;

wire inst_finish1d = inst_finished_delay & ~inst_finished_delay2;
wire inst_finish2d = inst_finished_delay2& ~inst_finished_delay3;



wire [31:0] mem_raddr0;
wire [31:0] mem_raddr1;
wire [31:0] mem_raddr2;

wire  [31:0] mem_rdata0;
wire  [31:0] mem_rdata1;
wire  [31:0] mem_rdata2;

wire        mem_wen0;
wire [31:0] mem_waddr0;
wire [31:0] mem_wdata0;
wire        GM_step;



  wire [31:0] GM_x0;
  wire [31:0] GM_x1;
  wire [31:0] GM_x10;
  wire [31:0] GM_x11;
  wire [31:0] GM_x12;
  wire [31:0] GM_x13;
  wire [31:0] GM_x14;
  wire [31:0] GM_x15;
  wire [31:0] GM_x16;
  wire [31:0] GM_x17;
  wire [31:0] GM_x18;
  wire [31:0] GM_x19;
  wire [31:0] GM_x2;
  wire [31:0] GM_x20;
  wire [31:0] GM_x21;
  wire [31:0] GM_x22;
  wire [31:0] GM_x23;
  wire [31:0] GM_x24;
  wire [31:0] GM_x25;
  wire [31:0] GM_x26;
  wire [31:0] GM_x27;
  wire [31:0] GM_x28;
  wire [31:0] GM_x29;
  wire [31:0] GM_x3;
  wire [31:0] GM_x30;
  wire [31:0] GM_x31;
  wire [31:0] GM_x4;
  wire [31:0] GM_x5;
  wire [31:0] GM_x6;
  wire [31:0] GM_x7;
  wire [31:0] GM_x8;
  wire [31:0] GM_x9;
  wire [31:0] GM_pc;

riscv GM(
  .clk(clock),
  .rst(reset),
  .step(GM_step),
      .x0(GM_x0),
      .x1(GM_x1),
      .x2(GM_x2),
      .x3(GM_x3),
      .x4(GM_x4),
      .x5(GM_x5),
      .x6(GM_x6),
      .x7(GM_x7),
      .x8(GM_x8),
      .x9(GM_x9),
      .x10(GM_x10),
      .x11(GM_x11),
      .x12(GM_x12),
      .x13(GM_x13),
      .x14(GM_x14),
      .x15(GM_x15),
      .x16(GM_x16),
      .x17(GM_x17),
      .x18(GM_x18),
      .x19(GM_x19),
      .x20(GM_x20),
      .x21(GM_x21),
      .x22(GM_x22),
      .x23(GM_x23),
      .x24(GM_x24),
      .x25(GM_x25),
      .x26(GM_x26),
      .x27(GM_x27),
      .x28(GM_x28),
      .x29(GM_x29),
      .x30(GM_x30),
      .x31(GM_x31),
      .pc (GM_pc),
  .mem_raddr0(mem_raddr0),
  .mem_raddr1(mem_raddr1),
  .mem_raddr2(mem_raddr2),

  .mem_rdata0(mem_rdata0),
  .mem_rdata1(mem_rdata1),
  .mem_rdata2(mem_rdata2),
  
  .mem_wen0(mem_wen0),
  .mem_waddr0(mem_waddr0),
  .mem_wdata0(mem_wdata0)
  

  );




  wire        reg_mem_mismatch_nxt;
  wire        load_not_ack_yet;
  wire        resp_a_non_monitored_req;
  wire        sm_GM_step;
  wire        sm_Assumpt_Time;

ShareMem sm(
    .clock(clock), .reset(reset),

    .io_dmem_req_ready(io_dmem_req_ready),

    .io_dmem_replay_next_rand(io_dmem_replay_next_rand),


    .io_imem_resp_bits_replay(io_imem_resp_bits_replay),
    .io_imem_resp_valid(io_imem_resp_valid),



    .io_dmem_s1_kill(io_dmem_s1_kill),
    .io_dmem_req_valid(io_dmem_req_valid),
    .io_dmem_req_bits_addr(io_dmem_req_bits_addr),
    .io_dmem_req_bits_tag(io_dmem_req_bits_tag),
    .io_dmem_req_bits_cmd(io_dmem_req_bits_cmd),
    .io_dmem_req_bits_typ(io_dmem_req_bits_typ),
    .io_dmem_req_bits_data(io_dmem_req_bits_data),
    .io_dmem_s1_data(io_dmem_s1_data),

    .io_dmem_resp_bits_addr(io_dmem_resp_bits_addr),
    .io_dmem_resp_bits_tag(io_dmem_resp_bits_tag),
    .io_dmem_resp_bits_cmd(io_dmem_resp_bits_cmd),
    .io_dmem_resp_bits_typ(io_dmem_resp_bits_typ),
    .io_dmem_resp_bits_data(io_dmem_resp_bits_data),
    .io_dmem_resp_bits_has_data(io_dmem_resp_bits_has_data),

    .io_dmem_s2_nack(io_dmem_s2_nack),
    .io_dmem_replay_next(io_dmem_replay_next),
    .io_dmem_resp_valid(io_dmem_resp_valid),
    .io_dmem_resp_bits_replay(io_dmem_resp_bits_replay),
    .io_dmem_ordered(io_dmem_ordered),


    .io_imem_req_valid(io_imem_req_valid),
    .io_imem_req_bits_pc(io_imem_req_bits_pc),

    .io_imem_resp_ready(io_imem_resp_ready),
    .io_imem_resp_bits_pc(io_imem_resp_bits_pc),
    .io_imem_resp_bits_data(io_imem_resp_bits_data),


    .reg_mem_mismatch_nxt(reg_mem_mismatch_nxt),



    .mem_raddr0(mem_raddr0),
    .mem_raddr1(mem_raddr1),
    .mem_raddr2(mem_raddr2),

    .mem_rdata0(mem_rdata0),
    .mem_rdata1(mem_rdata1),
    .mem_rdata2(mem_rdata2),

    .mem_wen0(mem_wen0),
    .mem_waddr0(mem_waddr0),
    .mem_wdata0(mem_wdata0),






    .ex_monitor(ex_monitor),
    .load_not_ack_yet(load_not_ack_yet),
    .resp_a_non_monitored_req(resp_a_non_monitored_req),

    .GM_step(sm_GM_step),
    .Assumpt_Time(sm_Assumpt_Time)
     );



  wire [31:0] IMPL_ibuf_io_pc_o;
  wire [31:0] IMPL_wb_reg_pc_o;
  wire [31:0] first_valid_pc;
  wire IMPL_ctrl_killd_o;
  wire IMPL_ctrl_killx_o;
  wire IMPL_ctrl_killm_o;
  wire IMPL_wb_reg_valid_o;


  wire [31:0] IMPL_ibuf_io_inst_0_bits_inst_bits_o;
  wire        IMPL_ibuf_io_inst_0_valid_o;
  wire        IMPL_ex_reg_valid_o;
  wire        IMPL_mem_reg_valid_o;
  wire        IMPL_wb_valid_o;
  wire [31:0] IMPL_wb_reg_inst_o;

  wire no_first_valid_pc;

  wire IMPL_id_rs_0_in_use;
  wire IMPL_id_rs_1_in_use;
  wire [31:0] IMPL_ex_rs_0_o;
  wire [31:0] IMPL_ex_rs_1_o;


  wire [4:0]  rf_idx_i;
  wire [31:0] rf_idx_o;


  wire [31:0] IMPL_x0;
  wire [31:0] IMPL_x1;
  wire [31:0] IMPL_x10;
  wire [31:0] IMPL_x11;
  wire [31:0] IMPL_x12;
  wire [31:0] IMPL_x13;
  wire [31:0] IMPL_x14;
  wire [31:0] IMPL_x15;
  wire [31:0] IMPL_x16;
  wire [31:0] IMPL_x17;
  wire [31:0] IMPL_x18;
  wire [31:0] IMPL_x19;
  wire [31:0] IMPL_x2;
  wire [31:0] IMPL_x20;
  wire [31:0] IMPL_x21;
  wire [31:0] IMPL_x22;
  wire [31:0] IMPL_x23;
  wire [31:0] IMPL_x24;
  wire [31:0] IMPL_x25;
  wire [31:0] IMPL_x26;
  wire [31:0] IMPL_x27;
  wire [31:0] IMPL_x28;
  wire [31:0] IMPL_x29;
  wire [31:0] IMPL_x3;
  wire [31:0] IMPL_x30;
  wire [31:0] IMPL_x31;
  wire [31:0] IMPL_x4;
  wire [31:0] IMPL_x5;
  wire [31:0] IMPL_x6;
  wire [31:0] IMPL_x7;
  wire [31:0] IMPL_x8;
  wire [31:0] IMPL_x9;

Rocket dut(
    .clock(clock),
    .reset(reset),
    
    .io_interrupts_debug(io_interrupts_debug),
    .io_interrupts_mtip(io_interrupts_mtip),
    .io_interrupts_msip(io_interrupts_msip),
    .io_interrupts_meip(io_interrupts_meip),
    .io_hartid(32'd0),


      .io_imem_req_valid(io_imem_req_valid),
      .io_imem_req_bits_pc(io_imem_req_bits_pc),
      .io_imem_req_bits_speculative(),

      .io_imem_resp_valid(io_imem_resp_valid),
      .io_imem_resp_bits_replay(io_imem_resp_bits_replay),


      .io_imem_resp_ready(io_imem_resp_ready),
      .io_imem_resp_bits_pc(io_imem_resp_bits_pc),
      .io_imem_resp_bits_data(io_imem_resp_bits_data),
      .io_imem_resp_bits_mask(2'b11),
      .io_imem_resp_bits_xcpt_if(1'b0),
      
      .io_imem_resp_bits_btb_valid(io_imem_resp_bits_btb_valid),
      .io_imem_resp_bits_btb_bits_taken(),
      .io_imem_resp_bits_btb_bits_mask(),
      .io_imem_resp_bits_btb_bits_bridx(),
      .io_imem_resp_bits_btb_bits_target(),
      .io_imem_resp_bits_btb_bits_entry(),
      .io_imem_resp_bits_btb_bits_bht_history(),
      .io_imem_resp_bits_btb_bits_bht_value(),

      .io_imem_npc(),

    
    .io_dmem_req_ready(io_dmem_req_ready),
    .io_dmem_replay_next(io_dmem_replay_next),
    .io_dmem_resp_valid(io_dmem_resp_valid),
    .io_dmem_resp_bits_replay(io_dmem_resp_bits_replay),


    .io_dmem_req_valid(io_dmem_req_valid),
    .io_dmem_req_bits_addr(io_dmem_req_bits_addr),
    .io_dmem_req_bits_cmd(io_dmem_req_bits_cmd),
    .io_dmem_req_bits_typ(io_dmem_req_bits_typ),
    .io_dmem_req_bits_data(io_dmem_req_bits_data),
    .io_dmem_req_bits_tag(io_dmem_req_bits_tag),
    .io_dmem_req_bits_phys(),

    .io_dmem_s1_kill(io_dmem_s1_kill),
    .io_dmem_s2_nack(io_dmem_s2_nack),
    .io_dmem_s1_data(io_dmem_s1_data),
    .io_dmem_ordered(io_dmem_ordered),
    .io_dmem_xcpt_ma_ld(1'b0),
    .io_dmem_xcpt_ma_st(1'b0),
    .io_dmem_xcpt_pf_ld(1'b0),
    .io_dmem_xcpt_pf_st(1'b0),


    .io_dmem_resp_bits_addr(io_dmem_resp_bits_addr),
    .io_dmem_resp_bits_tag(io_dmem_resp_bits_tag),
    .io_dmem_resp_bits_cmd(io_dmem_resp_bits_cmd),
    .io_dmem_resp_bits_typ(io_dmem_resp_bits_typ),
    .io_dmem_resp_bits_data(io_dmem_resp_bits_data),
    .io_dmem_resp_bits_has_data(io_dmem_resp_bits_has_data),
    .io_dmem_resp_bits_data_word_bypass(io_dmem_resp_bits_data_word_bypass),
    .io_dmem_resp_bits_store_data(),
    .io_dmem_invalidate_lr(),

    .io_rocc_fpu_resp_ready(1'b0),
    .io_rocc_fpu_req_valid(1'b0),
    .io_rocc_autl_grant_bits_is_builtin_type(),
    .io_rocc_autl_grant_bits_client_xact_id(),
    .io_rocc_autl_grant_ready(1'b1),
    .io_rocc_autl_acquire_bits_is_builtin_type(1'b1),
    .io_rocc_autl_acquire_bits_client_xact_id(1'b0),
    .io_rocc_autl_acquire_valid(1'b0),
    .io_rocc_busy(1'b0),
    .io_rocc_interrupt(1'b0),
    .io_rocc_mem_invalidate_lr(1'b1),
    .io_rocc_mem_s1_kill(1'b0),
    .io_rocc_mem_req_valid(1'b0),
    .io_rocc_resp_valid(1'b0),
    .io_rocc_cmd_ready(1'b0),
    .io_fpu_cp_resp_valid(1'b0),
    .io_fpu_cp_resp_bits_data(33'd0),
    .io_fpu_fcsr_rdy(1'b1),
    .io_fpu_nack_mem(1'b0),
    .io_fpu_illegal_rm(1'b0),
    .io_fpu_fcsr_flags_valid(1'b0),
    .io_fpu_fcsr_flags_bits(5'd0),
    .io_fpu_toint_data(0),



      .ibuf_io_inst_0_bits_inst_bits_o(IMPL_ibuf_io_inst_0_bits_inst_bits_o),
      .ibuf_io_inst_0_valid_o(IMPL_ibuf_io_inst_0_valid_o),
      .ex_reg_valid_o(IMPL_ex_reg_valid_o),
      .mem_reg_valid_o(IMPL_mem_reg_valid_o),
      .wb_valid_o(IMPL_wb_valid_o),
      .wb_reg_valid_o(IMPL_wb_reg_valid_o),
      .wb_reg_inst_o(IMPL_wb_reg_inst_o),

      .ctrl_killd_o(IMPL_ctrl_killd_o),
      .ctrl_killx_o(IMPL_ctrl_killx_o),
      .ctrl_killm_o(IMPL_ctrl_killm_o),


      .ibuf_io_pc_o(IMPL_ibuf_io_pc_o),
      .wb_reg_pc_o(IMPL_wb_reg_pc_o),
      .first_valid_pc(first_valid_pc),
      .no_first_valid_pc(no_first_valid_pc),

      .rf_idx_i(rf_idx_i),
      .rf_idx_o(rf_idx_o),

      .id_rs_0_in_use(IMPL_id_rs_0_in_use),
      .id_rs_1_in_use(IMPL_id_rs_1_in_use),

      .ex_rs_0_o(IMPL_ex_rs_0_o),
      .ex_rs_1_o(IMPL_ex_rs_1_o),


      .x0(IMPL_x0),
      .x1(IMPL_x1),
      .x2(IMPL_x2),
      .x3(IMPL_x3),
      .x4(IMPL_x4),
      .x5(IMPL_x5),
      .x6(IMPL_x6),
      .x7(IMPL_x7),
      .x8(IMPL_x8),
      .x9(IMPL_x9),
      .x10(IMPL_x10),
      .x11(IMPL_x11),
      .x12(IMPL_x12),
      .x13(IMPL_x13),
      .x14(IMPL_x14),
      .x15(IMPL_x15),
      .x16(IMPL_x16),
      .x17(IMPL_x17),
      .x18(IMPL_x18),
      .x19(IMPL_x19),
      .x20(IMPL_x20),
      .x21(IMPL_x21),
      .x22(IMPL_x22),
      .x23(IMPL_x23),
      .x24(IMPL_x24),
      .x25(IMPL_x25),
      .x26(IMPL_x26),
      .x27(IMPL_x27),
      .x28(IMPL_x28),
      .x29(IMPL_x29),
      .x30(IMPL_x30),
      .x31(IMPL_x31)


    );

reg nondetStart;
wire inst_begin_cond = ~inst_begin & nondetStart & ~inst_issued;
assume property (~nondetStart | (IMPL_ibuf_io_inst_0_valid_o & ~ IMPL_ctrl_killd_o) );






reg inst_has_begun = 0;
always @(posedge clock) begin
  if(reset)
    inst_has_begun <= 1'b0;
  else if(inst_begin_cond)
    inst_has_begun <= 1'b1;
end

always @(posedge clock) begin
  if(reset)
    inst_begin <= 1'b0;
  else if(inst_begin_cond )
    inst_begin <= 1'b1;
  else if( inst_begin & IMPL_ex_reg_valid_o)
    inst_begin <= 1'b0;
end

always @(posedge clock) begin
  if(reset)
    inst_issued <= 1'b0;
  else if( inst_begin & IMPL_ex_reg_valid_o )
    inst_issued <= 1'b1;
end

always @(posedge clock) begin
  if(reset) 
    ex_monitor <= 1'b0;
  else if(inst_begin & IMPL_ex_reg_valid_o & ~IMPL_ctrl_killx_o)
    ex_monitor <= 1'b1;
  else if(ex_monitor & IMPL_mem_reg_valid_o)
    ex_monitor <= 1'b0;
  else if(IMPL_ctrl_killx_o)
    ex_monitor <= 1'b0;
end

always @(posedge clock) begin
  if(reset)
    mem_monitor <= 1'b0;
  else if(ex_monitor & IMPL_mem_reg_valid_o & ~IMPL_ctrl_killm_o)
    mem_monitor <= 1'b1;
  else if(mem_monitor & IMPL_wb_valid_o)
    mem_monitor <= 1'b0;
  else if(IMPL_ctrl_killm_o)
    mem_monitor <= 1'b0;
end

always @(posedge clock) begin
  if(reset) begin 
    inst_finished <= 1'b0;
    inst_finished_delay <= 1'b0;
    inst_finished_delay2 <= 1'b0;
    inst_finished_delay3 <= 1'b0;
  end
  else begin
    inst_finished_delay <= inst_finished;
    inst_finished_delay2 <= inst_finished_delay;
    inst_finished_delay3 <= inst_finished_delay2;
    if(mem_monitor & IMPL_wb_valid_o)
      inst_finished <= 1'b1;
  end
end


wire before_next_inst_commited = this_inst_finished & (IMPL_wb_valid_o);
always @(posedge clock) begin 
  if(reset)
    second_finished <= 1'b0;
  else if(before_next_inst_commited)
    second_finished <= 1'b1;
end



wire inst_gpr_assert_cond = mem_monitor & IMPL_wb_valid_o;

    assume property (~( inst_gpr_assert_cond ) | (IMPL_x0 == GM_x0) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x1 == GM_x1) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x2 == GM_x2) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x3 == GM_x3) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x4 == GM_x4) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x5 == GM_x5) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x6 == GM_x6) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x7 == GM_x7) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x8 == GM_x8) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x9 == GM_x9) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x10 == GM_x10) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x11 == GM_x11) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x12 == GM_x12) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x13 == GM_x13) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x14 == GM_x14) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x15 == GM_x15) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x16 == GM_x16) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x17 == GM_x17) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x18 == GM_x18) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x19 == GM_x19) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x20 == GM_x20) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x21 == GM_x21) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x22 == GM_x22) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x23 == GM_x23) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x24 == GM_x24) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x25 == GM_x25) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x26 == GM_x26) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x27 == GM_x27) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x28 == GM_x28) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x29 == GM_x29) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x30 == GM_x30) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x31 == GM_x31) );


    assume property (~( inst_begin_cond ) | (IMPL_ibuf_io_pc_o == GM_pc) );



    reg [31:0] instruction_interested;
    always @(posedge clock) begin 
        if(inst_begin_cond)
            instruction_interested <= IMPL_ibuf_io_inst_0_bits_inst_bits_o;
    end

    assume property ( ~ (GM_step) | (instruction_interested == mem_rdata0 ) );



    assign  sm_GM_step = GM_step;
    assign  sm_Assumpt_Time = IMPL_ibuf_io_inst_0_valid_o;

    wire isLB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000003;
    wire isLW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002003;
    wire isLH = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001003;
    wire isLD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003003;
    wire isLBU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004003;
    wire isLHU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005003;
    wire isLWU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006003;
    wire isSB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000023;
    wire isSH = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001023;
    wire isSW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002023;
    wire isSD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003023;
    wire isBEQ = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000063;
    wire isBNE = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001063;
    wire isBLT = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004063;
    wire isBGE = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005063;
    wire isBLTU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006063;
    wire isBGEU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007063;
    wire isJAL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h0000006f;
    wire isJALR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000067;
    wire isLUI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h00000037;
    wire isAUIPC = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h00000017;
    wire isADDI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000013;
    wire isSLTI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002013;
    wire isSLTIU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003013;
    wire isXORI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004013;
    wire isORI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006013;
    wire isANDI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007013;
    wire isSRLI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00005013;
    wire isSRAI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40005013;
    wire isSLLI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00001013;
    wire isADD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00000033;
    wire isSUB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40000033;
    wire isSLL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00001033;
    wire isSLT = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00002033;
    wire isSLTU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00003033;
    wire isXOR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00004033;
    wire isSRL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00005033;
    wire isSRA = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40005033;
    wire isOR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00006033;
    wire isAND = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00007033;
    wire isCSRRW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001073;
    wire isCSRRS = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002073;
    wire isCSRRC = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003073;
    wire isCSRRWI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005073;
    wire isCSRRSI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006073;
    wire isCSRRCI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007073;
    wire isECALL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h00000073;
    wire isEBREAK = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h00100073;
    wire isSRET = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h10200073;
    wire isMRET = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h30200073;
    wire isSFENCE_VM = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfff07fff) == 32'h10400073;


    wire WBisLB = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000003;
    wire WBisLW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002003;
    wire WBisLH = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001003;
    wire WBisLD = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003003;
    wire WBisLBU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004003;
    wire WBisLHU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005003;
    wire WBisLWU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006003;
    wire WBisSB = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000023;
    wire WBisSH = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001023;
    wire WBisSW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002023;
    wire WBisSD = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003023;
    wire WBisBEQ = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000063;
    wire WBisBNE = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001063;
    wire WBisBLT = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004063;
    wire WBisBGE = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005063;
    wire WBisBLTU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006063;
    wire WBisBGEU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007063;
    wire WBisJAL = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h0000006f;
    wire WBisJALR = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000067;
    wire WBisLUI = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h00000037;
    wire WBisAUIPC = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h00000017;
    wire WBisADDI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000013;
    wire WBisSLTI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002013;
    wire WBisSLTIU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003013;
    wire WBisXORI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004013;
    wire WBisORI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006013;
    wire WBisANDI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007013;
    wire WBisSRLI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00005013;
    wire WBisSRAI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40005013;
    wire WBisSLLI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00001013;
    wire WBisADD = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00000033;
    wire WBisSUB = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40000033;
    wire WBisSLL = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00001033;
    wire WBisSLT = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00002033;
    wire WBisSLTU = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00003033;
    wire WBisXOR = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00004033;
    wire WBisSRL = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00005033;
    wire WBisSRA = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40005033;
    wire WBisOR = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00006033;
    wire WBisAND = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00007033;
    wire WBisCSRRW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001073;
    wire WBisCSRRS = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002073;
    wire WBisCSRRC = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003073;
    wire WBisCSRRWI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005073;
    wire WBisCSRRSI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006073;
    wire WBisCSRRCI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007073;
    wire WBisECALL = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h00000073;
    wire WBisEBREAK = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h00100073;
    wire WBisSRET = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h10200073;
    wire WBisMRET = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h30200073;
    wire WBisSFENCE_VM = (IMPL_wb_reg_inst_o & 32'hfff07fff) == 32'h10400073;



    wire DECODE_isLoad = isLW | isLB | isLBU | isLH | isLHU;
    wire WBisBranch = WBisBEQ | WBisBNE | WBisBGEU | WBisBGE | WBisBLT | WBisBLTU;
    wire DECODE_validInstructions = 
      isSB | isSH | isSW | isLW | isLB | isLBU | isLH | isLHU |
       isBEQ | isBNE | isBLT | isBGE | isBLTU | isBGEU | isJAL | isJALR | 
      isLUI | isAUIPC | isADDI | isSLTI | isSLTIU | isXORI | isORI | isANDI | 
      isSRLI | isSRAI | isSLLI | isADD | isSUB | isSLL | isSLT | isSLTU | isXOR | 
      isSRL | isSRA | isOR | isAND ;
    wire WB_validInstructions = 
      WBisSB | WBisSH | WBisSW | WBisLW | WBisLB | WBisLBU | WBisLH | WBisLHU |
       WBisBEQ | WBisBNE | WBisBLT | WBisBGE | WBisBLTU | WBisBGEU | WBisJAL | WBisJALR | 
      WBisLUI | WBisAUIPC | WBisADDI | WBisSLTI | WBisSLTIU | WBisXORI | WBisORI | WBisANDI | 
      WBisSRLI | WBisSRAI | WBisSLLI | WBisADD | WBisSUB | WBisSLL | WBisSLT | WBisSLTU | WBisXOR | 
      WBisSRL | WBisSRA | WBisOR | WBisAND ;





    wire[31:0] WBimmS = { { 20{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31:25], IMPL_wb_reg_inst_o[11:7] };
    wire[31:0] WBimmI = { { 20{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31:20] };
    wire[31:0] WBimmJ = { { 11{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31] , IMPL_wb_reg_inst_o[19:12] , IMPL_wb_reg_inst_o[20], IMPL_wb_reg_inst_o[30:21],1'b0 };
    wire[31:0] WBimmB = { { 19{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31], IMPL_wb_reg_inst_o[7], IMPL_wb_reg_inst_o[30:25], IMPL_wb_reg_inst_o[11:8], 1'b0 };
    assign rf_idx_i = IMPL_wb_reg_inst_o[19:15];
    wire[1:0] loadAddr = rf_idx_o[1:0] + WBimmI[1:0];
    wire[1:0] storeAddr= rf_idx_o[1:0] + WBimmS[1:0];


    wire CommitPointAll = IMPL_wb_valid_o;
    assume property (~CommitPointAll | (~WBisJAL  |(( IMPL_wb_reg_pc_o + WBimmJ ) & 2'b11) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisJALR |(( rf_idx_o + WBimmI )&2'b10) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisBranch | ((  IMPL_wb_reg_pc_o + WBimmB) & 2'b11) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisLH | (loadAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisLHU | (loadAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisLW | (loadAddr == 2'b00 ) ));

    assume property (~CommitPointAll | (~WBisSH | (storeAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisSW | (storeAddr == 2'b00 ) ));
    assume property (~CommitPointAll | (GM_x0 == 0) );
    assume property (~CommitPointAll | (GM_pc[1:0] == 2'b00) );
    assume property (GM_x0 == 0);
    


    assume property ( ~(inst_has_begun | inst_begin_cond) | (io_interrupts_debug == 1'b0) );

    


      assume property (~IMPL_ibuf_io_inst_0_valid_o |  (isBEQ|isADD|isLW|isSW) );



    assume property (~IMPL_wb_reg_valid_o | WB_validInstructions);


    wire justFinish = inst_finished & ~inst_finished_delay;


    reg isInstLoad = 1'b0;
    reg delay_check = 1'b0;
    reg check_ready = 1'b0;
    reg check_ready_delay1 = 1'b0;
    wire delay_check_point = check_ready & ~check_ready_delay1;

    reg[4:0] inst_decode_rd;
    always @(posedge clock) begin 
      if(reset) begin
        isInstLoad <= 1'b0;
      end
      else if(inst_begin_cond) begin
        isInstLoad <= DECODE_isLoad;
        inst_decode_rd <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[11:7];
      end
    end


    always @(posedge clock) begin 
      if(reset)
        delay_check <= 1'b0;
      else if(mem_monitor & IMPL_wb_valid_o & isInstLoad & (load_not_ack_yet & ~ (io_dmem_resp_valid & io_dmem_resp_bits_has_data ) )) 
        delay_check <= 1'b1;
      else if(delay_check & (io_dmem_resp_valid & io_dmem_resp_bits_has_data )  )
        delay_check <= 1'b0;
    end

    always @(posedge clock) begin 
      if(reset)
        check_ready <= 1'b0;
      else if( delay_check & (io_dmem_resp_valid & io_dmem_resp_bits_has_data )  ) 
        check_ready <= 1'b1;
    end

    always @(posedge clock) begin
      if(reset)
        check_ready_delay1 <= 1'b0;
      else
        check_ready_delay1 <= check_ready;
    end


    assign GM_step = mem_monitor & IMPL_wb_valid_o;
    assert property ( justFinish |-> (GM_x0 == IMPL_x0) );

    property x1_no_resp_overlap;
      (
        ~resp_a_non_monitored_req ##1
        ( justFinish & ( ~delay_check | (inst_decode_rd != 5'd1 )  ) )
      )  |-> (GM_x1 == IMPL_x1);
    endproperty

    reg[31:0] GM_origin_x1;
    always @(*) begin 
      if(inst_gpr_assert_cond)
        GM_origin_x1 <= GM_x1;
    end

    property x1_resp_overlap ;
      (
          (resp_a_non_monitored_req && (io_dmem_resp_bits_tag[5:1] == 5'd1) ) ##1
          (justFinish)
      )  |-> (GM_origin_x1 == GM_x1);
    endproperty

    property x1_load_delay;
      ( delay_check_point & (inst_decode_rd == 5'd1) ) |->  (GM_x1 == IMPL_x1) ;
    endproperty





    x1_nro: assert property (x1_no_resp_overlap);
    x1_ro:  assert property (x1_resp_overlap);
    x1_ld:  assert property (x1_load_delay);








    always @(posedge clock) begin 
      assume property ( io_imem_req_valid |-> ##[1:$] io_imem_resp_valid );
    end


    sequence dmem_req_VALID;
      io_dmem_req_valid ##1 ~io_dmem_s1_kill ##1 ~io_dmem_s2_nack;
    endsequence


    always @(posedge clock) begin
      assume property (dmem_req_VALID |-> ##[1:$] io_dmem_replay_next_rand );
    end

    will_finish: assert property ( inst_finished |-> ##[1:$] (before_next_inst_commited && ( IMPL_wb_reg_pc_o == GM_pc) ) );



    pc_a: assert property ( before_next_inst_commited |-> ( IMPL_wb_reg_pc_o == GM_pc)  );


    mem_match: assert property ( inst_finish1d |->  ~reg_mem_mismatch_nxt );




 

   reg[31:0] id_rs_0_reg;
   reg[4:0]  id_rs_0_field;
   reg[31:0] id_rs_1_reg;
   reg[4:0]  id_rs_1_field;

   reg       id_rs_0_in_use;
   reg       id_rs_1_in_use;

   always @(posedge clock) begin 
    if(reset) begin 
      id_rs_0_in_use <= 1'b0;
      id_rs_1_in_use <= 1'b0;
      id_rs_0_field  <= 5'd0;
      id_rs_1_field  <= 5'd0;
    end
    else begin 
      if(inst_begin_cond) begin 
        id_rs_0_in_use <= IMPL_id_rs_0_in_use;
        id_rs_1_in_use <= IMPL_id_rs_1_in_use;
        id_rs_0_field <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[19:15];
        id_rs_1_field <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[24:20];
      end
    end
   end

   always @(posedge clock) begin 
    if(inst_begin & IMPL_ex_reg_valid_o & ~IMPL_ctrl_killx_o ) begin 
      id_rs_0_reg <= IMPL_ex_rs_0_o;
      id_rs_1_reg <= IMPL_ex_rs_1_o;
    end
   end


     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd0 ) || (IMPL_x0 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd1 ) || (IMPL_x1 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd2 ) || (IMPL_x2 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd3 ) || (IMPL_x3 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd4 ) || (IMPL_x4 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd5 ) || (IMPL_x5 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd6 ) || (IMPL_x6 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd7 ) || (IMPL_x7 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd8 ) || (IMPL_x8 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd9 ) || (IMPL_x9 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd10 ) || (IMPL_x10 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd11 ) || (IMPL_x11 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd12 ) || (IMPL_x12 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd13 ) || (IMPL_x13 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd14 ) || (IMPL_x14 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd15 ) || (IMPL_x15 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd16 ) || (IMPL_x16 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd17 ) || (IMPL_x17 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd18 ) || (IMPL_x18 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd19 ) || (IMPL_x19 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd20 ) || (IMPL_x20 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd21 ) || (IMPL_x21 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd22 ) || (IMPL_x22 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd23 ) || (IMPL_x23 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd24 ) || (IMPL_x24 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd25 ) || (IMPL_x25 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd26 ) || (IMPL_x26 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd27 ) || (IMPL_x27 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd28 ) || (IMPL_x28 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd29 ) || (IMPL_x29 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd30 ) || (IMPL_x30 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd31 ) || (IMPL_x31 == id_rs_0_reg ) ) );

     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd0  ) || (IMPL_x0  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd1  ) || (IMPL_x1  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd2  ) || (IMPL_x2  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd3  ) || (IMPL_x3  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd4  ) || (IMPL_x4  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd5  ) || (IMPL_x5  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd6  ) || (IMPL_x6  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd7  ) || (IMPL_x7  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd8  ) || (IMPL_x8  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd9  ) || (IMPL_x9  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd10 ) || (IMPL_x10 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd11 ) || (IMPL_x11 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd12 ) || (IMPL_x12 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd13 ) || (IMPL_x13 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd14 ) || (IMPL_x14 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd15 ) || (IMPL_x15 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd16 ) || (IMPL_x16 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd17 ) || (IMPL_x17 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd18 ) || (IMPL_x18 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd19 ) || (IMPL_x19 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd20 ) || (IMPL_x20 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd21 ) || (IMPL_x21 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd22 ) || (IMPL_x22 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd23 ) || (IMPL_x23 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd24 ) || (IMPL_x24 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd25 ) || (IMPL_x25 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd26 ) || (IMPL_x26 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd27 ) || (IMPL_x27 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd28 ) || (IMPL_x28 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd29 ) || (IMPL_x29 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd30 ) || (IMPL_x30 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd31 ) || (IMPL_x31 == id_rs_1_reg ) ) );








endmodule
module RocketFV(input clock, input reset,

  input io_interrupts_debug,
  input io_dmem_req_ready,
  input io_dmem_replay_next_rand,
  input io_imem_resp_bits_replay,
  input io_imem_resp_valid,
  input io_imem_resp_bits_btb_valid
  );




reg io_interrupts_mtip = 1'b0;
reg io_interrupts_msip = 1'b0;
reg io_interrupts_meip = 1'b0;














wire          io_dmem_req_valid;
wire [31:0]   io_dmem_req_bits_addr;
wire [4:0]    io_dmem_req_bits_cmd;
wire [2:0]    io_dmem_req_bits_typ;
wire [31:0]   io_dmem_req_bits_data;
wire [6:0]    io_dmem_req_bits_tag;
wire [31:0]   io_dmem_s1_data;

wire          io_dmem_s1_kill;
wire          io_dmem_s2_nack;
wire          io_dmem_replay_next; 
wire          io_dmem_resp_valid;
wire          io_dmem_resp_bits_replay;

wire  [31:0]  io_dmem_resp_bits_addr;
wire  [6:0]   io_dmem_resp_bits_tag;
wire  [4:0]   io_dmem_resp_bits_cmd;
wire  [2:0]   io_dmem_resp_bits_typ;
wire  [31:0]  io_dmem_resp_bits_data;
wire          io_dmem_resp_bits_has_data;
wire  [31:0]  io_dmem_resp_bits_data_word_bypass = io_dmem_resp_bits_data;




wire  io_imem_req_valid;
wire [31:0] io_imem_req_bits_pc;

wire  io_imem_resp_ready;
wire  [31:0] io_imem_resp_bits_pc;
wire  [31:0] io_imem_resp_bits_data;











reg ex_monitor=0;
reg mem_monitor=0;

reg inst_begin = 0;
reg inst_issued = 0;
reg inst_finished = 0;
reg inst_finished_delay = 0;
reg inst_finished_delay2= 0;
reg inst_finished_delay3= 0;

reg second_finished = 0;
wire this_inst_finished = inst_finished & ~second_finished;

wire inst_finish1d = inst_finished_delay & ~inst_finished_delay2;
wire inst_finish2d = inst_finished_delay2& ~inst_finished_delay3;



wire [31:0] mem_raddr0;
wire [31:0] mem_raddr1;
wire [31:0] mem_raddr2;

wire  [31:0] mem_rdata0;
wire  [31:0] mem_rdata1;
wire  [31:0] mem_rdata2;

wire        mem_wen0;
wire [31:0] mem_waddr0;
wire [31:0] mem_wdata0;
wire        GM_step;



  wire [31:0] GM_x0;
  wire [31:0] GM_x1;
  wire [31:0] GM_x10;
  wire [31:0] GM_x11;
  wire [31:0] GM_x12;
  wire [31:0] GM_x13;
  wire [31:0] GM_x14;
  wire [31:0] GM_x15;
  wire [31:0] GM_x16;
  wire [31:0] GM_x17;
  wire [31:0] GM_x18;
  wire [31:0] GM_x19;
  wire [31:0] GM_x2;
  wire [31:0] GM_x20;
  wire [31:0] GM_x21;
  wire [31:0] GM_x22;
  wire [31:0] GM_x23;
  wire [31:0] GM_x24;
  wire [31:0] GM_x25;
  wire [31:0] GM_x26;
  wire [31:0] GM_x27;
  wire [31:0] GM_x28;
  wire [31:0] GM_x29;
  wire [31:0] GM_x3;
  wire [31:0] GM_x30;
  wire [31:0] GM_x31;
  wire [31:0] GM_x4;
  wire [31:0] GM_x5;
  wire [31:0] GM_x6;
  wire [31:0] GM_x7;
  wire [31:0] GM_x8;
  wire [31:0] GM_x9;
  wire [31:0] GM_pc;

riscv GM(
  .clk(clock),
  .rst(reset),
  .step(GM_step),
      .x0(GM_x0),
      .x1(GM_x1),
      .x2(GM_x2),
      .x3(GM_x3),
      .x4(GM_x4),
      .x5(GM_x5),
      .x6(GM_x6),
      .x7(GM_x7),
      .x8(GM_x8),
      .x9(GM_x9),
      .x10(GM_x10),
      .x11(GM_x11),
      .x12(GM_x12),
      .x13(GM_x13),
      .x14(GM_x14),
      .x15(GM_x15),
      .x16(GM_x16),
      .x17(GM_x17),
      .x18(GM_x18),
      .x19(GM_x19),
      .x20(GM_x20),
      .x21(GM_x21),
      .x22(GM_x22),
      .x23(GM_x23),
      .x24(GM_x24),
      .x25(GM_x25),
      .x26(GM_x26),
      .x27(GM_x27),
      .x28(GM_x28),
      .x29(GM_x29),
      .x30(GM_x30),
      .x31(GM_x31),
      .pc (GM_pc),
  .mem_raddr0(mem_raddr0),
  .mem_raddr1(mem_raddr1),
  .mem_raddr2(mem_raddr2),

  .mem_rdata0(mem_rdata0),
  .mem_rdata1(mem_rdata1),
  .mem_rdata2(mem_rdata2),
  
  .mem_wen0(mem_wen0),
  .mem_waddr0(mem_waddr0),
  .mem_wdata0(mem_wdata0)
  

  );




  wire        reg_mem_mismatch_nxt;
  wire        load_not_ack_yet;
  wire        resp_a_non_monitored_req;
  wire        sm_GM_step;
  wire        sm_Assumpt_Time;

ShareMem sm(
    .clock(clock), .reset(reset),

    .io_dmem_req_ready(io_dmem_req_ready),

    .io_dmem_replay_next_rand(io_dmem_replay_next_rand),


    .io_imem_resp_bits_replay(io_imem_resp_bits_replay),
    .io_imem_resp_valid(io_imem_resp_valid),



    .io_dmem_s1_kill(io_dmem_s1_kill),
    .io_dmem_req_valid(io_dmem_req_valid),
    .io_dmem_req_bits_addr(io_dmem_req_bits_addr),
    .io_dmem_req_bits_tag(io_dmem_req_bits_tag),
    .io_dmem_req_bits_cmd(io_dmem_req_bits_cmd),
    .io_dmem_req_bits_typ(io_dmem_req_bits_typ),
    .io_dmem_req_bits_data(io_dmem_req_bits_data),
    .io_dmem_s1_data(io_dmem_s1_data),

    .io_dmem_resp_bits_addr(io_dmem_resp_bits_addr),
    .io_dmem_resp_bits_tag(io_dmem_resp_bits_tag),
    .io_dmem_resp_bits_cmd(io_dmem_resp_bits_cmd),
    .io_dmem_resp_bits_typ(io_dmem_resp_bits_typ),
    .io_dmem_resp_bits_data(io_dmem_resp_bits_data),
    .io_dmem_resp_bits_has_data(io_dmem_resp_bits_has_data),

    .io_dmem_s2_nack(io_dmem_s2_nack),
    .io_dmem_replay_next(io_dmem_replay_next),
    .io_dmem_resp_valid(io_dmem_resp_valid),
    .io_dmem_resp_bits_replay(io_dmem_resp_bits_replay),
    .io_dmem_ordered(io_dmem_ordered),


    .io_imem_req_valid(io_imem_req_valid),
    .io_imem_req_bits_pc(io_imem_req_bits_pc),

    .io_imem_resp_ready(io_imem_resp_ready),
    .io_imem_resp_bits_pc(io_imem_resp_bits_pc),
    .io_imem_resp_bits_data(io_imem_resp_bits_data),


    .reg_mem_mismatch_nxt(reg_mem_mismatch_nxt),



    .mem_raddr0(mem_raddr0),
    .mem_raddr1(mem_raddr1),
    .mem_raddr2(mem_raddr2),

    .mem_rdata0(mem_rdata0),
    .mem_rdata1(mem_rdata1),
    .mem_rdata2(mem_rdata2),

    .mem_wen0(mem_wen0),
    .mem_waddr0(mem_waddr0),
    .mem_wdata0(mem_wdata0),






    .ex_monitor(ex_monitor),
    .load_not_ack_yet(load_not_ack_yet),
    .resp_a_non_monitored_req(resp_a_non_monitored_req),

    .GM_step(sm_GM_step),
    .Assumpt_Time(sm_Assumpt_Time)
     );



  wire [31:0] IMPL_ibuf_io_pc_o;
  wire [31:0] IMPL_wb_reg_pc_o;
  wire [31:0] first_valid_pc;
  wire IMPL_ctrl_killd_o;
  wire IMPL_ctrl_killx_o;
  wire IMPL_ctrl_killm_o;
  wire IMPL_wb_reg_valid_o;


  wire [31:0] IMPL_ibuf_io_inst_0_bits_inst_bits_o;
  wire        IMPL_ibuf_io_inst_0_valid_o;
  wire        IMPL_ex_reg_valid_o;
  wire        IMPL_mem_reg_valid_o;
  wire        IMPL_wb_valid_o;
  wire [31:0] IMPL_wb_reg_inst_o;

  wire no_first_valid_pc;

  wire IMPL_id_rs_0_in_use;
  wire IMPL_id_rs_1_in_use;
  wire [31:0] IMPL_ex_rs_0_o;
  wire [31:0] IMPL_ex_rs_1_o;


  wire [4:0]  rf_idx_i;
  wire [31:0] rf_idx_o;


  wire [31:0] IMPL_x0;
  wire [31:0] IMPL_x1;
  wire [31:0] IMPL_x10;
  wire [31:0] IMPL_x11;
  wire [31:0] IMPL_x12;
  wire [31:0] IMPL_x13;
  wire [31:0] IMPL_x14;
  wire [31:0] IMPL_x15;
  wire [31:0] IMPL_x16;
  wire [31:0] IMPL_x17;
  wire [31:0] IMPL_x18;
  wire [31:0] IMPL_x19;
  wire [31:0] IMPL_x2;
  wire [31:0] IMPL_x20;
  wire [31:0] IMPL_x21;
  wire [31:0] IMPL_x22;
  wire [31:0] IMPL_x23;
  wire [31:0] IMPL_x24;
  wire [31:0] IMPL_x25;
  wire [31:0] IMPL_x26;
  wire [31:0] IMPL_x27;
  wire [31:0] IMPL_x28;
  wire [31:0] IMPL_x29;
  wire [31:0] IMPL_x3;
  wire [31:0] IMPL_x30;
  wire [31:0] IMPL_x31;
  wire [31:0] IMPL_x4;
  wire [31:0] IMPL_x5;
  wire [31:0] IMPL_x6;
  wire [31:0] IMPL_x7;
  wire [31:0] IMPL_x8;
  wire [31:0] IMPL_x9;

Rocket dut(
    .clock(clock),
    .reset(reset),
    
    .io_interrupts_debug(io_interrupts_debug),
    .io_interrupts_mtip(io_interrupts_mtip),
    .io_interrupts_msip(io_interrupts_msip),
    .io_interrupts_meip(io_interrupts_meip),
    .io_hartid(32'd0),


      .io_imem_req_valid(io_imem_req_valid),
      .io_imem_req_bits_pc(io_imem_req_bits_pc),
      .io_imem_req_bits_speculative(),

      .io_imem_resp_valid(io_imem_resp_valid),
      .io_imem_resp_bits_replay(io_imem_resp_bits_replay),


      .io_imem_resp_ready(io_imem_resp_ready),
      .io_imem_resp_bits_pc(io_imem_resp_bits_pc),
      .io_imem_resp_bits_data(io_imem_resp_bits_data),
      .io_imem_resp_bits_mask(2'b11),
      .io_imem_resp_bits_xcpt_if(1'b0),
      
      .io_imem_resp_bits_btb_valid(io_imem_resp_bits_btb_valid),
      .io_imem_resp_bits_btb_bits_taken(),
      .io_imem_resp_bits_btb_bits_mask(),
      .io_imem_resp_bits_btb_bits_bridx(),
      .io_imem_resp_bits_btb_bits_target(),
      .io_imem_resp_bits_btb_bits_entry(),
      .io_imem_resp_bits_btb_bits_bht_history(),
      .io_imem_resp_bits_btb_bits_bht_value(),

      .io_imem_npc(),

    
    .io_dmem_req_ready(io_dmem_req_ready),
    .io_dmem_replay_next(io_dmem_replay_next),
    .io_dmem_resp_valid(io_dmem_resp_valid),
    .io_dmem_resp_bits_replay(io_dmem_resp_bits_replay),


    .io_dmem_req_valid(io_dmem_req_valid),
    .io_dmem_req_bits_addr(io_dmem_req_bits_addr),
    .io_dmem_req_bits_cmd(io_dmem_req_bits_cmd),
    .io_dmem_req_bits_typ(io_dmem_req_bits_typ),
    .io_dmem_req_bits_data(io_dmem_req_bits_data),
    .io_dmem_req_bits_tag(io_dmem_req_bits_tag),
    .io_dmem_req_bits_phys(),

    .io_dmem_s1_kill(io_dmem_s1_kill),
    .io_dmem_s2_nack(io_dmem_s2_nack),
    .io_dmem_s1_data(io_dmem_s1_data),
    .io_dmem_ordered(io_dmem_ordered),
    .io_dmem_xcpt_ma_ld(1'b0),
    .io_dmem_xcpt_ma_st(1'b0),
    .io_dmem_xcpt_pf_ld(1'b0),
    .io_dmem_xcpt_pf_st(1'b0),


    .io_dmem_resp_bits_addr(io_dmem_resp_bits_addr),
    .io_dmem_resp_bits_tag(io_dmem_resp_bits_tag),
    .io_dmem_resp_bits_cmd(io_dmem_resp_bits_cmd),
    .io_dmem_resp_bits_typ(io_dmem_resp_bits_typ),
    .io_dmem_resp_bits_data(io_dmem_resp_bits_data),
    .io_dmem_resp_bits_has_data(io_dmem_resp_bits_has_data),
    .io_dmem_resp_bits_data_word_bypass(io_dmem_resp_bits_data_word_bypass),
    .io_dmem_resp_bits_store_data(),
    .io_dmem_invalidate_lr(),

    .io_rocc_fpu_resp_ready(1'b0),
    .io_rocc_fpu_req_valid(1'b0),
    .io_rocc_autl_grant_bits_is_builtin_type(),
    .io_rocc_autl_grant_bits_client_xact_id(),
    .io_rocc_autl_grant_ready(1'b1),
    .io_rocc_autl_acquire_bits_is_builtin_type(1'b1),
    .io_rocc_autl_acquire_bits_client_xact_id(1'b0),
    .io_rocc_autl_acquire_valid(1'b0),
    .io_rocc_busy(1'b0),
    .io_rocc_interrupt(1'b0),
    .io_rocc_mem_invalidate_lr(1'b1),
    .io_rocc_mem_s1_kill(1'b0),
    .io_rocc_mem_req_valid(1'b0),
    .io_rocc_resp_valid(1'b0),
    .io_rocc_cmd_ready(1'b0),
    .io_fpu_cp_resp_valid(1'b0),
    .io_fpu_cp_resp_bits_data(33'd0),
    .io_fpu_fcsr_rdy(1'b1),
    .io_fpu_nack_mem(1'b0),
    .io_fpu_illegal_rm(1'b0),
    .io_fpu_fcsr_flags_valid(1'b0),
    .io_fpu_fcsr_flags_bits(5'd0),
    .io_fpu_toint_data(0),



      .ibuf_io_inst_0_bits_inst_bits_o(IMPL_ibuf_io_inst_0_bits_inst_bits_o),
      .ibuf_io_inst_0_valid_o(IMPL_ibuf_io_inst_0_valid_o),
      .ex_reg_valid_o(IMPL_ex_reg_valid_o),
      .mem_reg_valid_o(IMPL_mem_reg_valid_o),
      .wb_valid_o(IMPL_wb_valid_o),
      .wb_reg_valid_o(IMPL_wb_reg_valid_o),
      .wb_reg_inst_o(IMPL_wb_reg_inst_o),

      .ctrl_killd_o(IMPL_ctrl_killd_o),
      .ctrl_killx_o(IMPL_ctrl_killx_o),
      .ctrl_killm_o(IMPL_ctrl_killm_o),


      .ibuf_io_pc_o(IMPL_ibuf_io_pc_o),
      .wb_reg_pc_o(IMPL_wb_reg_pc_o),
      .first_valid_pc(first_valid_pc),
      .no_first_valid_pc(no_first_valid_pc),

      .rf_idx_i(rf_idx_i),
      .rf_idx_o(rf_idx_o),

      .id_rs_0_in_use(IMPL_id_rs_0_in_use),
      .id_rs_1_in_use(IMPL_id_rs_1_in_use),

      .ex_rs_0_o(IMPL_ex_rs_0_o),
      .ex_rs_1_o(IMPL_ex_rs_1_o),


      .x0(IMPL_x0),
      .x1(IMPL_x1),
      .x2(IMPL_x2),
      .x3(IMPL_x3),
      .x4(IMPL_x4),
      .x5(IMPL_x5),
      .x6(IMPL_x6),
      .x7(IMPL_x7),
      .x8(IMPL_x8),
      .x9(IMPL_x9),
      .x10(IMPL_x10),
      .x11(IMPL_x11),
      .x12(IMPL_x12),
      .x13(IMPL_x13),
      .x14(IMPL_x14),
      .x15(IMPL_x15),
      .x16(IMPL_x16),
      .x17(IMPL_x17),
      .x18(IMPL_x18),
      .x19(IMPL_x19),
      .x20(IMPL_x20),
      .x21(IMPL_x21),
      .x22(IMPL_x22),
      .x23(IMPL_x23),
      .x24(IMPL_x24),
      .x25(IMPL_x25),
      .x26(IMPL_x26),
      .x27(IMPL_x27),
      .x28(IMPL_x28),
      .x29(IMPL_x29),
      .x30(IMPL_x30),
      .x31(IMPL_x31)


    );

reg nondetStart;
wire inst_begin_cond = ~inst_begin & nondetStart & ~inst_issued;
assume property (~nondetStart | (IMPL_ibuf_io_inst_0_valid_o & ~ IMPL_ctrl_killd_o) );






reg inst_has_begun = 0;
always @(posedge clock) begin
  if(reset)
    inst_has_begun <= 1'b0;
  else if(inst_begin_cond)
    inst_has_begun <= 1'b1;
end

always @(posedge clock) begin
  if(reset)
    inst_begin <= 1'b0;
  else if(inst_begin_cond )
    inst_begin <= 1'b1;
  else if( inst_begin & IMPL_ex_reg_valid_o)
    inst_begin <= 1'b0;
end

always @(posedge clock) begin
  if(reset)
    inst_issued <= 1'b0;
  else if( inst_begin & IMPL_ex_reg_valid_o )
    inst_issued <= 1'b1;
end

always @(posedge clock) begin
  if(reset) 
    ex_monitor <= 1'b0;
  else if(inst_begin & IMPL_ex_reg_valid_o & ~IMPL_ctrl_killx_o)
    ex_monitor <= 1'b1;
  else if(ex_monitor & IMPL_mem_reg_valid_o)
    ex_monitor <= 1'b0;
  else if(IMPL_ctrl_killx_o)
    ex_monitor <= 1'b0;
end

always @(posedge clock) begin
  if(reset)
    mem_monitor <= 1'b0;
  else if(ex_monitor & IMPL_mem_reg_valid_o & ~IMPL_ctrl_killm_o)
    mem_monitor <= 1'b1;
  else if(mem_monitor & IMPL_wb_valid_o)
    mem_monitor <= 1'b0;
  else if(IMPL_ctrl_killm_o)
    mem_monitor <= 1'b0;
end

always @(posedge clock) begin
  if(reset) begin 
    inst_finished <= 1'b0;
    inst_finished_delay <= 1'b0;
    inst_finished_delay2 <= 1'b0;
    inst_finished_delay3 <= 1'b0;
  end
  else begin
    inst_finished_delay <= inst_finished;
    inst_finished_delay2 <= inst_finished_delay;
    inst_finished_delay3 <= inst_finished_delay2;
    if(mem_monitor & IMPL_wb_valid_o)
      inst_finished <= 1'b1;
  end
end


wire before_next_inst_commited = this_inst_finished & (IMPL_wb_valid_o);
always @(posedge clock) begin 
  if(reset)
    second_finished <= 1'b0;
  else if(before_next_inst_commited)
    second_finished <= 1'b1;
end



wire inst_gpr_assert_cond = mem_monitor & IMPL_wb_valid_o;

    assume property (~( inst_gpr_assert_cond ) | (IMPL_x0 == GM_x0) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x1 == GM_x1) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x2 == GM_x2) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x3 == GM_x3) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x4 == GM_x4) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x5 == GM_x5) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x6 == GM_x6) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x7 == GM_x7) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x8 == GM_x8) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x9 == GM_x9) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x10 == GM_x10) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x11 == GM_x11) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x12 == GM_x12) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x13 == GM_x13) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x14 == GM_x14) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x15 == GM_x15) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x16 == GM_x16) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x17 == GM_x17) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x18 == GM_x18) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x19 == GM_x19) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x20 == GM_x20) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x21 == GM_x21) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x22 == GM_x22) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x23 == GM_x23) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x24 == GM_x24) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x25 == GM_x25) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x26 == GM_x26) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x27 == GM_x27) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x28 == GM_x28) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x29 == GM_x29) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x30 == GM_x30) );
    assume property (~( inst_gpr_assert_cond ) | (IMPL_x31 == GM_x31) );


    assume property (~( inst_begin_cond ) | (IMPL_ibuf_io_pc_o == GM_pc) );



    reg [31:0] instruction_interested;
    always @(posedge clock) begin 
        if(inst_begin_cond)
            instruction_interested <= IMPL_ibuf_io_inst_0_bits_inst_bits_o;
    end

    assume property ( ~ (GM_step) | (instruction_interested == mem_rdata0 ) );



    assign  sm_GM_step = GM_step;
    assign  sm_Assumpt_Time = IMPL_ibuf_io_inst_0_valid_o;

    wire isLB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000003;
    wire isLW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002003;
    wire isLH = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001003;
    wire isLD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003003;
    wire isLBU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004003;
    wire isLHU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005003;
    wire isLWU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006003;
    wire isSB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000023;
    wire isSH = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001023;
    wire isSW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002023;
    wire isSD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003023;
    wire isBEQ = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000063;
    wire isBNE = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001063;
    wire isBLT = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004063;
    wire isBGE = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005063;
    wire isBLTU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006063;
    wire isBGEU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007063;
    wire isJAL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h0000006f;
    wire isJALR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000067;
    wire isLUI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h00000037;
    wire isAUIPC = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000007f) == 32'h00000017;
    wire isADDI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00000013;
    wire isSLTI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002013;
    wire isSLTIU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003013;
    wire isXORI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00004013;
    wire isORI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006013;
    wire isANDI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007013;
    wire isSRLI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00005013;
    wire isSRAI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40005013;
    wire isSLLI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00001013;
    wire isADD = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00000033;
    wire isSUB = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40000033;
    wire isSLL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00001033;
    wire isSLT = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00002033;
    wire isSLTU = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00003033;
    wire isXOR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00004033;
    wire isSRL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00005033;
    wire isSRA = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h40005033;
    wire isOR = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00006033;
    wire isAND = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfe00707f) == 32'h00007033;
    wire isCSRRW = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00001073;
    wire isCSRRS = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00002073;
    wire isCSRRC = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00003073;
    wire isCSRRWI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00005073;
    wire isCSRRSI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00006073;
    wire isCSRRCI = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'h0000707f) == 32'h00007073;
    wire isECALL = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h00000073;
    wire isEBREAK = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h00100073;
    wire isSRET = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h10200073;
    wire isMRET = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hffffffff) == 32'h30200073;
    wire isSFENCE_VM = (IMPL_ibuf_io_inst_0_bits_inst_bits_o & 32'hfff07fff) == 32'h10400073;


    wire WBisLB = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000003;
    wire WBisLW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002003;
    wire WBisLH = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001003;
    wire WBisLD = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003003;
    wire WBisLBU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004003;
    wire WBisLHU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005003;
    wire WBisLWU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006003;
    wire WBisSB = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000023;
    wire WBisSH = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001023;
    wire WBisSW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002023;
    wire WBisSD = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003023;
    wire WBisBEQ = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000063;
    wire WBisBNE = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001063;
    wire WBisBLT = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004063;
    wire WBisBGE = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005063;
    wire WBisBLTU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006063;
    wire WBisBGEU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007063;
    wire WBisJAL = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h0000006f;
    wire WBisJALR = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000067;
    wire WBisLUI = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h00000037;
    wire WBisAUIPC = (IMPL_wb_reg_inst_o & 32'h0000007f) == 32'h00000017;
    wire WBisADDI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00000013;
    wire WBisSLTI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002013;
    wire WBisSLTIU = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003013;
    wire WBisXORI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00004013;
    wire WBisORI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006013;
    wire WBisANDI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007013;
    wire WBisSRLI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00005013;
    wire WBisSRAI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40005013;
    wire WBisSLLI = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00001013;
    wire WBisADD = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00000033;
    wire WBisSUB = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40000033;
    wire WBisSLL = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00001033;
    wire WBisSLT = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00002033;
    wire WBisSLTU = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00003033;
    wire WBisXOR = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00004033;
    wire WBisSRL = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00005033;
    wire WBisSRA = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h40005033;
    wire WBisOR = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00006033;
    wire WBisAND = (IMPL_wb_reg_inst_o & 32'hfe00707f) == 32'h00007033;
    wire WBisCSRRW = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00001073;
    wire WBisCSRRS = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00002073;
    wire WBisCSRRC = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00003073;
    wire WBisCSRRWI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00005073;
    wire WBisCSRRSI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00006073;
    wire WBisCSRRCI = (IMPL_wb_reg_inst_o & 32'h0000707f) == 32'h00007073;
    wire WBisECALL = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h00000073;
    wire WBisEBREAK = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h00100073;
    wire WBisSRET = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h10200073;
    wire WBisMRET = (IMPL_wb_reg_inst_o & 32'hffffffff) == 32'h30200073;
    wire WBisSFENCE_VM = (IMPL_wb_reg_inst_o & 32'hfff07fff) == 32'h10400073;



    wire DECODE_isLoad = isLW | isLB | isLBU | isLH | isLHU;
    wire WBisBranch = WBisBEQ | WBisBNE | WBisBGEU | WBisBGE | WBisBLT | WBisBLTU;
    wire DECODE_validInstructions = 
      isSB | isSH | isSW | isLW | isLB | isLBU | isLH | isLHU |
       isBEQ | isBNE | isBLT | isBGE | isBLTU | isBGEU | isJAL | isJALR | 
      isLUI | isAUIPC | isADDI | isSLTI | isSLTIU | isXORI | isORI | isANDI | 
      isSRLI | isSRAI | isSLLI | isADD | isSUB | isSLL | isSLT | isSLTU | isXOR | 
      isSRL | isSRA | isOR | isAND ;
    wire WB_validInstructions = 
      WBisSB | WBisSH | WBisSW | WBisLW | WBisLB | WBisLBU | WBisLH | WBisLHU |
       WBisBEQ | WBisBNE | WBisBLT | WBisBGE | WBisBLTU | WBisBGEU | WBisJAL | WBisJALR | 
      WBisLUI | WBisAUIPC | WBisADDI | WBisSLTI | WBisSLTIU | WBisXORI | WBisORI | WBisANDI | 
      WBisSRLI | WBisSRAI | WBisSLLI | WBisADD | WBisSUB | WBisSLL | WBisSLT | WBisSLTU | WBisXOR | 
      WBisSRL | WBisSRA | WBisOR | WBisAND ;





    wire[31:0] WBimmS = { { 20{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31:25], IMPL_wb_reg_inst_o[11:7] };
    wire[31:0] WBimmI = { { 20{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31:20] };
    wire[31:0] WBimmJ = { { 11{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31] , IMPL_wb_reg_inst_o[19:12] , IMPL_wb_reg_inst_o[20], IMPL_wb_reg_inst_o[30:21],1'b0 };
    wire[31:0] WBimmB = { { 19{IMPL_wb_reg_inst_o[31]} } , IMPL_wb_reg_inst_o[31], IMPL_wb_reg_inst_o[7], IMPL_wb_reg_inst_o[30:25], IMPL_wb_reg_inst_o[11:8], 1'b0 };
    assign rf_idx_i = IMPL_wb_reg_inst_o[19:15];
    wire[1:0] loadAddr = rf_idx_o[1:0] + WBimmI[1:0];
    wire[1:0] storeAddr= rf_idx_o[1:0] + WBimmS[1:0];


    wire CommitPointAll = IMPL_wb_valid_o;
    assume property (~CommitPointAll | (~WBisJAL  |(( IMPL_wb_reg_pc_o + WBimmJ ) & 2'b11) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisJALR |(( rf_idx_o + WBimmI )&2'b10) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisBranch | ((  IMPL_wb_reg_pc_o + WBimmB) & 2'b11) == 2'b00 ) );
    assume property (~CommitPointAll | (~WBisLH | (loadAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisLHU | (loadAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisLW | (loadAddr == 2'b00 ) ));

    assume property (~CommitPointAll | (~WBisSH | (storeAddr[0] == 1'b0 ) ));
    assume property (~CommitPointAll | (~WBisSW | (storeAddr == 2'b00 ) ));
    assume property (~CommitPointAll | (GM_x0 == 0) );
    assume property (~CommitPointAll | (GM_pc[1:0] == 2'b00) );
    assume property (GM_x0 == 0);
    


    assume property ( ~(inst_has_begun | inst_begin_cond) | (io_interrupts_debug == 1'b0) );

    


      assume property (~IMPL_ibuf_io_inst_0_valid_o |  (isBEQ|isADD|isLW|isSW) );



    assume property (~IMPL_wb_reg_valid_o | WB_validInstructions);


    wire justFinish = inst_finished & ~inst_finished_delay;


    reg isInstLoad = 1'b0;
    reg delay_check = 1'b0;
    reg check_ready = 1'b0;
    reg check_ready_delay1 = 1'b0;
    wire delay_check_point = check_ready & ~check_ready_delay1;

    reg[4:0] inst_decode_rd;
    always @(posedge clock) begin 
      if(reset) begin
        isInstLoad <= 1'b0;
      end
      else if(inst_begin_cond) begin
        isInstLoad <= DECODE_isLoad;
        inst_decode_rd <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[11:7];
      end
    end


    always @(posedge clock) begin 
      if(reset)
        delay_check <= 1'b0;
      else if(mem_monitor & IMPL_wb_valid_o & isInstLoad & (load_not_ack_yet & ~ (io_dmem_resp_valid & io_dmem_resp_bits_has_data ) )) 
        delay_check <= 1'b1;
      else if(delay_check & (io_dmem_resp_valid & io_dmem_resp_bits_has_data )  )
        delay_check <= 1'b0;
    end

    always @(posedge clock) begin 
      if(reset)
        check_ready <= 1'b0;
      else if( delay_check & (io_dmem_resp_valid & io_dmem_resp_bits_has_data )  ) 
        check_ready <= 1'b1;
    end

    always @(posedge clock) begin
      if(reset)
        check_ready_delay1 <= 1'b0;
      else
        check_ready_delay1 <= check_ready;
    end


    assign GM_step = mem_monitor & IMPL_wb_valid_o;
    assert property ( justFinish |-> (GM_x0 == IMPL_x0) );

    property x1_no_resp_overlap;
      (
        ~resp_a_non_monitored_req ##1
        ( justFinish & ( ~delay_check | (inst_decode_rd != 5'd1 )  ) )
      )  |-> (GM_x1 == IMPL_x1);
    endproperty

    reg[31:0] GM_origin_x1;
    always @(*) begin 
      if(inst_gpr_assert_cond)
        GM_origin_x1 <= GM_x1;
    end

    property x1_resp_overlap ;
      (
          (resp_a_non_monitored_req && (io_dmem_resp_bits_tag[5:1] == 5'd1) ) ##1
          (justFinish)
      )  |-> (GM_origin_x1 == GM_x1);
    endproperty

    property x1_load_delay;
      ( delay_check_point & (inst_decode_rd == 5'd1) ) |->  (GM_x1 == IMPL_x1) ;
    endproperty





    x1_nro: assert property (x1_no_resp_overlap);
    x1_ro:  assert property (x1_resp_overlap);
    x1_ld:  assert property (x1_load_delay);








    always @(posedge clock) begin 
      assume property ( io_imem_req_valid |-> ##[1:$] io_imem_resp_valid );
    end


    sequence dmem_req_VALID;
      io_dmem_req_valid ##1 ~io_dmem_s1_kill ##1 ~io_dmem_s2_nack;
    endsequence


    always @(posedge clock) begin
      assume property (dmem_req_VALID |-> ##[1:$] io_dmem_replay_next_rand );
    end

    will_finish: assert property ( inst_finished |-> ##[1:$] (before_next_inst_commited && ( IMPL_wb_reg_pc_o == GM_pc) ) );



    pc_a: assert property ( before_next_inst_commited |-> ( IMPL_wb_reg_pc_o == GM_pc)  );


    mem_match: assert property ( inst_finish1d |->  ~reg_mem_mismatch_nxt );




 

   reg[31:0] id_rs_0_reg;
   reg[4:0]  id_rs_0_field;
   reg[31:0] id_rs_1_reg;
   reg[4:0]  id_rs_1_field;

   reg       id_rs_0_in_use;
   reg       id_rs_1_in_use;

   always @(posedge clock) begin 
    if(reset) begin 
      id_rs_0_in_use <= 1'b0;
      id_rs_1_in_use <= 1'b0;
      id_rs_0_field  <= 5'd0;
      id_rs_1_field  <= 5'd0;
    end
    else begin 
      if(inst_begin_cond) begin 
        id_rs_0_in_use <= IMPL_id_rs_0_in_use;
        id_rs_1_in_use <= IMPL_id_rs_1_in_use;
        id_rs_0_field <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[19:15];
        id_rs_1_field <= IMPL_ibuf_io_inst_0_bits_inst_bits_o[24:20];
      end
    end
   end

   always @(posedge clock) begin 
    if(inst_begin & IMPL_ex_reg_valid_o & ~IMPL_ctrl_killx_o ) begin 
      id_rs_0_reg <= IMPL_ex_rs_0_o;
      id_rs_1_reg <= IMPL_ex_rs_1_o;
    end
   end


     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd0 ) || (IMPL_x0 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd1 ) || (IMPL_x1 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd2 ) || (IMPL_x2 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd3 ) || (IMPL_x3 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd4 ) || (IMPL_x4 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd5 ) || (IMPL_x5 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd6 ) || (IMPL_x6 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd7 ) || (IMPL_x7 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd8 ) || (IMPL_x8 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd9 ) || (IMPL_x9 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd10 ) || (IMPL_x10 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd11 ) || (IMPL_x11 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd12 ) || (IMPL_x12 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd13 ) || (IMPL_x13 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd14 ) || (IMPL_x14 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd15 ) || (IMPL_x15 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd16 ) || (IMPL_x16 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd17 ) || (IMPL_x17 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd18 ) || (IMPL_x18 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd19 ) || (IMPL_x19 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd20 ) || (IMPL_x20 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd21 ) || (IMPL_x21 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd22 ) || (IMPL_x22 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd23 ) || (IMPL_x23 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd24 ) || (IMPL_x24 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd25 ) || (IMPL_x25 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd26 ) || (IMPL_x26 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd27 ) || (IMPL_x27 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd28 ) || (IMPL_x28 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd29 ) || (IMPL_x29 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd30 ) || (IMPL_x30 == id_rs_0_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_0_in_use == 1'b1 && id_rs_0_field == 5'd31 ) || (IMPL_x31 == id_rs_0_reg ) ) );

     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd0  ) || (IMPL_x0  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd1  ) || (IMPL_x1  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd2  ) || (IMPL_x2  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd3  ) || (IMPL_x3  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd4  ) || (IMPL_x4  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd5  ) || (IMPL_x5  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd6  ) || (IMPL_x6  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd7  ) || (IMPL_x7  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd8  ) || (IMPL_x8  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd9  ) || (IMPL_x9  == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd10 ) || (IMPL_x10 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd11 ) || (IMPL_x11 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd12 ) || (IMPL_x12 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd13 ) || (IMPL_x13 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd14 ) || (IMPL_x14 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd15 ) || (IMPL_x15 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd16 ) || (IMPL_x16 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd17 ) || (IMPL_x17 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd18 ) || (IMPL_x18 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd19 ) || (IMPL_x19 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd20 ) || (IMPL_x20 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd21 ) || (IMPL_x21 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd22 ) || (IMPL_x22 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd23 ) || (IMPL_x23 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd24 ) || (IMPL_x24 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd25 ) || (IMPL_x25 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd26 ) || (IMPL_x26 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd27 ) || (IMPL_x27 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd28 ) || (IMPL_x28 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd29 ) || (IMPL_x29 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd30 ) || (IMPL_x30 == id_rs_1_reg ) ) );
     assert property (~inst_gpr_assert_cond || ( ~( id_rs_1_in_use == 1'b1 && id_rs_1_field == 5'd31 ) || (IMPL_x31 == id_rs_1_reg ) ) );








endmodule