module tb_top;

logic clk;
logic nreset;

wire        gb_cart_clk;
wire        gb_cart_nreset;
wire        gb_cart_nrd;
wire        gb_cart_nwr;
wire        gb_cart_ncs;
wire [15:0] gb_cart_addr;
wire [ 7:0] gb_cart_data;

clkgen clkgen_inst (
  .clk   (clk),
  .nreset(nreset)
);

gb gb_inst (
  .clk   (clk),
  .nreset(nreset),

  .cart_clk_o   (gb_cart_clk),
  .cart_nreset_o(gb_cart_nreset),
  .cart_nrd_o   (gb_cart_nrd),
  .cart_nwr_o   (gb_cart_nwr),
  .cart_ncs_o   (gb_cart_ncs),
  .cart_addr_o  (gb_cart_addr),
  .cart_data_io (gb_cart_data)
);

cart cart_inst (
  .clk     (gb_cart_clk),
  .nreset  (gb_cart_nreset),
  .nrd_i   (gb_cart_nrd),
  .nwr_i   (gb_cart_nwr),
  .ncs_i   (gb_cart_ncs),
  .addr_i  (gb_cart_addr),
  .data_io (gb_cart_data)
);


`ifdef SVA_ENABLE
`include "sva_common.svh"
`SVA_DEF_CLK(clk);
`SVA_DEF_NRESET(nreset);

logic        instr_valid;
logic        instr_undef;
logic        halted;
logic [15:0] current_pc;
logic [ 7:0] current_opcode[2:0];

logic        we;
logic [15:0] last_write_address;
logic [ 7:0] last_write_value;

logic        vram_sel;
logic        hiram_sel;
logic        ppu_sel;

assign halted      = gb_inst.cpu_inst.ctrl_inst.halted_r;
assign instr_valid = gb_inst.cpu_inst.instr_valid;
assign instr_undef = gb_inst.cpu_inst.ctrl_inst.instr_undef;
assign current_opcode = gb_inst.cpu_inst.instr;

assign we      = gb_inst.cpu_we;

assign vram_sel  = gb_inst.vram_sel;
assign hiram_sel = gb_inst.hiram_sel;
assign ppu_sel   = gb_inst.ppu_inst.sva_ppu_sel;

always_ff @(posedge clk or negedge nreset) begin
  if (!nreset)
    current_pc <= '0;
  else if (instr_valid)
    current_pc <= gb_inst.cpu_inst.pc_r;
end

always_ff @(posedge clk or negedge nreset) begin
  if (!nreset) begin
    last_write_address <= '0;
    last_write_value   <= '0;
  end else if (we) begin
    last_write_address <= gb_inst.cpu_addr;
    last_write_value   <= gb_inst.cpu_wdata;
  end
end

`SVA_ASSERT_PROP_FATAL(undefined_opcode_pushed,
  halted |-> !instr_undef,
  $sformatf("PC: 0x%X | Undefined opcode pushed: 0x%X (0x%X, 0x%X)", current_pc, current_opcode[0], current_opcode[1], current_opcode[2])
);

logic selected_memory_implemented;

assign selected_memory_implemented = hiram_sel | vram_sel | ppu_sel;

`SVA_ASSERT_PROP(write_to_unimplemented_memory,
  we |-> selected_memory_implemented,
  $sformatf("PC: 0x%X | Write to unimplemented memory: 0x%X <= 0x%X",
    current_pc, last_write_address, last_write_value)
);

`endif /* SVA_ENABLE */
endmodule : tb_top