chalmers-lava2000 1.0.2 → 1.1.0

raw patch · 82 files changed

+5274/−5284 lines, 82 filesdep ~basedep ~haskell98dep ~processPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, haskell98, process

API changes (from Hackage documentation)

Files

• Lava.hs +36/−0
• Lava/Arithmetic.hs +66/−0
• Lava/Captain.hs +151/−0
• Lava/Combinational.hs +39/−0
• Lava/ConstructiveAnalysis.hs +113/−0
• Lava/Eprover.hs +154/−0
• Lava/Error.hs +47/−0
• Lava/Fixit.hs +133/−0
• Lava/Generic.hs +420/−0
• Lava/HeerHugo.hs +144/−0
• Lava/IOBuffering.hs +10/−0
• Lava/Isc.hs +173/−0
• Lava/LavaDir.hs +7/−0
• Lava/LavaRandom.hs +18/−0
• Lava/Limmat.hs +150/−0
• Lava/Modoc.hs +150/−0
• Lava/MyST.hs +62/−0
• Lava/Netlist.hs +60/−0
• Lava/Operators.hs +96/−0
• Lava/Patterns.hs +96/−0
• Lava/Property.hs +399/−0
• Lava/Ref.hs +181/−0
• Lava/Retime.hs +59/−0
• Lava/Satnik.hs +150/−0
• Lava/Satzoo.hs +150/−0
• Lava/Sequent.hs +18/−0
• Lava/Sequential.hs +137/−0
• Lava/SequentialCircuits.hs +68/−0
• Lava/SequentialConstructive.hs +173/−0
• Lava/Signal.hs +350/−0
• Lava/SignalTry.hs +15/−0
• Lava/Smv.hs +155/−0
• Lava/Stable.hs +60/−0
• Lava/Table.hs +72/−0
• Lava/Test.hs +23/−0
• Lava/Verification.hs +475/−0
• Lava/Vhdl.hs +199/−0
• Lava/Vis.hs +265/−0
• Lava/Zchaff.hs +150/−0
• Lava2000.hs +0/−36
• Lava2000/Arithmetic.hs +0/−66
• Lava2000/Captain.hs +0/−151
• Lava2000/Combinational.hs +0/−39
• Lava2000/ConstructiveAnalysis.hs +0/−113
• Lava2000/Eprover.hs +0/−154
• Lava2000/Error.hs +0/−47
• Lava2000/Fixit.hs +0/−133
• Lava2000/Generic.hs +0/−420
• Lava2000/HeerHugo.hs +0/−144
• Lava2000/IOBuffering.hs +0/−10
• Lava2000/Isc.hs +0/−173
• Lava2000/LavaDir.hs +0/−16
• Lava2000/LavaRandom.hs +0/−18
• Lava2000/Limmat.hs +0/−150
• Lava2000/Modoc.hs +0/−150
• Lava2000/MyST.hs +0/−62
• Lava2000/Netlist.hs +0/−60
• Lava2000/Operators.hs +0/−96
• Lava2000/Patterns.hs +0/−96
• Lava2000/Property.hs +0/−399
• Lava2000/Ref.hs +0/−181
• Lava2000/Retime.hs +0/−59
• Lava2000/Satnik.hs +0/−150
• Lava2000/Satzoo.hs +0/−150
• Lava2000/Sequent.hs +0/−18
• Lava2000/Sequential.hs +0/−137
• Lava2000/SequentialCircuits.hs +0/−68
• Lava2000/SequentialConstructive.hs +0/−173
• Lava2000/Signal.hs +0/−350
• Lava2000/SignalTry.hs +0/−15
• Lava2000/Smv.hs +0/−155
• Lava2000/Stable.hs +0/−60
• Lava2000/Table.hs +0/−72
• Lava2000/Test.hs +0/−23
• Lava2000/Verification.hs +0/−475
• Lava2000/Vhdl.hs +0/−199
• Lava2000/Vis.hs +0/−265
• Lava2000/Zchaff.hs +0/−150
• README +3/−4
• Scripts/satzoo.wrapper +1/−2
• Scripts/smv.wrapper +1/−2
• chalmers-lava2000.cabal +45/−43

@@ -0,0 +1,36 @@+module Lava+  ( module Lava.Signal+  , module Lava.Generic+  , module Lava.Operators+  , module Lava.Combinational+  , module Lava.Sequential+  , module Lava.SequentialConstructive+  , module Lava.ConstructiveAnalysis+  , module Lava.Test+  , module Lava.Verification+  , module Lava.Vis+  , module Lava.Fixit+  , module Lava.Smv+  , module Lava.Satzoo+  , module Lava.Property+  , module Lava.Retime+  , module Lava.Vhdl+  )+ where++import Lava.Signal+import Lava.Generic+import Lava.Operators+import Lava.Combinational+import Lava.Sequential+import Lava.SequentialConstructive+import Lava.ConstructiveAnalysis+import Lava.Test+import Lava.Verification+import Lava.Vis+import Lava.Fixit+import Lava.Smv+import Lava.Satzoo+import Lava.Property+import Lava.Retime+import Lava.Vhdl

@@ -0,0 +1,66 @@+module Lava.Arithmetic where++import Lava+import Lava.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.++

@@ -0,0 +1,151 @@+module Lava.Captain+  ( captain+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava.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.+

@@ -0,0 +1,39 @@+module Lava.Combinational where++import Lava.Ref+import Lava.Generic+import Lava.Signal+import Lava.Netlist+import Lava.Sequent+import Lava.Error++import Lava.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 Lava.Error.CombinationalLoop)++  define r s =+    do s' <- mmap readSTRef s+       writeSTRef r (eval s')++----------------------------------------------------------------+-- the end.+

@@ -0,0 +1,113 @@+module Lava.ConstructiveAnalysis where++import Lava.Signal+import Lava.Operators+import Lava.Error+import Lava.Generic+import Lava.Sequent+import Lava.Ref++import Lava.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.+

@@ -0,0 +1,154 @@+module Lava.Eprover+  ( eprover+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStrLn+  , hClose+  , try+  )++import Lava.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 Lava\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 Lava.Error.DelayEval+                  DelayInt  x y -> wrong Lava.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.+

@@ -0,0 +1,47 @@+module Lava.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.+

@@ -0,0 +1,133 @@+module Lava.Fixit+  ( fixit+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava.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.+

@@ -0,0 +1,420 @@+module Lava.Generic where++import Lava.Signal+import Lava.Sequent+import Lava.Error++import Lava.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 Lava.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 Lava.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 Lava.Error.IncompatibleStructures+  safe f xs = f xs++----------------------------------------------------------------+-- the end.+

@@ -0,0 +1,144 @@+module Lava.HeerHugo+  ( heerhugo+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , ""+       , "( 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 Lava.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.+

@@ -0,0 +1,10 @@+module Lava.IOBuffering where++import IO+  ( hSetBuffering+  , stdout+  , BufferMode(..)+  )++noBuffering :: IO ()+noBuffering = hSetBuffering stdout NoBuffering

@@ -0,0 +1,173 @@+module Lava.Isc+ ( IscMethod(..)+ , isc+ , iscWith+ ) where++import Lava.Ref+import Lava.Signal+import Lava.Generic++import Lava.Property+import Lava.LavaDir+import Lava.Sequent+import Lava.Netlist+import Lava.Verification+import Lava.IOBuffering++import Array+import Lava.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+-}

@@ -0,0 +1,7 @@+module Lava.LavaDir where++import Paths_chalmers_lava2000++getLavaDir :: IO FilePath+getLavaDir = getDataDir+

@@ -0,0 +1,18 @@+module Lava.LavaRandom+  ( Rnd+  , newRnd+  , next+  , split+  )+ where++import Random+  ( StdGen+  , newStdGen+  , next+  , split+  )++type Rnd = StdGen++newRnd = newStdGen

@@ -0,0 +1,150 @@+module Lava.Limmat+  ( limmat+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , "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 Lava.Error.DelayEval+             _             -> wrong Lava.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.+

@@ -0,0 +1,150 @@+module Lava.Modoc+  ( modoc+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , "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 Lava.Error.DelayEval+             _             -> wrong Lava.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.+

@@ -0,0 +1,62 @@+module Lava.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+

@@ -0,0 +1,60 @@+module Lava.Netlist+  ( netlist+  , netlistIO+  , netlistST+  )+ where++import Lava.Ref+import Lava.Signal+import Lava.Generic+import Lava.Sequent++import Lava.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.+

@@ -0,0 +1,96 @@+module Lava.Operators where++import Lava.Signal+import Lava.Generic+import Lava.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 Lava.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.+

@@ -0,0 +1,96 @@+module Lava.Patterns where++import Lava++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.+

@@ -0,0 +1,399 @@+module Lava.Property+  ( Gen+  , generate+  , ChoiceWithSig+  , Fresh(..)+  , CoFresh(..)+  , double+  , triple+  , list+  , listOf+  , results+  , sequential+  , forAll+  , Property(..)+  , Checkable(..)+  , ShowModel(..)+  , Model+  , properties+  )+ where++import Lava.Signal+import Lava.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.+

@@ -0,0 +1,181 @@+module Lava.Ref+  ( Ref+  , ref+  , deref+  , memoRef++  , TableIO+  , tableIO+  , extendIO+  , findIO+  , memoRefIO++  , TableST+  , tableST+  , extendST+  , findST+  , memoRefST+  )+ where++import Lava.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.+++

@@ -0,0 +1,59 @@+module Lava.Retime+  ( timeTransform+  )+ where++import Lava.Signal+import Lava.Generic+import Lava.Sequent+import Lava.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.+

@@ -0,0 +1,150 @@+module Lava.Satnik+  ( satnik+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , "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 Lava.Error.DelayEval+             _             -> wrong Lava.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.+

@@ -0,0 +1,150 @@+module Lava.Satzoo+  ( satzoo+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , "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 Lava.Error.DelayEval+             _             -> wrong Lava.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.+

@@ -0,0 +1,18 @@+module Lava.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.++

@@ -0,0 +1,137 @@+module Lava.Sequential+  ( simulateSeq+  )+ where++import Lava.Ref+import Lava.Signal+import Lava.Netlist+import Lava.Sequent+import Lava.Generic++import Lava.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.+

@@ -0,0 +1,68 @@+module Lava.SequentialCircuits where++import Lava++----------------------------------------------------------------+-- 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.++

@@ -0,0 +1,173 @@+module Lava.SequentialConstructive+  ( simulateCon+  )+ where++import Lava.Ref+import Lava.Signal+import Lava.Netlist+import Lava.Sequent+import Lava.Generic+import Lava.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 Lava.Error.UndefinedWire++        updateWire rwire time v =+          do wire <- readIORef rwire+             mv   <- valueWire rwire time+             case mv of+               Just v' | v =/= v'  -> wrong Lava.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.+

@@ -0,0 +1,350 @@+module Lava.Signal where++import Lava.Ref+import Lava.Sequent+import Lava.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 Lava.Error.DelayEval+    DelayInt  s s' -> wrong Lava.Error.DelayEval+    VarBool   s    -> wrong Lava.Error.VarEval+    VarInt    s    -> wrong Lava.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.+

@@ -0,0 +1,15 @@+module Lava.SignalTry where++import Lava.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] []))

@@ -0,0 +1,155 @@+module Lava.Smv+  ( smv+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , ""+       , "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 Lava.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.+

@@ -0,0 +1,60 @@+module Lava.Stable where++import Lava.Signal+import Lava.Operators+import Lava.Generic+import Lava.Sequent+import Lava.Ref++import Lava.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.+

@@ -0,0 +1,72 @@+module Lava.Table+  ( table+  , tableProp+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.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.+

@@ -0,0 +1,23 @@+module Lava.Test where++import Lava.Signal+import Lava.Sequential+import Lava.Generic++import Lava.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.+

@@ -0,0 +1,475 @@+module Lava.Verification+  ( Option(..)+  , verify+  , verifyWith+  , ProofResult(..)+  , verifyDir+  , checkVerifyDir+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir++import List+  ( intersperse+  , isPrefixOf+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava.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.+

@@ -0,0 +1,199 @@+module Lava.Vhdl+  ( writeVhdl+  , writeVhdlInput+  , writeVhdlInputOutput+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Error+import Lava.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 Lava.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.+

@@ -0,0 +1,265 @@+module Lava.Vis+  ( vis+  , writeVis+  , writeVisInput+  , writeVisInputOutput+  , equivCheckVisInput+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava.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.+

@@ -0,0 +1,150 @@+module Lava.Zchaff+  ( zchaff+  )+ where++import Lava.Signal+import Lava.Netlist+import Lava.Generic+import Lava.Sequent+import Lava.Property+import Lava.Error+import Lava.LavaDir+import Lava.Verification++import List+  ( intersperse+  , nub+  )++import IO+  ( openFile+  , IOMode(..)+  , hPutStr+  , hClose+  )++import Lava.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 Lava"+       , "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 Lava.Error.DelayEval+             _             -> wrong Lava.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.+

@@ -1,36 +0,0 @@-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

@@ -1,66 +0,0 @@-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.--

@@ -1,151 +0,0 @@-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.-

@@ -1,39 +0,0 @@-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.-

@@ -1,113 +0,0 @@-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.-

@@ -1,154 +0,0 @@-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.-

@@ -1,47 +0,0 @@-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.-

@@ -1,133 +0,0 @@-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.-

@@ -1,420 +0,0 @@-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.-

@@ -1,144 +0,0 @@-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.-

@@ -1,10 +0,0 @@-module Lava2000.IOBuffering where--import IO-  ( hSetBuffering-  , stdout-  , BufferMode(..)-  )--noBuffering :: IO ()-noBuffering = hSetBuffering stdout NoBuffering

@@ -1,173 +0,0 @@-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--}

@@ -1,16 +0,0 @@-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

@@ -1,18 +0,0 @@-module Lava2000.LavaRandom-  ( Rnd-  , newRnd-  , next-  , split-  )- where--import Random-  ( StdGen-  , newStdGen-  , next-  , split-  )--type Rnd = StdGen--newRnd = newStdGen

@@ -1,150 +0,0 @@-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.-