diff --git a/common/Makefile.inc b/common/Makefile.inc
new file mode 100644
index 0000000..b8e4f35
--- /dev/null
+++ b/common/Makefile.inc
@@ -0,0 +1,10 @@
+hw-y += hw.ads
+hw-y += hw-mmio_range.ads
+hw-y += hw-mmio_regs.adb
+hw-y += hw-mmio_regs.ads
+hw-y += hw-port_io.adb
+hw-y += hw-port_io.ads
+hw-y += hw-sub_regs.ads
+hw-y += hw-time.ads
+hw-y += hw-time.adb
+hw-y += hw-time-timer.ads
diff --git a/common/hw-mmio_range.ads b/common/hw-mmio_range.ads
new file mode 100644
index 0000000..1b33630
--- /dev/null
+++ b/common/hw-mmio_range.ads
@@ -0,0 +1,35 @@
+--
+-- Copyright (C) 2015-2016 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.
+--
+
+with System;
+
+generic
+   Base_Addr : Word64;
+   type Element_T is mod <>;
+   type Index_T is range <>;
+   type Array_T is array (Index_T) of Element_T;
+package HW.MMIO_Range
+with
+   Abstract_State =>
+     ((State with External),
+      Base_Address),
+   Initializes => Base_Address
+is
+
+   procedure Read (Value : out Element_T; Index : in Index_T);
+
+   procedure Write (Index : in Index_T; Value : in Element_T);
+
+   procedure Set_Base_Address (Base : Word64);
+
+end HW.MMIO_Range;
diff --git a/common/hw-mmio_regs.adb b/common/hw-mmio_regs.adb
new file mode 100644
index 0000000..5eea563
--- /dev/null
+++ b/common/hw-mmio_regs.adb
@@ -0,0 +1,92 @@
+--
+-- Copyright (C) 2016 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 body HW.MMIO_Regs
+is
+
+   generic
+      type Word_T is mod <>;
+   procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T);
+
+   procedure Read_G (Value : out Word_T; Idx : Subs_P.Index_T)
+   is
+      Off : constant Range_P.Index_T := Range_P.Index_T
+        ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+      pragma Warnings
+        (GNAT, Off, """Mask"" is not modified, could be declared constant",
+         Reason => "Ada RM forbids making it constant.");
+      Mask : Word64 := Shift_Left (1, Regs (Idx).MSB + 1 - Regs (Idx).LSB) - 1;
+      pragma Warnings
+        (GNAT, On, """Mask"" is not modified, could be declared constant");
+      Temp : Range_P.Element_T;
+   begin
+      Range_P.Read (Temp, Off);
+      Value := Word_T (Shift_Right (Word64 (Temp), Regs (Idx).LSB) and Mask);
+   end Read_G;
+
+   procedure Read_I is new Read_G (Word8);
+   procedure Read (Value : out Word8; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word16);
+   procedure Read (Value : out Word16; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word32);
+   procedure Read (Value : out Word32; Idx : Subs_P.Index_T) renames Read_I;
+
+   procedure Read_I is new Read_G (Word64);
+   procedure Read (Value : out Word64; Idx : Subs_P.Index_T) renames Read_I;
+
+   ----------------------------------------------------------------------------
+
+   generic
+      type Word_T is mod <>;
+   procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T);
+
+   procedure Write_G (Idx : Subs_P.Index_T; Value : Word_T)
+   is
+      Off : constant Range_P.Index_T := Range_P.Index_T
+        ((Byte_Offset + Regs (Idx).Byte_Offset) / (Range_P.Element_T'Size / 8));
+      pragma Warnings
+        (GNAT, Off, """Mask"" is not modified, could be declared constant",
+         Reason => "Ada RM forbids making it constant.");
+      Mask : Word64 :=
+         Shift_Left (1, Regs (Idx).MSB + 1) - Shift_Left (1, Regs (Idx).LSB);
+      pragma Warnings
+        (GNAT, On, """Mask"" is not modified, could be declared constant");
+      Temp : Range_P.Element_T;
+   begin
+      if Regs (Idx).MSB - Regs (Idx).LSB + 1 = Range_P.Element_T'Size then
+         Range_P.Write (Off, Range_P.Element_T (Value));
+      else
+         -- read/modify/write
+         Range_P.Read (Temp, Off);
+         Temp := Range_P.Element_T
+           ((Word64 (Temp) and not Mask) or
+            (Shift_Left (Word64 (Value), Regs (Idx).LSB)));
+         Range_P.Write (Off, Temp);
+      end if;
+   end Write_G;
+
+   procedure Write_I is new Write_G (Word8);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word8) renames Write_I;
+
+   procedure Write_I is new Write_G (Word16);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word16) renames Write_I;
+
+   procedure Write_I is new Write_G (Word32);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word32) renames Write_I;
+
+   procedure Write_I is new Write_G (Word64);
+   procedure Write (Idx : Subs_P.Index_T; Value : Word64) renames Write_I;
+
+end HW.MMIO_Regs;
diff --git a/common/hw-mmio_regs.ads b/common/hw-mmio_regs.ads
new file mode 100644
index 0000000..9aafed9
--- /dev/null
+++ b/common/hw-mmio_regs.ads
@@ -0,0 +1,127 @@
+--
+-- Copyright (C) 2016 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.
+--
+
+with HW.Sub_Regs;
+with HW.MMIO_Range;
+
+use type HW.Word64;
+
+generic
+   with package Range_P is new MMIO_Range (<>);
+   Byte_Offset_O : Natural := 0;
+
+   with package Subs_P is new Sub_Regs (<>);
+   Regs : Subs_P.Array_T;
+
+package HW.MMIO_Regs
+is
+
+   Byte_Offset : Natural := Byte_Offset_O;
+
+   ----------------------------------------------------------------------------
+
+   procedure Read (Value : out Word8; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word8'Size;
+
+   procedure Read (Value : out Word16; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word16'Size;
+
+   procedure Read (Value : out Word32; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word32'Size;
+
+   procedure Read (Value : out Word64; Idx : Subs_P.Index_T)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Word64'Size;
+
+   ----------------------------------------------------------------------------
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word8)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word16)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word32)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+   procedure Write (Idx : Subs_P.Index_T; Value : Word64)
+   with
+      Pre =>   ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) >= Integer (Range_P.Index_T'First) and
+               ((Byte_Offset + Regs (Idx).Byte_Offset) /
+                (Range_P.Element_T'Size / 8)) <= Integer (Range_P.Index_T'Last) and
+               Range_P.Element_T'Size <= Word64'Size and
+               Regs (Idx).MSB < Range_P.Element_T'Size and
+               Regs (Idx).MSB >= Regs (Idx).LSB and
+               Regs (Idx).MSB - Regs (Idx).LSB + 1 <= Value'Size and
+               Word64 (Value) < Word64 (2 ** (Regs (Idx).MSB + 1 - Regs (Idx).LSB));
+
+end HW.MMIO_Regs;
diff --git a/common/hw-port_io.adb b/common/hw-port_io.adb
new file mode 100644
index 0000000..e8adfc2
--- /dev/null
+++ b/common/hw-port_io.adb
@@ -0,0 +1,71 @@
+--
+-- 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.
+--
+
+with System;
+with System.Machine_Code;
+
+package body HW.Port_IO
+with
+   Refined_State  => (State => null),
+   SPARK_Mode     => Off
+is
+
+   generic
+      type Word is private;
+   procedure Port_In (Value : out Word; Port : Port_Type);
+
+   procedure Port_In (Value : out Word; Port : Port_Type) is
+   begin
+      System.Machine_Code.Asm
+        ("in %1, %0",
+         Inputs   => (Port_Type'Asm_Input ("Nd", Port)),
+         Outputs  => (Word'Asm_Output ("=a", Value)),
+         Volatile => True);
+   end Port_In;
+
+   procedure InB_Body is new Port_In (Word => Word8);
+   procedure InB (Value : out Word8; Port : Port_Type) renames InB_Body;
+
+   procedure InW_Body is new Port_In (Word => Word16);
+   procedure InW (Value : out Word16; Port : Port_Type) renames InW_Body;
+
+   procedure InL_Body is new Port_In (Word => Word32);
+   procedure InL (Value : out Word32; Port : Port_Type) renames InL_Body;
+
+   ----------------------------------------------------------------------------
+
+   generic
+      type Word is private;
+   procedure Port_Out (Port : Port_Type; Value : Word);
+
+   procedure Port_Out (Port : Port_Type; Value : Word) is
+   begin
+      System.Machine_Code.Asm
+        ("out %1, %0",
+         Inputs   => (Port_Type'Asm_Input ("Nd", Port),
+                      Word'Asm_Input ("a", Value)),
+         Volatile => True);
+   end Port_Out;
+
+   procedure OutB_Body is new Port_Out (Word => Word8);
+   procedure OutB (Port : Port_Type; Value : Word8) renames OutB_Body;
+
+   procedure OutW_Body is new Port_Out (Word => Word16);
+   procedure OutW (Port : Port_Type; Value : Word16) renames OutW_Body;
+
+   procedure OutL_Body is new Port_Out (Word => Word32);
+   procedure OutL (Port : Port_Type; Value : Word32) renames OutL_Body;
+
+end HW.Port_IO;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-port_io.ads b/common/hw-port_io.ads
new file mode 100644
index 0000000..a5d0e9e
--- /dev/null
+++ b/common/hw-port_io.ads
@@ -0,0 +1,61 @@
+--
+-- 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;
diff --git a/common/hw-sub_regs.ads b/common/hw-sub_regs.ads
new file mode 100644
index 0000000..ca04c1d
--- /dev/null
+++ b/common/hw-sub_regs.ads
@@ -0,0 +1,26 @@
+--
+-- Copyright (C) 2016 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.
+--
+
+generic
+   type Index_T is (<>);
+package HW.Sub_Regs is
+
+   type T is record
+      Byte_Offset : Natural;
+      MSB    : Natural;
+      LSB   : Natural;
+   end record;
+
+   type Array_T is array (Index_T) of T;
+
+end HW.Sub_Regs;
diff --git a/common/hw-time-timer.ads b/common/hw-time-timer.ads
new file mode 100644
index 0000000..4676815
--- /dev/null
+++ b/common/hw-time-timer.ads
@@ -0,0 +1,41 @@
+--
+-- Copyright (C) 2015-2016 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.
+--
+
+private package HW.Time.Timer
+   with
+      Abstract_State => ((Timer_State with Part_Of => HW.Time.State),
+                         (Abstract_Time with
+                           Part_Of => HW.Time.State,
+                           External => Async_Writers)),
+      Initializes => (Timer_State)
+is
+
+   -- Returns the highest point in time that has definitely passed.
+   function Raw_Value_Min return T
+   with
+      Volatile_Function,
+      Global => (Input => Abstract_Time),
+      Depends => (Raw_Value_Min'Result => Abstract_Time);
+
+   -- Returns the highest point in time that might have been reached yet.
+   function Raw_Value_Max return T
+   with
+      Volatile_Function,
+      Global => (Input => Abstract_Time),
+      Depends => (Raw_Value_Max'Result => Abstract_Time);
+
+   function Hz return T
+   with
+      Global => (Input => Timer_State);
+
+end HW.Time.Timer;
diff --git a/common/hw-time.adb b/common/hw-time.adb
new file mode 100644
index 0000000..3162de1
--- /dev/null
+++ b/common/hw-time.adb
@@ -0,0 +1,105 @@
+--
+-- Copyright (C) 2015-2016 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.
+--
+
+with HW;
+with HW.Time.Timer;
+
+use type HW.Word64;
+
+package body HW.Time
+   with Refined_State => (State => (Timer.Timer_State, Timer.Abstract_Time))
+is
+
+   function Now return T
+   with
+      Refined_Global => (Input => Timer.Abstract_Time)
+   is
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Current;
+   end Now;
+
+   function US_From_Now (US : Natural) return T
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Current : constant T := Timer.Raw_Value_Max;
+   begin
+      return Current + (T (US) * Timer.Hz + 999_999) / 1_000_000;
+   end US_From_Now;
+
+   function MS_From_Now (MS : Natural) return T
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Current : constant T := Timer.Raw_Value_Max;
+   begin
+      return Current + (T (MS) * Timer.Hz + 999) / 1_000;
+   end MS_From_Now;
+
+   function Now_US return Int64
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      MHz : constant T := Timer.Hz / 1_000_000;
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Int64 ((Current and (2 ** 63 - 1)) / (if MHz = 0 then 1 else MHz));
+   end Now_US;
+
+   ----------------------------------------------------------------------------
+
+   procedure Delay_Until (Deadline : T)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time))
+   is
+      Current: T;
+   begin
+      loop
+         Current := Timer.Raw_Value_Min;
+         exit when Current >= Deadline;
+      end loop;
+   end Delay_Until;
+
+   procedure U_Delay (US : Natural)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Deadline : constant T := US_From_Now (US);
+   begin
+      Delay_Until (Deadline);
+   end U_Delay;
+
+   procedure M_Delay (MS : Natural)
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time, Timer.Timer_State))
+   is
+      Deadline : constant T := MS_From_Now (MS);
+   begin
+      Delay_Until (Deadline);
+   end M_Delay;
+
+   ----------------------------------------------------------------------------
+
+   function Timed_Out (Deadline : T) return Boolean
+   with
+      Refined_Global => (Input => (Timer.Abstract_Time))
+   is
+      Current : constant T := Timer.Raw_Value_Min;
+   begin
+      return Current >= Deadline;
+   end Timed_Out;
+
+end HW.Time;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw-time.ads b/common/hw-time.ads
new file mode 100644
index 0000000..743279b
--- /dev/null
+++ b/common/hw-time.ads
@@ -0,0 +1,75 @@
+--
+-- Copyright (C) 2015-2016 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.Time
+   with Abstract_State => (State with External => Async_Writers)
+is
+
+   type T is private;
+
+   function Now return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function US_From_Now (US : Natural) return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function MS_From_Now (MS : Natural) return T
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   function Now_US return Int64
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+   ----------------------------------------------------------------------------
+
+   pragma Warnings
+     (GNATprove, Off, "subprogram ""*Delay*"" has no effect",
+      Reason => "No effect on dataflow but time always passes.");
+
+   -- Delay execution until Deadline has been reached.
+   procedure Delay_Until (Deadline : T)
+   with
+      Global => (Input => State);
+
+   procedure U_Delay (US : Natural)
+   with
+      Global => (Input => State);
+
+   procedure M_Delay (MS : Natural)
+   with
+      Global => (Input => State);
+
+   pragma Warnings
+     (GNATprove, On, "subprogram ""*Delay*"" has no effect");
+
+   ----------------------------------------------------------------------------
+
+   function Timed_Out (Deadline : T) return Boolean
+   with
+      Volatile_Function,
+      Global => (Input => State);
+
+private
+
+   type T is new Word64;
+
+end HW.Time;
+
+--  vim: set ts=8 sts=3 sw=3 et:
diff --git a/common/hw.ads b/common/hw.ads
new file mode 100644
index 0000000..6bfca91
--- /dev/null
+++ b/common/hw.ads
@@ -0,0 +1,58 @@
+--
+-- 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.
+--
+
+with Interfaces;
+
+package HW is
+
+   type Bit is mod 2 ** 1;
+
+   subtype Byte is Interfaces.Unsigned_8;
+   subtype Word8 is Byte;
+   function Shift_Left  (Value : Word8; Amount : Natural) return Word8
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word8; Amount : Natural) return Word8
+      renames Interfaces.Shift_Right;
+
+   subtype Word16 is Interfaces.Unsigned_16;
+   function Shift_Left  (Value : Word16; Amount : Natural) return Word16
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word16; Amount : Natural) return Word16
+      renames Interfaces.Shift_Right;
+
+   subtype Word32 is Interfaces.Unsigned_32;
+   function Shift_Left  (Value : Word32; Amount : Natural) return Word32
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word32; Amount : Natural) return Word32
+      renames Interfaces.Shift_Right;
+
+   subtype Word64 is Interfaces.Unsigned_64;
+   function Shift_Left  (Value : Word64; Amount : Natural) return Word64
+      renames Interfaces.Shift_Left;
+   function Shift_Right (Value : Word64; Amount : Natural) return Word64
+      renames Interfaces.Shift_Right;
+
+   subtype Int8 is Interfaces.Integer_8;
+   subtype Int16 is Interfaces.Integer_16;
+   subtype Int32 is Interfaces.Integer_32;
+   subtype Int64 is Interfaces.Integer_64;
+
+   subtype Pos8 is Interfaces.Integer_8 range 1 .. Interfaces.Integer_8'Last;
+   subtype Pos16 is Interfaces.Integer_16 range 1 .. Interfaces.Integer_16'Last;
+   subtype Pos32 is Interfaces.Integer_32 range 1 .. Interfaces.Integer_32'Last;
+   subtype Pos64 is Interfaces.Integer_64 range 1 .. Interfaces.Integer_64'Last;
+
+   subtype Buffer_Range is Natural range 0 .. Natural'Last - 1;
+   type Buffer is array (Buffer_Range range <>) of Byte;
+
+end HW;