module tb_top;

logic clk;
logic nreset;

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

gb gb_inst (
  .clk   (clk),
  .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;

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;

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 code here
`include "sva_common.svh"
`SVA_DEF_CLK(clk);
`SVA_DEF_NRESET(nreset);

`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;

`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)
);

endmodule : tb_top