library ieee;  use ieee.std_logic_1164.all, ieee.numeric_bit.all;

use work.dlx_types.all;

architecture verifier of dlx_test is

  component clock_gen is
    port ( clk : out bit;
           reset : out bit );
  end component clock_gen;

  component memory is
    port ( clk : in bit;
           a : in dlx_address;
           d : inout dlx_bus_word;
           width : in dlx_mem_width;
           write_enable : in bit;
           burst : in bit := '0';
           mem_enable : in bit;
           ready : out bit );
  end component memory;

  component dlx is
    port ( clk : in bit;
           reset : in bit;
           halt : out bit;
           a : out dlx_address;
           d : inout dlx_bus_word;
           width : out dlx_mem_width;
           write_enable : out bit;
           ifetch : out bit;
           mem_enable : out bit;
           ready : in bit );
  end component dlx;

  signal clk, reset : bit;

  signal a_behav : dlx_address;
  signal d_behav : dlx_bus_word;
  signal halt_behav : bit;
  signal width_behav : dlx_mem_width;
  signal write_enable_behav, mem_enable_behav, ifetch_behav : bit;

  signal a_rtl : dlx_address;
  signal d_rtl : dlx_bus_word;
  signal halt_rtl : bit;
  signal width_rtl : dlx_mem_width;
  signal write_enable_rtl, mem_enable_rtl, ifetch_rtl : bit;

  signal ready_mem : bit;

begin

  cg : component clock_gen
    port map ( clk => clk, reset => reset );

  mem : component memory
    port map ( clk => clk,
               a => a_behav, d => d_behav,
               width => width_behav, write_enable => write_enable_behav,
               burst => open,
               mem_enable => mem_enable_behav, ready => ready_mem );

  proc_behav : component dlx
    port map ( clk => clk, reset => reset, halt => halt_behav,
               a => a_behav, d => d_behav,
               width => width_behav, write_enable => write_enable_behav,
               ifetch => ifetch_behav,
               mem_enable => mem_enable_behav, ready => ready_mem );

  proc_rtl : component dlx
    port map ( clk => clk, reset => reset, halt => halt_rtl,
               a => a_rtl, d => d_rtl,
               width => width_rtl, write_enable => write_enable_rtl,
               ifetch => ifetch_rtl,
               mem_enable => mem_enable_rtl, ready => ready_mem );

  verification_section : block is
  begin

    fwd_data_from_mem_to_rtl : 
      d_rtl <= d_behav when mem_enable_rtl = '1'
                            and write_enable_rtl = '0' else
               disabled_dlx_word;

    monitor : process
    begin
      monitor_loop : loop
        -- wait for a command, valid on rising edge of phi2
        wait until rising_edge(clk)
                   and mem_enable_behav = '1' and mem_enable_rtl = '1';
        --
        -- compare the command information
        assert a_behav = a_rtl
          report "addresses differ";
        assert write_enable_behav = write_enable_rtl
          report "write enable states differ";
        assert ifetch_behav = ifetch_rtl
          report "instruction fetch states differ";
        assert width_behav = width_rtl
          report "widths differ";
        if write_enable_behav = '1' and write_enable_rtl = '1' then
          assert d_behav = d_rtl
            report "write data differs";
        end if;
        --
        -- wait for the response from memory
        ready_loop : loop 
          wait until rising_edge(clk);
          exit monitor_loop when reset = '1';
          exit ready_loop when ready_mem = '1';
        end loop ready_loop;
      end loop monitor_loop;
      --
      -- get here when reset is asserted
      wait on clk until rising_edge(clk) and reset = '0';
      --
      -- process monitor now starts again from beginning
    end process monitor;

  end block verification_section;

end architecture verifier;