--
-- Copyright (C) 2015 secunet Security Networks AG
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; version 2 of the License.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
-- GNU General Public License for more details.
--

package HW.Port_IO
with
   Abstract_State => (State with External => (Async_Readers, Async_Writers))
is

   type Port_Type is mod 2**16;

   procedure InB (Value : out Word8; Port : Port_Type)
   with
      Global   => (In_Out => State),
      Depends  => ((Value, State) => (Port, State)),
      Inline_Always;

   procedure InW (Value : out Word16; Port : Port_Type)
   with
      Global   => (In_Out => State),
      Depends  => ((Value, State) => (Port, State)),
      Pre      => Port mod 2 = 0,
      Inline_Always;

   procedure InL (Value : out Word32; Port : Port_Type)
   with
      Global   => (In_Out => State),
      Depends  => ((Value, State) => (Port, State)),
      Pre      => Port mod 4 = 0,
      Inline_Always;

   procedure OutB (Port : Port_Type; Value : Word8)
   with
      Global   => (In_Out => State),
      Depends  => (State =>+ (Port, Value)),
      Inline_Always;

   procedure OutW (Port : Port_Type; Value : Word16)
   with
      Global   => (In_Out => State),
      Depends  => (State =>+ (Port, Value)),
      Pre      => Port mod 2 = 0,
      Inline_Always;

   procedure OutL (Port : Port_Type; Value : Word32)
   with
      Global   => (In_Out => State),
      Depends  => (State =>+ (Port, Value)),
      Pre      => Port mod 4 = 0,
      Inline_Always;

end HW.Port_IO;