diff --git a/INSTALL b/INSTALL
new file mode 100644
--- /dev/null
+++ b/INSTALL
@@ -0,0 +1,5 @@
+Install the package by running:
+
+  runghc Setup configure
+  runghc Setup build
+  runghc Setup install
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright Koen Claessen 2008
+
+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 Koen Claessen 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/Lava2000.hs b/Lava2000.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000.hs
@@ -0,0 +1,36 @@
+module Lava2000
+  ( module Lava2000.Signal
+  , module Lava2000.Generic
+  , module Lava2000.Operators
+  , module Lava2000.Combinational
+  , module Lava2000.Sequential
+  , module Lava2000.SequentialConstructive
+  , module Lava2000.ConstructiveAnalysis
+  , module Lava2000.Test
+  , module Lava2000.Verification
+  , module Lava2000.Vis
+  , module Lava2000.Fixit
+  , module Lava2000.Smv
+  , module Lava2000.Satzoo
+  , module Lava2000.Property
+  , module Lava2000.Retime
+  , module Lava2000.Vhdl
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Generic
+import Lava2000.Operators
+import Lava2000.Combinational
+import Lava2000.Sequential
+import Lava2000.SequentialConstructive
+import Lava2000.ConstructiveAnalysis
+import Lava2000.Test
+import Lava2000.Verification
+import Lava2000.Vis
+import Lava2000.Fixit
+import Lava2000.Smv
+import Lava2000.Satzoo
+import Lava2000.Property
+import Lava2000.Retime
+import Lava2000.Vhdl
diff --git a/Lava2000/Arithmetic.hs b/Lava2000/Arithmetic.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Arithmetic.hs
@@ -0,0 +1,66 @@
+module Lava2000.Arithmetic where
+
+import Lava2000
+import Lava2000.Patterns
+
+----------------------------------------------------------------
+-- Basic Components
+
+halfAdd (a, b) = (sum, carry)
+  where
+    sum   = xor2 (a, b)
+    carry = and2 (a, b)
+
+fullAdd (carryIn, (a, b)) = (sum, carryOut)
+  where
+    (sum1, carry1) = halfAdd (a, b)
+    (sum, carry2)  = halfAdd (carryIn, sum1)
+    carryOut       = xor2 (carry1, carry2)
+
+bitAdder = row halfAdd
+
+adder (carryIn, ([],   []))   = ([], carryIn)
+adder (carryIn, (as,   []))   = bitAdder (carryIn, as)
+adder (carryIn, ([],   bs))   = bitAdder (carryIn, bs)
+adder (carryIn, (a:as, b:bs)) = (s:ss, carryOut)
+  where
+    (s, carry)     = fullAdd (carryIn, (a, b))
+    (ss, carryOut) = adder (carry, (as, bs))
+
+binAdder (as, bs) = sum ++ [carryOut]
+  where
+    (sum, carryOut) = adder (low, (as, bs))
+
+bitMulti (a, bs) = [ and2 (a, b) | b <- bs ]
+
+multi ([],   []) = []
+multi (as,   []) = replicate (length as) low
+multi ([],   bs) = replicate (length bs) low
+multi (a:as, bs) = m : ms
+  where
+    (m:abs) = bitMulti (a, bs)
+    asbs    = multi (as, bs)
+    (ms,_)  = adder (low, (abs, asbs))
+
+numBreak num = (bit, num')
+  where
+    digit = imod (num, 2)
+    bit   = int2bit digit
+    num'  = idiv (num, 2)
+
+int2bin 0 num = []
+int2bin n num = (bit:bits)
+  where
+    (bit,num') = numBreak num
+    bits       = int2bin (n-1) num'
+
+bin2int []     = 0
+bin2int (b:bs) = num
+  where
+    num' = bin2int bs
+    num  = bit2int b + 2 * num'
+
+----------------------------------------------------------------
+-- the end.
+
+
diff --git a/Lava2000/Captain.hs b/Lava2000/Captain.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Captain.hs
@@ -0,0 +1,151 @@
+module Lava2000.Captain
+  ( captain
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import System.IO
+import System.IO.Unsafe
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- captain
+
+captain :: Checkable a => a -> IO ProofResult
+captain a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cpt"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do handle <- openFile file WriteMode
+     var <- newIORef 0
+
+     hPutStr handle $ unlines $
+       [ "// Generated by Lava 2000"
+       , ""
+       , "definitions:"
+       , ""
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1; v = "w" ++ show n'
+              writeIORef var n'
+              return v
+
+         define v s =
+           case s of
+             Bool True     -> op0 "TRUE"
+             Bool False    -> op0 "FALSE"
+             Inv x         -> op1 "~" x
+
+             And []        -> define v (Bool True)
+             And [x]       -> op0 x
+             And xs        -> opl "&" xs
+
+             Or  []        -> define v (Bool False)
+             Or  [x]       -> op0 x
+             Or  xs        -> opl "#" xs
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> op0 (xor xs)
+
+             VarBool s     -> op0 s
+             DelayBool x y -> delay x y
+
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+            w i = v ++ "_" ++ show i
+
+            op0 s =
+              hPutStr handle $ "  " ++ v ++ " := " ++ s ++ ".\n"
+
+            op1 op s =
+              op0 (op ++ s)
+
+            opl op xs =
+              op0 (concat (intersperse (" " ++ op ++ " ") xs))
+
+            xor [x]    = x
+            xor [x,y]  = "~(" ++ x ++ " <-> " ++ y ++ ")"
+            xor (x:xs) = "(" ++ x ++ " & ~("
+                      ++ concat (intersperse " # " xs)
+                      ++ ") # (~" ++ x ++ " & " ++ xor xs ++ "))"
+
+            delay x y = wrong DelayEval
+
+     outvs <- netlistIO new define (struct props)
+     hPutStr handle $ unlines $
+       [ ""
+       , "prove:"
+       , ""
+       ] ++
+       [ "  " ++ w ++ "."
+       | w <- flatten outvs
+       ]
+
+     hClose handle
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Captain Prove: "
+     before
+     putStr "... "
+     putStrLn "(Written file)"
+     {-
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/smv.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+     -}
+     return Indeterminate
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Combinational.hs b/Lava2000/Combinational.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Combinational.hs
@@ -0,0 +1,39 @@
+module Lava2000.Combinational where
+
+import Lava2000.Ref
+import Lava2000.Generic
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Sequent
+import Lava2000.Error
+
+import Lava2000.MyST
+  ( ST
+  , STRef
+  , newSTRef
+  , readSTRef
+  , writeSTRef
+  , runST
+  )
+
+----------------------------------------------------------------
+-- simulate
+
+simulate :: Generic b => (a -> b) -> a -> b
+simulate circ inp = runST (
+  do sr <- netlistST new define (struct (circ inp))
+     sa <- mmap (fmap symbol . readSTRef) sr
+     let res = construct sa
+     return res
+  )
+ where
+  new =
+    newSTRef (wrong Lava2000.Error.CombinationalLoop)
+
+  define r s =
+    do s' <- mmap readSTRef s
+       writeSTRef r (eval s')
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/ConstructiveAnalysis.hs b/Lava2000/ConstructiveAnalysis.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/ConstructiveAnalysis.hs
@@ -0,0 +1,113 @@
+module Lava2000.ConstructiveAnalysis where
+
+import Lava2000.Signal
+import Lava2000.Operators
+import Lava2000.Error
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Ref
+
+import Lava2000.MyST
+  ( STRef
+  , newSTRef
+  , readSTRef
+  , writeSTRef
+  , runST
+  , fixST
+  , unsafeInterleaveST
+  )
+
+import List
+  ( isPrefixOf
+  )
+
+----------------------------------------------------------------
+-- constructive analysis
+
+constructive :: (Generic a, Generic b) => (a -> b) -> (a -> Signal Bool)
+constructive circ inp =
+  runST
+  ( do defined <- newSTRef []
+       table   <- tableST
+
+       let gather (Symbol sym) =
+             do ms <- findST table sym
+                case ms of
+                  Just s  -> do return s
+                  Nothing -> fixST (\s ->
+                                do extendST table sym s
+                                   ss <- mmap (unsafeInterleaveST . gather) (deref sym)
+                                   define ss
+                             )
+
+           define (Bool b) =
+             do return (bool b, bool (not b))
+
+           define (DelayBool ~(inipos,inineg) ~(nextpos,nextneg)) =
+             do return (respos, inv respos)
+            where
+             respos = delay inipos nextpos
+
+           define (VarBool s) =
+             do return (respos, inv respos)
+            where
+             respos
+               | tag `isPrefixOf` s = Signal (pickSymbol (drop (length tag) s) inp)
+               | otherwise          = var s
+
+           define (Inv ~(xpos,xneg)) =
+             do result ( andl [xneg]
+                       , orl  [xpos]
+                       )
+
+           define (And xs) =
+             do result ( andl [ xpos | (xpos,_) <- xs ]
+                       , orl  [ xneg | (_,xneg) <- xs ]
+                       )
+
+           define (Or xs) =
+             do result ( orl  [ xpos | (xpos,_) <- xs ]
+                       , andl [ xneg | (_,xneg) <- xs ]
+                       )
+
+           define (Xor xs) =
+             do result ( xorpos xs
+                       , xorneg xs
+                       )
+            where
+             xorpos []               = low
+             xorpos [(xpos,xneg)]    = xpos
+             xorpos ((xpos,xneg):xs) =
+               or2 ( andl (xpos : [ xneg | (_,xneg) <- xs ])
+                   , andl [ xneg, xorpos xs ]
+                   )
+
+             xorneg xs =
+               or2 ( andl [ xneg | (_,xneg) <- xs ]
+                   , orl  [ and2 (xpos,ypos)
+                          | (xpos,ypos) <- pairs [ xpos | (_,xpos) <- xs ]
+                          ]
+                   )
+
+             pairs []     = []
+             pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+           define s =
+             do wrong NoArithmetic
+
+           result (xpos,xneg) =
+             do defs <- readSTRef defined
+                writeSTRef defined ((xpos <#> xneg) : defs)
+                return (xpos,xneg)
+
+        in mmap gather (struct (circ (symbolize tag inp)))
+
+       defs <- readSTRef defined
+       return (andl defs)
+  )
+ where
+  tag = "#constr#"
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Eprover.hs b/Lava2000/Eprover.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Eprover.hs
@@ -0,0 +1,154 @@
+module Lava2000.Eprover
+  ( eprover
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStrLn
+  , hClose
+  , try
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- eprover
+
+eprover :: Checkable a => a -> IO ProofResult
+eprover a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.tptp"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do han <- openFile file WriteMode
+     hPutStrLn han "% Generated by Lava2000\n"
+     hPutStrLn han "% definitions:\n"
+     ref <- newIORef (2 :: Int)
+
+     let clause kind xs =
+           hPutStrLn han $ unlines $
+             [ "input_clause(name," ++ kind ++ ",["
+             , concat (intersperse ", " xs)
+             , "])."
+             ]
+
+         new =
+           do n <- readIORef ref
+              let n' = n+1
+              n' `seq` writeIORef ref n'
+              return ("*" ++ show n')
+
+         define v s =
+           do definition v $
+                case s of
+                  Bool True  -> int 1
+                  Bool False -> int 0
+                  VarBool s  -> op2 "mod" s (int 2)
+                  Inv x      -> op1 "inv" x
+
+                  And xs     -> opl (int 1) "and" xs
+                  Or  xs     -> opl (int 0) "or" xs
+                  Xor xs     -> xor xs
+
+                  Int n      -> int n
+                  Neg x      -> op1 "neg" x
+                  Div x y    -> op2 "div" x y
+                  Mod x y    -> op2 "mod" x y
+                  Plus xs    -> opl (int 0) "add" xs
+                  Times xs   -> opl (int 1) "mul" xs
+                  Gte x y    -> op2 "gte" x y
+                  If x y z   -> op3 "if" x y z
+                  VarInt s   -> s
+
+                  Equal []     -> int 1
+                  Equal (x:xs) -> opl (int 1) "and" [op2 "eq" x y | y <- xs]
+
+                  DelayBool x y -> wrong Lava2000.Error.DelayEval
+                  DelayInt  x y -> wrong Lava2000.Error.DelayEval
+           where
+            definition v s =
+              clause "axiom" [ "++equal(" ++ v ++ ":" ++ s ++ "," ++ v ++ ")" ]
+
+            op1 f x     = f ++ "(" ++ x ++ ")"
+            op2 f x y   = f ++ "(" ++ x ++ "," ++ y ++ ")"
+            op3 f x y z = f ++ "(" ++ x ++ "," ++ y ++ "," ++ z ++ ")"
+
+            opl z f []     = z
+            opl z f [x]    = x
+            opl z f (x:xs) = op2 f x (opl z f xs)
+
+            int n = opl "cZero" "add" (replicate n "cOne")
+
+            xor []     = int 0
+            xor [x]    = x
+            xor [x,y]  = op2 "xor" x y
+            xor (x:xs) = op2 "or" (op2 "and" x (op1 "inv" (opl (int 0) "or" xs)))
+                                  (op2 "and" (op1 "inv" x) (xor xs))
+
+     outvs <- netlistIO new define (struct props)
+     hPutStrLn han "% conjecture:\n"
+     clause "conjecture" [ "--truth(" ++ v ++ ")" | v <- flatten outvs ]
+     hClose han
+
+     try (do readFile theoryFile
+             system ("cat " ++ theoryFile ++ " >> " ++ file))
+
+     return ()
+ where
+  theoryFile = "theory.tptp"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Eprover: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/eprover.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Error.hs b/Lava2000/Error.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Error.hs
@@ -0,0 +1,47 @@
+module Lava2000.Error
+  ( Error(..)
+  , wrong
+  )
+ where
+
+----------------------------------------------------------------
+-- Error
+
+data Error
+  = DelayEval
+  | VarEval
+  | CombinationalLoop
+  | BadCombinationalLoop
+  | UndefinedWire
+  | IncompatibleStructures
+  | NoEquality
+  | NoArithmetic
+  | EnumOnSymbols
+
+  | Internal_OptionNotFound
+ deriving (Eq, Show)
+
+wrong :: Error -> a
+wrong err =
+  error $
+    case err of
+      DelayEval              -> "evaluating a delay component"
+      VarEval                -> "evaluating a symbolic value"
+      CombinationalLoop      -> "combinational loop"
+      BadCombinationalLoop   -> "short circuit"
+      UndefinedWire          -> "undriven output"
+      IncompatibleStructures -> "combining incompatible structures"
+      NoEquality             -> "no equality defined for this type"
+      NoArithmetic           -> "arithmetic operations are not supported"
+      EnumOnSymbols          -> "enumerating symbolic values"
+
+      Internal_OptionNotFound -> internal "option not found"
+      _                       -> internal "unknown error"
+
+internal :: String -> String
+internal msg = "INTERNAL ERROR: " ++ msg
+            ++ ".\nPlease report this as a bug to `koen@cs.chalmers.se'."
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Fixit.hs b/Lava2000/Fixit.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Fixit.hs
@@ -0,0 +1,133 @@
+module Lava2000.Fixit
+  ( fixit
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- fixit
+
+fixit :: Checkable a => a -> IO ProofResult
+fixit a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.circ"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do han <- openFile file WriteMode
+     var <- newIORef 0
+     hPutStr han "INTERNALS{low := FALSE;}\n"
+     hPutStr han "INTERNALS{high := TRUE;}\n"
+     hPutStr han "LATCHES{initt := low (high);}\n"
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return ("w" ++ show n')
+
+         define v s =
+           do hPutStr han (def ++ "\n")
+          where
+           def =
+             case s of
+               Bool True     -> prop $ "TRUE"
+               Bool False    -> prop $ "FALSE"
+               Inv x         -> prop $ "~" ++ x
+               And xs        -> prop $ ops "&" xs "TRUE"
+               Or  xs        -> prop $ ops "#" xs "FALSE"
+               Xor xs        -> prop $ xorlist xs
+
+               VarBool s     -> var s
+               DelayBool x y -> latch x y
+               _             -> wrong Lava2000.Error.NoArithmetic
+
+           prop form =
+             "INTERNALS{" ++ v ++ " := " ++ form ++ ";}"
+
+           var s =
+             prop s ++ " PSEUDOS{" ++ s ++ ";}"
+
+           latch x y =
+                "LATCHES{" ++ v ++ "_x := " ++ y ++ " (low);}\n"
+             ++ "INTERNALS{" ++ v ++ " := (initt & " ++ x
+             ++ ") # (~initt & " ++ v ++ "_x);}"
+
+           ops op []  nul = nul
+           ops op [x] nul = x
+           ops op xs  nul =
+             "(" ++ concat (intersperse (" " ++ op ++ " ") xs) ++ ")"
+
+           xorlist []     = "FALSE"
+           xorlist [x]    = x
+           xorlist [x,y]  = x ++ " #! " ++ y
+           xorlist (x:xs) = "(" ++ x_not_xs ++ ") # (" ++ not_x_xor_xs ++ ")"
+            where
+             x_not_xs     = x ++ concatMap (" & ~" ++) xs
+             not_x_xor_xs = "~" ++ x ++ " & (" ++ xorlist xs ++ ")"
+
+     ~(Compound vs) <- netlistIO new define (struct props)
+     define "bad" (And [ "~" ++ v | Object v <- vs ])
+     hClose han
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Fixit: "
+     before
+     putStr "... "
+     system ("rm -f " ++ verifyDir ++ "/fixit.lock")
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/fixit.wrapper "
+                ++ file
+                ++ " -showTime -dir=forward -sat=prove"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Generic.hs b/Lava2000/Generic.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Generic.hs
@@ -0,0 +1,420 @@
+module Lava2000.Generic where
+
+import Lava2000.Signal
+import Lava2000.Sequent
+import Lava2000.Error
+
+import Lava2000.LavaRandom
+  ( Rnd
+  , split
+  , next
+  )
+
+import List
+  ( transpose
+  )
+
+----------------------------------------------------------------
+-- Struct
+
+data Struct a
+  = Compound [Struct a]
+  | Object a
+ deriving (Eq, Show)
+
+flatten :: Struct a -> [a]
+flatten (Object a)    = [a]
+flatten (Compound ss) = concatMap flatten ss
+
+transStruct :: Struct [a] -> [Struct a]
+transStruct (Object as)   = map Object as
+transStruct (Compound ss) =
+  map Compound . transpose . map transStruct $ ss
+
+-- structural operations
+
+instance Functor Struct where
+  fmap f (Object a)    = Object (f a)
+  fmap f (Compound xs) = Compound (map (fmap f) xs)
+
+instance Sequent Struct where
+  sequent (Object m) =
+    do a <- m
+       return (Object a)
+
+  sequent (Compound xs) =
+    do as <- sequence [ sequent x | x <- xs ]
+       return (Compound as)
+
+----------------------------------------------------------------
+-- Generic datatypes
+
+class Generic a where
+  struct    :: a -> Struct Symbol
+  construct :: Struct Symbol -> a
+
+instance Generic Symbol where
+  struct    s          = Object s
+  construct (Object s) = s
+
+instance Generic (Signal a) where
+  struct    (Signal s) = Object s
+  construct (Object s) = Signal s
+
+instance Generic () where
+  struct    ()            = Compound []
+  construct (Compound []) = ()
+
+instance Generic a => Generic [a] where
+  struct    xs            = Compound (map struct xs)
+  construct (Compound xs) = map construct xs
+
+instance (Generic a, Generic b) => Generic (a,b) where
+  struct    (a,b)            = Compound [struct a, struct b]
+  construct (Compound [a,b]) = (construct a, construct b)
+
+instance (Generic a, Generic b, Generic c) => Generic (a,b,c) where
+  struct    (a,b,c)            = Compound [struct a, struct b, struct c]
+  construct (Compound [a,b,c]) = (construct a, construct b, construct c)
+
+instance (Generic a, Generic b, Generic c, Generic d) => Generic (a,b,c,d) where
+  struct    (a,b,c,d)            = Compound [struct a, struct b, struct c, struct d]
+  construct (Compound [a,b,c,d]) = (construct a, construct b, construct c, construct d)
+
+instance (Generic a, Generic b, Generic c, Generic d, Generic e) => Generic (a,b,c,d,e) where
+  struct    (a,b,c,d,e)            = Compound [struct a, struct b, struct c, struct d, struct e]
+  construct (Compound [a,b,c,d,e]) = (construct a, construct b, construct c, construct d, construct e)
+
+instance (Generic a, Generic b, Generic c, Generic d, Generic e, Generic f) => Generic (a,b,c,d,e,f) where
+  struct    (a,b,c,d,e,f)            = Compound [struct a, struct b, struct c, struct d, struct e, struct f]
+  construct (Compound [a,b,c,d,e,f]) = (construct a, construct b, construct c, construct d, construct e, construct f)
+
+instance (Generic a, Generic b, Generic c, Generic d, Generic e, Generic f, Generic g) => Generic (a,b,c,d,e,f,g) where
+  struct    (a,b,c,d,e,f,g)            = Compound [struct a, struct b, struct c, struct d, struct e, struct f, struct g]
+  construct (Compound [a,b,c,d,e,f,g]) = (construct a, construct b, construct c, construct d, construct e, construct f, construct g)
+
+----------------------------------------------------------------
+-- Ops
+
+data Ops
+  = Ops { equalSymbol :: Symbol -> Symbol -> Signal Bool
+        , delaySymbol :: Symbol -> Symbol -> Symbol
+        , ifSymbol    :: Signal Bool -> (Symbol, Symbol) -> Symbol
+        , varSymbol   :: String -> Symbol
+        , zeroSymbol  :: Symbol
+        }
+
+opsBool :: Ops
+opsBool =
+  Ops { equalSymbol = \x y     -> equalBool (Signal x) (Signal y)
+      , delaySymbol = \x y     -> unSignal $ delayBool (Signal x) (Signal y)
+      , ifSymbol    = \c (x,y) -> unSignal $ ifBool c  (Signal x,  Signal y)
+      , varSymbol   = \s       -> symbol (VarBool s)
+      , zeroSymbol  =             symbol (Bool False)
+      }
+
+opsInt :: Ops
+opsInt =
+  Ops { equalSymbol = \x y     -> equalInt (Signal x) (Signal y)
+      , delaySymbol = \x y     -> unSignal $ delayInt (Signal x) (Signal y)
+      , ifSymbol    = \c (x,y) -> unSignal $ ifInt c  (Signal x,  Signal y)
+      , varSymbol   = \s       -> symbol (VarInt s)
+      , zeroSymbol  =             symbol (Int 0)
+      }
+
+unSignal :: Signal a -> Symbol
+unSignal (Signal s) = s
+
+ops :: Symbol -> Ops
+ops s =
+  case unsymbol s of
+    Bool b         -> opsBool
+    Inv s          -> opsBool
+    And xs         -> opsBool
+    Or xs          -> opsBool
+    Xor xs         -> opsBool
+
+    Int n          -> opsInt
+    Neg s          -> opsInt
+    Div s1 s2      -> opsInt
+    Mod s1 s2      -> opsInt
+    Plus xs        -> opsInt
+    Times xs       -> opsInt
+    Gte x y        -> opsBool
+    Equal xs       -> opsBool
+    If x y z       -> opsInt
+
+    DelayBool s s' -> opsBool
+    DelayInt  s s' -> opsInt
+    VarBool s      -> opsBool
+    VarInt  s      -> opsInt
+
+----------------------------------------------------------------
+-- generic definitions
+
+equal :: Generic a => (a, a) -> Signal Bool
+equal (x, y) = eq (struct x) (struct y)
+ where
+  eq (Object a)    (Object b)    = equalSymbol (ops a) a b
+  eq (Compound as) (Compound bs) = eqs as bs
+  eq _             _             = low
+
+  eqs []     []     = high
+  eqs (a:as) (b:bs) = andl [eq a b, eqs as bs]
+  eqs _      _      = low
+
+delay :: Generic a => a -> a -> a
+delay x y = construct (del (struct x) (struct y))
+ where
+  del (Object a)    ~(Object b)    = Object (delaySymbol (ops a) a b)
+  del (Compound as) ~(Compound bs) = Compound (lazyZipWith del as bs)
+  del _             _              = wrong Lava2000.Error.IncompatibleStructures
+
+zeroify :: Generic a => a -> a
+zeroify x = construct (zero (struct x))
+ where
+  zero (Object a)    = Object (zeroSymbol (ops a))
+  zero (Compound as) = Compound [ zero a | a <- as ]
+
+symbolize :: Generic a => String -> a -> a
+symbolize s x = construct (sym s (struct x))
+ where
+  sym s (Object a)    = Object (varSymbol (ops a) s)
+  sym s (Compound as) = Compound [ sym (s ++ "_" ++ show i) a
+                                 | (a,i) <- as `zip` [0..]
+                                 ]
+
+pickSymbol :: Generic a => String -> a -> Symbol
+pickSymbol s a = pick (numbers s) (struct a)
+ where
+  pick _      (Object a)    = a
+  pick (n:ns) (Compound as) = pick ns (as !! n)
+
+  numbers ('_':s) = read s1 : numbers s2
+   where
+    s1 = takeWhile (/= '_') s
+    s2 = dropWhile (/= '_') s
+
+----------------------------------------------------------------
+-- Constructive
+
+class ConstructiveSig a where
+  zeroSig   :: Signal a
+  varSig    :: String -> Signal a
+  randomSig :: Rnd -> Signal a
+
+class Generic a => Constructive a where
+  zero   :: a
+  var    :: String -> a
+  random :: Rnd -> a
+
+zeroList :: Constructive a => Int -> [a]
+zeroList n = replicate n zero
+
+varList :: Constructive a => Int -> String -> [a]
+varList n s = [ var (s ++ "_" ++ show i) | i <- [0..(n-1)] ]
+
+randomList :: Constructive a => Int -> Rnd -> [a]
+randomList n rnd = take n [ random rnd' | rnd' <- splitRndList rnd ]
+
+splitRndList :: Rnd -> [Rnd]
+splitRndList rnd = rnd1 : splitRndList rnd2 where (rnd1, rnd2) = split rnd
+
+valRnd :: Rnd -> Int
+valRnd rnd = i where (i, _) = next rnd
+
+-- instances
+
+instance ConstructiveSig Bool where
+  zeroSig       = low
+  varSig        = varBool
+  randomSig rnd = looping (take n [ bit rnd' | rnd' <- splitRndList rnd2 ])
+   where
+    (rnd1,rnd2) = split rnd
+    n           = 30 + (valRnd rnd1 `mod` 10)
+    bit rnd     = bool (even (valRnd rnd))
+    looping xs  = out where out = foldr delay out xs
+
+instance ConstructiveSig Int where
+  zeroSig     = int 0
+  varSig      = varInt
+  randomSig rnd = looping (take n [ num rnd' | rnd' <- splitRndList rnd2 ])
+   where
+    (rnd1,rnd2) = split rnd
+    n           = 30 + (valRnd rnd1 `mod` 10)
+    num rnd     = int (20 + (valRnd rnd `mod` 20))
+    looping xs  = out where out = foldr delay out xs
+
+instance ConstructiveSig a => Constructive (Signal a) where
+  zero   = zeroSig
+  var    = varSig
+  random = randomSig
+
+instance Constructive () where
+  zero       = ()
+  var s      = ()
+  random rnd = ()
+
+instance (Constructive a, Constructive b)
+      => Constructive (a, b) where
+  zero       = (zero, zero)
+  var s      = (var (s ++ "_1"), var (s ++ "_2"))
+  random rnd = (random rnd1, random rnd2)
+   where (rnd1, rnd2) = split rnd
+
+instance (Constructive a, Constructive b, Constructive c)
+      => Constructive (a, b, c) where
+  zero     = (zero, zero, zero)
+  var s    = (var (s ++ "_1"), var (s ++ "_2"), var (s ++ "_3"))
+  random rnd = (random rnd1, random rnd2, random rnd3)
+   where (rnd1: rnd2 : rnd3 : _) = splitRndList rnd
+
+instance (Constructive a, Constructive b, Constructive c, Constructive d)
+      => Constructive (a, b, c, d) where
+  zero     = (zero, zero, zero, zero)
+  var s    = (var (s ++ "_1"), var (s ++ "_2"), var (s ++ "_3"), var (s ++ "_4"))
+  random rnd = (random rnd1, random rnd2, random rnd3, random rnd4)
+   where (rnd1: rnd2 : rnd3 : rnd4 : _) = splitRndList rnd
+
+instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e)
+      => Constructive (a, b, c, d, e) where
+  zero     = (zero, zero, zero, zero, zero)
+  var s    = (var (s ++ "_1"), var (s ++ "_2"), var (s ++ "_3"), var (s ++ "_4"), var (s ++ "_5"))
+  random rnd = (random rnd1, random rnd2, random rnd3, random rnd4, random rnd5)
+   where (rnd1: rnd2 : rnd3 : rnd4 : rnd5 : _) = splitRndList rnd
+
+instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e, Constructive f)
+      => Constructive (a, b, c, d, e, f) where
+  zero     = (zero, zero, zero, zero, zero, zero)
+  var s    = (var (s ++ "_1"), var (s ++ "_2"), var (s ++ "_3"), var (s ++ "_4"), var (s ++ "_5"), var (s ++ "_6"))
+  random rnd = (random rnd1, random rnd2, random rnd3, random rnd4, random rnd5, random rnd6)
+   where (rnd1: rnd2 : rnd3 : rnd4 : rnd5 : rnd6 : _) = splitRndList rnd
+
+instance (Constructive a, Constructive b, Constructive c, Constructive d, Constructive e, Constructive f, Constructive g)
+      => Constructive (a, b, c, d, e, f, g) where
+  zero     = (zero, zero, zero, zero, zero, zero, zero)
+  var s    = (var (s ++ "_1"), var (s ++ "_2"), var (s ++ "_3"), var (s ++ "_4"), var (s ++ "_5"), var (s ++ "_6"), var (s ++ "_7"))
+  random rnd = (random rnd1, random rnd2, random rnd3, random rnd4, random rnd5, random rnd6, random rnd7)
+   where (rnd1: rnd2 : rnd3 : rnd4 : rnd5 : rnd6 : rnd7 : _) = splitRndList rnd
+
+----------------------------------------------------------------
+-- Finite
+
+class ConstructiveSig a => FiniteSig a where
+  domainSig :: [Signal a]
+
+class Constructive a => Finite a where
+  domain :: [a]
+
+domainList :: Finite a => Int -> [[a]]
+domainList 0 = [[]]
+domainList n = [ a:as | a <- domain, as <- domainList (n-1) ]
+
+-- instances
+
+instance FiniteSig Bool where
+  domainSig = [low, high]
+
+instance FiniteSig a => Finite (Signal a) where
+  domain = domainSig
+
+instance Finite () where
+  domain = [ () ]
+
+instance (Finite a, Finite b)
+      => Finite (a, b) where
+  domain = [ (a,b) | a <- domain, b <- domain ]
+
+instance (Finite a, Finite b, Finite c)
+      => Finite (a, b, c) where
+  domain = [ (a,b,c) | a <- domain, b <- domain, c <- domain ]
+
+instance (Finite a, Finite b, Finite c, Finite d)
+      => Finite (a, b, c, d) where
+  domain = [ (a,b,c,d) | a <- domain, b <- domain, c <- domain, d <- domain ]
+
+instance (Finite a, Finite b, Finite c, Finite d, Finite e)
+      => Finite (a, b, c, d, e) where
+  domain = [ (a,b,c,d,e) | a <- domain, b <- domain, c <- domain, d <- domain, e <- domain ]
+
+instance (Finite a, Finite b, Finite c, Finite d, Finite e, Finite f)
+      => Finite (a, b, c, d, e, f) where
+  domain = [ (a,b,c,d,e,f) | a <- domain, b <- domain, c <- domain, d <- domain, e <- domain, f <- domain ]
+
+instance (Finite a, Finite b, Finite c, Finite d, Finite e, Finite f, Finite g)
+      => Finite (a, b, c, d, e, f, g) where
+  domain = [ (a,b,c,d,e,f,g) | a <- domain, b <- domain, c <- domain, d <- domain, e <- domain, f <- domain, g <- domain ]
+
+----------------------------------------------------------------
+-- Choice
+
+class Choice a where
+  ifThenElse :: Signal Bool -> (a, a) -> a
+
+-- instances
+
+instance Choice Symbol where
+  ifThenElse cond (x, y) = ifSymbol (ops x) cond (x, y)
+
+instance Choice (Signal a) where
+  ifThenElse cond (Signal x, Signal y) =
+    Signal (ifThenElse cond (x, y))
+
+instance Choice () where
+  ifThenElse cond (_, _) = ()
+
+instance Choice a => Choice [a] where
+  ifThenElse cond (xs, ys) =
+    strongZipWith (curry (ifThenElse cond)) xs ys
+
+instance (Choice a, Choice b) => Choice (a,b) where
+  ifThenElse cond ((x1,x2),(y1,y2)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2))
+
+instance (Choice a, Choice b, Choice c) => Choice (a,b,c) where
+  ifThenElse cond ((x1,x2,x3),(y1,y2,y3)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2), ifThenElse cond (x3,y3))
+
+instance (Choice a, Choice b, Choice c, Choice d) => Choice (a,b,c,d) where
+  ifThenElse cond ((x1,x2,x3,x4),(y1,y2,y3,y4)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2), ifThenElse cond (x3,y3), ifThenElse cond (x4,y4))
+
+instance (Choice a, Choice b, Choice c, Choice d, Choice e) => Choice (a,b,c,d,e) where
+  ifThenElse cond ((x1,x2,x3,x4,x5),(y1,y2,y3,y4,y5)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2), ifThenElse cond (x3,y3), ifThenElse cond (x4,y4), ifThenElse cond (x5,y5))
+
+instance (Choice a, Choice b, Choice c, Choice d, Choice e, Choice f) => Choice (a,b,c,d,e,f) where
+  ifThenElse cond ((x1,x2,x3,x4,x5,x6),(y1,y2,y3,y4,y5,y6)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2), ifThenElse cond (x3,y3), ifThenElse cond (x4,y4), ifThenElse cond (x5,y5),
+     ifThenElse cond (x6,y6))
+
+instance (Choice a, Choice b, Choice c, Choice d, Choice e, Choice f, Choice g) => Choice (a,b,c,d,e,f,g) where
+  ifThenElse cond ((x1,x2,x3,x4,x5,x6,x7),(y1,y2,y3,y4,y5,y6,y7)) =
+    (ifThenElse cond (x1,y1), ifThenElse cond (x2,y2), ifThenElse cond (x3,y3), ifThenElse cond (x4,y4), ifThenElse cond (x5,y5),
+     ifThenElse cond (x6,y6), ifThenElse cond (x7,y7))
+
+instance Choice b => Choice (a -> b) where
+  ifThenElse cond (f, g) =
+    \a -> ifThenElse cond (f a, g a)
+
+mux :: Choice a => (Signal Bool, (a, a)) -> a
+mux (cond, (a, b)) = ifThenElse cond (b, a)
+
+----------------------------------------------------------------
+-- helper functions
+
+strongZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+strongZipWith f (x:xs) (y:ys) = f x y : strongZipWith f xs ys
+strongZipWith f []     []     = []
+strongZipWith f _      _      = wrong Lava2000.Error.IncompatibleStructures
+
+lazyZipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
+lazyZipWith f []     _  = []
+lazyZipWith f (x:xs) ys = f x (safe head ys) : lazyZipWith f xs (safe tail ys)
+ where
+  safe f [] = wrong Lava2000.Error.IncompatibleStructures
+  safe f xs = f xs
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/HeerHugo.hs b/Lava2000/HeerHugo.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/HeerHugo.hs
@@ -0,0 +1,144 @@
+module Lava2000.HeerHugo
+  ( heerhugo
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- heerhugo
+
+heerhugo :: Checkable a => a -> IO ProofResult
+heerhugo a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.hh"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do handle <- openFile file WriteMode
+     var <- newIORef 0
+
+     hPutStr handle $ unlines $
+       [ "% Generated by Lava2000"
+       , ""
+       , "( 1 & ~0 &"
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1; v = "w" ++ show n'
+              writeIORef var n'
+              return v
+
+         define v s =
+           case s of
+             Bool True     -> op0 "1"
+             Bool False    -> op0 "0"
+             Inv x         -> op1 "~" x
+
+             And []        -> define v (Bool True)
+             And [x]       -> op0 x
+             And xs        -> opl "&" xs
+
+             Or  []        -> define v (Bool False)
+             Or  [x]       -> op0 x
+             Or  xs        -> opl "|" xs
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> op0 (xor xs)
+
+             VarBool s     -> op0 s
+             DelayBool x y -> delay x y
+
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+            w i = v ++ "_" ++ show i
+
+            op0 s =
+              hPutStr handle $ "(" ++ v ++ " <-> " ++ s ++ ") &\n"
+
+            op1 op s =
+              op0 (op ++ "(" ++ s ++ ")")
+
+            opl op xs =
+              op0 (concat (intersperse (" " ++ op ++ " ") xs))
+
+            xor [x]    = x
+            xor [x,y]  = "~(" ++ x ++ " <-> " ++ y ++ ")"
+            xor (x:xs) = "(" ++ x ++ " & ~("
+                      ++ concat (intersperse " | " xs)
+                      ++ ") | (~" ++ x ++ " & " ++ xor xs ++ "))"
+
+            delay x y = wrong DelayEval
+
+     outvs <- netlistIO new define (struct props)
+     hPutStr handle $ unlines $
+       [ "~(" ++ concat (intersperse " & " (flatten outvs)) ++ ")"
+       , ")"
+       ]
+
+     hClose handle
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "HeerHugo: "
+     before
+     putStr "... "
+     putStrLn "(Written file)"
+     {-
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/smv.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+     -}
+     return Indeterminate
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/IOBuffering.hs b/Lava2000/IOBuffering.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/IOBuffering.hs
@@ -0,0 +1,10 @@
+module Lava2000.IOBuffering where
+
+import IO
+  ( hSetBuffering
+  , stdout
+  , BufferMode(..)
+  )
+
+noBuffering :: IO ()
+noBuffering = hSetBuffering stdout NoBuffering
diff --git a/Lava2000/Isc.hs b/Lava2000/Isc.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Isc.hs
@@ -0,0 +1,173 @@
+module Lava2000.Isc
+ ( IscMethod(..)
+ , isc
+ , iscWith
+ ) where
+
+import Lava2000.Ref
+import Lava2000.Signal
+import Lava2000.Generic
+
+import Lava2000.Property
+import Lava2000.LavaDir
+import Lava2000.Sequent
+import Lava2000.Netlist
+import Lava2000.Verification
+import Lava2000.IOBuffering
+
+import Array
+import Lava2000.MyST
+import List(intersperse)
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------------------------------------------
+-- options
+
+data IscMethod
+ = StepMin
+ | StepMax
+ | Mixed
+ | Bmc
+
+----------------------------------------------------------------------------------------------------
+-- toplevel proving
+
+isc :: Checkable a => a -> IO ProofResult
+isc = iscWith Mixed 10
+
+iscWith :: Checkable a => IscMethod -> Int -> a -> IO ProofResult
+iscWith m n a =
+  do checkVerifyDir
+     noBuffering
+     net_ netfile a
+     lavadir <- getLavaDir
+--     r <- system (lavadir ++ execute)
+     r <- system (execute)
+     return $ case r of
+       ExitSuccess   -> Valid
+       ExitFailure 1 -> Indeterminate
+       ExitFailure _ -> Falsifiable
+
+ where
+--  execute = "/Scripts/isc "
+  execute = "isc "
+	    ++ netfile ++ " "
+	    ++ (m2par m) ++ " " ++ show n
+  netfile = verifyDir ++ "/circuit.net"
+
+  m2par StepMin = "-smin"
+  m2par StepMax = "-smax"
+  m2par Mixed   = "-mix"
+  m2par Bmc     = "-bmc"
+
+----------------------------------------------------------------------------------------------------
+-- netlist
+
+data Sign a  = Pos a | Not a deriving (Show, Read)
+
+sneg (Pos x) = Not x
+sneg (Not x) = Pos x
+
+type NetList = Array Int (S (Sign Int))
+
+instance Functor Sign where
+  fmap f (Pos x) = Pos (f x)
+  fmap f (Not x) = Not (f x)
+
+
+showS :: S String -> String
+showS (Bool b)     = "Bool " ++ show b
+showS (Or [x,y])   = "Or " ++ "[" ++ x ++ ',' : y ++ "]"
+showS (Xor [x,y])  = "Xor " ++ "[" ++ x ++ ',' : y ++ "]"
+showS (VarBool v)  = "VarBool " ++ show v
+showS (DelayBool x y) = "DelayBool (" ++ x ++ ") (" ++ y ++ ")"
+showS _               = error "showS"
+
+showN :: NetList -> String
+showN = showA . fmap (showS . fmap show)
+
+showA :: Array Int String -> String
+showA a = "array " ++ show (bounds a) ++ " [" ++
+	  concat (intersperse "," (map (\ (i,s) -> "(" ++ show i ++ "," ++ s ++ ")")
+		                         (assocs a)))
+	  ++ "]"
+
+showAll (n,p) = "(" ++ showN n ++ "," ++ show p ++ ")"
+
+net_ :: Checkable a => String -> a -> IO ()
+net_ file a = do
+  p <- net a
+  writeFile file (showAll p)
+
+net :: Checkable a => a -> IO (NetList, Sign Int)
+net a =
+  do (props,_) <- properties a
+     let top = case props of
+                [x] -> x
+		xs  -> andl xs
+     let (tab, Object top') = table (struct top)
+     return (array (0, length tab-1) tab, top')
+
+
+table :: Sequent f => f Symbol -> ([(Int,S (Sign Int))], f (Sign Int))
+table str =
+  runST
+  ( do ref   <- newSTRef 0
+       table <- newSTRef []
+
+       let define sym = do
+             tab <- readSTRef table
+	     case sym of
+	       And xs -> bin Or (map sneg xs) >>= return . sneg
+	       Or xs  -> bin Or xs
+	       Xor xs -> bin Xor xs
+--			    v <- new
+--			    writeSTRef table ((v,x):tab)
+--			    return (Not v)
+	       Inv x  -> return (sneg x)
+	       x      -> do v <- new
+			    writeSTRef table ((v,x):tab)
+			    return (Pos v)
+
+           bin f [x]      = return x
+	   bin f (x:y:xs) = do
+               v <- new
+	       tab <- readSTRef table
+	       writeSTRef table ((v, f [x,y]) : tab)
+	       bin f (Pos v:xs)
+
+           new = do
+	     n <- readSTRef ref
+	     writeSTRef ref (n+1)
+	     return n
+
+       str' <- netlistST_ define str
+       tab  <- readSTRef table
+       return (tab, str')
+  )
+
+netlistST_ :: Sequent f => (S v -> ST s v) -> f Symbol -> ST s (f v)
+netlistST_ define symbols =
+  do tab <- tableST
+
+     let gather (Symbol sym) =
+           do visited <- findST tab sym
+              case visited of
+                Just v  -> do return v
+                Nothing -> fixST $ \v -> do
+                              extendST tab sym v
+                              s <- mmap gather (deref sym)
+                              define s
+
+      in mmap gather symbols
+
+
+{-
+isLow  (Bool False) = True
+isLow  (Inv s)      = isHigh (unsymbol s)
+isLow  _            = False
+isHigh (Bool True)  = True
+isHigh (Inv s)      = isLow (unsymbol s)
+isHigh _            = False
+-}
diff --git a/Lava2000/LavaDir.hs b/Lava2000/LavaDir.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/LavaDir.hs
@@ -0,0 +1,16 @@
+module Lava2000.LavaDir where
+
+import System
+  ( getEnv
+  )
+
+import IO
+  ( try
+  )
+
+getLavaDir :: IO FilePath
+getLavaDir =
+  do ees <- try (getEnv "LAVADIR")
+     return $ case ees of
+                Left _  -> {-INSERT LAVADIR-} "/home/emax/Program/chalmers-lava2000/"
+                Right s -> s
diff --git a/Lava2000/LavaRandom.hs b/Lava2000/LavaRandom.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/LavaRandom.hs
@@ -0,0 +1,18 @@
+module Lava2000.LavaRandom
+  ( Rnd
+  , newRnd
+  , next
+  , split
+  )
+ where
+
+import Random
+  ( StdGen
+  , newStdGen
+  , next
+  , split
+  )
+
+type Rnd = StdGen
+
+newRnd = newStdGen
diff --git a/Lava2000/Limmat.hs b/Lava2000/Limmat.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Limmat.hs
@@ -0,0 +1,150 @@
+module Lava2000.Limmat
+  ( limmat
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- limmat
+
+limmat :: Checkable a => a -> IO ProofResult
+limmat a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cnf"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+     cls <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "c Generated by Lava2000"
+       , "c "
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return n'
+
+         clause xs =
+           do n <- readIORef cls
+              let n' = n+1 in n' `seq` writeIORef cls n'
+              hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n")
+
+         define v s =
+           case s of
+             Bool True     -> clause [ v ]
+             Bool False    -> clause [ -v ]
+             Inv x         -> clause [ -x, -v ] >> clause [ x, v ]
+
+             And []        -> define v (Bool True)
+             And xs        -> conjunction v xs
+
+             Or  []        -> define v (Bool False)
+             Or  xs        -> conjunction (-v) (map negate xs)
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> exactly1 v xs
+
+             VarBool s     -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n")
+
+             DelayBool x y -> wrong Lava2000.Error.DelayEval
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+
+            conjunction v xs =
+              do clause (v : map negate xs)
+                 sequence_ [ clause [ -v, x ] | x <- xs ]
+
+            exactly1 v xs =
+              do clause (-v : xs)
+                 sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ]
+                 sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ]
+
+            pairs []     = []
+            pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+            pick []      = []
+            pick (x:xs)  = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ]
+
+     outvs <- netlistIO new define (struct props)
+     clause (map negate (flatten outvs))
+
+     nvar <- readIORef var
+     ncls <- readIORef cls
+     hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n")
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Limmat: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/limmat.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Modoc.hs b/Lava2000/Modoc.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Modoc.hs
@@ -0,0 +1,150 @@
+module Lava2000.Modoc
+  ( modoc
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- modoc
+
+modoc :: Checkable a => a -> IO ProofResult
+modoc a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cnf"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+     cls <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "c Generated by Lava2000"
+       , "c "
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return n'
+
+         clause xs =
+           do n <- readIORef cls
+              let n' = n+1 in n' `seq` writeIORef cls n'
+              hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n")
+
+         define v s =
+           case s of
+             Bool True     -> clause [ v ]
+             Bool False    -> clause [ -v ]
+             Inv x         -> clause [ -x, -v ] >> clause [ x, v ]
+
+             And []        -> define v (Bool True)
+             And xs        -> conjunction v xs
+
+             Or  []        -> define v (Bool False)
+             Or  xs        -> conjunction (-v) (map negate xs)
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> exactly1 v xs
+
+             VarBool s     -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n")
+
+             DelayBool x y -> wrong Lava2000.Error.DelayEval
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+
+            conjunction v xs =
+              do clause (v : map negate xs)
+                 sequence_ [ clause [ -v, x ] | x <- xs ]
+
+            exactly1 v xs =
+              do clause (-v : xs)
+                 sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ]
+                 sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ]
+
+            pairs []     = []
+            pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+            pick []      = []
+            pick (x:xs)  = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ]
+
+     outvs <- netlistIO new define (struct props)
+     clause (map negate (flatten outvs))
+
+     nvar <- readIORef var
+     ncls <- readIORef cls
+     hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n")
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Modoc: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/modoc.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/MyST.hs b/Lava2000/MyST.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/MyST.hs
@@ -0,0 +1,62 @@
+module Lava2000.MyST
+  ( ST
+  , STRef
+  , newSTRef
+  , readSTRef
+  , writeSTRef
+  , runST
+  , fixST
+
+  , unsafePerformST
+  , unsafeInterleaveST
+  , unsafeIOtoST
+  )
+ where
+
+import System.IO
+import System.IO.Unsafe
+import Data.IORef
+
+newtype ST s a
+  = ST (IO a)
+
+unST :: ST s a -> IO a
+unST (ST io) = io
+
+instance Functor (ST s) where
+  fmap f (ST io) = ST (fmap f io)
+
+instance Monad (ST s) where
+  return a    = ST (return a)
+  ST io >>= k = ST (do a <- io ; unST (k a))
+
+newtype STRef s a
+  = STRef (IORef a)
+
+instance Eq (STRef s a) where
+  STRef r1 == STRef r2 = r1 == r2
+
+newSTRef :: a -> ST s (STRef s a)
+newSTRef a = ST (STRef `fmap` newIORef a)
+
+readSTRef :: STRef s a -> ST s a
+readSTRef (STRef r) = ST (readIORef r)
+
+writeSTRef :: STRef s a -> a -> ST s ()
+writeSTRef (STRef r) a = ST (writeIORef r a)
+
+runST :: (forall s . ST s a) -> a
+runST st = unsafePerformST st
+
+fixST :: (a -> ST s a) -> ST s a
+fixST f = ST (fixIO (unST . f))
+
+unsafePerformST :: ST s a -> a
+unsafePerformST (ST io) = unsafePerformIO io
+
+unsafeInterleaveST :: ST s a -> ST s a
+unsafeInterleaveST (ST io) = ST (unsafeInterleaveIO io)
+
+unsafeIOtoST :: IO a -> ST s a
+unsafeIOtoST = ST
+
diff --git a/Lava2000/Netlist.hs b/Lava2000/Netlist.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Netlist.hs
@@ -0,0 +1,60 @@
+module Lava2000.Netlist
+  ( netlist
+  , netlistIO
+  , netlistST
+  )
+ where
+
+import Lava2000.Ref
+import Lava2000.Signal
+import Lava2000.Generic
+import Lava2000.Sequent
+
+import Lava2000.MyST
+  ( ST
+  )
+
+----------------------------------------------------------------
+-- netlist
+
+netlist :: Functor f => (S a -> a) -> f Symbol -> f a
+netlist phi symbols = fmap cata symbols
+ where
+  cata (Symbol sym) = cata' sym
+  cata'             = memoRef (phi . fmap cata . deref)
+
+netlistIO :: Sequent f => IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
+netlistIO new define symbols =
+  do tab <- tableIO
+
+     let gather (Symbol sym) =
+           do visited <- findIO tab sym
+              case visited of
+                Just v  -> do return v
+                Nothing -> do v <- new
+                              extendIO tab sym v
+                              s <- mmap gather (deref sym)
+                              define v s
+                              return v
+
+      in mmap gather symbols
+
+netlistST :: Sequent f => ST s v -> (v -> S v -> ST s ()) -> f Symbol -> ST s (f v)
+netlistST new define symbols =
+  do tab <- tableST
+
+     let gather (Symbol sym) =
+           do visited <- findST tab sym
+              case visited of
+                Just v  -> do return v
+                Nothing -> do v <- new
+                              extendST tab sym v
+                              s <- mmap gather (deref sym)
+                              define v s
+                              return v
+
+      in mmap gather symbols
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Operators.hs b/Lava2000/Operators.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Operators.hs
@@ -0,0 +1,96 @@
+module Lava2000.Operators where
+
+import Lava2000.Signal
+import Lava2000.Generic
+import Lava2000.Error
+
+infix  4 <==>
+infixr 3 <&>
+infixr 2 <|>, ==>, <==
+infixr 2 <=>, <#>
+infixr 1 |->
+
+----------------------------------------------------------------------
+-- Gates
+
+and2 (x, y) = andl [x, y]
+or2  (x, y) = orl  [x, y]
+xor2 (x, y) = xorl [x, y]
+
+nand2 = inv . and2
+nor2  = inv . or2
+xnor2 = inv . xor2
+
+equiv (x, y) = xnor2 (x, y)
+impl  (x, y) = or2   (inv x, y)
+
+nandl = inv . andl
+norl  = inv . orl
+
+plus  (x, y) = plusl [x,y]
+sub   (x, y) = plusl [x, neg y]
+times (x, y) = timesl [x, y]
+imod  (x, y) = modulo x y
+idiv  (x, y) = divide x y
+
+----------------------------------------------------------------------
+-- Binary Operators
+
+x |->  y = delay  x  y
+x <==> y = equal (x, y)
+
+x <&> y = and2  (x, y)
+x <|> y = or2   (x, y)
+x <#> y = xor2  (x, y)
+x <=> y = equiv (x, y)
+x ==> y = impl  (x, y)
+x <== y = impl  (y, x)
+
+x %% y     = imod (x, y)
+gte (x, y) = gteInt x y
+x >>== y   = gte (x, y)
+
+imin (x, y) = ifThenElse (x >>== y) (y, x)
+imax (x, y) = ifThenElse (x >>== y) (x, y)
+
+class SignalInt a where
+  toSignalInt   :: Signal a   -> Signal Int
+  fromSignalInt :: Signal Int -> Signal a
+
+instance SignalInt Int where
+  toSignalInt   = id
+  fromSignalInt = id
+
+instance SignalInt a => Num (Signal a) where
+  x + y    = fromSignalInt $ plus (toSignalInt x, toSignalInt y)
+  x - y    = fromSignalInt $ sub (toSignalInt x, toSignalInt y)
+  x * y    = fromSignalInt $ times (toSignalInt x, toSignalInt y)
+  negate x = fromSignalInt $ neg (toSignalInt x)
+
+  fromInteger = fromSignalInt . int . fromInteger
+
+instance SignalInt a => Fractional (Signal a) where
+  x / y = fromSignalInt $ idiv (toSignalInt x, toSignalInt y)
+
+instance SignalInt a => Enum (Signal a) where
+  toEnum n = fromSignalInt (int n)
+  fromEnum (Signal s) =
+    case unsymbol s of
+      Int n -> n
+      _     -> wrong Lava2000.Error.EnumOnSymbols
+
+instance SignalInt a => Ord (Signal a) where
+  min x y = fromSignalInt $ imin (toSignalInt x, toSignalInt y)
+  max x y = fromSignalInt $ imax (toSignalInt x, toSignalInt y)
+
+
+
+----------------------------------------------------------------------
+-- Convert
+
+int2bit n = n <==> (1 :: Signal Int)
+bit2int b = ifThenElse b (1 :: Signal Int, 0)
+
+----------------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Patterns.hs b/Lava2000/Patterns.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Patterns.hs
@@ -0,0 +1,96 @@
+module Lava2000.Patterns where
+
+import Lava2000
+
+infixr 5 ->-
+infixr 4 -|-
+
+{-
+This Lava module defines some often used wiring circuits
+and connection patterns.
+-}
+
+----------------------------------------------------------------
+-- Wiring Circuits
+
+swap  (a,b) = (b,a)
+swapl [a,b] = [b,a]
+
+copy a      = (a,a)
+
+riffle   = halveList ->- zipp ->- unpair
+unriffle = pair ->- unzipp ->- append
+
+zipp ([],   [])   = []
+zipp (a:as, b:bs) = (a,b) : zipp (as, bs)
+
+unzipp []          = ([],   [])
+unzipp ((a,b):abs) = (a:as, b:bs)
+  where
+    (as, bs) = unzipp abs
+
+pair (x:y:xs) = (x,y) : pair xs
+pair xs       = []
+
+unpair ((x,y):xys) = x : y : unpair xys
+unpair []          = []
+
+halveList inps = (left,right)
+  where
+    left  = take half inps
+    right = drop half inps
+    half  = length inps `div` 2
+
+append (a,b) = a ++ b
+
+----------------------------------------------------------------
+-- Connection Patterns
+
+serial circ1 circ2 = circ2 . circ1
+circ1 ->- circ2    = serial circ1 circ2
+
+compose []           = id
+compose (circ:circs) = circ ->- compose circs
+
+composeN n circ = compose (replicate n circ)
+
+par circ1 circ2 (a, b) = (circ1 a, circ2 b)
+circ1 -|- circ2        = par circ1 circ2
+
+parl circ1 circ2 = halveList ->- (circ1 -|- circ2) ->- append
+
+
+two circ = parl circ circ
+ilv circ = unriffle ->- two circ ->- riffle
+
+iter 0 comb circ = circ
+iter n comb circ = comb (iter (n-1) comb circ)
+
+twoN n circ = iter n two circ
+ilvN n circ = iter n ilv circ
+
+bfly 0 circ = id
+bfly n circ = ilv (bfly (n-1) circ) ->- twoN (n-1) circ
+
+pmap circ = pair ->- map circ ->- unpair
+
+tri circ []         = []
+tri circ (inp:inps) = inp : (map circ ->- tri circ) inps
+
+mirror circ (a, b) = (c, d)
+  where
+    (d, c) = circ (b, a)
+
+row circ (carryIn, [])   = ([], carryIn)
+row circ (carryIn, a:as) = (b:bs, carryOut)
+  where
+    (b, carry)     = circ (carryIn, a)
+    (bs, carryOut) = row circ (carry, as)
+
+column circ = mirror (row (mirror circ))
+
+grid circ = row (column circ)
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Property.hs b/Lava2000/Property.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Property.hs
@@ -0,0 +1,399 @@
+module Lava2000.Property
+  ( Gen
+  , generate
+  , ChoiceWithSig
+  , Fresh(..)
+  , CoFresh(..)
+  , double
+  , triple
+  , list
+  , listOf
+  , results
+  , sequential
+  , forAll
+  , Property(..)
+  , Checkable(..)
+  , ShowModel(..)
+  , Model
+  , properties
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Generic
+
+import Monad
+  ( liftM2
+  , liftM3
+  , liftM4
+  , liftM5
+  )
+
+import List
+  ( intersperse
+  , transpose
+  )
+
+import Data.IORef
+import System.IO.Unsafe
+
+----------------------------------------------------------------
+-- Gen Monad
+
+newtype Gen a
+  = Gen (Tree Int -> a)
+
+instance Functor Gen where
+  fmap f (Gen m) = Gen (\t -> f (m t))
+
+instance Monad Gen where
+  return a =
+    Gen (\t -> a)
+
+  Gen m >>= k =
+    Gen (\(Fork _ t1 t2) -> let a = m t1 ; Gen m2 = k a in m2 t2)
+
+generate :: Gen a -> IO a
+generate (Gen m) =
+  do t <- newTree
+     return (m t)
+
+-- Gen Tree
+
+data Tree a
+  = Fork a (Tree a) (Tree a)
+
+newTree :: IO (Tree Int)
+newTree =
+  do var <- newIORef 0
+     tree var
+ where
+  tree var = unsafeInterleaveIO $
+    do n  <- new var
+       t1 <- tree var
+       t2 <- tree var
+       return (Fork n t1 t2)
+
+  new var = unsafeInterleaveIO $
+    do n <- readIORef var
+       let n' = n+1
+       n' `seq` writeIORef var n'
+       return n
+
+----------------------------------------------------------------
+-- Fresh
+
+class Fresh a where
+  fresh :: Gen a
+
+instance Fresh () where
+  fresh = return ()
+
+instance ConstructiveSig a => Fresh (Signal a) where
+  fresh = Gen (\(Fork n _ _) -> varSig ("i" ++ show n))
+
+instance (Fresh a, Fresh b) => Fresh (a,b) where
+  fresh = liftM2 (,) fresh fresh
+
+instance (Fresh a, Fresh b, Fresh c) => Fresh (a,b,c) where
+  fresh = liftM3 (,,) fresh fresh fresh
+
+instance (Fresh a, Fresh b, Fresh c, Fresh d) => Fresh (a,b,c,d) where
+  fresh = liftM4 (,,,) fresh fresh fresh fresh
+
+instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e) => Fresh (a,b,c,d,e) where
+  fresh = liftM5 (,,,,) fresh fresh fresh fresh fresh
+
+instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f) => Fresh (a,b,c,d,e,f) where
+  fresh = liftM6 (,,,,,) fresh fresh fresh fresh fresh fresh
+
+instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f, Fresh g) => Fresh (a,b,c,d,e,f,g) where
+  fresh = liftM7 (,,,,,,) fresh fresh fresh fresh fresh fresh fresh
+
+-- CoFresh
+
+class ChoiceWithSig a where
+  ifThenElseWithSig :: Choice b => Signal a -> (b, b) -> b
+
+class CoFresh a where
+  cofresh :: (Choice b, Fresh b) => Gen b -> Gen (a -> b)
+
+instance ChoiceWithSig Bool where
+  ifThenElseWithSig = ifThenElse
+
+instance CoFresh () where
+  cofresh gen =
+    do b <- gen
+       return (\_ -> b)
+
+instance ChoiceWithSig a => CoFresh (Signal a) where
+  cofresh gen =
+    do b1 <- gen
+       b2 <- gen
+       return (\a -> ifThenElseWithSig a (b1, b2))
+
+instance (CoFresh a, CoFresh b) => CoFresh (a, b) where
+  cofresh gen =
+    do f <- cofresh (cofresh gen)
+       return (\(a, b) -> f a b)
+
+instance (CoFresh a, CoFresh b, CoFresh c) => CoFresh (a, b, c) where
+  cofresh gen =
+    do f <- cofresh (cofresh (cofresh gen))
+       return (\(a, b, c) -> f a b c)
+
+instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d) => CoFresh (a, b, c, d) where
+  cofresh gen =
+    do f <- cofresh (cofresh (cofresh (cofresh gen)))
+       return (\(a, b, c, d) -> f a b c d)
+
+instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e) => CoFresh (a, b, c, d, e) where
+  cofresh gen =
+    do f <- cofresh (cofresh (cofresh (cofresh (cofresh gen))))
+       return (\(a, b, c, d, e) -> f a b c d e)
+
+instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f) => CoFresh (a, b, c, d, e, f) where
+  cofresh gen =
+    do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen)))))
+       return (\(a, b, c, d, e, g) -> f a b c d e g)
+
+instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f, CoFresh g) => CoFresh (a, b, c, d, e, f, g) where
+  cofresh gen =
+    do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen))))))
+       return (\(a, b, c, d, e, g, h) -> f a b c d e g h)
+
+instance (CoFresh a, Choice b, Fresh b) => Fresh (a -> b) where
+  fresh = cofresh fresh
+
+instance CoFresh a => CoFresh [a] where
+  cofresh gen =
+    do fs <- sequence [ cofreshList i gen | i <- [0..] ]
+       return (\as -> (fs !! length as) as)
+
+instance (Finite a, CoFresh b) => CoFresh (a -> b) where
+  cofresh gen =
+    do f <- cofresh gen
+       return (\g -> f (map g domain))
+
+cofreshList :: (CoFresh a, Choice b, Fresh b) => Int -> Gen b -> Gen ([a] -> b)
+cofreshList 0 gen =
+  do x <- gen
+     return (\[] -> x)
+
+cofreshList k gen =
+  do f <- cofreshList (k-1) (cofresh gen)
+     return (\(a:as) -> f as a)
+
+----------------------------------------------------------------
+-- some combinators
+
+double :: Gen a -> Gen (a,a)
+double gen = liftM2 (,) gen gen
+
+triple :: Gen a -> Gen (a,a,a)
+triple gen = liftM3 (,,) gen gen gen
+
+list :: Fresh a => Int -> Gen [a]
+list n = sequence [ fresh | i <- [1..n] ]
+
+listOf :: Int -> Gen a -> Gen [a]
+listOf n gen = sequence [ gen | i <- [1..n] ]
+
+----------------------------------------------------------------
+-- combinators for circuits
+
+results :: Int -> Gen (a -> b) -> Gen (a -> [b])
+results n gen =
+  do fs <- sequence [ gen | i <- [1..n] ]
+     return (\a -> map ($ a) fs)
+
+sequential :: (CoFresh a, Fresh b, Choice b) => Int -> Gen (a -> b)
+sequential n =
+  do fb     <- fresh
+     fstate <- results n fresh
+     let circ inp = (fb inp, fstate inp)
+     return (loop circ)
+ where
+  loop circ a = b
+    where
+      (b, state) = circ (a, delay (zeroList n) (state :: [Signal Bool]))
+
+----------------------------------------------------------------
+-- checkable
+
+newtype Property
+  = P (Gen ([Signal Bool], Model -> [[String]]))
+
+class Checkable a where
+  property :: a -> Property
+
+instance Checkable Property where
+  property p = p
+
+instance Checkable Bool where
+  property b = property (bool b)
+
+instance Checkable a => Checkable (Signal a) where
+  property (Signal s) = P (return ([Signal s], \_ -> []))
+
+instance Checkable a => Checkable [a] where
+  property as = P $
+    do sms <- sequence [ gen | (P gen) <- map property as ]
+       return (concat (map fst sms), \model -> concat (map (($ model) . snd) sms))
+
+instance Checkable a => Checkable (Gen a) where
+  property m = P (do a <- m ; let P m' = property a in m')
+
+instance (Fresh a, ShowModel a, Checkable b) => Checkable (a -> b) where
+  property f = forAll fresh f
+
+----------------------------------------------------------------
+-- quantify
+
+type Model
+  = [(String, [String])]
+
+name :: Signal a -> String
+name (Signal s) =
+  case unsymbol s of
+    VarBool v -> v
+    VarInt v  -> v
+    _         -> error "no name"
+
+class ShowModel a where
+  showModel :: Model -> a -> [String]
+
+instance ShowModel (Signal a) where
+  showModel model sig =
+    case lookup (name sig) model of
+      Just xs -> xs
+      Nothing -> []
+
+instance ShowModel () where
+  showModel model () =
+    ["()"]
+
+instance (ShowModel a, ShowModel b) => ShowModel (a, b) where
+  showModel model (a, b) =
+    zipWith' (\x y -> "(" ++ x ++ "," ++ y ++ ")")
+      (showModel model a) (showModel model b)
+
+instance (ShowModel a, ShowModel b, ShowModel c) => ShowModel (a, b, c) where
+  showModel model (a, b, c) =
+    zipWith3' (\x y z -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ ")")
+      (showModel model a) (showModel model b) (showModel model c)
+
+instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d) => ShowModel (a, b, c, d) where
+  showModel model (a, b, c, d) =
+    zipWith4' (\x y z v -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ ")")
+      (showModel model a) (showModel model b) (showModel model c) (showModel model d)
+
+instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e) => ShowModel (a, b, c, d, e) where
+  showModel model (a, b, c, d, e) =
+    zipWith5' (\x y z v w -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ ")")
+      (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e)
+
+instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f) => ShowModel (a, b, c, d, e, f) where
+  showModel model (a, b, c, d, e, f) =
+    zipWith6' (\x y z v w p -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ ")")
+      (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model f)
+
+instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f, ShowModel g) => ShowModel (a, b, c, d, e, f, g) where
+  showModel model (a, b, c, d, e, f, g) =
+    zipWith7' (\x y z v w p q -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ "," ++ q ++ ")")
+      (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model f) (showModel model g)
+
+instance ShowModel a => ShowModel [a] where
+  showModel model as =
+    map (\xs -> "[" ++ concat (intersperse "," xs)
+                    ++ "]")
+      (transpose (map (showModel model) as))
+
+instance ShowModel (a -> b) where
+  showModel model sig = []
+
+zipWith' f []     []     = []
+zipWith' f []     ys     = zipWith' f ["?"] ys
+zipWith' f xs     []     = zipWith' f xs ["?"]
+zipWith' f (x:xs) (y:ys) = f x y : zipWith' f xs ys
+
+zipWith3' f []     []     []     = []
+zipWith3' f []     ys     zs     = zipWith3' f ["?"] ys zs
+zipWith3' f xs     []     zs     = zipWith3' f xs ["?"] zs
+zipWith3' f xs     ys     []     = zipWith3' f xs ys ["?"]
+zipWith3' f (x:xs) (y:ys) (z:zs) = f x y z : zipWith3' f xs ys zs
+
+zipWith4' f []     []     []     []     = []
+zipWith4' f []     ys     zs     vs     = zipWith4' f ["?"] ys zs vs
+zipWith4' f xs     []     zs     vs     = zipWith4' f xs ["?"] zs vs
+zipWith4' f xs     ys     []     vs     = zipWith4' f xs ys ["?"] vs
+zipWith4' f xs     ys     zs     []     = zipWith4' f xs ys zs ["?"]
+zipWith4' f (x:xs) (y:ys) (z:zs) (v:vs) = f x y z v : zipWith4' f xs ys zs vs
+
+zipWith5' f []     []     []     []     []     = []
+zipWith5' f []     ys     zs     vs     ws     = zipWith5' f ["?"] ys zs vs ws
+zipWith5' f xs     []     zs     vs     ws     = zipWith5' f xs ["?"] zs vs ws
+zipWith5' f xs     ys     []     vs     ws     = zipWith5' f xs ys ["?"] vs ws
+zipWith5' f xs     ys     zs     []     ws     = zipWith5' f xs ys zs ["?"] ws
+zipWith5' f xs     ys     zs     vs     []     = zipWith5' f xs ys zs vs ["?"]
+zipWith5' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) = f x y z v w : zipWith5' f xs ys zs vs ws
+
+zipWith6' f []     []     []     []     []     []     = []
+zipWith6' f []     ys     zs     vs     ws     ps     = zipWith6' f ["?"] ys zs vs ws ps
+zipWith6' f xs     []     zs     vs     ws     ps     = zipWith6' f xs ["?"] zs vs ws ps
+zipWith6' f xs     ys     []     vs     ws     ps     = zipWith6' f xs ys ["?"] vs ws ps
+zipWith6' f xs     ys     zs     []     ws     ps     = zipWith6' f xs ys zs ["?"] ws ps
+zipWith6' f xs     ys     zs     vs     []     ps     = zipWith6' f xs ys zs vs ["?"] ps
+zipWith6' f xs     ys     zs     vs     ws     []     = zipWith6' f xs ys zs vs ws ["?"]
+zipWith6' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) = f x y z v w p : zipWith6' f xs ys zs vs ws ps
+
+zipWith7' f []     []     []     []     []     []     []     = []
+zipWith7' f []     ys     zs     vs     ws     ps     qs     = zipWith7' f ["?"] ys zs vs ws ps qs
+zipWith7' f xs     []     zs     vs     ws     ps     qs     = zipWith7' f xs ["?"] zs vs ws ps qs
+zipWith7' f xs     ys     []     vs     ws     ps     qs     = zipWith7' f xs ys ["?"] vs ws ps qs
+zipWith7' f xs     ys     zs     []     ws     ps     qs     = zipWith7' f xs ys zs ["?"] ws ps qs
+zipWith7' f xs     ys     zs     vs     []     ps     qs     = zipWith7' f xs ys zs vs ["?"] ps qs
+zipWith7' f xs     ys     zs     vs     ws     []     qs     = zipWith7' f xs ys zs vs ws ["?"] qs
+zipWith7' f xs     ys     zs     vs     ws     ps     []     = zipWith7' f xs ys zs vs ws ps ["?"]
+zipWith7' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) (q:qs) = f x y z v w p q : zipWith7' f xs ys zs vs ws ps qs
+
+forAll :: (ShowModel a, Checkable b) => Gen a -> (a -> b) -> Property
+forAll gen body = P $
+  do a <- gen
+     let P m = property (body a)
+     (sigs, mod) <- m
+     return (sigs, \model -> showModel model a : mod model)
+
+----------------------------------------------------------------
+-- evaluate
+
+properties :: Checkable a => a -> IO ([Signal Bool], Model -> [[String]])
+properties a = generate gen
+ where
+  (P gen) = property a
+
+----------------------------------------------------------------
+-- bweeuh
+
+liftM6 f g1 g2 g3 g4 g5 g6 =
+  do a1 <- g1
+     a2 <- g2
+     a3 <- g3
+     a4 <- g4
+     a5 <- g5
+     a6 <- g6
+     return (f a1 a2 a3 a4 a5 a6)
+
+liftM7 f g1 g2 g3 g4 g5 g6 g7 =
+  do a1 <- g1
+     a2 <- g2
+     a3 <- g3
+     a4 <- g4
+     a5 <- g5
+     a6 <- g6
+     a7 <- g7
+     return (f a1 a2 a3 a4 a5 a6 a7)
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Ref.hs b/Lava2000/Ref.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Ref.hs
@@ -0,0 +1,181 @@
+module Lava2000.Ref
+  ( Ref       -- * -> * ; Eq, Show
+  , ref       -- :: a     -> Ref a
+  , deref     -- :: Ref a -> a
+  , memoRef   -- :: (Ref a -> b) -> (Ref a -> b)
+
+  , TableIO   -- :: * -> * -> * ; Eq
+  , tableIO   -- :: IO (TableIO a b)
+  , extendIO  -- :: TableIO a b -> Ref a -> b -> IO ()
+  , findIO    -- :: TableIO a b -> Ref a -> IO (Maybe b)
+  , memoRefIO -- :: (Ref a -> IO b) -> (Ref a -> IO b)
+
+  , TableST   -- :: * -> * -> * -> * ; Eq
+  , tableST   -- :: ST (TableST s a b)
+  , extendST  -- :: TableST s a b -> Ref a -> b -> ST s ()
+  , findST    -- :: TableST s a b -> Ref a -> ST s (Maybe b)
+  , memoRefST -- :: (Ref a -> ST s b) -> (Ref a -> ST s b)
+  )
+ where
+
+import Lava2000.MyST
+
+import System.IO
+import System.IO.Unsafe
+import Data.IORef
+
+unsafeCoerce :: a -> b
+unsafeCoerce a = unsafePerformIO $
+  do writeIORef ref a
+     readIORef ref
+ where
+  ref = unsafePerformIO $ newIORef undefined
+  -- Defined here because Unsafe.Coerce doesn't exist in Hugs.
+
+{-
+
+Warning! One should regard this module as a portable
+extension to the Haskell language. It is not Haskell.
+
+-}
+
+{-
+
+Here is how we implement Tables of Refs:
+
+A Table is nothing but a unique tag, of type TableTag.
+TableTag can be anything, as long as it is easy
+to create new ones, and we can compare them for
+equality. (I chose IORef ()).
+
+So how do we store Refs in a Table? We do not
+want the Tables keeping track of their Refs
+(which would be disastrous when the table
+becomes big, and we would not have any garbage
+collection).
+
+Instead, every Ref keeps track of the value it
+has in each table it is in. This has the advantage
+that we have a constant lookup time (if the number of
+Tables we are using is small), and we get garbage
+collection of table entries for free.
+
+The disadvantage is that, since the types of the
+Tables vary, the Ref has no idea what type of
+values it is supposed to store. So we use dynamic
+types.
+
+A Ref is implemented as follows: it has two pieces
+of information. The first one is an updatable
+list of entries for each table it is a member in.
+Since it is an updatable list, it is an IORef, which
+we also use to compare two Refs. The second part is
+just the value the Ref is pointing at (this can never
+change anyway).
+
+-}
+
+-----------------------------------------------------------------
+-- Ref
+
+data Ref a
+  = Ref (IORef [(TableTag, Dyn)]) a
+
+instance Eq (Ref a) where
+  Ref r1 _ == Ref r2 _ = r1 == r2
+
+instance Show a => Show (Ref a) where
+  showsPrec _ (Ref _ a) = showChar '{' . shows a . showChar '}'
+
+ref :: a -> Ref a
+ref a = unsafePerformIO $
+  do r <- newIORef []
+     return (Ref r a)
+
+deref :: Ref a -> a
+deref (Ref _ a) = a
+
+-----------------------------------------------------------------
+-- Table IO
+
+type TableTag
+  = IORef ()
+
+newtype TableIO a b
+  = TableIO TableTag
+ deriving Eq
+
+tableIO :: IO (TableIO a b)
+tableIO = TableIO `fmap` newIORef ()
+
+findIO :: TableIO a b -> Ref a -> IO (Maybe b)
+findIO (TableIO t) (Ref r _) =
+  do list <- readIORef r
+     return (fromDyn `fmap` lookup t list)
+
+extendIO :: TableIO a b -> Ref a -> b -> IO ()
+extendIO (TableIO t) (Ref r _) b =
+  do list <- readIORef r
+     writeIORef r ((t,toDyn b) : filter ((/= t) . fst) list)
+
+-----------------------------------------------------------------
+-- Table ST
+
+newtype TableST s a b
+  = TableST (TableIO a b)
+ deriving Eq
+
+tableST :: ST s (TableST s a b)
+tableST = unsafeIOtoST (TableST `fmap` tableIO)
+
+findST :: TableST s a b -> Ref a -> ST s (Maybe b)
+findST (TableST tab) r = unsafeIOtoST (findIO tab r)
+
+extendST :: TableST s a b -> Ref a -> b -> ST s ()
+extendST (TableST tab) r b = unsafeIOtoST (extendIO tab r b)
+
+-----------------------------------------------------------------
+-- Memo
+
+memoRef :: (Ref a -> b) -> (Ref a -> b)
+memoRef f = unsafePerformIO . memoRefIO (return . f)
+
+memoRefIO :: (Ref a -> IO b) -> (Ref a -> IO b)
+memoRefIO f = unsafePerformIO $
+  do tab <- tableIO
+     let f' r = do mb <- findIO tab r
+                   case mb of
+                     Just b  -> do return b
+                     Nothing -> fixIO $ \b ->
+                                  do extendIO tab r b
+                                     f r
+     return f'
+
+memoRefST :: (Ref a -> ST s b) -> (Ref a -> ST s b)
+memoRefST f = unsafePerformST $
+  do tab <- tableST
+     let f' r = do mb <- findST tab r
+                   case mb of
+                     Just b  -> do return b
+                     Nothing -> fixST $ \b ->
+                                  do extendST tab r b
+                                     f r
+     return f'
+
+-----------------------------------------------------------------
+-- Dyn
+
+data Dyn
+  = Dyn
+
+toDyn :: a -> Dyn
+toDyn = unsafeCoerce
+
+fromDyn :: Dyn -> a
+fromDyn = unsafeCoerce
+
+-----------------------------------------------------------------
+-- the end.
+
+
+
diff --git a/Lava2000/Retime.hs b/Lava2000/Retime.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Retime.hs
@@ -0,0 +1,59 @@
+module Lava2000.Retime
+  ( timeTransform
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Netlist
+
+import List
+  ( isPrefixOf
+  )
+
+----------------------------------------------------------------
+-- time transformation
+
+timeTransform :: (Generic a, Generic b) => (a -> b) -> ([a] -> [b])
+timeTransform circ []           = []
+timeTransform circ inps@(inp:_) =
+    map construct
+  . transStruct
+  . netlist phi
+  . struct
+  . circ
+  . symbolize tag
+  $ inp
+ where
+  n = length inps
+
+  phi (DelayBool ini next) =
+    delay DelayBool ini next
+
+  phi (DelayInt ini next) =
+    delay DelayInt ini next
+
+  phi (VarBool s) | tag `isPrefixOf` s =
+    var (drop (length tag) s)
+
+  phi (VarInt s) | tag `isPrefixOf` s =
+    var (drop (length tag) s)
+
+  phi s =
+    take n (cycle (map symbol (zips s)))
+
+  delay del ~(ini0:_) next =
+    (symbol (del ini0 (last next)) : list (n-1) (init next))
+
+  var s =
+    map (pickSymbol s) inps
+
+  list 0 _       = []
+  list n ~(x:xs) = x : list (n-1) xs
+
+  tag = "#retime#"
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Satnik.hs b/Lava2000/Satnik.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Satnik.hs
@@ -0,0 +1,150 @@
+module Lava2000.Satnik
+  ( satnik
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- satnik
+
+satnik :: Checkable a => a -> IO ProofResult
+satnik a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cnf"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+     cls <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "c Generated by Lava2000"
+       , "c "
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return n'
+
+         clause xs =
+           do n <- readIORef cls
+              let n' = n+1 in n' `seq` writeIORef cls n'
+              hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n")
+
+         define v s =
+           case s of
+             Bool True     -> clause [ v ]
+             Bool False    -> clause [ -v ]
+             Inv x         -> clause [ -x, -v ] >> clause [ x, v ]
+
+             And []        -> define v (Bool True)
+             And xs        -> conjunction v xs
+
+             Or  []        -> define v (Bool False)
+             Or  xs        -> conjunction (-v) (map negate xs)
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> exactly1 v xs
+
+             VarBool s     -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n")
+
+             DelayBool x y -> wrong Lava2000.Error.DelayEval
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+
+            conjunction v xs =
+              do clause (v : map negate xs)
+                 sequence_ [ clause [ -v, x ] | x <- xs ]
+
+            exactly1 v xs =
+              do clause (-v : xs)
+                 sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ]
+                 sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ]
+
+            pairs []     = []
+            pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+            pick []      = []
+            pick (x:xs)  = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ]
+
+     outvs <- netlistIO new define (struct props)
+     clause (map negate (flatten outvs))
+
+     nvar <- readIORef var
+     ncls <- readIORef cls
+     hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n")
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Satnik: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/satnik.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Satzoo.hs b/Lava2000/Satzoo.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Satzoo.hs
@@ -0,0 +1,150 @@
+module Lava2000.Satzoo
+  ( satzoo
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- satzoo
+
+satzoo :: Checkable a => a -> IO ProofResult
+satzoo a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cnf"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+     cls <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "c Generated by Lava2000"
+       , "c "
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return n'
+
+         clause xs =
+           do n <- readIORef cls
+              let n' = n+1 in n' `seq` writeIORef cls n'
+              hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n")
+
+         define v s =
+           case s of
+             Bool True     -> clause [ v ]
+             Bool False    -> clause [ -v ]
+             Inv x         -> clause [ -x, -v ] >> clause [ x, v ]
+
+             And []        -> define v (Bool True)
+             And xs        -> conjunction v xs
+
+             Or  []        -> define v (Bool False)
+             Or  xs        -> conjunction (-v) (map negate xs)
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> exactly1 v xs
+
+             VarBool s     -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n")
+
+             DelayBool x y -> wrong Lava2000.Error.DelayEval
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+
+            conjunction v xs =
+              do clause (v : map negate xs)
+                 sequence_ [ clause [ -v, x ] | x <- xs ]
+
+            exactly1 v xs =
+              do clause (-v : xs)
+                 sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ]
+                 sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ]
+
+            pairs []     = []
+            pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+            pick []      = []
+            pick (x:xs)  = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ]
+
+     outvs <- netlistIO new define (struct props)
+     clause (map negate (flatten outvs))
+
+     nvar <- readIORef var
+     ncls <- readIORef cls
+     hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n")
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Satzoo: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/satzoo.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Sequent.hs b/Lava2000/Sequent.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Sequent.hs
@@ -0,0 +1,18 @@
+module Lava2000.Sequent where
+
+----------------------------------------------------------------
+-- Sequent (monadic Functor)
+
+class Functor s => Sequent s where
+  sequent :: Monad m => s (m a) -> m (s a)
+
+instance Sequent [] where
+  sequent = sequence
+
+mmap :: (Monad m, Sequent s) => (a -> m b) -> s a -> m (s b)
+mmap f = sequent . fmap f
+
+----------------------------------------------------------------
+-- the end.
+
+
diff --git a/Lava2000/Sequential.hs b/Lava2000/Sequential.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Sequential.hs
@@ -0,0 +1,137 @@
+module Lava2000.Sequential
+  ( simulateSeq
+  )
+ where
+
+import Lava2000.Ref
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Sequent
+import Lava2000.Generic
+
+import Lava2000.MyST
+  ( ST
+  , STRef
+  , newSTRef
+  , readSTRef
+  , writeSTRef
+  , unsafeInterleaveST
+  , runST
+  )
+
+----------------------------------------------------------------
+-- wire datatype
+
+type Var s
+  = (STRef s (S Symbol), STRef s (Wire s))
+
+data Wire s
+  = Wire
+    { dependencies :: [Var s]
+    , kick         :: ST s ()
+    }
+
+----------------------------------------------------------------
+-- simulate
+
+simulateSeq :: (Generic a, Generic b) => (a -> b) -> [a] -> [b]
+simulateSeq circ []   = []
+simulateSeq circ inps = runST (
+  do roots <- newSTRef []
+
+     let root r =
+           do rs <- readSTRef roots
+              writeSTRef roots (r:rs)
+
+         new =
+           do rval <- newSTRef (error "val?")
+              rwir <- newSTRef (error "wire?")
+              return (rval, rwir)
+
+         define r s =
+           case s of
+             DelayBool s s' -> delay s s'
+             DelayInt  s s' -> delay s s'
+             _ ->
+               do relate r (arguments s) $
+                    eval `fmap` mmap (readSTRef . fst) s
+          where
+           delay ri@(rinit,_) r1@(pre,_) =
+               do state <- newSTRef Nothing
+                  r2 <- new
+                  root r2
+
+                  relate r [ri] $
+                    do ms <- readSTRef state
+                       case ms of
+                         Just s  -> return s
+                         Nothing ->
+                           do s <- readSTRef rinit
+                              writeSTRef state (Just s)
+                              return s
+
+                  relate r2 [r,r1] $
+                    do s <- readSTRef pre
+                       writeSTRef state (Just s)
+                       return s
+
+     sr   <- netlistST new define (struct (circ (input inps)))
+     rs   <- readSTRef roots
+     step <- drive (flatten sr ++ rs)
+
+     outs <- lazyloop $
+       do step
+          s <- mmap (fmap symbol . readSTRef . fst) sr
+          return (construct s)
+
+     let res = takes inps outs
+     return res
+  )
+
+-- evaluation order
+
+relate :: Var s -> [Var s] -> ST s (S Symbol) -> ST s ()
+relate (rval, rwir) rs f =
+  do writeSTRef rwir $
+       Wire{ dependencies = rs
+           , kick = do b <- f
+                       writeSTRef rval b
+           }
+
+drive :: [Var s] -> ST s (ST s ())
+drive [] =
+  do return (return ())
+
+drive ((rval,rwir):rs) =
+  do wire <- readSTRef rwir
+     writeSTRef rwir (error "detected combinational loop")
+     driv1 <- drive (dependencies wire)
+     writeSTRef rwir $
+       Wire { dependencies = [], kick = return () }
+     driv2 <- drive rs
+     return $
+       do driv1
+          kick wire
+          driv2
+
+----------------------------------------------------------------
+-- helper functions
+
+lazyloop :: ST s a -> ST s [a]
+lazyloop m =
+  do a  <- m
+     as <- unsafeInterleaveST (lazyloop m)
+     return (a:as)
+
+input :: Generic a => [a] -> a
+input xs = out
+ where
+  out = foldr delay out xs
+
+takes :: [a] -> [b] -> [b]
+takes []     _      = []
+takes (_:xs) (y:ys) = y : takes xs ys
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/SequentialCircuits.hs b/Lava2000/SequentialCircuits.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/SequentialCircuits.hs
@@ -0,0 +1,68 @@
+module Lava2000.SequentialCircuits where
+
+import Lava2000
+
+----------------------------------------------------------------
+-- Sequential Circuits
+
+edge inp = change
+  where
+    inp'   = delay low inp
+    change = xor2 (inp, inp')
+
+toggle change = out
+  where
+    out' = delay low out
+    out  = xor2 (change, out')
+
+delayClk init (clk, inp) = out
+  where
+    out = delay init val
+    val = mux (clk, (out, inp))
+
+delayN 0 init inp = inp
+delayN n init inp = out
+  where
+    out  = delay init rest
+    rest = delayN (n-1) init inp
+
+always inp = ok
+  where
+    sofar = delay high ok
+    ok    = and2 (inp, sofar)
+
+constant x = ok
+  where
+    init = delay high low
+    same = x <==> delay zero x
+    ok   = always (init <|> same)
+
+puls n () = out
+  where
+    out  = delayN (n-1) low last
+    last = delay high out
+
+outputList sigs () = out
+  where
+    out = foldr (|->) out sigs
+
+rowSeq circ inp = out
+  where
+    carryIn         = delay zero carryOut
+    (out, carryOut) = circ (carryIn, inp)
+
+rowSeqReset circ (reset,inp) = out
+  where
+    carryIn         = delay zero carry
+    carry           = mux (reset, (carryOut, zero))
+    (out, carryOut) = circ (carryIn, inp)
+
+rowSeqPeriod n circ inp = out
+  where
+    reset = puls n ()
+    out   = rowSeqReset circ (reset, inp)
+
+----------------------------------------------------------------
+-- the end.
+
+
diff --git a/Lava2000/SequentialConstructive.hs b/Lava2000/SequentialConstructive.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/SequentialConstructive.hs
@@ -0,0 +1,173 @@
+module Lava2000.SequentialConstructive
+  ( simulateCon
+  )
+ where
+
+import Lava2000.Ref
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Sequent
+import Lava2000.Generic
+import Lava2000.Error
+
+import Data.IORef
+import System.IO.Unsafe
+
+----------------------------------------------------------------
+-- wire datatype
+
+type Time
+  = IORef ()
+
+data Timed a
+  = a `At` Time
+  | Uninitialized
+
+data Wire
+  = Wire
+    { components :: [Component]
+    , value      :: Timed (S Symbol)
+    }
+
+type Component
+  = Time -> IO ()
+
+----------------------------------------------------------------
+-- simulate
+
+simulateCon :: (Generic a, Generic b) => (a -> b) -> [a] -> [b]
+simulateCon circ inps = unsafePerformIO $
+ do micro <- newSet
+    macro <- newSet
+    time0 <- newIORef ()
+
+    let new =
+          do rwire <- newIORef (Wire{ components = [], value = Uninitialized })
+             return rwire
+
+        define rwire (DelayBool init next) =
+          do delay rwire init next
+
+        define rwire (DelayInt init next) =
+          do delay rwire init next
+
+        define rwire sym =
+          case arguments sym of
+            []   -> addSet macro constant
+            args -> sequence_ [ compWire rarg propagate | rarg <- args ]
+         where
+          propagate time =
+            do sym' <- mmap (`valueWire` time) sym
+               case evalLazy sym' of
+                 Nothing -> return ()
+                 Just v  -> updateWire rwire time v
+
+          constant time =
+            do propagate time
+               addSet macro constant
+
+        delay rwire init next =
+          do compWire next nextState
+             compWire init initState
+         where
+          nextState time =
+            do mv <- valueWire next time
+               case mv of
+                 Nothing -> return ()
+                 Just v  -> addSet macro (\t -> updateWire rwire t v)
+
+          initState time
+            | time == time0 = do mv <- valueWire init time
+                                 case mv of
+                                   Nothing -> return ()
+                                   Just v  -> updateWire rwire time v
+            | otherwise     = do return ()
+
+        compWire rwire comp =
+          do wire <- readIORef rwire
+             writeIORef rwire (wire{ components = comp : components wire })
+
+        valueWire rwire time =
+          do wire <- readIORef rwire
+             return $
+               case value wire of
+                 v `At` time'
+                   | time == time' -> Just v
+                 _                 -> Nothing
+
+        actualValueWire rwire time =
+          do mv <- valueWire rwire time
+             case mv of
+               Just v  -> return v
+               Nothing -> wrong Lava2000.Error.UndefinedWire
+
+        updateWire rwire time v =
+          do wire <- readIORef rwire
+             mv   <- valueWire rwire time
+             case mv of
+               Just v' | v =/= v'  -> wrong Lava2000.Error.BadCombinationalLoop
+                       | otherwise -> return ()
+
+               _ -> do writeIORef rwire (wire{ value = v `At` time })
+                       sequence_ [ addSet micro comp | comp <- components wire ]
+
+        Bool b1 =/= Bool b2 = b1 /= b2
+        Int  n1 =/= Int  n2 = n1 /= n2
+        _       =/= _       = True
+
+    sr <- netlistIO new define (struct (circ (input inps)))
+
+    outs <- timedLazyLoop time0 $ \time ->
+      do emptySet macro ($ time)
+         while (emptySet micro ($ time))
+         s <- mmap (`actualValueWire` time) sr
+         return (construct (symbol `fmap` s))
+
+    let res = takes inps outs
+    return res
+
+----------------------------------------------------------------
+-- helper functions
+
+newSet :: IO (IORef [a])
+newSet = newIORef []
+
+addSet :: IORef [a] -> a -> IO ()
+addSet rset x =
+  do xs <- readIORef rset
+     writeIORef rset (x:xs)
+
+emptySet :: IORef [a] -> (a -> IO ()) -> IO Bool
+emptySet rset action =
+  do xs <- readIORef rset
+     writeIORef rset []
+     case xs of
+       [] -> do return False
+       _  -> do sequence [ action x | x <- xs ]
+                return True
+
+while :: Monad m => m Bool -> m ()
+while m =
+  do b <- m
+     if b then while m
+          else return ()
+
+timedLazyLoop :: Time -> (Time -> IO a) -> IO [a]
+timedLazyLoop t m =
+  do a  <- m t
+     t' <- newIORef ()
+     as <- unsafeInterleaveIO (timedLazyLoop t' m)
+     return (a:as)
+
+input :: Generic a => [a] -> a
+input xs = out
+ where
+  out = foldr delay out xs
+
+takes :: [a] -> [b] -> [b]
+takes []     _      = []
+takes (_:xs) (y:ys) = y : takes xs ys
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Signal.hs b/Lava2000/Signal.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Signal.hs
@@ -0,0 +1,350 @@
+module Lava2000.Signal where
+
+import Lava2000.Ref
+import Lava2000.Sequent
+import Lava2000.Error
+
+import List
+  ( transpose
+  )
+
+----------------------------------------------------------------
+-- Signal, Symbol, S
+
+newtype Signal a
+  = Signal Symbol
+
+newtype Symbol
+  = Symbol (Ref (S Symbol))
+
+data S s
+  = Bool      Bool
+  | Inv       s
+  | And       [s]
+  | Or        [s]
+  | Xor       [s]
+  | VarBool   String
+  | DelayBool s s
+
+  | Int      Int
+  | Neg      s
+  | Div      s s
+  | Mod      s s
+  | Plus     [s]
+  | Times    [s]
+  | Gte      s s
+  | Equal    [s]
+  | If       s s s
+  | VarInt   String
+  | DelayInt s s
+
+symbol :: S Symbol -> Symbol
+symbol = Symbol . ref
+
+unsymbol :: Symbol -> S Symbol
+unsymbol (Symbol r) = deref r
+
+instance Eq (Signal a) where
+  Signal (Symbol r1) == Signal (Symbol r2) = r1 == r2
+
+----------------------------------------------------------------
+-- operations
+
+-- on bits
+
+bool :: Bool -> Signal Bool
+bool b = lift0 (Bool b)
+
+low, high :: Signal Bool
+low  = bool False
+high = bool True
+
+inv :: Signal Bool -> Signal Bool
+inv = lift1 Inv
+
+andl, orl, xorl :: [Signal Bool] -> Signal Bool
+andl = liftl And
+orl  = liftl Or
+xorl = liftl Xor
+
+equalBool :: Signal Bool -> Signal Bool -> Signal Bool
+equalBool x y = inv (xorl [x,y])
+
+ifBool :: Signal Bool -> (Signal Bool, Signal Bool) -> Signal Bool
+ifBool c (x,y) = orl[andl[c,x],andl[inv c,y]]
+
+delayBool :: Signal Bool -> Signal Bool -> Signal Bool
+delayBool = lift2 DelayBool
+
+varBool :: String -> Signal Bool
+varBool s = lift0 (VarBool s)
+
+-- on ints
+
+int :: Int -> Signal Int
+int n = lift0 (Int n)
+
+neg :: Signal Int -> Signal Int
+neg = lift1 Neg
+
+divide, modulo :: Signal Int -> Signal Int -> Signal Int
+divide = lift2 Div
+modulo = lift2 Mod
+
+plusl, timesl :: [Signal Int] -> Signal Int
+plusl  = liftl Plus
+timesl = liftl Times
+
+equall :: [Signal Int] -> Signal Bool
+equall = liftl Equal
+
+gteInt :: Signal Int -> Signal Int -> Signal Bool
+gteInt = lift2 Gte
+
+equalInt :: Signal Int -> Signal Int -> Signal Bool
+equalInt x y = equall [x,y]
+
+ifInt :: Signal Bool -> (Signal Int, Signal Int) -> Signal a
+ifInt c (x,y) = lift3 If c x y
+
+delayInt :: Signal Int -> Signal Int -> Signal Int
+delayInt = lift2 DelayInt
+
+varInt :: String -> Signal Int
+varInt s = lift0 (VarInt s)
+
+-- liftings
+
+lift0 :: S Symbol -> Signal a
+lift0 oper = Signal (symbol oper)
+
+lift1 :: (Symbol -> S Symbol) -> Signal a -> Signal b
+lift1 oper (Signal a) = Signal (symbol (oper a))
+
+lift2 :: (Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c
+lift2 oper (Signal a) (Signal b) = Signal (symbol (oper a b))
+
+lift3 :: (Symbol -> Symbol -> Symbol -> S Symbol)
+      -> Signal a -> Signal b -> Signal c -> Signal d
+lift3 oper (Signal a) (Signal b) (Signal c) = Signal (symbol (oper a b c))
+
+liftl :: ([Symbol] -> S Symbol) -> [Signal a] -> Signal c
+liftl oper sigas = Signal (symbol (oper (map (\(Signal a) -> a) sigas)))
+
+----------------------------------------------------------------
+-- evaluate
+
+eval :: S (S a) -> S a
+eval s =
+  case s of
+    Bool b       -> Bool b
+    Inv (Bool b) -> Bool (not b)
+    And xs       -> Bool . all bval $ xs
+    Or xs        -> Bool . any bval $ xs
+    Xor xs       -> Bool . (1 ==) . length . filter bval $ xs
+
+    Int n                 -> Int n
+    Neg (Int n)           -> Int (-n)
+    Div (Int n1) (Int n2) -> Int (n1 `div` n2)
+    Mod (Int n1) (Int n2) -> Int (n1 `mod` n2)
+    Plus xs               -> Int  . sum     . map nval $ xs
+    Times xs              -> Int  . product . map nval $ xs
+    Gte (Int n1) (Int n2) -> Bool (n1 >= n2)
+    Equal xs              -> Bool . equal   . map nval $ xs
+    If (Bool c) x y       -> if c then x else y
+
+    DelayBool s s' -> wrong Lava2000.Error.DelayEval
+    DelayInt  s s' -> wrong Lava2000.Error.DelayEval
+    VarBool   s    -> wrong Lava2000.Error.VarEval
+    VarInt    s    -> wrong Lava2000.Error.VarEval
+ where
+  bval (Bool b) = b
+  nval (Int n)  = n
+
+  equal (x:y:xs) = x == y && equal (y:xs)
+  equal _        = True
+
+evalLazy :: S (Maybe (S a)) -> Maybe (S a)
+evalLazy s =
+  case s of
+    -- lazy
+    And xs
+      | any (`bval` False) xs        -> bans False
+
+    Or xs
+      | any (`bval` True) xs         -> bans True
+
+    Xor xs
+      | number (`bval` True) xs >= 2 -> bans False
+
+    -- strict
+    _ -> eval `fmap` sequent s
+
+ where
+  bans = Just . Bool
+
+  bval (Just (Bool b)) b' = b == b'
+  bval _               _  = False
+
+  number p = length . filter p
+
+arguments :: S a -> [a]
+arguments s =
+  case s of
+    Bool b     -> []
+    Inv s      -> [s]
+    And xs     -> xs
+    Or xs      -> xs
+    Xor xs     -> xs
+
+    Int n      -> []
+    Neg s      -> [s]
+    Div s1 s2  -> [s1,s2]
+    Mod s1 s2  -> [s1,s2]
+    Plus xs    -> xs
+    Times xs   -> xs
+    Gte x y    -> [x,y]
+    Equal xs   -> xs
+    If x y z   -> [x,y,z]
+
+    DelayBool s s' -> [s,s']
+    DelayInt  s s' -> [s,s']
+    VarBool s      -> []
+    VarInt  s      -> []
+
+zips :: S [a] -> [S a]
+zips s =
+  case s of
+    Bool b     -> [Bool b]
+    Inv s      -> map Inv s
+    And xs     -> map And (transpose xs)
+    Or xs      -> map Or  (transpose xs)
+    Xor xs     -> map Xor (transpose xs)
+
+    Int n      -> [Int n]
+    Neg s      -> map Neg s
+    Div s1 s2  -> zipWith Div s1 s2
+    Mod s1 s2  -> zipWith Mod s1 s2
+    Plus xs    -> map Plus  (transpose xs)
+    Times xs   -> map Times (transpose xs)
+    Gte x y    -> zipWith Gte x y
+    Equal xs   -> map Equal (transpose xs)
+    If x y z   -> zipWith3 If x y z
+
+    DelayBool s s' -> zipWith DelayBool s s'
+    DelayInt  s s' -> zipWith DelayInt s s'
+    VarBool s      -> [VarBool s]
+    VarInt  s      -> [VarInt  s]
+
+----------------------------------------------------------------
+-- properties of S
+
+instance Functor S where
+  fmap f s =
+    case s of
+      Bool b    -> Bool b
+      Inv x     -> Inv (f x)
+      And xs    -> And (map f xs)
+      Or  xs    -> Or  (map f xs)
+      Xor xs    -> Xor (map f xs)
+
+      Int   n   -> Int n
+      Neg   x   -> Neg   (f x)
+      Div   x y -> Div   (f x) (f y)
+      Mod   x y -> Mod   (f x) (f y)
+      Plus  xs  -> Plus  (map f xs)
+      Times xs  -> Times (map f xs)
+      Gte   x y -> Gte (f x) (f y)
+      Equal xs  -> Equal (map f xs)
+      If x y z  -> If (f x) (f y) (f z)
+
+      DelayBool x y -> DelayBool (f x) (f y)
+      DelayInt  x y -> DelayInt  (f x) (f y)
+      VarBool   v   -> VarBool v
+      VarInt    v   -> VarInt  v
+
+instance Sequent S where
+  sequent s =
+    case s of
+      Bool b    -> lift0 (Bool b)
+      Inv x     -> lift1 Inv x
+      And xs    -> liftl And xs
+      Or  xs    -> liftl Or  xs
+      Xor xs    -> liftl Xor xs
+
+      Int   n   -> lift0 (Int n)
+      Neg   x   -> lift1 Neg   x
+      Div   x y -> lift2 Div   x y
+      Mod   x y -> lift2 Mod   x y
+      Plus  xs  -> liftl Plus  xs
+      Times xs  -> liftl Times xs
+      Gte   x y -> lift2 Gte   x y
+      Equal xs  -> liftl Equal xs
+      If x y z  -> lift3 If x y z
+
+      DelayBool x y -> lift2 DelayBool x y
+      DelayInt  x y -> lift2 DelayInt x y
+      VarBool  v    -> lift0 (VarBool v)
+      VarInt   v    -> lift0 (VarInt v)
+   where
+    lift0 op =
+      do return op
+
+    lift1 op x =
+      do x' <- x
+         return (op x')
+
+    lift2 op x y =
+      do x' <- x
+         y' <- y
+         return (op x' y')
+
+    lift3 op x y z =
+      do x' <- x
+         y' <- y
+         z' <- z
+         return (op x' y' z')
+
+    liftl op xs =
+      do xs' <- sequence xs
+         return (op xs')
+
+instance Show (Signal a) where
+  showsPrec n (Signal s) =
+    showsPrec n s
+
+instance Show Symbol where
+  showsPrec n sym =
+    showsPrec n (unsymbol sym)
+
+instance Show a => Show (S a) where
+  showsPrec n s =
+    case s of
+      Bool True  -> showString "high"
+      Bool False -> showString "low"
+
+      Inv x      -> showString "inv"  . showList [x]
+      And xs     -> showString "andl" . showList xs
+      Or  xs     -> showString "orl"  . showList xs
+      Xor xs     -> showString "xorl" . showList xs
+
+      Int   i    -> showsPrec n i
+      Neg   x    -> showString "-" . showsPrec n x
+      Div   x y  -> showString "idiv" . showList [x,y]
+      Mod   x y  -> showString "imod" . showList [x,y]
+      Plus  xs   -> showString "plusl" . showList xs
+      Times xs   -> showString "timesl" . showList xs
+      Gte   x y  -> showString "gte" . showList [x,y]
+      Equal xs   -> showString "equall" . showList xs
+      If x y z   -> showString "ifThenElse" . showList [x,y,z]
+
+      DelayBool x y -> showString "delay" . showList [x,y]
+      DelayInt  x y -> showString "delay" . showList [x,y]
+
+      VarBool s     -> showString s
+      VarInt  s     -> showString s
+      _             -> showString "<<symbol>>"
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/SignalTry.hs b/Lava2000/SignalTry.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/SignalTry.hs
@@ -0,0 +1,15 @@
+module Lava2000.SignalTry where
+
+import Lava2000.Ref
+
+data Signal a
+  = Value a
+  | Symbol (Ref (Symbol a))
+
+data Symbol a
+  = forall x y . Function String ([x] -> [y] -> a) [Signal x] [Signal y]
+  | Delay (Signal a) (Signal a)
+  | Variable String
+
+and2 :: (Signal Bool, Signal Bool) -> Signal Bool
+and2 (x,y) = Symbol (ref (Function "and" (\xs _ -> and xs) [x,y] []))
diff --git a/Lava2000/Smv.hs b/Lava2000/Smv.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Smv.hs
@@ -0,0 +1,155 @@
+module Lava2000.Smv
+  ( smv
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- smv
+
+smv :: Checkable a => a -> IO ProofResult
+smv a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.smv"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "-- Generated by Lava2000"
+       , ""
+       , "MODULE main"
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1; v = "w" ++ show n'
+              n' `seq` writeIORef var n'
+              return v
+
+         define v s =
+           case s of
+             Bool True     -> op0 "1"
+             Bool False    -> op0 "0"
+             Inv x         -> op1 "!" x
+
+             And []        -> define v (Bool True)
+             And [x]       -> op0 x
+             And xs        -> opl "&" xs
+
+             Or  []        -> define v (Bool False)
+             Or  [x]       -> op0 x
+             Or  xs        -> opl "|" xs
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> op0 (xor xs)
+
+             VarBool s     -> do op0 s
+                                 hPutStr firstHandle ("VAR " ++ s ++ " : boolean;\n")
+             DelayBool x y -> delay x y
+
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+            w i = v ++ "_" ++ show i
+
+            op0 s =
+              hPutStr secondHandle $
+                "DEFINE " ++ v ++ " := " ++ s ++ ";\n"
+
+            op1 op s =
+              op0 (op ++ "(" ++ s ++ ")")
+
+            opl op xs =
+              op0 (concat (intersperse (" " ++ op ++ " ") xs))
+
+            xor [x]    = x
+            xor [x,y]  = "!(" ++ x ++ " <-> " ++ y ++ ")"
+            xor (x:xs) = "(" ++ x ++ " & !("
+                      ++ concat (intersperse " | " xs)
+                      ++ ") | (!" ++ x ++ " & (" ++ xor xs ++ ")))"
+
+            delay x y =
+              do hPutStr firstHandle ("VAR " ++ v ++ " : boolean;\n")
+                 hPutStr secondHandle $
+                      "ASSIGN init(" ++ v ++ ") := " ++ x ++ ";\n"
+                   ++ "ASSIGN next(" ++ v ++ ") := " ++ y ++ ";\n"
+
+     outvs <- netlistIO new define (struct props)
+     hPutStr secondHandle $ unlines $
+       [ "SPEC AG " ++ outv
+       | outv <- flatten outvs
+       ]
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Smv: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/smv.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Stable.hs b/Lava2000/Stable.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Stable.hs
@@ -0,0 +1,60 @@
+module Lava2000.Stable where
+
+import Lava2000.Signal
+import Lava2000.Operators
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Ref
+
+import Lava2000.MyST
+  ( STRef
+  , newSTRef
+  , readSTRef
+  , writeSTRef
+  , runST
+  , unsafeInterleaveST
+  )
+
+import List
+  ( isPrefixOf
+  )
+
+----------------------------------------------------------------
+-- stable analysis
+
+stable :: Generic a => a -> Signal Bool
+stable inp =
+  runST
+  ( do table     <- tableST
+       stableRef <- newSTRef []
+
+       let gather (Symbol sym) =
+             do ms <- findST table sym
+                case ms of
+                  Just () -> do return ()
+                  Nothing -> do extendST table sym ()
+                                mmap gather (deref sym)
+                                define (Symbol sym) (deref sym)
+
+           define out (DelayBool _ inn) =
+             do addStable (out <==> inn)
+
+           define out (DelayInt _ inn) =
+             do addStable (out <==> inn)
+
+           define _ _ =
+             do return ()
+
+           addStable x =
+             do stables <- readSTRef stableRef
+                writeSTRef stableRef (x:stables)
+
+        in mmap gather (struct inp)
+
+       stables <- readSTRef stableRef
+       return (andl stables)
+  )
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Table.hs b/Lava2000/Table.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Table.hs
@@ -0,0 +1,72 @@
+module Lava2000.Table
+  ( table
+  , tableProp
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.MyST
+
+{-
+
+Example use:
+
+Suppose we have a circuit:
+
+  f :: (Signal Bool, Signal Bool) -> Signal Bool
+  f (x,y) = and2 (y,x)
+
+Then we can look at its internal structure as follows:
+
+  table (struct (f (var "i")))
+
+will evaluate to
+
+  ([(1,And 2 3),(3,Var "i_1"),(2,Var "i_2")],Object 1)
+
+For circuits taking more complicated structures as arguments
+(such as lists), one has to instantiate the list size first
+of course.
+
+If you do not like the "Object 1" output, you can just use
+the function `flatten' to get a list of identifiers.
+
+-}
+
+----------------------------------------------------------------
+-- table
+
+tableProp :: Checkable a => a -> IO ([(Int,S Int)], [Int])
+tableProp a =
+  do (props,_) <- properties a
+     let (tab, ps) = table (struct props)
+     return (tab, flatten ps)
+
+table :: Sequent f => f Symbol -> ([(Int,S Int)], f Int)
+table str =
+  runST
+  ( do ref   <- newSTRef 0
+       table <- newSTRef []
+
+       let new =
+             do n <- readSTRef ref
+                let n' = n+1
+                writeSTRef ref n'
+                return n'
+
+           define v def =
+             do tab <- readSTRef table
+                writeSTRef table ((v,def):tab)
+
+       str' <- netlistST new define str
+       tab  <- readSTRef table
+       return (tab, str')
+  )
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Test.hs b/Lava2000/Test.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Test.hs
@@ -0,0 +1,23 @@
+module Lava2000.Test where
+
+import Lava2000.Signal
+import Lava2000.Sequential
+import Lava2000.Generic
+
+import Lava2000.LavaRandom
+  ( newRnd
+  )
+
+----------------------------------------------------------------
+-- test
+
+test :: (Constructive a, Show b, Generic b) => (a -> b) -> IO [b]
+test circ =
+  do rnd <- newRnd
+     let res = simulateSeq (\_ -> circ (random rnd)) (replicate 100 ())
+     print res
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Verification.hs b/Lava2000/Verification.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Verification.hs
@@ -0,0 +1,475 @@
+module Lava2000.Verification
+  ( Option(..)
+  , verify
+  , verifyWith
+  , ProofResult(..)
+  , verifyDir
+  , checkVerifyDir
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+
+import List
+  ( intersperse
+  , isPrefixOf
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+verifyDir :: FilePath
+verifyDir = "Verify"
+
+----------------------------------------------------------------
+-- Options
+
+data Option
+  = Name String
+  | ShowTime
+  | Sat Int
+  | NoBacktracking
+  | Depth Int
+  | Increasing
+  | RestrictStates
+ deriving (Eq, Show)
+
+defaultOptions :: [Option]
+defaultOptions =
+  [Increasing]
+
+defaultValues :: [Option]
+defaultValues =
+  [Name "circuit", Sat 1, Depth 1]
+
+sameOption :: Option -> Option -> Bool
+sameOption opt1 opt2 = tag opt1 == tag opt2
+ where
+  tag = head . words . show
+
+searchOptVal :: Read a => [Option] -> (a -> Option) -> a
+searchOptVal options what = search (options ++ defaultValues)
+ where
+  opt' = what undefined
+
+  search [] = wrong Lava2000.Error.Internal_OptionNotFound
+  search (opt:opts)
+    | sameOption opt opt' = read (words (show opt) !! 1)
+    | otherwise           = search opts
+
+searchOptBool :: [Option] -> Option -> Bool
+searchOptBool options what = what `elem` options
+
+----------------------------------------------------------------
+-- verify
+
+verify :: Checkable a => a -> IO ProofResult
+verify a = verifyWith defaultOptions a
+
+verifyWith :: Checkable a => [Option] -> a -> IO ProofResult
+verifyWith options a =
+  do checkVerifyDir
+     noBuffering
+
+     (props,model) <- properties a
+     (states,pins) <- writeDefinitions defsFile props
+     res <- proveAll defsFile states pins options
+     if res == Falsifiable
+       then displayModel outFile model
+       else return ()
+     return res
+ where
+  defsFile = verifyDir ++ "/" ++ nameOpt ++ ".defs"
+  outFile  = verifyDir ++ "/prover.out"
+  nameOpt  = searchOptVal options Name
+
+----------------------------------------------------------------
+-- proving
+
+proveAll :: FilePath -> [State] -> Int -> [Option] -> IO ProofResult
+proveAll defsFile states quests options =
+  case actions of
+    [[]] ->
+      do putStrLn "Nothing to prove! ... Valid."
+         return Valid
+
+    [[(labels, ini, assumps, obligs)]] ->
+      do proveUnit labels ini assumps obligs
+
+    _ ->
+      do tryAll actions
+ where
+  depths
+    | incrOpt && not (null states) = [depthOpt ..]
+    | otherwise                    = [depthOpt]
+
+  steps d
+    | null states = [ ([],                  True,  [],     [1]) ]
+    | otherwise   = [ (["base " ++ show d], True,  [],     [1..d])
+                    , (["step " ++ show d], False, [1..d], [d+1])
+                    ]
+
+  pins (labels, ini, assumps, obligs) n
+    | n == 1    = [ (labels, ini, map (pin 1) assumps, map (pin 1) obligs) ]
+    | otherwise = [ ( labels ++ ["pin " ++ show p]
+                    , ini
+                    , [ pin p ass | ass <- assumps, p <- [1..n] ]
+                      ++ [ pin p' obl | obl <- obligs, p' <- [1..p-1] ]
+                    , [ pin p obl | obl <- obligs ]
+                    )
+                  | p <- [1..n]
+                  ]
+   where
+    pin p a = (a, p)
+
+  actions =
+    [ concatMap (`pins` quests) (steps d) | d <- depths ]
+
+  nameOpt  = searchOptVal  options Name
+  depthOpt = searchOptVal  options Depth
+  incrOpt  = searchOptBool options Increasing
+  restrOpt = searchOptBool options RestrictStates
+
+  tryAll [] =
+    do result Indeterminate
+
+  tryAll ([] : rest) =
+    do result Valid
+
+  tryAll (((labels, ini, assumps, obligs) : tries) : rest) =
+    do r <-  proveUnit labels ini assumps obligs
+       case r of
+         Valid                 -> tryAll (tries : rest)
+         Falsifiable | not ini -> tryAll rest
+                     | ini     -> result Falsifiable
+         Indeterminate         -> result Indeterminate
+
+  result r =
+    do putStrLn "--"
+       putStrLn ("Result: " ++ show r ++ ".")
+       return r
+
+  proveUnit labels ini assumps obligs =
+    do proveFile mainFile create labels options
+   where
+    create =
+      do writeHeader
+         sequence
+              [ instantiateFile defsFile mainFile t
+              | t <- times
+              ]
+         appendAssumptions
+            $ [ quest ass
+              | ass <- assumps
+              ]
+           ++ [ "~" ++ init t
+              | t <- tail times
+              ]
+           ++ ( if ini then [init 1]
+                       else
+                if restrOpt then restrictStates
+                            else []
+              )
+         appendObligations
+            $ [ quest obl
+              | obl <- obligs
+              ]
+         appendFooter
+
+    mainFile =
+      verifyDir ++ "/" ++ clean (nameOpt ++ ".prov" ++ concatMap ("." ++) labels)
+
+    clean (' ':s) = '_':clean s
+    clean (c:s)   = c:clean s
+    clean []      = []
+
+    times =
+      nub [ t | (t, p) <- assumps ++ obligs ]
+
+    init t =
+      "init_t" ++ show t
+
+    quest (t, p) =
+      "quest_t" ++ show t ++ "_n" ++ show p
+
+    writeHeader = writeFile mainFile $ unlines $
+      [ "/* Generated by Lava 2000 */"
+      , "/* options: " ++ show options ++ " */"
+      , ""
+      , "AND("
+      , ""
+      ]
+
+    appendAssumptions []  = return ()
+    appendAssumptions ass = appendFile mainFile $ unlines $
+      [ ""
+      , "/* assumptions */"
+      , ""
+      ] ++ map (++ ",") ass
+
+    appendObligations obs = appendFile mainFile $ unlines $
+      [ ""
+      , "big_question <-> AND("
+      , "/* proof obligations */"
+      , ""
+      ] ++ map (++ ",") obs
+
+    appendFooter = appendFile mainFile $ unlines $
+      [ ""
+      , "/* the big question */"
+      , "TRUE)) -> big_question"
+      , ""
+      ]
+
+    restrictStates =
+      [ notEqual (t-1) (t'-1) states | t <- times, t' <- times, t' > t ]
+
+    notEqual t t' states =
+      "OR(" ++ concat (intersperse ", " [ "~(" ++ s ++ "_t" ++ show t ++ " "
+                                          ++ eq ++ " " ++ s ++ "_t" ++ show t' ++ ")"
+                                          | (eq,s) <- states ])
+            ++ ")"
+
+----------------------------------------------------------------
+-- primitive proving
+
+data ProofResult
+  = Valid
+  | Falsifiable
+  | Indeterminate
+ deriving (Eq, Show)
+
+proveFile :: FilePath -> IO () -> [String] -> [Option] -> IO ProofResult
+proveFile file before labels options =
+  do putStr ( "Proving:"
+           ++ concat (intersperse "," (map (" " ++) labels))
+           ++ " "
+            )
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/prover.wrapper "
+                ++ file
+                ++ " "
+                ++ opts
+                ++ " -model first"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+ where
+  satOpt    = searchOptVal  options Sat
+  noBackOpt = searchOptBool options NoBacktracking
+  timeOpt   = searchOptBool options ShowTime
+  opts      = (if timeOpt then "-showTime " else "")
+           ++ ("-t " ++ show satOpt ++ " ")
+           ++ (if noBackOpt then "" else "-b")
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ([State],Int)
+writeDefinitions file props =
+  do han <- openFile file WriteMode
+     var <- newIORef 0
+     sts <- newIORef []
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return (Now ("w" ++ show n'))
+
+         define v s =
+           do hPutStr han (def ++ ";\n")
+              case s of
+                DelayBool x y -> state ("<->",the y)
+                DelayInt  x y -> state ("=",the y)
+                _             -> return ()
+          where
+           def =
+             case s of
+               Bool True  -> prop $ "TRUE"
+               Bool False -> prop $ "FALSE"
+               Inv x      -> prop $ op1 "~" x
+               And xs     -> prop $ opl "AND" "," xs "TRUE"
+               Or  xs     -> prop $ opl "OR"  "," xs "FALSE"
+               Xor xs     -> prop $ opl "XOR" "," xs "FALSE"
+
+               Int   n    -> arit $ show n
+               Neg   x    -> arit $ op1 "-" x
+               Div   x y  -> arit $ op2 "/" x y
+               Mod   x y  -> arit $ op2 "%" x y
+               Plus  xs   -> arit $ opl "" "+" xs "0"
+               Times xs   -> arit $ opl "" "*" xs "1"
+               Gte   x y  -> prop $ op2 ">=" x y
+               Equal xs   -> prop $ equal xs
+               If x y z   -> iff x (op2 "=" v y) (op2 "=" v z)
+
+               VarBool s  -> prop $ op0 (Now s)
+               VarInt  s  -> arit $ op0 (Now s)
+
+               DelayBool x y -> iff ini (prop (op0 x)) (prop (op0 (pre y)))
+               DelayInt  x y -> iff ini (arit (op0 x)) (arit (op0 (pre y)))
+
+           prop form =
+             "(" ++ show v ++ " <-> (" ++ form ++ "))"
+
+           arit expr =
+             "(" ++ show v ++ " = (" ++ expr ++ "))"
+
+           iff c x y =
+             "(" ++ op0 c ++ " -> " ++ x ++ ") & (~"
+                 ++ op0 c ++ " -> " ++ y ++ ")"
+
+           state s =
+             do xs <- readIORef sts
+                writeIORef sts (s:xs)
+
+           op0 v      = show v
+           op1 op v   = op ++ show v
+           op2 op v w = "(" ++ show v ++ " " ++ op ++ " " ++ show w ++ ")"
+
+           opl fun con []  nul = nul
+           opl fun con [x] nul = show x
+           opl fun con xs  nul =
+             fun ++ "(" ++ concat (intersperse con (map show xs)) ++ ")"
+
+           equal (x:y:xs) =
+             (show x ++ " = " ++ show y) ++ " & " ++ equal (y:xs)
+           equal _ = "TRUE"
+
+     ~(Compound vs) <- netlistIO new define (struct props)
+     let quests = [ Index quest i | i <- [1..] ]
+     sequence [ hPutStr han (show q ++ " <-> " ++ show v ++ ";\n")
+              | (q, Object v) <- quests `zip` vs
+              ]
+     hClose han
+
+     states <- readIORef sts
+     return (states, length vs)
+
+type State
+  = (String, String)
+
+data Timed
+  = Now String
+  | Pre String
+
+instance Show Timed where
+  show (Now a) = a ++ "$now"
+  show (Pre a) = a ++ "$pre"
+
+the (Now a) = a
+the (Pre a) = a
+pre (Now a) = Pre a
+
+ini   = Now "init"
+quest = Now "quest"
+
+data Indexed
+  = Index Timed Int
+
+instance Show Indexed where
+  show (Index a n) = show a ++ "_n" ++ show n
+
+----------------------------------------------------------------
+-- models
+
+displayModel :: FilePath -> (Model -> [[String]]) -> IO ()
+displayModel file showModel =
+  do s <- readFile file
+     let (first : model) = lines s
+     if "# counter model" `isPrefixOf` first
+       then do let inps  = inputs model
+                   table = makeTable inps []
+                   repr  = showModel table
+               putStr (unlines (map showInput repr))
+       else return ()
+ where
+  inputs []     = []
+  inputs (l:ls) =
+    case words l of
+      [v@('i':_), "=", val] -> (v, val) : rest
+      [v@('i':_)]           -> (v, "high") : rest
+      ['~':v@('i':_)]       -> (v, "low") : rest
+      _                     -> rest
+   where
+    rest = inputs ls
+
+  makeTable [] table =
+    table
+
+  makeTable ((v,val):inps) table =
+    makeTable inps (extend name (read time) val table)
+   where
+    n    = length v
+    name = take (n - length time - 2) v
+    time = reverse . takeWhile isDigit . reverse $ v
+    isDigit d = '0' <= d && d <= '9'
+
+  extend name time val [] =
+    extend name time val [(name, [])]
+
+  extend name time val (entry@(name',vals):table)
+    | name == name' = updated : table
+    | otherwise     = entry : extend name time val table
+   where
+    updated = (name', make (time - 1) vals ++ [val] ++ drop time vals)
+
+    make 0 xs     = []
+    make n []     = make n ["?"]
+    make n (x:xs) = x : make (n-1) xs
+
+  showInput [x] = x
+  showInput xs  = "<" ++ concat (intersperse "," xs) ++ ">"
+
+----------------------------------------------------------------
+-- instantiation
+
+instantiateFile :: FilePath -> FilePath -> Int -> IO ()
+instantiateFile from to t =
+  do appendFile to ("/* time instance " ++ show t ++ " */\n")
+     system ( "sed "
+           ++ "-e 's/$now/_t" ++ show t     ++ "/g' "
+           ++ "-e 's/$pre/_t" ++ show (t-1) ++ "/g' "
+           ++ "-e 's/;/,/g' "
+           ++ " < " ++ from ++ " >> " ++ to
+            )
+     return ()
+
+----------------------------------------------------------------
+-- helper functions
+
+checkVerifyDir :: IO ()
+checkVerifyDir =
+  do system ("mkdir -p " ++ verifyDir)
+     return ()
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Vhdl.hs b/Lava2000/Vhdl.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Vhdl.hs
@@ -0,0 +1,199 @@
+module Lava2000.Vhdl
+  ( writeVhdl
+  , writeVhdlInput
+  , writeVhdlInputOutput
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Error
+import Lava2000.LavaDir
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import System.IO
+  ( stdout
+  , BufferMode (..)
+  , hSetBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- write vhdl
+
+writeVhdl :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
+writeVhdl name circ =
+  do writeVhdlInput name circ (var "inp")
+
+writeVhdlInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
+writeVhdlInput name circ inp =
+  do writeVhdlInputOutput name circ inp (symbolize "outp" (circ inp))
+
+writeVhdlInputOutput :: (Generic a, Generic b)
+                     => String -> (a -> b) -> a -> b -> IO ()
+writeVhdlInputOutput name circ inp out =
+  do writeItAll name inp (circ inp) out
+
+writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO ()
+writeItAll name inp out out' =
+  do hSetBuffering stdout NoBuffering
+     putStr ("Writing to file \"" ++ file ++ "\" ... ")
+     writeDefinitions file name inp out out'
+     putStrLn "Done."
+ where
+  file = name ++ ".vhd"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: (Generic a, Generic b)
+                 => FilePath -> String -> a -> b -> b -> IO ()
+writeDefinitions file name inp out out' =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "-- Generated by Lava 2000"
+       , ""
+       , "use work.all;"
+       , ""
+       , "entity"
+       , "  " ++ name
+       , "is"
+       , "port"
+       , "  -- clock"
+       , "  ( " ++ "clk" ++ " : in bit"
+       , ""
+       , "  -- inputs"
+       ] ++
+       [ "  ; " ++ v ++ " : in bit"
+       | VarBool v <- inps
+       ] ++
+       [ ""
+       , "  -- outputs"
+       ] ++
+       [ "  ; " ++ v ++ " : out bit"
+       | VarBool v <- outs'
+       ] ++
+       [ "  );"
+       , "end entity " ++ name ++ ";"
+       , ""
+       , "architecture"
+       , "  structural"
+       , "of"
+       , "  " ++ name
+       , "is"
+       ]
+
+     hPutStr secondHandle $ unlines $
+       [ "begin"
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1; v = "w" ++ show n'
+              writeIORef var n'
+              hPutStr firstHandle ("  signal " ++ v ++ " : bit;\n")
+              return v
+
+         define v s =
+           case s of
+             Bool True     -> port "vdd"  []
+             Bool False    -> port "gnd"  []
+             Inv x         -> port "inv"  [x]
+
+             And []        -> define v (Bool True)
+             And [x]       -> port "id"   [x]
+             And [x,y]     -> port "and2" [x,y]
+             And (x:xs)    -> define (w 0) (And xs)
+                           >> define v (And [x,w 0])
+
+             Or  []        -> define v (Bool False)
+             Or  [x]       -> port "id"   [x]
+             Or  [x,y]     -> port "or2"  [x,y]
+             Or  (x:xs)    -> define (w 0) (Or xs)
+                           >> define v (Or [x,w 0])
+
+             Xor  []       -> define v (Bool False)
+             Xor  [x]      -> port "id"   [x]
+             Xor  [x,y]    -> port "xor2" [x,y]
+             Xor  (x:xs)   -> define (w 0) (Or xs)
+                           >> define (w 1) (Inv (w 0))
+                           >> define (w 2) (And [x, w 1])
+
+                           >> define (w 3) (Inv x)
+                           >> define (w 4) (Xor xs)
+                           >> define (w 5) (And [w 3, w 4])
+                           >> define v     (Or [w 2, w 5])
+
+             VarBool s     -> port "id" [s]
+             DelayBool x y -> port "delay" [x, y]
+
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+            w i = v ++ "_" ++ show i
+
+            port name args =
+              do hPutStr secondHandle $
+                      "  "
+                   ++ make 9 ("c_" ++ v)
+                   ++ " : entity "
+                   ++ make 5 name
+                   ++ " port map ("
+                   ++ concat (intersperse ", " ("clk" : args ++ [v]))
+                   ++ ");\n"
+
+     outvs <- netlistIO new define (struct out)
+     hPutStr secondHandle $ unlines $
+       [ ""
+       , "  -- naming outputs"
+       ]
+
+     sequence
+       [ define v' (VarBool v)
+       | (v,v') <- flatten outvs `zip` [ v' | VarBool v' <- outs' ]
+       ]
+
+     hPutStr secondHandle $ unlines $
+       [ "end structural;"
+       ]
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  sigs x = map unsymbol . flatten . struct $ x
+
+  inps  = sigs inp
+  outs' = sigs out'
+
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+  make n s = take (n `max` length s) (s ++ repeat ' ')
+
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Vis.hs b/Lava2000/Vis.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Vis.hs
@@ -0,0 +1,265 @@
+module Lava2000.Vis
+  ( vis
+  , writeVis
+  , writeVisInput
+  , writeVisInputOutput
+  , equivCheckVisInput
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- vis
+
+vis :: Checkable a => a -> IO ProofResult
+vis a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile $
+       writeDefinitions defsFile "circuit"
+         (Nothing :: Maybe ()) (delay high (andl props)) (var "good")
+ where
+  defsFile = verifyDir ++ "/circuit.mv"
+
+----------------------------------------------------------------
+-- write Vis
+
+writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
+writeVis name circ =
+  do writeVisInput name circ (var "inp")
+
+writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
+writeVisInput name circ inp =
+  do writeVisInputOutput name circ inp (symbolize "outp" (circ inp))
+
+writeVisInputOutput :: (Generic a, Generic b)
+                     => String -> (a -> b) -> a -> b -> IO ()
+writeVisInputOutput name circ inp out =
+  do writeItAll name inp (circ inp) out
+
+writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO ()
+writeItAll name inp out out' =
+  do noBuffering
+     putStr ("Writing to file \"" ++ file ++ "\" ... ")
+     writeDefinitions file name (Just inp) out out'
+     putStrLn "Done."
+ where
+  file = name ++ ".mv"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: (Generic a, Generic b)
+                 => FilePath -> String -> Maybe a -> b -> b -> IO ()
+writeDefinitions file name minp out out' =
+  do firstHandle  <- openFile file1 WriteMode
+     secondHandle <- openFile file2 WriteMode
+     var <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ ".model " ++ name
+       ] ++
+       [ ".inputs " ++ v
+       | VarBool v <- inps
+       ]
+
+     hPutStr secondHandle $ unlines $
+       [ ".outputs " ++ v
+       | VarBool v <- outs'
+       ] ++
+       [ ".table  -> low"
+       , "0"
+       , ".latch low initt"
+       , ".reset initt"
+       , "1"
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+                  v  = "w" ++ show n'
+              writeIORef var n'
+              return v
+
+         define v s =
+           case s of
+             Bool True     -> port (\_   -> True)  []
+             Bool False    -> port (\_   -> False) []
+             Inv x         -> port (\[p] -> not p) [x]
+
+             And []        -> define v (Bool True)
+             And [x]       -> port (\[p]   -> p)      [x]
+             And [x,y]     -> port (\[p,q] -> p && q) [x,y]
+             And (x:xs)    -> define (w 0) (And xs)
+                           >> define v (And [x,w 0])
+
+             Or  []        -> define v (Bool False)
+             Or  [x]       -> port (\[p]   -> p)      [x]
+             Or  [x,y]     -> port (\[p,q] -> p || q) [x,y]
+             Or  (x:xs)    -> define (w 0) (Or xs)
+                           >> define v (Or [x,w 0])
+
+             Xor  []       -> define v (Bool False)
+             Xor  [x]      -> port (\[p]   -> p)      [x]
+             Xor  [x,y]    -> port (\[p,q] -> p /= q) [x,y]
+             Xor  (x:xs)   -> define (w 0) (Or xs)
+                           >> define (w 1) (Inv (w 0))
+                           >> define (w 2) (And [x, w 1])
+
+                           >> define (w 3) (Inv x)
+                           >> define (w 4) (Xor xs)
+                           >> define (w 5) (And [w 3, w 4])
+                           >> define v     (Or [w 2, w 5])
+
+             VarBool s     -> do port (\[p] -> p) [s]
+                                 case (minp,s) of
+                                   (Nothing, 'i':_) -> input s
+                                   _ -> return ()
+             DelayBool x y -> delay x y
+
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+            w i = v ++ "_" ++ show i
+
+            input s =
+              do hPutStr firstHandle $
+                   ".inputs " ++ s ++ "\n"
+
+            port oper args =
+              do hPutStr secondHandle $
+                      ".table "
+                   ++ unwords args
+                   ++ " -> "
+                   ++ v ++ "\n"
+                   ++ unlines
+                      [ line (xs ++ [oper xs])
+                      | xs <- binary (length args)
+                      ]
+             where
+              line bs =
+                unwords (map (\b -> if b then "1" else "0") bs)
+
+              binary 0 = [[]]
+              binary n = map (False:) xs ++ map (True:) xs
+               where
+                xs = binary (n-1)
+
+            delay x y =
+              do hPutStr secondHandle $ unlines
+                    [ ".latch " ++ y ++ " " ++ v ++ "_x"
+                    , ".reset " ++ v ++ "_x"
+                    , "0"
+                    , ".table initt " ++ x ++ " " ++ v ++ "_x -> " ++ v
+                    , "1 - - =" ++ x
+                    , "0 - - =" ++ v ++ "_x"
+                    ]
+
+     outvs <- netlistIO new define (struct out)
+
+     sequence
+       [ define v' (VarBool v)
+       | (v,v') <- flatten outvs `zip` [ v' | VarBool v' <- outs' ]
+       ]
+
+     hPutStr secondHandle $ unlines $
+       [ ".end"
+       ]
+
+     hClose firstHandle
+     hClose secondHandle
+     system ("cat " ++ file1 ++ " " ++ file2 ++ " > " ++ file)
+     system ("rm " ++ file1 ++ " " ++ file2)
+     return ()
+ where
+  file1 = file ++ "_1"
+  file2 = file ++ "_2"
+
+  sigs x = map unsymbol . flatten . struct $ x
+
+  inps  = case minp of
+            Just inp -> sigs inp
+            Nothing  -> []
+  outs' = sigs out'
+
+  make n s = take (n `max` length s) (s ++ repeat ' ')
+
+----------------------------------------------------------------
+-- equivalence checking
+
+equivCheckVisInput circ1 circ2 inp =
+  do checkVerifyDir
+     noBuffering
+     writeVisInput name1 circ1 inp
+     writeVisInput name2 circ2 inp
+     putStr "Vis: ... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/vis.wrapper "
+                ++ name1 ++ " " ++ name2
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+ where
+  name  = "Verify/circuit"
+  name1 = name ++ "_1"
+  name2 = name ++ "_2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Vis: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/vis-reach.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/Lava2000/Zchaff.hs b/Lava2000/Zchaff.hs
new file mode 100644
--- /dev/null
+++ b/Lava2000/Zchaff.hs
@@ -0,0 +1,150 @@
+module Lava2000.Zchaff
+  ( zchaff
+  )
+ where
+
+import Lava2000.Signal
+import Lava2000.Netlist
+import Lava2000.Generic
+import Lava2000.Sequent
+import Lava2000.Property
+import Lava2000.Error
+import Lava2000.LavaDir
+import Lava2000.Verification
+
+import List
+  ( intersperse
+  , nub
+  )
+
+import IO
+  ( openFile
+  , IOMode(..)
+  , hPutStr
+  , hClose
+  )
+
+import Lava2000.IOBuffering
+  ( noBuffering
+  )
+
+import Data.IORef
+
+import System.Cmd (system)
+import System.Exit (ExitCode(..))
+
+----------------------------------------------------------------
+-- zchaff
+
+zchaff :: Checkable a => a -> IO ProofResult
+zchaff a =
+  do checkVerifyDir
+     noBuffering
+     (props,_) <- properties a
+     proveFile defsFile (writeDefinitions defsFile props)
+ where
+  defsFile = verifyDir ++ "/circuit.cnf"
+
+----------------------------------------------------------------
+-- definitions
+
+writeDefinitions :: FilePath -> [Signal Bool] -> IO ()
+writeDefinitions file props =
+  do firstHandle  <- openFile firstFile WriteMode
+     secondHandle <- openFile secondFile WriteMode
+     var <- newIORef 0
+     cls <- newIORef 0
+
+     hPutStr firstHandle $ unlines $
+       [ "c Generated by Lava2000"
+       , "c "
+       ]
+
+     let new =
+           do n <- readIORef var
+              let n' = n+1
+              writeIORef var n'
+              return n'
+
+         clause xs =
+           do n <- readIORef cls
+              let n' = n+1 in n' `seq` writeIORef cls n'
+              hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n")
+
+         define v s =
+           case s of
+             Bool True     -> clause [ v ]
+             Bool False    -> clause [ -v ]
+             Inv x         -> clause [ -x, -v ] >> clause [ x, v ]
+
+             And []        -> define v (Bool True)
+             And xs        -> conjunction v xs
+
+             Or  []        -> define v (Bool False)
+             Or  xs        -> conjunction (-v) (map negate xs)
+
+             Xor  []       -> define v (Bool False)
+             Xor  xs       -> exactly1 v xs
+
+             VarBool s     -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n")
+
+             DelayBool x y -> wrong Lava2000.Error.DelayEval
+             _             -> wrong Lava2000.Error.NoArithmetic
+           where
+
+            conjunction v xs =
+              do clause (v : map negate xs)
+                 sequence_ [ clause [ -v, x ] | x <- xs ]
+
+            exactly1 v xs =
+              do clause (-v : xs)
+                 sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ]
+                 sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ]
+
+            pairs []     = []
+            pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs
+
+            pick []      = []
+            pick (x:xs)  = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ]
+
+     outvs <- netlistIO new define (struct props)
+     clause (map negate (flatten outvs))
+
+     nvar <- readIORef var
+     ncls <- readIORef cls
+     hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n")
+
+     hClose firstHandle
+     hClose secondHandle
+
+     system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file)
+     system ("rm " ++ firstFile ++ " " ++ secondFile)
+     return ()
+ where
+  firstFile  = file ++ "-1"
+  secondFile = file ++ "-2"
+
+----------------------------------------------------------------
+-- primitive proving
+
+proveFile :: FilePath -> IO () -> IO ProofResult
+proveFile file before =
+  do putStr "Zchaff: "
+     before
+     putStr "... "
+     lavadir <- getLavaDir
+     x <- system ( lavadir
+                ++ "/Scripts/zchaff.wrapper "
+                ++ file
+                ++ " -showTime"
+                 )
+     let res = case x of
+                 ExitSuccess   -> Valid
+                 ExitFailure 1 -> Indeterminate
+                 ExitFailure _ -> Falsifiable
+     putStrLn (show res ++ ".")
+     return res
+
+----------------------------------------------------------------
+-- the end.
+
diff --git a/README b/README
new file mode 100644
--- /dev/null
+++ b/README
@@ -0,0 +1,6 @@
+To get verification working (on Linux), change the path
+
+  /home/emax/Program/chalmers-lava2000/
+
+in Development/Lava2000/LavaDir.hs to the appropriate path, and change the wrapper scripts in the Scripts/ directory to point to the correct binaries.
+
diff --git a/Scripts/satzoo.wrapper b/Scripts/satzoo.wrapper
new file mode 100644
--- /dev/null
+++ b/Scripts/satzoo.wrapper
@@ -0,0 +1,81 @@
+#!/bin/sh
+#----------------------------------------------------------------
+#- Wrapper for satzoo
+#- to be used by the Lava system
+#----------------------------------------------------------------
+
+#- This file gets `File' as an argument, and produces the file
+#- File.out, containing the output of prover.
+
+trap 'echo "(^C) \c"' INT
+
+#----------------------------------------------------------------
+#- Variables
+
+#- options
+
+cd "`dirname $1`"
+File="`echo $1 | sed s!.*/!!`"
+shift
+ShowTime="no"
+
+if [ "$1" = "-showTime" ]
+then
+  ShowTime="yes"
+  shift
+fi
+
+Args="$*"
+
+#- derived
+
+Output="$File.out"
+
+#- constants
+
+Satzoo="/home/emax/Program/Satzoo/satzoo"
+Time="/tmp/lava-proof-time-$$"
+
+#----------------------------------------------------------------
+#- Running Satzoo
+
+satzoo_()
+{
+  time $Satzoo $Args $File 2> $Time
+}
+
+satzoo_ > $Output
+
+#----------------------------------------------------------------
+#- Time
+
+seconds()
+{
+  if [ "$ShowTime" = "yes" ]
+  then
+    echo "(t=$2) \c"
+  fi
+}
+
+seconds `tail -3 $Time`
+cat $Time >> $Output
+rm $Time 2> /dev/null
+
+#----------------------------------------------------------------
+#- Check Output
+
+if grep "UNSATISFIABLE" $Output > /dev/null
+then
+  #- VALID
+  exit 0
+else if grep "SATISFIABLE" $Output > /dev/null
+then
+  #- FALSIFIABLE
+  exit 2
+else
+  #- INDETERMINATE
+  exit 1
+fi; fi
+
+#----------------------------------------------------------------
+#- the end.
diff --git a/Scripts/smv.wrapper b/Scripts/smv.wrapper
new file mode 100644
--- /dev/null
+++ b/Scripts/smv.wrapper
@@ -0,0 +1,81 @@
+#!/bin/sh
+#----------------------------------------------------------------
+#- Wrapper for smv
+#- to be used by the Lava system
+#----------------------------------------------------------------
+
+#- This file gets `File' as an argument, and produces the file
+#- File.out, containing the output of prover.
+
+trap 'echo "(^C) \c"' INT
+
+#----------------------------------------------------------------
+#- Variables
+
+#- options
+
+cd "`dirname $1`"
+File="`echo $1 | sed s!.*/!!`"
+shift
+ShowTime="no"
+
+if [ "$1" = "-showTime" ]
+then
+  ShowTime="yes"
+  shift
+fi
+
+Args="$*"
+
+#- derived
+
+Output="$File.out"
+
+#- constants
+
+Smv="/home/emax/Program/SMV/bin/smv"
+Time="/tmp/lava-proof-time-$$"
+
+#----------------------------------------------------------------
+#- Running Smv
+
+smv_()
+{
+  /usr/bin/time $Smv $File $Args 2> $Time
+}
+
+smv_ > $Output
+
+#----------------------------------------------------------------
+#- Time
+
+seconds()
+{
+  if [ "$ShowTime" = "yes" ]
+  then
+    echo "(t=$2) \c"
+  fi
+}
+
+seconds `tail -3 $Time`
+cat $Time >> $Output
+rm $Time 2> /dev/null
+
+#----------------------------------------------------------------
+#- Check Output
+
+if grep "....false" $Output > /dev/null
+then
+  #- FALSIFIABLE
+  exit 2
+else if grep "....true" $Output > /dev/null
+then
+  #- VALID
+  exit 0
+else
+  #- INDETERMINATE
+  exit 1
+fi; fi
+
+#----------------------------------------------------------------
+#- the end.
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,3 @@
+#!/usr/bin/env runhaskell
+> import Distribution.Simple
+> main = defaultMain
diff --git a/Vhdl/lava.vhd b/Vhdl/lava.vhd
new file mode 100644
--- /dev/null
+++ b/Vhdl/lava.vhd
@@ -0,0 +1,178 @@
+---------------------------------------------------------------------
+-- Lava Gates
+---------------------------------------------------------------------
+-- Koen Claessen, koen@cs.chalmers.se, 20000323
+
+---------------------------------------------------------------------
+-- entity declarations
+
+entity
+  vdd
+is
+port
+  ( clk   : in bit
+  ; outp  : out bit
+  );
+end entity vdd;
+
+entity
+  gnd
+is
+port
+  ( clk   : in bit
+  ; outp  : out bit
+  );
+end entity gnd;
+
+entity
+  id
+is
+port
+  ( clk   : in bit
+  ; inp   : in bit
+  ; outp  : out bit
+  );
+end entity id;
+
+entity
+  inv
+is
+port
+  ( clk   : in bit
+  ; inp   : in bit
+  ; outp  : out bit
+  );
+end entity inv;
+
+entity
+  and2
+is
+port
+  ( clk   : in bit
+  ; inp_1 : in bit
+  ; inp_2 : in bit
+  ; outp  : out bit
+  );
+end entity and2;
+
+entity
+  or2
+is
+port
+  ( clk   : in bit
+  ; inp_1 : in bit
+  ; inp_2 : in bit
+  ; outp  : out bit
+  );
+end entity or2;
+
+entity
+  xor2
+is
+port
+  ( clk   : in bit
+  ; inp_1 : in bit
+  ; inp_2 : in bit
+  ; outp  : out bit
+  );
+end entity xor2;
+
+entity
+  delay
+is
+port
+  ( clk   : in bit
+  ; init  : in bit
+  ; inp   : in bit
+  ; outp  : out bit
+  );
+end entity delay;
+
+---------------------------------------------------------------------
+-- behavioral descriptions
+
+architecture
+  behavioral
+of
+  vdd
+is
+begin
+  outp <= '1';
+end;
+
+architecture
+  behavioral
+of
+  gnd
+is
+begin
+  outp <= '0';
+end;
+
+architecture
+  behavioral
+of
+  id
+is
+begin
+  outp <= inp;
+end;
+
+architecture
+  behavioral
+of
+  inv
+is
+begin
+  outp <= not inp;
+end;
+
+architecture
+  behavioral
+of
+  and2
+is
+begin
+  outp <= inp_1 and inp_2;
+end;
+
+architecture
+  behavioral
+of
+  or2
+is
+begin
+  outp <= inp_1 or inp_2;
+end;
+
+architecture
+  behavioral
+of
+  xor2
+is
+begin
+  outp <= inp_1 xor inp_2;
+end;
+
+architecture
+  behavioral
+of
+  delay
+is
+begin
+  latch : process is
+    variable state : bit;
+  begin
+    state := init;
+    loop
+      wait until clk = '1';
+      outp <= state;
+      state := inp;
+    end loop;
+  end process latch;
+end;
+
+---------------------------------------------------------------------
+-- the end.
+
+
diff --git a/chalmers-lava2000.cabal b/chalmers-lava2000.cabal
new file mode 100644
--- /dev/null
+++ b/chalmers-lava2000.cabal
@@ -0,0 +1,63 @@
+name:                chalmers-lava2000
+version:             1.0
+synopsis:            Hardware description library
+description:         Hardware description library
+category:            Hardware
+license:             BSD3
+license-file:        LICENSE
+copyright:           (c) 2008. Koen Claessen <koen@chalmers.se>
+author:              Koen Claessen <koen@chalmers.se>
+maintainer:          Emil Axelsson <emax@chalmers.se>
+cabal-version:       >= 1.2
+build-type:          Simple
+tested-with:         GHC ==6.8.3
+data-files:          README, INSTALL
+extra-source-files:  Vhdl/lava.vhd, Scripts/satzoo.wrapper, Scripts/smv.wrapper
+
+library
+    exposed-modules:
+                     Lava2000
+                     Lava2000.Arithmetic
+                     Lava2000.Captain
+                     Lava2000.Combinational
+                     Lava2000.ConstructiveAnalysis
+                     Lava2000.Eprover
+                     Lava2000.Error
+                     Lava2000.Fixit
+                     Lava2000.Generic
+                     Lava2000.HeerHugo
+                     Lava2000.IOBuffering
+                     Lava2000.Isc
+                     Lava2000.LavaDir
+                     Lava2000.LavaRandom
+                     Lava2000.Limmat
+                     Lava2000.Modoc
+                     Lava2000.MyST
+                     Lava2000.Netlist
+                     Lava2000.Operators
+                     Lava2000.Patterns
+                     Lava2000.Property
+                     Lava2000.Ref
+                     Lava2000.Retime
+                     Lava2000.Satnik
+                     Lava2000.Satzoo
+                     Lava2000.Sequent
+                     Lava2000.Sequential
+                     Lava2000.SequentialCircuits
+                     Lava2000.SequentialConstructive
+                     Lava2000.Signal
+                     Lava2000.SignalTry
+                     Lava2000.Smv
+                     Lava2000.Stable
+                     Lava2000.Table
+                     Lava2000.Test
+                     Lava2000.Verification
+                     Lava2000.Vhdl
+                     Lava2000.Vis
+                     Lava2000.Zchaff
+
+    build-Depends:   base, haskell98, process
+
+    extensions:      Rank2Types, ExistentialQuantification
+    ghc-options:     -fno-warn-overlapping-patterns -fno-warn-missing-methods
+