diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013, Galois, Inc.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Galois, Inc. nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/examples/ExampleTypes.hs b/examples/ExampleTypes.hs
new file mode 100644
--- /dev/null
+++ b/examples/ExampleTypes.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module ExampleTypes where
+
+import Ivory.BitData
+
+[bitdata|
+ bitdata SPIBaud :: Bits 3
+   = spi_baud_div_2   as 0
+   | spi_baud_div_4   as 1
+   | spi_baud_div_8   as 2
+   | spi_baud_div_16  as 3
+   | spi_baud_div_32  as 4
+   | spi_baud_div_64  as 5
+   | spi_baud_div_128 as 6
+   | spi_baud_div_256 as 7
+|]
diff --git a/ivory-hw.cabal b/ivory-hw.cabal
new file mode 100644
--- /dev/null
+++ b/ivory-hw.cabal
@@ -0,0 +1,57 @@
+-- Initial ivory-hw.cabal generated by cabal init.  For further
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                ivory-hw
+version:             0.1.0.0
+license:             BSD3
+license-file:        LICENSE
+author:              Galois, Inc.
+maintainer:          jamesjb@galois.com
+copyright:           2013 Galois, Inc.
+synopsis:            Ivory hardware model (STM32F4).
+description:         Hardware model for Ivory.  Currently, the STM32F4 is supported; others may be added.
+homepage:            http://smaccmpilot.org/languages/ivory-introduction.html
+build-type:          Simple
+cabal-version:       >= 1.10
+category:            Language
+build-type:          Simple
+cabal-version:       >=1.10
+data-files: support/ivory_hw_prim.h
+source-repository    this
+  type:     git
+  location: https://github.com/GaloisInc/ivory
+  tag:      hackage-hw-0100
+
+
+library
+  exposed-modules:     Ivory.HW,
+                       Ivory.HW.Reg,
+                       Ivory.HW.BitData,
+                       Ivory.HW.Module,
+                       Ivory.HW.SearchDir
+  other-modules:       Ivory.HW.IOArea,
+                       Ivory.HW.STM32F4,
+                       Ivory.HW.Machine,
+                       Ivory.HW.Prim,
+                       Paths_ivory_hw,
+                       ExampleTypes
+  hs-source-dirs:      src, examples
+  build-depends:       base ==4.6.*,
+                       filepath,
+                       ivory,
+                       ivory-bitdata,
+                       ivory-backend-c
+  default-language:     Haskell2010
+  ghc-options:         -Wall
+
+
+-- executable ivory-hw-example
+--   main-is:             Example.hs
+--   other-modules:       ExampleTypes
+--   hs-source-dirs:      examples
+--   build-depends:       base >= 4.6,
+--                        ivory,
+--                        ivory-backend-c,
+--                        ivory-bitdata,
+--                        ivory-hw
+
diff --git a/src/Ivory/HW.hs b/src/Ivory/HW.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW.hs
@@ -0,0 +1,18 @@
+--
+-- HW.hs --- I/O register access from Ivory.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW (
+  -- * I/O Registers
+  Reg(), IvoryIOReg(), mkReg, readReg, writeReg
+
+  -- * Bit Data I/O registers
+  , BitDataReg(), mkBitDataReg, getReg, setReg, modifyReg
+) where
+
+import Ivory.HW.Reg
+import Ivory.HW.BitData
+import Ivory.HW.Prim
diff --git a/src/Ivory/HW/BitData.hs b/src/Ivory/HW/BitData.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/BitData.hs
@@ -0,0 +1,46 @@
+{-# LANGUAGE FlexibleContexts #-}
+--
+-- BitData.hs --- Linking registers to bitdata.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.BitData where
+
+import Ivory.BitData
+import Ivory.Language
+
+import Ivory.HW.Prim
+import Ivory.HW.Reg
+
+-- | A register associated with a bit data type.
+newtype BitDataReg d = BitDataReg (Reg (BitDataRep d))
+
+-- | Create a bit data register given its address.
+mkBitDataReg :: IvoryIOReg (BitDataRep d) => Integer -> BitDataReg d
+mkBitDataReg = BitDataReg . mkReg
+
+getReg :: (BitData d, IvoryIOReg (BitDataRep d))
+       => BitDataReg d -> Ivory eff d
+getReg (BitDataReg r) = do
+  val <- readReg r
+  return $ fromRep val
+
+-- | Set a register to a value taken from a block of bit
+-- modifications.  The previous value is discarded.
+setReg :: (BitData d, IvoryIOReg (BitDataRep d))
+       => BitDataReg d -> BitDataM d a -> Ivory eff a
+setReg (BitDataReg r) mf = do
+  let (result, val) = runBits 0 mf
+  writeReg r val
+  return result
+
+-- | Modify a register by a set of bit modification actions.
+modifyReg :: (BitData d, IvoryIOReg (BitDataRep d))
+          => BitDataReg d -> BitDataM d a -> Ivory eff a
+modifyReg (BitDataReg r) mf = do
+  val <- readReg r
+  let (result, val') = runBits val mf
+  writeReg r val'
+  return result
diff --git a/src/Ivory/HW/IOArea.hs b/src/Ivory/HW/IOArea.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/IOArea.hs
@@ -0,0 +1,20 @@
+--
+-- IOArea.hs --- Memory area type definition.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.IOArea where
+
+-- | A region of the I/O address space.
+data IOArea = IOArea
+  { ioAreaStart :: Integer
+  , ioAreaEnd   :: Integer
+  } deriving Show
+
+-- | "addrInBounds addr size area" returns True if the address range
+-- "[addr, addr + size)" lies within the bounds of "area".
+addrInBounds :: Integer -> Integer -> IOArea -> Bool
+addrInBounds addr size (IOArea start end) =
+  (size >= 0) && (addr >= start) && (addr + size <= end)
diff --git a/src/Ivory/HW/Machine.hs b/src/Ivory/HW/Machine.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/Machine.hs
@@ -0,0 +1,10 @@
+--
+-- Machine.hs --- Imports the current machine module.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.Machine (ioAreas) where
+
+import Ivory.HW.STM32F4
diff --git a/src/Ivory/HW/Module.hs b/src/Ivory/HW/Module.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/Module.hs
@@ -0,0 +1,15 @@
+--
+-- Module.hs --- Ivory module for 'ivory-hw'.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.Module where
+
+import Ivory.Language
+
+hw_moduledef :: ModuleDef
+hw_moduledef = do
+  inclHeader "ivory_hw_prim.h"
+  sourceDep  "ivory_hw_prim.h"
diff --git a/src/Ivory/HW/Prim.hs b/src/Ivory/HW/Prim.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/Prim.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeOperators #-}
+--
+-- Prim.hs --- I/O register primitives.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.Prim where
+
+import Ivory.Language
+
+class IvoryBits a => IvoryIOReg a where
+  ioRegSize  :: a -> Integer
+  ioRegRead  :: Def ('[Uint32] :-> a)
+  ioRegWrite :: Def ('[Uint32, a] :-> ())
+
+ioRegReadU8 :: Def ('[Uint32] :-> Uint8)
+ioRegReadU8 = importProc "ivory_hw_io_read_u8" "ivory_hw_prim.h"
+
+ioRegWriteU8 :: Def ('[Uint32, Uint8] :-> ())
+ioRegWriteU8 = importProc "ivory_hw_io_write_u8" "ivory_hw_prim.h"
+
+instance IvoryIOReg Uint8 where
+  ioRegSize _  = 1
+  ioRegRead  = ioRegReadU8
+  ioRegWrite = ioRegWriteU8
+
+ioRegReadU16 :: Def ('[Uint32] :-> Uint16)
+ioRegReadU16 = importProc "ivory_hw_io_read_u16" "ivory_hw_prim.h"
+
+ioRegWriteU16 :: Def ('[Uint32, Uint16] :-> ())
+ioRegWriteU16 = importProc "ivory_hw_io_write_u16" "ivory_hw_prim.h"
+
+instance IvoryIOReg Uint16 where
+  ioRegSize _  = 2
+  ioRegRead  = ioRegReadU16
+  ioRegWrite = ioRegWriteU16
+
+ioRegReadU32 :: Def ('[Uint32] :-> Uint32)
+ioRegReadU32 = importProc "ivory_hw_io_read_u32" "ivory_hw_prim.h"
+
+ioRegWriteU32 :: Def ('[Uint32, Uint32] :-> ())
+ioRegWriteU32 = importProc "ivory_hw_io_write_u32" "ivory_hw_prim.h"
+
+instance IvoryIOReg Uint32 where
+  ioRegSize _  = 4
+  ioRegRead  = ioRegReadU32
+  ioRegWrite = ioRegWriteU32
diff --git a/src/Ivory/HW/Reg.hs b/src/Ivory/HW/Reg.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/Reg.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+--
+-- Reg.hs --- I/O register access from Ivory.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.Reg where
+
+import Numeric (showHex)
+import Ivory.Language
+
+import Ivory.HW.IOArea
+import Ivory.HW.Prim
+import Ivory.HW.Machine
+
+-- | An I/O register containing a value of type "t".  Define registers
+-- using the "mkReg" functions.
+data Reg t = Reg Integer
+
+-- | Smart constructor that ensures a register address is in bounds
+-- when created.  This raises an error if the address is invalid.
+mkReg :: forall t. IvoryIOReg t => Integer -> Reg t
+mkReg addr =
+  if (any (addrInBounds addr (ioRegSize (undefined :: t))) ioAreas)
+    then Reg addr
+    else error $ "I/O register out of bounds at address 0x" ++
+                 (showHex addr "")
+
+-- | Read an I/O register, returning an Ivory value.
+readReg :: IvoryIOReg a => Reg a -> Ivory eff a
+readReg (Reg addr) = call ioRegRead (fromIntegral addr)
+
+-- | Write an I/O register from an Ivory value.
+writeReg :: IvoryIOReg a => Reg a -> a -> Ivory eff ()
+writeReg (Reg addr) val = call_ ioRegWrite (fromIntegral addr) val
diff --git a/src/Ivory/HW/STM32F4.hs b/src/Ivory/HW/STM32F4.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/STM32F4.hs
@@ -0,0 +1,27 @@
+--
+-- STM32F4.hs --- Machine definition for the STM32F4.
+--
+-- Copyright (C) 2013, Galois, Inc.
+-- All Rights Reserved.
+--
+
+module Ivory.HW.STM32F4 where
+
+import Ivory.HW.IOArea
+
+-- STM32F4 I/O memory areas.
+ioAPB1, ioAPB2 :: IOArea
+ioAPB1 = IOArea 0x40000000 0x40008000
+ioAPB2 = IOArea 0x40010000 0x40015800
+
+ioAHB1, ioAHB2, ioAHB3 :: IOArea
+ioAHB1 = IOArea 0x40020000 0x40080000
+ioAHB2 = IOArea 0x50000000 0x50060C00
+ioAHB3 = IOArea 0x60000000 0xA0001000
+
+ioCM4 :: IOArea
+ioCM4 = IOArea 0xE0000000 0xE0100000
+
+-- | All I/O memory areas for this machine.
+ioAreas :: [IOArea]
+ioAreas = [ioAPB1, ioAPB2, ioAHB1, ioAHB2, ioAHB3, ioCM4]
diff --git a/src/Ivory/HW/SearchDir.hs b/src/Ivory/HW/SearchDir.hs
new file mode 100644
--- /dev/null
+++ b/src/Ivory/HW/SearchDir.hs
@@ -0,0 +1,13 @@
+
+module Ivory.HW.SearchDir where
+
+import System.FilePath
+
+import qualified Paths_ivory_hw
+
+searchDir :: IO FilePath
+searchDir = do
+  base <- Paths_ivory_hw.getDataDir
+  return $ base </> "support"
+
+
diff --git a/support/ivory_hw_prim.h b/support/ivory_hw_prim.h
new file mode 100644
--- /dev/null
+++ b/support/ivory_hw_prim.h
@@ -0,0 +1,52 @@
+/* -*- Mode: C; indent-tabs-mode: nil; c-basic-offset: 4 -*- */
+/*
+ * ivory_hw_prim.h --- Ivory HW primitives for I/O register access.
+ *
+ * Copyright (C) 2013, Galois, Inc.
+ * All Rights Reserved.
+ */
+
+#ifndef __SMACCMPILOT_IVORY_HW_PRIM_H__
+#define __SMACCMPILOT_IVORY_HW_PRIM_H__
+
+#include <stdint.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+static inline uint8_t ivory_hw_io_read_u8(uint32_t addr)
+{
+    return *((volatile uint8_t *)addr);
+}
+
+static inline void ivory_hw_io_write_u8(uint32_t addr, uint8_t value)
+{
+    *((volatile uint8_t *)addr) = value;
+}
+
+static inline uint16_t ivory_hw_io_read_u16(uint32_t addr)
+{
+    return *((volatile uint16_t *)addr);
+}
+
+static inline void ivory_hw_io_write_u16(uint32_t addr, uint16_t value)
+{
+    *((volatile uint16_t *)addr) = value;
+}
+
+static inline uint32_t ivory_hw_io_read_u32(uint32_t addr)
+{
+    return *((volatile uint32_t *)addr);
+}
+
+static inline void ivory_hw_io_write_u32(uint32_t addr, uint32_t value)
+{
+    *((volatile uint32_t *)addr) = value;
+}
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif  /* !defined __SMACCMPILOT_IVORY_HW_PRIM_H__ */