diff --git a/Lava.hs b/Lava.hs new file mode 100644 --- /dev/null +++ b/Lava.hs @@ -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 diff --git a/Lava/Arithmetic.hs b/Lava/Arithmetic.hs new file mode 100644 --- /dev/null +++ b/Lava/Arithmetic.hs @@ -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. + + diff --git a/Lava/Captain.hs b/Lava/Captain.hs new file mode 100644 --- /dev/null +++ b/Lava/Captain.hs @@ -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. + diff --git a/Lava/Combinational.hs b/Lava/Combinational.hs new file mode 100644 --- /dev/null +++ b/Lava/Combinational.hs @@ -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. + diff --git a/Lava/ConstructiveAnalysis.hs b/Lava/ConstructiveAnalysis.hs new file mode 100644 --- /dev/null +++ b/Lava/ConstructiveAnalysis.hs @@ -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. + diff --git a/Lava/Eprover.hs b/Lava/Eprover.hs new file mode 100644 --- /dev/null +++ b/Lava/Eprover.hs @@ -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. + diff --git a/Lava/Error.hs b/Lava/Error.hs new file mode 100644 --- /dev/null +++ b/Lava/Error.hs @@ -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. + diff --git a/Lava/Fixit.hs b/Lava/Fixit.hs new file mode 100644 --- /dev/null +++ b/Lava/Fixit.hs @@ -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. + diff --git a/Lava/Generic.hs b/Lava/Generic.hs new file mode 100644 --- /dev/null +++ b/Lava/Generic.hs @@ -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. + diff --git a/Lava/HeerHugo.hs b/Lava/HeerHugo.hs new file mode 100644 --- /dev/null +++ b/Lava/HeerHugo.hs @@ -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. + diff --git a/Lava/IOBuffering.hs b/Lava/IOBuffering.hs new file mode 100644 --- /dev/null +++ b/Lava/IOBuffering.hs @@ -0,0 +1,10 @@ +module Lava.IOBuffering where + +import IO + ( hSetBuffering + , stdout + , BufferMode(..) + ) + +noBuffering :: IO () +noBuffering = hSetBuffering stdout NoBuffering diff --git a/Lava/Isc.hs b/Lava/Isc.hs new file mode 100644 --- /dev/null +++ b/Lava/Isc.hs @@ -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 +-} diff --git a/Lava/LavaDir.hs b/Lava/LavaDir.hs new file mode 100644 --- /dev/null +++ b/Lava/LavaDir.hs @@ -0,0 +1,7 @@ +module Lava.LavaDir where + +import Paths_chalmers_lava2000 + +getLavaDir :: IO FilePath +getLavaDir = getDataDir + diff --git a/Lava/LavaRandom.hs b/Lava/LavaRandom.hs new file mode 100644 --- /dev/null +++ b/Lava/LavaRandom.hs @@ -0,0 +1,18 @@ +module Lava.LavaRandom + ( Rnd + , newRnd + , next + , split + ) + where + +import Random + ( StdGen + , newStdGen + , next + , split + ) + +type Rnd = StdGen + +newRnd = newStdGen diff --git a/Lava/Limmat.hs b/Lava/Limmat.hs new file mode 100644 --- /dev/null +++ b/Lava/Limmat.hs @@ -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. + diff --git a/Lava/Modoc.hs b/Lava/Modoc.hs new file mode 100644 --- /dev/null +++ b/Lava/Modoc.hs @@ -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. + diff --git a/Lava/MyST.hs b/Lava/MyST.hs new file mode 100644 --- /dev/null +++ b/Lava/MyST.hs @@ -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 + diff --git a/Lava/Netlist.hs b/Lava/Netlist.hs new file mode 100644 --- /dev/null +++ b/Lava/Netlist.hs @@ -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. + diff --git a/Lava/Operators.hs b/Lava/Operators.hs new file mode 100644 --- /dev/null +++ b/Lava/Operators.hs @@ -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. + diff --git a/Lava/Patterns.hs b/Lava/Patterns.hs new file mode 100644 --- /dev/null +++ b/Lava/Patterns.hs @@ -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. + diff --git a/Lava/Property.hs b/Lava/Property.hs new file mode 100644 --- /dev/null +++ b/Lava/Property.hs @@ -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. + diff --git a/Lava/Ref.hs b/Lava/Ref.hs new file mode 100644 --- /dev/null +++ b/Lava/Ref.hs @@ -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. + + + diff --git a/Lava/Retime.hs b/Lava/Retime.hs new file mode 100644 --- /dev/null +++ b/Lava/Retime.hs @@ -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. + diff --git a/Lava/Satnik.hs b/Lava/Satnik.hs new file mode 100644 --- /dev/null +++ b/Lava/Satnik.hs @@ -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. + diff --git a/Lava/Satzoo.hs b/Lava/Satzoo.hs new file mode 100644 --- /dev/null +++ b/Lava/Satzoo.hs @@ -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. + diff --git a/Lava/Sequent.hs b/Lava/Sequent.hs new file mode 100644 --- /dev/null +++ b/Lava/Sequent.hs @@ -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. + + diff --git a/Lava/Sequential.hs b/Lava/Sequential.hs new file mode 100644 --- /dev/null +++ b/Lava/Sequential.hs @@ -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. + diff --git a/Lava/SequentialCircuits.hs b/Lava/SequentialCircuits.hs new file mode 100644 --- /dev/null +++ b/Lava/SequentialCircuits.hs @@ -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. + + diff --git a/Lava/SequentialConstructive.hs b/Lava/SequentialConstructive.hs new file mode 100644 --- /dev/null +++ b/Lava/SequentialConstructive.hs @@ -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. + diff --git a/Lava/Signal.hs b/Lava/Signal.hs new file mode 100644 --- /dev/null +++ b/Lava/Signal.hs @@ -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 "<>" + +---------------------------------------------------------------- +-- the end. + diff --git a/Lava/SignalTry.hs b/Lava/SignalTry.hs new file mode 100644 --- /dev/null +++ b/Lava/SignalTry.hs @@ -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] [])) diff --git a/Lava/Smv.hs b/Lava/Smv.hs new file mode 100644 --- /dev/null +++ b/Lava/Smv.hs @@ -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. + diff --git a/Lava/Stable.hs b/Lava/Stable.hs new file mode 100644 --- /dev/null +++ b/Lava/Stable.hs @@ -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. + diff --git a/Lava/Table.hs b/Lava/Table.hs new file mode 100644 --- /dev/null +++ b/Lava/Table.hs @@ -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. + diff --git a/Lava/Test.hs b/Lava/Test.hs new file mode 100644 --- /dev/null +++ b/Lava/Test.hs @@ -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. + diff --git a/Lava/Verification.hs b/Lava/Verification.hs new file mode 100644 --- /dev/null +++ b/Lava/Verification.hs @@ -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. + diff --git a/Lava/Vhdl.hs b/Lava/Vhdl.hs new file mode 100644 --- /dev/null +++ b/Lava/Vhdl.hs @@ -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. + diff --git a/Lava/Vis.hs b/Lava/Vis.hs new file mode 100644 --- /dev/null +++ b/Lava/Vis.hs @@ -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. + diff --git a/Lava/Zchaff.hs b/Lava/Zchaff.hs new file mode 100644 --- /dev/null +++ b/Lava/Zchaff.hs @@ -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. + diff --git a/Lava2000.hs b/Lava2000.hs deleted file mode 100644 --- a/Lava2000.hs +++ /dev/null @@ -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 diff --git a/Lava2000/Arithmetic.hs b/Lava2000/Arithmetic.hs deleted file mode 100644 --- a/Lava2000/Arithmetic.hs +++ /dev/null @@ -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. - - diff --git a/Lava2000/Captain.hs b/Lava2000/Captain.hs deleted file mode 100644 --- a/Lava2000/Captain.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Combinational.hs b/Lava2000/Combinational.hs deleted file mode 100644 --- a/Lava2000/Combinational.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/ConstructiveAnalysis.hs b/Lava2000/ConstructiveAnalysis.hs deleted file mode 100644 --- a/Lava2000/ConstructiveAnalysis.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Eprover.hs b/Lava2000/Eprover.hs deleted file mode 100644 --- a/Lava2000/Eprover.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Error.hs b/Lava2000/Error.hs deleted file mode 100644 --- a/Lava2000/Error.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Fixit.hs b/Lava2000/Fixit.hs deleted file mode 100644 --- a/Lava2000/Fixit.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Generic.hs b/Lava2000/Generic.hs deleted file mode 100644 --- a/Lava2000/Generic.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/HeerHugo.hs b/Lava2000/HeerHugo.hs deleted file mode 100644 --- a/Lava2000/HeerHugo.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/IOBuffering.hs b/Lava2000/IOBuffering.hs deleted file mode 100644 --- a/Lava2000/IOBuffering.hs +++ /dev/null @@ -1,10 +0,0 @@ -module Lava2000.IOBuffering where - -import IO - ( hSetBuffering - , stdout - , BufferMode(..) - ) - -noBuffering :: IO () -noBuffering = hSetBuffering stdout NoBuffering diff --git a/Lava2000/Isc.hs b/Lava2000/Isc.hs deleted file mode 100644 --- a/Lava2000/Isc.hs +++ /dev/null @@ -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 --} diff --git a/Lava2000/LavaDir.hs b/Lava2000/LavaDir.hs deleted file mode 100644 --- a/Lava2000/LavaDir.hs +++ /dev/null @@ -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 diff --git a/Lava2000/LavaRandom.hs b/Lava2000/LavaRandom.hs deleted file mode 100644 --- a/Lava2000/LavaRandom.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Lava2000.LavaRandom - ( Rnd - , newRnd - , next - , split - ) - where - -import Random - ( StdGen - , newStdGen - , next - , split - ) - -type Rnd = StdGen - -newRnd = newStdGen diff --git a/Lava2000/Limmat.hs b/Lava2000/Limmat.hs deleted file mode 100644 --- a/Lava2000/Limmat.hs +++ /dev/null @@ -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. - diff --git a/Lava2000/Modoc.hs b/Lava2000/Modoc.hs deleted file mode 100644 --- a/Lava2000/Modoc.hs +++ /dev/null @@ -1,150 +0,0 @@ -module Lava2000.Modoc - ( modoc - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- modoc - -modoc :: Checkable a => a -> IO ProofResult -modoc a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile (writeDefinitions defsFile props) - where - defsFile = verifyDir ++ "/circuit.cnf" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO () -writeDefinitions file props = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - cls <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "c Generated by Lava2000" - , "c " - ] - - let new = - do n <- readIORef var - let n' = n+1 - writeIORef var n' - return n' - - clause xs = - do n <- readIORef cls - let n' = n+1 in n' `seq` writeIORef cls n' - hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n") - - define v s = - case s of - Bool True -> clause [ v ] - Bool False -> clause [ -v ] - Inv x -> clause [ -x, -v ] >> clause [ x, v ] - - And [] -> define v (Bool True) - And xs -> conjunction v xs - - Or [] -> define v (Bool False) - Or xs -> conjunction (-v) (map negate xs) - - Xor [] -> define v (Bool False) - Xor xs -> exactly1 v xs - - VarBool s -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n") - - DelayBool x y -> wrong Lava2000.Error.DelayEval - _ -> wrong Lava2000.Error.NoArithmetic - where - - conjunction v xs = - do clause (v : map negate xs) - sequence_ [ clause [ -v, x ] | x <- xs ] - - exactly1 v xs = - do clause (-v : xs) - sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ] - sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ] - - pairs [] = [] - pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs - - pick [] = [] - pick (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ] - - outvs <- netlistIO new define (struct props) - clause (map negate (flatten outvs)) - - nvar <- readIORef var - ncls <- readIORef cls - hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n") - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - firstFile = file ++ "-1" - secondFile = file ++ "-2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Modoc: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/modoc.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/MyST.hs b/Lava2000/MyST.hs deleted file mode 100644 --- a/Lava2000/MyST.hs +++ /dev/null @@ -1,62 +0,0 @@ -module Lava2000.MyST - ( ST - , STRef - , newSTRef - , readSTRef - , writeSTRef - , runST - , fixST - - , unsafePerformST - , unsafeInterleaveST - , unsafeIOtoST - ) - where - -import System.IO -import System.IO.Unsafe -import Data.IORef - -newtype ST s a - = ST (IO a) - -unST :: ST s a -> IO a -unST (ST io) = io - -instance Functor (ST s) where - fmap f (ST io) = ST (fmap f io) - -instance Monad (ST s) where - return a = ST (return a) - ST io >>= k = ST (do a <- io ; unST (k a)) - -newtype STRef s a - = STRef (IORef a) - -instance Eq (STRef s a) where - STRef r1 == STRef r2 = r1 == r2 - -newSTRef :: a -> ST s (STRef s a) -newSTRef a = ST (STRef `fmap` newIORef a) - -readSTRef :: STRef s a -> ST s a -readSTRef (STRef r) = ST (readIORef r) - -writeSTRef :: STRef s a -> a -> ST s () -writeSTRef (STRef r) a = ST (writeIORef r a) - -runST :: (forall s . ST s a) -> a -runST st = unsafePerformST st - -fixST :: (a -> ST s a) -> ST s a -fixST f = ST (fixIO (unST . f)) - -unsafePerformST :: ST s a -> a -unsafePerformST (ST io) = unsafePerformIO io - -unsafeInterleaveST :: ST s a -> ST s a -unsafeInterleaveST (ST io) = ST (unsafeInterleaveIO io) - -unsafeIOtoST :: IO a -> ST s a -unsafeIOtoST = ST - diff --git a/Lava2000/Netlist.hs b/Lava2000/Netlist.hs deleted file mode 100644 --- a/Lava2000/Netlist.hs +++ /dev/null @@ -1,60 +0,0 @@ -module Lava2000.Netlist - ( netlist - , netlistIO - , netlistST - ) - where - -import Lava2000.Ref -import Lava2000.Signal -import Lava2000.Generic -import Lava2000.Sequent - -import Lava2000.MyST - ( ST - ) - ----------------------------------------------------------------- --- netlist - -netlist :: Functor f => (S a -> a) -> f Symbol -> f a -netlist phi symbols = fmap cata symbols - where - cata (Symbol sym) = cata' sym - cata' = memoRef (phi . fmap cata . deref) - -netlistIO :: Sequent f => IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v) -netlistIO new define symbols = - do tab <- tableIO - - let gather (Symbol sym) = - do visited <- findIO tab sym - case visited of - Just v -> do return v - Nothing -> do v <- new - extendIO tab sym v - s <- mmap gather (deref sym) - define v s - return v - - in mmap gather symbols - -netlistST :: Sequent f => ST s v -> (v -> S v -> ST s ()) -> f Symbol -> ST s (f v) -netlistST new define symbols = - do tab <- tableST - - let gather (Symbol sym) = - do visited <- findST tab sym - case visited of - Just v -> do return v - Nothing -> do v <- new - extendST tab sym v - s <- mmap gather (deref sym) - define v s - return v - - in mmap gather symbols - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Operators.hs b/Lava2000/Operators.hs deleted file mode 100644 --- a/Lava2000/Operators.hs +++ /dev/null @@ -1,96 +0,0 @@ -module Lava2000.Operators where - -import Lava2000.Signal -import Lava2000.Generic -import Lava2000.Error - -infix 4 <==> -infixr 3 <&> -infixr 2 <|>, ==>, <== -infixr 2 <=>, <#> -infixr 1 |-> - ----------------------------------------------------------------------- --- Gates - -and2 (x, y) = andl [x, y] -or2 (x, y) = orl [x, y] -xor2 (x, y) = xorl [x, y] - -nand2 = inv . and2 -nor2 = inv . or2 -xnor2 = inv . xor2 - -equiv (x, y) = xnor2 (x, y) -impl (x, y) = or2 (inv x, y) - -nandl = inv . andl -norl = inv . orl - -plus (x, y) = plusl [x,y] -sub (x, y) = plusl [x, neg y] -times (x, y) = timesl [x, y] -imod (x, y) = modulo x y -idiv (x, y) = divide x y - ----------------------------------------------------------------------- --- Binary Operators - -x |-> y = delay x y -x <==> y = equal (x, y) - -x <&> y = and2 (x, y) -x <|> y = or2 (x, y) -x <#> y = xor2 (x, y) -x <=> y = equiv (x, y) -x ==> y = impl (x, y) -x <== y = impl (y, x) - -x %% y = imod (x, y) -gte (x, y) = gteInt x y -x >>== y = gte (x, y) - -imin (x, y) = ifThenElse (x >>== y) (y, x) -imax (x, y) = ifThenElse (x >>== y) (x, y) - -class SignalInt a where - toSignalInt :: Signal a -> Signal Int - fromSignalInt :: Signal Int -> Signal a - -instance SignalInt Int where - toSignalInt = id - fromSignalInt = id - -instance SignalInt a => Num (Signal a) where - x + y = fromSignalInt $ plus (toSignalInt x, toSignalInt y) - x - y = fromSignalInt $ sub (toSignalInt x, toSignalInt y) - x * y = fromSignalInt $ times (toSignalInt x, toSignalInt y) - negate x = fromSignalInt $ neg (toSignalInt x) - - fromInteger = fromSignalInt . int . fromInteger - -instance SignalInt a => Fractional (Signal a) where - x / y = fromSignalInt $ idiv (toSignalInt x, toSignalInt y) - -instance SignalInt a => Enum (Signal a) where - toEnum n = fromSignalInt (int n) - fromEnum (Signal s) = - case unsymbol s of - Int n -> n - _ -> wrong Lava2000.Error.EnumOnSymbols - -instance SignalInt a => Ord (Signal a) where - min x y = fromSignalInt $ imin (toSignalInt x, toSignalInt y) - max x y = fromSignalInt $ imax (toSignalInt x, toSignalInt y) - - - ----------------------------------------------------------------------- --- Convert - -int2bit n = n <==> (1 :: Signal Int) -bit2int b = ifThenElse b (1 :: Signal Int, 0) - ----------------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Patterns.hs b/Lava2000/Patterns.hs deleted file mode 100644 --- a/Lava2000/Patterns.hs +++ /dev/null @@ -1,96 +0,0 @@ -module Lava2000.Patterns where - -import Lava2000 - -infixr 5 ->- -infixr 4 -|- - -{- -This Lava module defines some often used wiring circuits -and connection patterns. --} - ----------------------------------------------------------------- --- Wiring Circuits - -swap (a,b) = (b,a) -swapl [a,b] = [b,a] - -copy a = (a,a) - -riffle = halveList ->- zipp ->- unpair -unriffle = pair ->- unzipp ->- append - -zipp ([], []) = [] -zipp (a:as, b:bs) = (a,b) : zipp (as, bs) - -unzipp [] = ([], []) -unzipp ((a,b):abs) = (a:as, b:bs) - where - (as, bs) = unzipp abs - -pair (x:y:xs) = (x,y) : pair xs -pair xs = [] - -unpair ((x,y):xys) = x : y : unpair xys -unpair [] = [] - -halveList inps = (left,right) - where - left = take half inps - right = drop half inps - half = length inps `div` 2 - -append (a,b) = a ++ b - ----------------------------------------------------------------- --- Connection Patterns - -serial circ1 circ2 = circ2 . circ1 -circ1 ->- circ2 = serial circ1 circ2 - -compose [] = id -compose (circ:circs) = circ ->- compose circs - -composeN n circ = compose (replicate n circ) - -par circ1 circ2 (a, b) = (circ1 a, circ2 b) -circ1 -|- circ2 = par circ1 circ2 - -parl circ1 circ2 = halveList ->- (circ1 -|- circ2) ->- append - - -two circ = parl circ circ -ilv circ = unriffle ->- two circ ->- riffle - -iter 0 comb circ = circ -iter n comb circ = comb (iter (n-1) comb circ) - -twoN n circ = iter n two circ -ilvN n circ = iter n ilv circ - -bfly 0 circ = id -bfly n circ = ilv (bfly (n-1) circ) ->- twoN (n-1) circ - -pmap circ = pair ->- map circ ->- unpair - -tri circ [] = [] -tri circ (inp:inps) = inp : (map circ ->- tri circ) inps - -mirror circ (a, b) = (c, d) - where - (d, c) = circ (b, a) - -row circ (carryIn, []) = ([], carryIn) -row circ (carryIn, a:as) = (b:bs, carryOut) - where - (b, carry) = circ (carryIn, a) - (bs, carryOut) = row circ (carry, as) - -column circ = mirror (row (mirror circ)) - -grid circ = row (column circ) - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Property.hs b/Lava2000/Property.hs deleted file mode 100644 --- a/Lava2000/Property.hs +++ /dev/null @@ -1,399 +0,0 @@ -module Lava2000.Property - ( Gen - , generate - , ChoiceWithSig - , Fresh(..) - , CoFresh(..) - , double - , triple - , list - , listOf - , results - , sequential - , forAll - , Property(..) - , Checkable(..) - , ShowModel(..) - , Model - , properties - ) - where - -import Lava2000.Signal -import Lava2000.Generic - -import Monad - ( liftM2 - , liftM3 - , liftM4 - , liftM5 - ) - -import List - ( intersperse - , transpose - ) - -import Data.IORef -import System.IO.Unsafe - ----------------------------------------------------------------- --- Gen Monad - -newtype Gen a - = Gen (Tree Int -> a) - -instance Functor Gen where - fmap f (Gen m) = Gen (\t -> f (m t)) - -instance Monad Gen where - return a = - Gen (\t -> a) - - Gen m >>= k = - Gen (\(Fork _ t1 t2) -> let a = m t1 ; Gen m2 = k a in m2 t2) - -generate :: Gen a -> IO a -generate (Gen m) = - do t <- newTree - return (m t) - --- Gen Tree - -data Tree a - = Fork a (Tree a) (Tree a) - -newTree :: IO (Tree Int) -newTree = - do var <- newIORef 0 - tree var - where - tree var = unsafeInterleaveIO $ - do n <- new var - t1 <- tree var - t2 <- tree var - return (Fork n t1 t2) - - new var = unsafeInterleaveIO $ - do n <- readIORef var - let n' = n+1 - n' `seq` writeIORef var n' - return n - ----------------------------------------------------------------- --- Fresh - -class Fresh a where - fresh :: Gen a - -instance Fresh () where - fresh = return () - -instance ConstructiveSig a => Fresh (Signal a) where - fresh = Gen (\(Fork n _ _) -> varSig ("i" ++ show n)) - -instance (Fresh a, Fresh b) => Fresh (a,b) where - fresh = liftM2 (,) fresh fresh - -instance (Fresh a, Fresh b, Fresh c) => Fresh (a,b,c) where - fresh = liftM3 (,,) fresh fresh fresh - -instance (Fresh a, Fresh b, Fresh c, Fresh d) => Fresh (a,b,c,d) where - fresh = liftM4 (,,,) fresh fresh fresh fresh - -instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e) => Fresh (a,b,c,d,e) where - fresh = liftM5 (,,,,) fresh fresh fresh fresh fresh - -instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f) => Fresh (a,b,c,d,e,f) where - fresh = liftM6 (,,,,,) fresh fresh fresh fresh fresh fresh - -instance (Fresh a, Fresh b, Fresh c, Fresh d, Fresh e, Fresh f, Fresh g) => Fresh (a,b,c,d,e,f,g) where - fresh = liftM7 (,,,,,,) fresh fresh fresh fresh fresh fresh fresh - --- CoFresh - -class ChoiceWithSig a where - ifThenElseWithSig :: Choice b => Signal a -> (b, b) -> b - -class CoFresh a where - cofresh :: (Choice b, Fresh b) => Gen b -> Gen (a -> b) - -instance ChoiceWithSig Bool where - ifThenElseWithSig = ifThenElse - -instance CoFresh () where - cofresh gen = - do b <- gen - return (\_ -> b) - -instance ChoiceWithSig a => CoFresh (Signal a) where - cofresh gen = - do b1 <- gen - b2 <- gen - return (\a -> ifThenElseWithSig a (b1, b2)) - -instance (CoFresh a, CoFresh b) => CoFresh (a, b) where - cofresh gen = - do f <- cofresh (cofresh gen) - return (\(a, b) -> f a b) - -instance (CoFresh a, CoFresh b, CoFresh c) => CoFresh (a, b, c) where - cofresh gen = - do f <- cofresh (cofresh (cofresh gen)) - return (\(a, b, c) -> f a b c) - -instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d) => CoFresh (a, b, c, d) where - cofresh gen = - do f <- cofresh (cofresh (cofresh (cofresh gen))) - return (\(a, b, c, d) -> f a b c d) - -instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e) => CoFresh (a, b, c, d, e) where - cofresh gen = - do f <- cofresh (cofresh (cofresh (cofresh (cofresh gen)))) - return (\(a, b, c, d, e) -> f a b c d e) - -instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f) => CoFresh (a, b, c, d, e, f) where - cofresh gen = - do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen))))) - return (\(a, b, c, d, e, g) -> f a b c d e g) - -instance (CoFresh a, CoFresh b, CoFresh c, CoFresh d, CoFresh e, CoFresh f, CoFresh g) => CoFresh (a, b, c, d, e, f, g) where - cofresh gen = - do f <- cofresh (cofresh (cofresh (cofresh (cofresh (cofresh (cofresh gen)))))) - return (\(a, b, c, d, e, g, h) -> f a b c d e g h) - -instance (CoFresh a, Choice b, Fresh b) => Fresh (a -> b) where - fresh = cofresh fresh - -instance CoFresh a => CoFresh [a] where - cofresh gen = - do fs <- sequence [ cofreshList i gen | i <- [0..] ] - return (\as -> (fs !! length as) as) - -instance (Finite a, CoFresh b) => CoFresh (a -> b) where - cofresh gen = - do f <- cofresh gen - return (\g -> f (map g domain)) - -cofreshList :: (CoFresh a, Choice b, Fresh b) => Int -> Gen b -> Gen ([a] -> b) -cofreshList 0 gen = - do x <- gen - return (\[] -> x) - -cofreshList k gen = - do f <- cofreshList (k-1) (cofresh gen) - return (\(a:as) -> f as a) - ----------------------------------------------------------------- --- some combinators - -double :: Gen a -> Gen (a,a) -double gen = liftM2 (,) gen gen - -triple :: Gen a -> Gen (a,a,a) -triple gen = liftM3 (,,) gen gen gen - -list :: Fresh a => Int -> Gen [a] -list n = sequence [ fresh | i <- [1..n] ] - -listOf :: Int -> Gen a -> Gen [a] -listOf n gen = sequence [ gen | i <- [1..n] ] - ----------------------------------------------------------------- --- combinators for circuits - -results :: Int -> Gen (a -> b) -> Gen (a -> [b]) -results n gen = - do fs <- sequence [ gen | i <- [1..n] ] - return (\a -> map ($ a) fs) - -sequential :: (CoFresh a, Fresh b, Choice b) => Int -> Gen (a -> b) -sequential n = - do fb <- fresh - fstate <- results n fresh - let circ inp = (fb inp, fstate inp) - return (loop circ) - where - loop circ a = b - where - (b, state) = circ (a, delay (zeroList n) (state :: [Signal Bool])) - ----------------------------------------------------------------- --- checkable - -newtype Property - = P (Gen ([Signal Bool], Model -> [[String]])) - -class Checkable a where - property :: a -> Property - -instance Checkable Property where - property p = p - -instance Checkable Bool where - property b = property (bool b) - -instance Checkable a => Checkable (Signal a) where - property (Signal s) = P (return ([Signal s], \_ -> [])) - -instance Checkable a => Checkable [a] where - property as = P $ - do sms <- sequence [ gen | (P gen) <- map property as ] - return (concat (map fst sms), \model -> concat (map (($ model) . snd) sms)) - -instance Checkable a => Checkable (Gen a) where - property m = P (do a <- m ; let P m' = property a in m') - -instance (Fresh a, ShowModel a, Checkable b) => Checkable (a -> b) where - property f = forAll fresh f - ----------------------------------------------------------------- --- quantify - -type Model - = [(String, [String])] - -name :: Signal a -> String -name (Signal s) = - case unsymbol s of - VarBool v -> v - VarInt v -> v - _ -> error "no name" - -class ShowModel a where - showModel :: Model -> a -> [String] - -instance ShowModel (Signal a) where - showModel model sig = - case lookup (name sig) model of - Just xs -> xs - Nothing -> [] - -instance ShowModel () where - showModel model () = - ["()"] - -instance (ShowModel a, ShowModel b) => ShowModel (a, b) where - showModel model (a, b) = - zipWith' (\x y -> "(" ++ x ++ "," ++ y ++ ")") - (showModel model a) (showModel model b) - -instance (ShowModel a, ShowModel b, ShowModel c) => ShowModel (a, b, c) where - showModel model (a, b, c) = - zipWith3' (\x y z -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ ")") - (showModel model a) (showModel model b) (showModel model c) - -instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d) => ShowModel (a, b, c, d) where - showModel model (a, b, c, d) = - zipWith4' (\x y z v -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ ")") - (showModel model a) (showModel model b) (showModel model c) (showModel model d) - -instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e) => ShowModel (a, b, c, d, e) where - showModel model (a, b, c, d, e) = - zipWith5' (\x y z v w -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ ")") - (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) - -instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f) => ShowModel (a, b, c, d, e, f) where - showModel model (a, b, c, d, e, f) = - zipWith6' (\x y z v w p -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ ")") - (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model f) - -instance (ShowModel a, ShowModel b, ShowModel c, ShowModel d, ShowModel e, ShowModel f, ShowModel g) => ShowModel (a, b, c, d, e, f, g) where - showModel model (a, b, c, d, e, f, g) = - zipWith7' (\x y z v w p q -> "(" ++ x ++ "," ++ y ++ "," ++ z ++ "," ++ v ++ "," ++ w ++ "," ++ p ++ "," ++ q ++ ")") - (showModel model a) (showModel model b) (showModel model c) (showModel model d) (showModel model e) (showModel model f) (showModel model g) - -instance ShowModel a => ShowModel [a] where - showModel model as = - map (\xs -> "[" ++ concat (intersperse "," xs) - ++ "]") - (transpose (map (showModel model) as)) - -instance ShowModel (a -> b) where - showModel model sig = [] - -zipWith' f [] [] = [] -zipWith' f [] ys = zipWith' f ["?"] ys -zipWith' f xs [] = zipWith' f xs ["?"] -zipWith' f (x:xs) (y:ys) = f x y : zipWith' f xs ys - -zipWith3' f [] [] [] = [] -zipWith3' f [] ys zs = zipWith3' f ["?"] ys zs -zipWith3' f xs [] zs = zipWith3' f xs ["?"] zs -zipWith3' f xs ys [] = zipWith3' f xs ys ["?"] -zipWith3' f (x:xs) (y:ys) (z:zs) = f x y z : zipWith3' f xs ys zs - -zipWith4' f [] [] [] [] = [] -zipWith4' f [] ys zs vs = zipWith4' f ["?"] ys zs vs -zipWith4' f xs [] zs vs = zipWith4' f xs ["?"] zs vs -zipWith4' f xs ys [] vs = zipWith4' f xs ys ["?"] vs -zipWith4' f xs ys zs [] = zipWith4' f xs ys zs ["?"] -zipWith4' f (x:xs) (y:ys) (z:zs) (v:vs) = f x y z v : zipWith4' f xs ys zs vs - -zipWith5' f [] [] [] [] [] = [] -zipWith5' f [] ys zs vs ws = zipWith5' f ["?"] ys zs vs ws -zipWith5' f xs [] zs vs ws = zipWith5' f xs ["?"] zs vs ws -zipWith5' f xs ys [] vs ws = zipWith5' f xs ys ["?"] vs ws -zipWith5' f xs ys zs [] ws = zipWith5' f xs ys zs ["?"] ws -zipWith5' f xs ys zs vs [] = zipWith5' f xs ys zs vs ["?"] -zipWith5' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) = f x y z v w : zipWith5' f xs ys zs vs ws - -zipWith6' f [] [] [] [] [] [] = [] -zipWith6' f [] ys zs vs ws ps = zipWith6' f ["?"] ys zs vs ws ps -zipWith6' f xs [] zs vs ws ps = zipWith6' f xs ["?"] zs vs ws ps -zipWith6' f xs ys [] vs ws ps = zipWith6' f xs ys ["?"] vs ws ps -zipWith6' f xs ys zs [] ws ps = zipWith6' f xs ys zs ["?"] ws ps -zipWith6' f xs ys zs vs [] ps = zipWith6' f xs ys zs vs ["?"] ps -zipWith6' f xs ys zs vs ws [] = zipWith6' f xs ys zs vs ws ["?"] -zipWith6' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) = f x y z v w p : zipWith6' f xs ys zs vs ws ps - -zipWith7' f [] [] [] [] [] [] [] = [] -zipWith7' f [] ys zs vs ws ps qs = zipWith7' f ["?"] ys zs vs ws ps qs -zipWith7' f xs [] zs vs ws ps qs = zipWith7' f xs ["?"] zs vs ws ps qs -zipWith7' f xs ys [] vs ws ps qs = zipWith7' f xs ys ["?"] vs ws ps qs -zipWith7' f xs ys zs [] ws ps qs = zipWith7' f xs ys zs ["?"] ws ps qs -zipWith7' f xs ys zs vs [] ps qs = zipWith7' f xs ys zs vs ["?"] ps qs -zipWith7' f xs ys zs vs ws [] qs = zipWith7' f xs ys zs vs ws ["?"] qs -zipWith7' f xs ys zs vs ws ps [] = zipWith7' f xs ys zs vs ws ps ["?"] -zipWith7' f (x:xs) (y:ys) (z:zs) (v:vs) (w:ws) (p:ps) (q:qs) = f x y z v w p q : zipWith7' f xs ys zs vs ws ps qs - -forAll :: (ShowModel a, Checkable b) => Gen a -> (a -> b) -> Property -forAll gen body = P $ - do a <- gen - let P m = property (body a) - (sigs, mod) <- m - return (sigs, \model -> showModel model a : mod model) - ----------------------------------------------------------------- --- evaluate - -properties :: Checkable a => a -> IO ([Signal Bool], Model -> [[String]]) -properties a = generate gen - where - (P gen) = property a - ----------------------------------------------------------------- --- bweeuh - -liftM6 f g1 g2 g3 g4 g5 g6 = - do a1 <- g1 - a2 <- g2 - a3 <- g3 - a4 <- g4 - a5 <- g5 - a6 <- g6 - return (f a1 a2 a3 a4 a5 a6) - -liftM7 f g1 g2 g3 g4 g5 g6 g7 = - do a1 <- g1 - a2 <- g2 - a3 <- g3 - a4 <- g4 - a5 <- g5 - a6 <- g6 - a7 <- g7 - return (f a1 a2 a3 a4 a5 a6 a7) - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Ref.hs b/Lava2000/Ref.hs deleted file mode 100644 --- a/Lava2000/Ref.hs +++ /dev/null @@ -1,181 +0,0 @@ -module Lava2000.Ref - ( Ref - , ref - , deref - , memoRef - - , TableIO - , tableIO - , extendIO - , findIO - , memoRefIO - - , TableST - , tableST - , extendST - , findST - , memoRefST - ) - where - -import Lava2000.MyST - -import System.IO -import System.IO.Unsafe -import Data.IORef - -unsafeCoerce :: a -> b -unsafeCoerce a = unsafePerformIO $ - do writeIORef ref a - readIORef ref - where - ref = unsafePerformIO $ newIORef undefined - -- Defined here because Unsafe.Coerce doesn't exist in Hugs. - -{- - -Warning! One should regard this module as a portable -extension to the Haskell language. It is not Haskell. - --} - -{- - -Here is how we implement Tables of Refs: - -A Table is nothing but a unique tag, of type TableTag. -TableTag can be anything, as long as it is easy -to create new ones, and we can compare them for -equality. (I chose IORef ()). - -So how do we store Refs in a Table? We do not -want the Tables keeping track of their Refs -(which would be disastrous when the table -becomes big, and we would not have any garbage -collection). - -Instead, every Ref keeps track of the value it -has in each table it is in. This has the advantage -that we have a constant lookup time (if the number of -Tables we are using is small), and we get garbage -collection of table entries for free. - -The disadvantage is that, since the types of the -Tables vary, the Ref has no idea what type of -values it is supposed to store. So we use dynamic -types. - -A Ref is implemented as follows: it has two pieces -of information. The first one is an updatable -list of entries for each table it is a member in. -Since it is an updatable list, it is an IORef, which -we also use to compare two Refs. The second part is -just the value the Ref is pointing at (this can never -change anyway). - --} - ------------------------------------------------------------------ --- Ref - -data Ref a - = Ref (IORef [(TableTag, Dyn)]) a - -instance Eq (Ref a) where - Ref r1 _ == Ref r2 _ = r1 == r2 - -instance Show a => Show (Ref a) where - showsPrec _ (Ref _ a) = showChar '{' . shows a . showChar '}' - -ref :: a -> Ref a -ref a = unsafePerformIO $ - do r <- newIORef [] - return (Ref r a) - -deref :: Ref a -> a -deref (Ref _ a) = a - ------------------------------------------------------------------ --- Table IO - -type TableTag - = IORef () - -newtype TableIO a b - = TableIO TableTag - deriving Eq - -tableIO :: IO (TableIO a b) -tableIO = TableIO `fmap` newIORef () - -findIO :: TableIO a b -> Ref a -> IO (Maybe b) -findIO (TableIO t) (Ref r _) = - do list <- readIORef r - return (fromDyn `fmap` lookup t list) - -extendIO :: TableIO a b -> Ref a -> b -> IO () -extendIO (TableIO t) (Ref r _) b = - do list <- readIORef r - writeIORef r ((t,toDyn b) : filter ((/= t) . fst) list) - ------------------------------------------------------------------ --- Table ST - -newtype TableST s a b - = TableST (TableIO a b) - deriving Eq - -tableST :: ST s (TableST s a b) -tableST = unsafeIOtoST (TableST `fmap` tableIO) - -findST :: TableST s a b -> Ref a -> ST s (Maybe b) -findST (TableST tab) r = unsafeIOtoST (findIO tab r) - -extendST :: TableST s a b -> Ref a -> b -> ST s () -extendST (TableST tab) r b = unsafeIOtoST (extendIO tab r b) - ------------------------------------------------------------------ --- Memo - -memoRef :: (Ref a -> b) -> (Ref a -> b) -memoRef f = unsafePerformIO . memoRefIO (return . f) - -memoRefIO :: (Ref a -> IO b) -> (Ref a -> IO b) -memoRefIO f = unsafePerformIO $ - do tab <- tableIO - let f' r = do mb <- findIO tab r - case mb of - Just b -> do return b - Nothing -> fixIO $ \b -> - do extendIO tab r b - f r - return f' - -memoRefST :: (Ref a -> ST s b) -> (Ref a -> ST s b) -memoRefST f = unsafePerformST $ - do tab <- tableST - let f' r = do mb <- findST tab r - case mb of - Just b -> do return b - Nothing -> fixST $ \b -> - do extendST tab r b - f r - return f' - ------------------------------------------------------------------ --- Dyn - -data Dyn - = Dyn - -toDyn :: a -> Dyn -toDyn = unsafeCoerce - -fromDyn :: Dyn -> a -fromDyn = unsafeCoerce - ------------------------------------------------------------------ --- the end. - - - diff --git a/Lava2000/Retime.hs b/Lava2000/Retime.hs deleted file mode 100644 --- a/Lava2000/Retime.hs +++ /dev/null @@ -1,59 +0,0 @@ -module Lava2000.Retime - ( timeTransform - ) - where - -import Lava2000.Signal -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Netlist - -import List - ( isPrefixOf - ) - ----------------------------------------------------------------- --- time transformation - -timeTransform :: (Generic a, Generic b) => (a -> b) -> ([a] -> [b]) -timeTransform circ [] = [] -timeTransform circ inps@(inp:_) = - map construct - . transStruct - . netlist phi - . struct - . circ - . symbolize tag - $ inp - where - n = length inps - - phi (DelayBool ini next) = - delay DelayBool ini next - - phi (DelayInt ini next) = - delay DelayInt ini next - - phi (VarBool s) | tag `isPrefixOf` s = - var (drop (length tag) s) - - phi (VarInt s) | tag `isPrefixOf` s = - var (drop (length tag) s) - - phi s = - take n (cycle (map symbol (zips s))) - - delay del ~(ini0:_) next = - (symbol (del ini0 (last next)) : list (n-1) (init next)) - - var s = - map (pickSymbol s) inps - - list 0 _ = [] - list n ~(x:xs) = x : list (n-1) xs - - tag = "#retime#" - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Satnik.hs b/Lava2000/Satnik.hs deleted file mode 100644 --- a/Lava2000/Satnik.hs +++ /dev/null @@ -1,150 +0,0 @@ -module Lava2000.Satnik - ( satnik - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- satnik - -satnik :: Checkable a => a -> IO ProofResult -satnik a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile (writeDefinitions defsFile props) - where - defsFile = verifyDir ++ "/circuit.cnf" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO () -writeDefinitions file props = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - cls <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "c Generated by Lava2000" - , "c " - ] - - let new = - do n <- readIORef var - let n' = n+1 - writeIORef var n' - return n' - - clause xs = - do n <- readIORef cls - let n' = n+1 in n' `seq` writeIORef cls n' - hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n") - - define v s = - case s of - Bool True -> clause [ v ] - Bool False -> clause [ -v ] - Inv x -> clause [ -x, -v ] >> clause [ x, v ] - - And [] -> define v (Bool True) - And xs -> conjunction v xs - - Or [] -> define v (Bool False) - Or xs -> conjunction (-v) (map negate xs) - - Xor [] -> define v (Bool False) - Xor xs -> exactly1 v xs - - VarBool s -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n") - - DelayBool x y -> wrong Lava2000.Error.DelayEval - _ -> wrong Lava2000.Error.NoArithmetic - where - - conjunction v xs = - do clause (v : map negate xs) - sequence_ [ clause [ -v, x ] | x <- xs ] - - exactly1 v xs = - do clause (-v : xs) - sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ] - sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ] - - pairs [] = [] - pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs - - pick [] = [] - pick (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ] - - outvs <- netlistIO new define (struct props) - clause (map negate (flatten outvs)) - - nvar <- readIORef var - ncls <- readIORef cls - hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n") - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - firstFile = file ++ "-1" - secondFile = file ++ "-2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Satnik: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/satnik.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Satzoo.hs b/Lava2000/Satzoo.hs deleted file mode 100644 --- a/Lava2000/Satzoo.hs +++ /dev/null @@ -1,150 +0,0 @@ -module Lava2000.Satzoo - ( satzoo - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- satzoo - -satzoo :: Checkable a => a -> IO ProofResult -satzoo a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile (writeDefinitions defsFile props) - where - defsFile = verifyDir ++ "/circuit.cnf" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO () -writeDefinitions file props = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - cls <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "c Generated by Lava2000" - , "c " - ] - - let new = - do n <- readIORef var - let n' = n+1 - writeIORef var n' - return n' - - clause xs = - do n <- readIORef cls - let n' = n+1 in n' `seq` writeIORef cls n' - hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n") - - define v s = - case s of - Bool True -> clause [ v ] - Bool False -> clause [ -v ] - Inv x -> clause [ -x, -v ] >> clause [ x, v ] - - And [] -> define v (Bool True) - And xs -> conjunction v xs - - Or [] -> define v (Bool False) - Or xs -> conjunction (-v) (map negate xs) - - Xor [] -> define v (Bool False) - Xor xs -> exactly1 v xs - - VarBool s -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n") - - DelayBool x y -> wrong Lava2000.Error.DelayEval - _ -> wrong Lava2000.Error.NoArithmetic - where - - conjunction v xs = - do clause (v : map negate xs) - sequence_ [ clause [ -v, x ] | x <- xs ] - - exactly1 v xs = - do clause (-v : xs) - sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ] - sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ] - - pairs [] = [] - pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs - - pick [] = [] - pick (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ] - - outvs <- netlistIO new define (struct props) - clause (map negate (flatten outvs)) - - nvar <- readIORef var - ncls <- readIORef cls - hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n") - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - firstFile = file ++ "-1" - secondFile = file ++ "-2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Satzoo: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/satzoo.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Sequent.hs b/Lava2000/Sequent.hs deleted file mode 100644 --- a/Lava2000/Sequent.hs +++ /dev/null @@ -1,18 +0,0 @@ -module Lava2000.Sequent where - ----------------------------------------------------------------- --- Sequent (monadic Functor) - -class Functor s => Sequent s where - sequent :: Monad m => s (m a) -> m (s a) - -instance Sequent [] where - sequent = sequence - -mmap :: (Monad m, Sequent s) => (a -> m b) -> s a -> m (s b) -mmap f = sequent . fmap f - ----------------------------------------------------------------- --- the end. - - diff --git a/Lava2000/Sequential.hs b/Lava2000/Sequential.hs deleted file mode 100644 --- a/Lava2000/Sequential.hs +++ /dev/null @@ -1,137 +0,0 @@ -module Lava2000.Sequential - ( simulateSeq - ) - where - -import Lava2000.Ref -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Sequent -import Lava2000.Generic - -import Lava2000.MyST - ( ST - , STRef - , newSTRef - , readSTRef - , writeSTRef - , unsafeInterleaveST - , runST - ) - ----------------------------------------------------------------- --- wire datatype - -type Var s - = (STRef s (S Symbol), STRef s (Wire s)) - -data Wire s - = Wire - { dependencies :: [Var s] - , kick :: ST s () - } - ----------------------------------------------------------------- --- simulate - -simulateSeq :: (Generic a, Generic b) => (a -> b) -> [a] -> [b] -simulateSeq circ [] = [] -simulateSeq circ inps = runST ( - do roots <- newSTRef [] - - let root r = - do rs <- readSTRef roots - writeSTRef roots (r:rs) - - new = - do rval <- newSTRef (error "val?") - rwir <- newSTRef (error "wire?") - return (rval, rwir) - - define r s = - case s of - DelayBool s s' -> delay s s' - DelayInt s s' -> delay s s' - _ -> - do relate r (arguments s) $ - eval `fmap` mmap (readSTRef . fst) s - where - delay ri@(rinit,_) r1@(pre,_) = - do state <- newSTRef Nothing - r2 <- new - root r2 - - relate r [ri] $ - do ms <- readSTRef state - case ms of - Just s -> return s - Nothing -> - do s <- readSTRef rinit - writeSTRef state (Just s) - return s - - relate r2 [r,r1] $ - do s <- readSTRef pre - writeSTRef state (Just s) - return s - - sr <- netlistST new define (struct (circ (input inps))) - rs <- readSTRef roots - step <- drive (flatten sr ++ rs) - - outs <- lazyloop $ - do step - s <- mmap (fmap symbol . readSTRef . fst) sr - return (construct s) - - let res = takes inps outs - return res - ) - --- evaluation order - -relate :: Var s -> [Var s] -> ST s (S Symbol) -> ST s () -relate (rval, rwir) rs f = - do writeSTRef rwir $ - Wire{ dependencies = rs - , kick = do b <- f - writeSTRef rval b - } - -drive :: [Var s] -> ST s (ST s ()) -drive [] = - do return (return ()) - -drive ((rval,rwir):rs) = - do wire <- readSTRef rwir - writeSTRef rwir (error "detected combinational loop") - driv1 <- drive (dependencies wire) - writeSTRef rwir $ - Wire { dependencies = [], kick = return () } - driv2 <- drive rs - return $ - do driv1 - kick wire - driv2 - ----------------------------------------------------------------- --- helper functions - -lazyloop :: ST s a -> ST s [a] -lazyloop m = - do a <- m - as <- unsafeInterleaveST (lazyloop m) - return (a:as) - -input :: Generic a => [a] -> a -input xs = out - where - out = foldr delay out xs - -takes :: [a] -> [b] -> [b] -takes [] _ = [] -takes (_:xs) (y:ys) = y : takes xs ys - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/SequentialCircuits.hs b/Lava2000/SequentialCircuits.hs deleted file mode 100644 --- a/Lava2000/SequentialCircuits.hs +++ /dev/null @@ -1,68 +0,0 @@ -module Lava2000.SequentialCircuits where - -import Lava2000 - ----------------------------------------------------------------- --- Sequential Circuits - -edge inp = change - where - inp' = delay low inp - change = xor2 (inp, inp') - -toggle change = out - where - out' = delay low out - out = xor2 (change, out') - -delayClk init (clk, inp) = out - where - out = delay init val - val = mux (clk, (out, inp)) - -delayN 0 init inp = inp -delayN n init inp = out - where - out = delay init rest - rest = delayN (n-1) init inp - -always inp = ok - where - sofar = delay high ok - ok = and2 (inp, sofar) - -constant x = ok - where - init = delay high low - same = x <==> delay zero x - ok = always (init <|> same) - -puls n () = out - where - out = delayN (n-1) low last - last = delay high out - -outputList sigs () = out - where - out = foldr (|->) out sigs - -rowSeq circ inp = out - where - carryIn = delay zero carryOut - (out, carryOut) = circ (carryIn, inp) - -rowSeqReset circ (reset,inp) = out - where - carryIn = delay zero carry - carry = mux (reset, (carryOut, zero)) - (out, carryOut) = circ (carryIn, inp) - -rowSeqPeriod n circ inp = out - where - reset = puls n () - out = rowSeqReset circ (reset, inp) - ----------------------------------------------------------------- --- the end. - - diff --git a/Lava2000/SequentialConstructive.hs b/Lava2000/SequentialConstructive.hs deleted file mode 100644 --- a/Lava2000/SequentialConstructive.hs +++ /dev/null @@ -1,173 +0,0 @@ -module Lava2000.SequentialConstructive - ( simulateCon - ) - where - -import Lava2000.Ref -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Sequent -import Lava2000.Generic -import Lava2000.Error - -import Data.IORef -import System.IO.Unsafe - ----------------------------------------------------------------- --- wire datatype - -type Time - = IORef () - -data Timed a - = a `At` Time - | Uninitialized - -data Wire - = Wire - { components :: [Component] - , value :: Timed (S Symbol) - } - -type Component - = Time -> IO () - ----------------------------------------------------------------- --- simulate - -simulateCon :: (Generic a, Generic b) => (a -> b) -> [a] -> [b] -simulateCon circ inps = unsafePerformIO $ - do micro <- newSet - macro <- newSet - time0 <- newIORef () - - let new = - do rwire <- newIORef (Wire{ components = [], value = Uninitialized }) - return rwire - - define rwire (DelayBool init next) = - do delay rwire init next - - define rwire (DelayInt init next) = - do delay rwire init next - - define rwire sym = - case arguments sym of - [] -> addSet macro constant - args -> sequence_ [ compWire rarg propagate | rarg <- args ] - where - propagate time = - do sym' <- mmap (`valueWire` time) sym - case evalLazy sym' of - Nothing -> return () - Just v -> updateWire rwire time v - - constant time = - do propagate time - addSet macro constant - - delay rwire init next = - do compWire next nextState - compWire init initState - where - nextState time = - do mv <- valueWire next time - case mv of - Nothing -> return () - Just v -> addSet macro (\t -> updateWire rwire t v) - - initState time - | time == time0 = do mv <- valueWire init time - case mv of - Nothing -> return () - Just v -> updateWire rwire time v - | otherwise = do return () - - compWire rwire comp = - do wire <- readIORef rwire - writeIORef rwire (wire{ components = comp : components wire }) - - valueWire rwire time = - do wire <- readIORef rwire - return $ - case value wire of - v `At` time' - | time == time' -> Just v - _ -> Nothing - - actualValueWire rwire time = - do mv <- valueWire rwire time - case mv of - Just v -> return v - Nothing -> wrong Lava2000.Error.UndefinedWire - - updateWire rwire time v = - do wire <- readIORef rwire - mv <- valueWire rwire time - case mv of - Just v' | v =/= v' -> wrong Lava2000.Error.BadCombinationalLoop - | otherwise -> return () - - _ -> do writeIORef rwire (wire{ value = v `At` time }) - sequence_ [ addSet micro comp | comp <- components wire ] - - Bool b1 =/= Bool b2 = b1 /= b2 - Int n1 =/= Int n2 = n1 /= n2 - _ =/= _ = True - - sr <- netlistIO new define (struct (circ (input inps))) - - outs <- timedLazyLoop time0 $ \time -> - do emptySet macro ($ time) - while (emptySet micro ($ time)) - s <- mmap (`actualValueWire` time) sr - return (construct (symbol `fmap` s)) - - let res = takes inps outs - return res - ----------------------------------------------------------------- --- helper functions - -newSet :: IO (IORef [a]) -newSet = newIORef [] - -addSet :: IORef [a] -> a -> IO () -addSet rset x = - do xs <- readIORef rset - writeIORef rset (x:xs) - -emptySet :: IORef [a] -> (a -> IO ()) -> IO Bool -emptySet rset action = - do xs <- readIORef rset - writeIORef rset [] - case xs of - [] -> do return False - _ -> do sequence [ action x | x <- xs ] - return True - -while :: Monad m => m Bool -> m () -while m = - do b <- m - if b then while m - else return () - -timedLazyLoop :: Time -> (Time -> IO a) -> IO [a] -timedLazyLoop t m = - do a <- m t - t' <- newIORef () - as <- unsafeInterleaveIO (timedLazyLoop t' m) - return (a:as) - -input :: Generic a => [a] -> a -input xs = out - where - out = foldr delay out xs - -takes :: [a] -> [b] -> [b] -takes [] _ = [] -takes (_:xs) (y:ys) = y : takes xs ys - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Signal.hs b/Lava2000/Signal.hs deleted file mode 100644 --- a/Lava2000/Signal.hs +++ /dev/null @@ -1,350 +0,0 @@ -module Lava2000.Signal where - -import Lava2000.Ref -import Lava2000.Sequent -import Lava2000.Error - -import List - ( transpose - ) - ----------------------------------------------------------------- --- Signal, Symbol, S - -newtype Signal a - = Signal Symbol - -newtype Symbol - = Symbol (Ref (S Symbol)) - -data S s - = Bool Bool - | Inv s - | And [s] - | Or [s] - | Xor [s] - | VarBool String - | DelayBool s s - - | Int Int - | Neg s - | Div s s - | Mod s s - | Plus [s] - | Times [s] - | Gte s s - | Equal [s] - | If s s s - | VarInt String - | DelayInt s s - -symbol :: S Symbol -> Symbol -symbol = Symbol . ref - -unsymbol :: Symbol -> S Symbol -unsymbol (Symbol r) = deref r - -instance Eq (Signal a) where - Signal (Symbol r1) == Signal (Symbol r2) = r1 == r2 - ----------------------------------------------------------------- --- operations - --- on bits - -bool :: Bool -> Signal Bool -bool b = lift0 (Bool b) - -low, high :: Signal Bool -low = bool False -high = bool True - -inv :: Signal Bool -> Signal Bool -inv = lift1 Inv - -andl, orl, xorl :: [Signal Bool] -> Signal Bool -andl = liftl And -orl = liftl Or -xorl = liftl Xor - -equalBool :: Signal Bool -> Signal Bool -> Signal Bool -equalBool x y = inv (xorl [x,y]) - -ifBool :: Signal Bool -> (Signal Bool, Signal Bool) -> Signal Bool -ifBool c (x,y) = orl[andl[c,x],andl[inv c,y]] - -delayBool :: Signal Bool -> Signal Bool -> Signal Bool -delayBool = lift2 DelayBool - -varBool :: String -> Signal Bool -varBool s = lift0 (VarBool s) - --- on ints - -int :: Int -> Signal Int -int n = lift0 (Int n) - -neg :: Signal Int -> Signal Int -neg = lift1 Neg - -divide, modulo :: Signal Int -> Signal Int -> Signal Int -divide = lift2 Div -modulo = lift2 Mod - -plusl, timesl :: [Signal Int] -> Signal Int -plusl = liftl Plus -timesl = liftl Times - -equall :: [Signal Int] -> Signal Bool -equall = liftl Equal - -gteInt :: Signal Int -> Signal Int -> Signal Bool -gteInt = lift2 Gte - -equalInt :: Signal Int -> Signal Int -> Signal Bool -equalInt x y = equall [x,y] - -ifInt :: Signal Bool -> (Signal Int, Signal Int) -> Signal a -ifInt c (x,y) = lift3 If c x y - -delayInt :: Signal Int -> Signal Int -> Signal Int -delayInt = lift2 DelayInt - -varInt :: String -> Signal Int -varInt s = lift0 (VarInt s) - --- liftings - -lift0 :: S Symbol -> Signal a -lift0 oper = Signal (symbol oper) - -lift1 :: (Symbol -> S Symbol) -> Signal a -> Signal b -lift1 oper (Signal a) = Signal (symbol (oper a)) - -lift2 :: (Symbol -> Symbol -> S Symbol) -> Signal a -> Signal b -> Signal c -lift2 oper (Signal a) (Signal b) = Signal (symbol (oper a b)) - -lift3 :: (Symbol -> Symbol -> Symbol -> S Symbol) - -> Signal a -> Signal b -> Signal c -> Signal d -lift3 oper (Signal a) (Signal b) (Signal c) = Signal (symbol (oper a b c)) - -liftl :: ([Symbol] -> S Symbol) -> [Signal a] -> Signal c -liftl oper sigas = Signal (symbol (oper (map (\(Signal a) -> a) sigas))) - ----------------------------------------------------------------- --- evaluate - -eval :: S (S a) -> S a -eval s = - case s of - Bool b -> Bool b - Inv (Bool b) -> Bool (not b) - And xs -> Bool . all bval $ xs - Or xs -> Bool . any bval $ xs - Xor xs -> Bool . (1 ==) . length . filter bval $ xs - - Int n -> Int n - Neg (Int n) -> Int (-n) - Div (Int n1) (Int n2) -> Int (n1 `div` n2) - Mod (Int n1) (Int n2) -> Int (n1 `mod` n2) - Plus xs -> Int . sum . map nval $ xs - Times xs -> Int . product . map nval $ xs - Gte (Int n1) (Int n2) -> Bool (n1 >= n2) - Equal xs -> Bool . equal . map nval $ xs - If (Bool c) x y -> if c then x else y - - DelayBool s s' -> wrong Lava2000.Error.DelayEval - DelayInt s s' -> wrong Lava2000.Error.DelayEval - VarBool s -> wrong Lava2000.Error.VarEval - VarInt s -> wrong Lava2000.Error.VarEval - where - bval (Bool b) = b - nval (Int n) = n - - equal (x:y:xs) = x == y && equal (y:xs) - equal _ = True - -evalLazy :: S (Maybe (S a)) -> Maybe (S a) -evalLazy s = - case s of - -- lazy - And xs - | any (`bval` False) xs -> bans False - - Or xs - | any (`bval` True) xs -> bans True - - Xor xs - | number (`bval` True) xs >= 2 -> bans False - - -- strict - _ -> eval `fmap` sequent s - - where - bans = Just . Bool - - bval (Just (Bool b)) b' = b == b' - bval _ _ = False - - number p = length . filter p - -arguments :: S a -> [a] -arguments s = - case s of - Bool b -> [] - Inv s -> [s] - And xs -> xs - Or xs -> xs - Xor xs -> xs - - Int n -> [] - Neg s -> [s] - Div s1 s2 -> [s1,s2] - Mod s1 s2 -> [s1,s2] - Plus xs -> xs - Times xs -> xs - Gte x y -> [x,y] - Equal xs -> xs - If x y z -> [x,y,z] - - DelayBool s s' -> [s,s'] - DelayInt s s' -> [s,s'] - VarBool s -> [] - VarInt s -> [] - -zips :: S [a] -> [S a] -zips s = - case s of - Bool b -> [Bool b] - Inv s -> map Inv s - And xs -> map And (transpose xs) - Or xs -> map Or (transpose xs) - Xor xs -> map Xor (transpose xs) - - Int n -> [Int n] - Neg s -> map Neg s - Div s1 s2 -> zipWith Div s1 s2 - Mod s1 s2 -> zipWith Mod s1 s2 - Plus xs -> map Plus (transpose xs) - Times xs -> map Times (transpose xs) - Gte x y -> zipWith Gte x y - Equal xs -> map Equal (transpose xs) - If x y z -> zipWith3 If x y z - - DelayBool s s' -> zipWith DelayBool s s' - DelayInt s s' -> zipWith DelayInt s s' - VarBool s -> [VarBool s] - VarInt s -> [VarInt s] - ----------------------------------------------------------------- --- properties of S - -instance Functor S where - fmap f s = - case s of - Bool b -> Bool b - Inv x -> Inv (f x) - And xs -> And (map f xs) - Or xs -> Or (map f xs) - Xor xs -> Xor (map f xs) - - Int n -> Int n - Neg x -> Neg (f x) - Div x y -> Div (f x) (f y) - Mod x y -> Mod (f x) (f y) - Plus xs -> Plus (map f xs) - Times xs -> Times (map f xs) - Gte x y -> Gte (f x) (f y) - Equal xs -> Equal (map f xs) - If x y z -> If (f x) (f y) (f z) - - DelayBool x y -> DelayBool (f x) (f y) - DelayInt x y -> DelayInt (f x) (f y) - VarBool v -> VarBool v - VarInt v -> VarInt v - -instance Sequent S where - sequent s = - case s of - Bool b -> lift0 (Bool b) - Inv x -> lift1 Inv x - And xs -> liftl And xs - Or xs -> liftl Or xs - Xor xs -> liftl Xor xs - - Int n -> lift0 (Int n) - Neg x -> lift1 Neg x - Div x y -> lift2 Div x y - Mod x y -> lift2 Mod x y - Plus xs -> liftl Plus xs - Times xs -> liftl Times xs - Gte x y -> lift2 Gte x y - Equal xs -> liftl Equal xs - If x y z -> lift3 If x y z - - DelayBool x y -> lift2 DelayBool x y - DelayInt x y -> lift2 DelayInt x y - VarBool v -> lift0 (VarBool v) - VarInt v -> lift0 (VarInt v) - where - lift0 op = - do return op - - lift1 op x = - do x' <- x - return (op x') - - lift2 op x y = - do x' <- x - y' <- y - return (op x' y') - - lift3 op x y z = - do x' <- x - y' <- y - z' <- z - return (op x' y' z') - - liftl op xs = - do xs' <- sequence xs - return (op xs') - -instance Show (Signal a) where - showsPrec n (Signal s) = - showsPrec n s - -instance Show Symbol where - showsPrec n sym = - showsPrec n (unsymbol sym) - -instance Show a => Show (S a) where - showsPrec n s = - case s of - Bool True -> showString "high" - Bool False -> showString "low" - - Inv x -> showString "inv" . showList [x] - And xs -> showString "andl" . showList xs - Or xs -> showString "orl" . showList xs - Xor xs -> showString "xorl" . showList xs - - Int i -> showsPrec n i - Neg x -> showString "-" . showsPrec n x - Div x y -> showString "idiv" . showList [x,y] - Mod x y -> showString "imod" . showList [x,y] - Plus xs -> showString "plusl" . showList xs - Times xs -> showString "timesl" . showList xs - Gte x y -> showString "gte" . showList [x,y] - Equal xs -> showString "equall" . showList xs - If x y z -> showString "ifThenElse" . showList [x,y,z] - - DelayBool x y -> showString "delay" . showList [x,y] - DelayInt x y -> showString "delay" . showList [x,y] - - VarBool s -> showString s - VarInt s -> showString s - _ -> showString "<>" - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/SignalTry.hs b/Lava2000/SignalTry.hs deleted file mode 100644 --- a/Lava2000/SignalTry.hs +++ /dev/null @@ -1,15 +0,0 @@ -module Lava2000.SignalTry where - -import Lava2000.Ref - -data Signal a - = Value a - | Symbol (Ref (Symbol a)) - -data Symbol a - = forall x y . Function String ([x] -> [y] -> a) [Signal x] [Signal y] - | Delay (Signal a) (Signal a) - | Variable String - -and2 :: (Signal Bool, Signal Bool) -> Signal Bool -and2 (x,y) = Symbol (ref (Function "and" (\xs _ -> and xs) [x,y] [])) diff --git a/Lava2000/Smv.hs b/Lava2000/Smv.hs deleted file mode 100644 --- a/Lava2000/Smv.hs +++ /dev/null @@ -1,155 +0,0 @@ -module Lava2000.Smv - ( smv - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- smv - -smv :: Checkable a => a -> IO ProofResult -smv a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile (writeDefinitions defsFile props) - where - defsFile = verifyDir ++ "/circuit.smv" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO () -writeDefinitions file props = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "-- Generated by Lava2000" - , "" - , "MODULE main" - ] - - let new = - do n <- readIORef var - let n' = n+1; v = "w" ++ show n' - n' `seq` writeIORef var n' - return v - - define v s = - case s of - Bool True -> op0 "1" - Bool False -> op0 "0" - Inv x -> op1 "!" x - - And [] -> define v (Bool True) - And [x] -> op0 x - And xs -> opl "&" xs - - Or [] -> define v (Bool False) - Or [x] -> op0 x - Or xs -> opl "|" xs - - Xor [] -> define v (Bool False) - Xor xs -> op0 (xor xs) - - VarBool s -> do op0 s - hPutStr firstHandle ("VAR " ++ s ++ " : boolean;\n") - DelayBool x y -> delay x y - - _ -> wrong Lava2000.Error.NoArithmetic - where - w i = v ++ "_" ++ show i - - op0 s = - hPutStr secondHandle $ - "DEFINE " ++ v ++ " := " ++ s ++ ";\n" - - op1 op s = - op0 (op ++ "(" ++ s ++ ")") - - opl op xs = - op0 (concat (intersperse (" " ++ op ++ " ") xs)) - - xor [x] = x - xor [x,y] = "!(" ++ x ++ " <-> " ++ y ++ ")" - xor (x:xs) = "(" ++ x ++ " & !(" - ++ concat (intersperse " | " xs) - ++ ") | (!" ++ x ++ " & (" ++ xor xs ++ ")))" - - delay x y = - do hPutStr firstHandle ("VAR " ++ v ++ " : boolean;\n") - hPutStr secondHandle $ - "ASSIGN init(" ++ v ++ ") := " ++ x ++ ";\n" - ++ "ASSIGN next(" ++ v ++ ") := " ++ y ++ ";\n" - - outvs <- netlistIO new define (struct props) - hPutStr secondHandle $ unlines $ - [ "SPEC AG " ++ outv - | outv <- flatten outvs - ] - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - firstFile = file ++ "-1" - secondFile = file ++ "-2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Smv: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/smv.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Stable.hs b/Lava2000/Stable.hs deleted file mode 100644 --- a/Lava2000/Stable.hs +++ /dev/null @@ -1,60 +0,0 @@ -module Lava2000.Stable where - -import Lava2000.Signal -import Lava2000.Operators -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Ref - -import Lava2000.MyST - ( STRef - , newSTRef - , readSTRef - , writeSTRef - , runST - , unsafeInterleaveST - ) - -import List - ( isPrefixOf - ) - ----------------------------------------------------------------- --- stable analysis - -stable :: Generic a => a -> Signal Bool -stable inp = - runST - ( do table <- tableST - stableRef <- newSTRef [] - - let gather (Symbol sym) = - do ms <- findST table sym - case ms of - Just () -> do return () - Nothing -> do extendST table sym () - mmap gather (deref sym) - define (Symbol sym) (deref sym) - - define out (DelayBool _ inn) = - do addStable (out <==> inn) - - define out (DelayInt _ inn) = - do addStable (out <==> inn) - - define _ _ = - do return () - - addStable x = - do stables <- readSTRef stableRef - writeSTRef stableRef (x:stables) - - in mmap gather (struct inp) - - stables <- readSTRef stableRef - return (andl stables) - ) - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Table.hs b/Lava2000/Table.hs deleted file mode 100644 --- a/Lava2000/Table.hs +++ /dev/null @@ -1,72 +0,0 @@ -module Lava2000.Table - ( table - , tableProp - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.MyST - -{- - -Example use: - -Suppose we have a circuit: - - f :: (Signal Bool, Signal Bool) -> Signal Bool - f (x,y) = and2 (y,x) - -Then we can look at its internal structure as follows: - - table (struct (f (var "i"))) - -will evaluate to - - ([(1,And 2 3),(3,Var "i_1"),(2,Var "i_2")],Object 1) - -For circuits taking more complicated structures as arguments -(such as lists), one has to instantiate the list size first -of course. - -If you do not like the "Object 1" output, you can just use -the function `flatten' to get a list of identifiers. - --} - ----------------------------------------------------------------- --- table - -tableProp :: Checkable a => a -> IO ([(Int,S Int)], [Int]) -tableProp a = - do (props,_) <- properties a - let (tab, ps) = table (struct props) - return (tab, flatten ps) - -table :: Sequent f => f Symbol -> ([(Int,S Int)], f Int) -table str = - runST - ( do ref <- newSTRef 0 - table <- newSTRef [] - - let new = - do n <- readSTRef ref - let n' = n+1 - writeSTRef ref n' - return n' - - define v def = - do tab <- readSTRef table - writeSTRef table ((v,def):tab) - - str' <- netlistST new define str - tab <- readSTRef table - return (tab, str') - ) - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Test.hs b/Lava2000/Test.hs deleted file mode 100644 --- a/Lava2000/Test.hs +++ /dev/null @@ -1,23 +0,0 @@ -module Lava2000.Test where - -import Lava2000.Signal -import Lava2000.Sequential -import Lava2000.Generic - -import Lava2000.LavaRandom - ( newRnd - ) - ----------------------------------------------------------------- --- test - -test :: (Constructive a, Show b, Generic b) => (a -> b) -> IO [b] -test circ = - do rnd <- newRnd - let res = simulateSeq (\_ -> circ (random rnd)) (replicate 100 ()) - print res - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Verification.hs b/Lava2000/Verification.hs deleted file mode 100644 --- a/Lava2000/Verification.hs +++ /dev/null @@ -1,475 +0,0 @@ -module Lava2000.Verification - ( Option(..) - , verify - , verifyWith - , ProofResult(..) - , verifyDir - , checkVerifyDir - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir - -import List - ( intersperse - , isPrefixOf - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - -verifyDir :: FilePath -verifyDir = "Verify" - ----------------------------------------------------------------- --- Options - -data Option - = Name String - | ShowTime - | Sat Int - | NoBacktracking - | Depth Int - | Increasing - | RestrictStates - deriving (Eq, Show) - -defaultOptions :: [Option] -defaultOptions = - [Increasing] - -defaultValues :: [Option] -defaultValues = - [Name "circuit", Sat 1, Depth 1] - -sameOption :: Option -> Option -> Bool -sameOption opt1 opt2 = tag opt1 == tag opt2 - where - tag = head . words . show - -searchOptVal :: Read a => [Option] -> (a -> Option) -> a -searchOptVal options what = search (options ++ defaultValues) - where - opt' = what undefined - - search [] = wrong Lava2000.Error.Internal_OptionNotFound - search (opt:opts) - | sameOption opt opt' = read (words (show opt) !! 1) - | otherwise = search opts - -searchOptBool :: [Option] -> Option -> Bool -searchOptBool options what = what `elem` options - ----------------------------------------------------------------- --- verify - -verify :: Checkable a => a -> IO ProofResult -verify a = verifyWith defaultOptions a - -verifyWith :: Checkable a => [Option] -> a -> IO ProofResult -verifyWith options a = - do checkVerifyDir - noBuffering - - (props,model) <- properties a - (states,pins) <- writeDefinitions defsFile props - res <- proveAll defsFile states pins options - if res == Falsifiable - then displayModel outFile model - else return () - return res - where - defsFile = verifyDir ++ "/" ++ nameOpt ++ ".defs" - outFile = verifyDir ++ "/prover.out" - nameOpt = searchOptVal options Name - ----------------------------------------------------------------- --- proving - -proveAll :: FilePath -> [State] -> Int -> [Option] -> IO ProofResult -proveAll defsFile states quests options = - case actions of - [[]] -> - do putStrLn "Nothing to prove! ... Valid." - return Valid - - [[(labels, ini, assumps, obligs)]] -> - do proveUnit labels ini assumps obligs - - _ -> - do tryAll actions - where - depths - | incrOpt && not (null states) = [depthOpt ..] - | otherwise = [depthOpt] - - steps d - | null states = [ ([], True, [], [1]) ] - | otherwise = [ (["base " ++ show d], True, [], [1..d]) - , (["step " ++ show d], False, [1..d], [d+1]) - ] - - pins (labels, ini, assumps, obligs) n - | n == 1 = [ (labels, ini, map (pin 1) assumps, map (pin 1) obligs) ] - | otherwise = [ ( labels ++ ["pin " ++ show p] - , ini - , [ pin p ass | ass <- assumps, p <- [1..n] ] - ++ [ pin p' obl | obl <- obligs, p' <- [1..p-1] ] - , [ pin p obl | obl <- obligs ] - ) - | p <- [1..n] - ] - where - pin p a = (a, p) - - actions = - [ concatMap (`pins` quests) (steps d) | d <- depths ] - - nameOpt = searchOptVal options Name - depthOpt = searchOptVal options Depth - incrOpt = searchOptBool options Increasing - restrOpt = searchOptBool options RestrictStates - - tryAll [] = - do result Indeterminate - - tryAll ([] : rest) = - do result Valid - - tryAll (((labels, ini, assumps, obligs) : tries) : rest) = - do r <- proveUnit labels ini assumps obligs - case r of - Valid -> tryAll (tries : rest) - Falsifiable | not ini -> tryAll rest - | ini -> result Falsifiable - Indeterminate -> result Indeterminate - - result r = - do putStrLn "--" - putStrLn ("Result: " ++ show r ++ ".") - return r - - proveUnit labels ini assumps obligs = - do proveFile mainFile create labels options - where - create = - do writeHeader - sequence - [ instantiateFile defsFile mainFile t - | t <- times - ] - appendAssumptions - $ [ quest ass - | ass <- assumps - ] - ++ [ "~" ++ init t - | t <- tail times - ] - ++ ( if ini then [init 1] - else - if restrOpt then restrictStates - else [] - ) - appendObligations - $ [ quest obl - | obl <- obligs - ] - appendFooter - - mainFile = - verifyDir ++ "/" ++ clean (nameOpt ++ ".prov" ++ concatMap ("." ++) labels) - - clean (' ':s) = '_':clean s - clean (c:s) = c:clean s - clean [] = [] - - times = - nub [ t | (t, p) <- assumps ++ obligs ] - - init t = - "init_t" ++ show t - - quest (t, p) = - "quest_t" ++ show t ++ "_n" ++ show p - - writeHeader = writeFile mainFile $ unlines $ - [ "/* Generated by Lava 2000 */" - , "/* options: " ++ show options ++ " */" - , "" - , "AND(" - , "" - ] - - appendAssumptions [] = return () - appendAssumptions ass = appendFile mainFile $ unlines $ - [ "" - , "/* assumptions */" - , "" - ] ++ map (++ ",") ass - - appendObligations obs = appendFile mainFile $ unlines $ - [ "" - , "big_question <-> AND(" - , "/* proof obligations */" - , "" - ] ++ map (++ ",") obs - - appendFooter = appendFile mainFile $ unlines $ - [ "" - , "/* the big question */" - , "TRUE)) -> big_question" - , "" - ] - - restrictStates = - [ notEqual (t-1) (t'-1) states | t <- times, t' <- times, t' > t ] - - notEqual t t' states = - "OR(" ++ concat (intersperse ", " [ "~(" ++ s ++ "_t" ++ show t ++ " " - ++ eq ++ " " ++ s ++ "_t" ++ show t' ++ ")" - | (eq,s) <- states ]) - ++ ")" - ----------------------------------------------------------------- --- primitive proving - -data ProofResult - = Valid - | Falsifiable - | Indeterminate - deriving (Eq, Show) - -proveFile :: FilePath -> IO () -> [String] -> [Option] -> IO ProofResult -proveFile file before labels options = - do putStr ( "Proving:" - ++ concat (intersperse "," (map (" " ++) labels)) - ++ " " - ) - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/prover.wrapper " - ++ file - ++ " " - ++ opts - ++ " -model first" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - where - satOpt = searchOptVal options Sat - noBackOpt = searchOptBool options NoBacktracking - timeOpt = searchOptBool options ShowTime - opts = (if timeOpt then "-showTime " else "") - ++ ("-t " ++ show satOpt ++ " ") - ++ (if noBackOpt then "" else "-b") - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO ([State],Int) -writeDefinitions file props = - do han <- openFile file WriteMode - var <- newIORef 0 - sts <- newIORef [] - - let new = - do n <- readIORef var - let n' = n+1 - writeIORef var n' - return (Now ("w" ++ show n')) - - define v s = - do hPutStr han (def ++ ";\n") - case s of - DelayBool x y -> state ("<->",the y) - DelayInt x y -> state ("=",the y) - _ -> return () - where - def = - case s of - Bool True -> prop $ "TRUE" - Bool False -> prop $ "FALSE" - Inv x -> prop $ op1 "~" x - And xs -> prop $ opl "AND" "," xs "TRUE" - Or xs -> prop $ opl "OR" "," xs "FALSE" - Xor xs -> prop $ opl "XOR" "," xs "FALSE" - - Int n -> arit $ show n - Neg x -> arit $ op1 "-" x - Div x y -> arit $ op2 "/" x y - Mod x y -> arit $ op2 "%" x y - Plus xs -> arit $ opl "" "+" xs "0" - Times xs -> arit $ opl "" "*" xs "1" - Gte x y -> prop $ op2 ">=" x y - Equal xs -> prop $ equal xs - If x y z -> iff x (op2 "=" v y) (op2 "=" v z) - - VarBool s -> prop $ op0 (Now s) - VarInt s -> arit $ op0 (Now s) - - DelayBool x y -> iff ini (prop (op0 x)) (prop (op0 (pre y))) - DelayInt x y -> iff ini (arit (op0 x)) (arit (op0 (pre y))) - - prop form = - "(" ++ show v ++ " <-> (" ++ form ++ "))" - - arit expr = - "(" ++ show v ++ " = (" ++ expr ++ "))" - - iff c x y = - "(" ++ op0 c ++ " -> " ++ x ++ ") & (~" - ++ op0 c ++ " -> " ++ y ++ ")" - - state s = - do xs <- readIORef sts - writeIORef sts (s:xs) - - op0 v = show v - op1 op v = op ++ show v - op2 op v w = "(" ++ show v ++ " " ++ op ++ " " ++ show w ++ ")" - - opl fun con [] nul = nul - opl fun con [x] nul = show x - opl fun con xs nul = - fun ++ "(" ++ concat (intersperse con (map show xs)) ++ ")" - - equal (x:y:xs) = - (show x ++ " = " ++ show y) ++ " & " ++ equal (y:xs) - equal _ = "TRUE" - - ~(Compound vs) <- netlistIO new define (struct props) - let quests = [ Index quest i | i <- [1..] ] - sequence [ hPutStr han (show q ++ " <-> " ++ show v ++ ";\n") - | (q, Object v) <- quests `zip` vs - ] - hClose han - - states <- readIORef sts - return (states, length vs) - -type State - = (String, String) - -data Timed - = Now String - | Pre String - -instance Show Timed where - show (Now a) = a ++ "$now" - show (Pre a) = a ++ "$pre" - -the (Now a) = a -the (Pre a) = a -pre (Now a) = Pre a - -ini = Now "init" -quest = Now "quest" - -data Indexed - = Index Timed Int - -instance Show Indexed where - show (Index a n) = show a ++ "_n" ++ show n - ----------------------------------------------------------------- --- models - -displayModel :: FilePath -> (Model -> [[String]]) -> IO () -displayModel file showModel = - do s <- readFile file - let (first : model) = lines s - if "# counter model" `isPrefixOf` first - then do let inps = inputs model - table = makeTable inps [] - repr = showModel table - putStr (unlines (map showInput repr)) - else return () - where - inputs [] = [] - inputs (l:ls) = - case words l of - [v@('i':_), "=", val] -> (v, val) : rest - [v@('i':_)] -> (v, "high") : rest - ['~':v@('i':_)] -> (v, "low") : rest - _ -> rest - where - rest = inputs ls - - makeTable [] table = - table - - makeTable ((v,val):inps) table = - makeTable inps (extend name (read time) val table) - where - n = length v - name = take (n - length time - 2) v - time = reverse . takeWhile isDigit . reverse $ v - isDigit d = '0' <= d && d <= '9' - - extend name time val [] = - extend name time val [(name, [])] - - extend name time val (entry@(name',vals):table) - | name == name' = updated : table - | otherwise = entry : extend name time val table - where - updated = (name', make (time - 1) vals ++ [val] ++ drop time vals) - - make 0 xs = [] - make n [] = make n ["?"] - make n (x:xs) = x : make (n-1) xs - - showInput [x] = x - showInput xs = "<" ++ concat (intersperse "," xs) ++ ">" - ----------------------------------------------------------------- --- instantiation - -instantiateFile :: FilePath -> FilePath -> Int -> IO () -instantiateFile from to t = - do appendFile to ("/* time instance " ++ show t ++ " */\n") - system ( "sed " - ++ "-e 's/$now/_t" ++ show t ++ "/g' " - ++ "-e 's/$pre/_t" ++ show (t-1) ++ "/g' " - ++ "-e 's/;/,/g' " - ++ " < " ++ from ++ " >> " ++ to - ) - return () - ----------------------------------------------------------------- --- helper functions - -checkVerifyDir :: IO () -checkVerifyDir = - do system ("mkdir -p " ++ verifyDir) - return () - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Vhdl.hs b/Lava2000/Vhdl.hs deleted file mode 100644 --- a/Lava2000/Vhdl.hs +++ /dev/null @@ -1,199 +0,0 @@ -module Lava2000.Vhdl - ( writeVhdl - , writeVhdlInput - , writeVhdlInputOutput - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Error -import Lava2000.LavaDir - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import System.IO - ( stdout - , BufferMode (..) - , hSetBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- write vhdl - -writeVhdl :: (Constructive a, Generic b) => String -> (a -> b) -> IO () -writeVhdl name circ = - do writeVhdlInput name circ (var "inp") - -writeVhdlInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO () -writeVhdlInput name circ inp = - do writeVhdlInputOutput name circ inp (symbolize "outp" (circ inp)) - -writeVhdlInputOutput :: (Generic a, Generic b) - => String -> (a -> b) -> a -> b -> IO () -writeVhdlInputOutput name circ inp out = - do writeItAll name inp (circ inp) out - -writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO () -writeItAll name inp out out' = - do hSetBuffering stdout NoBuffering - putStr ("Writing to file \"" ++ file ++ "\" ... ") - writeDefinitions file name inp out out' - putStrLn "Done." - where - file = name ++ ".vhd" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: (Generic a, Generic b) - => FilePath -> String -> a -> b -> b -> IO () -writeDefinitions file name inp out out' = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "-- Generated by Lava 2000" - , "" - , "use work.all;" - , "" - , "entity" - , " " ++ name - , "is" - , "port" - , " -- clock" - , " ( " ++ "clk" ++ " : in bit" - , "" - , " -- inputs" - ] ++ - [ " ; " ++ v ++ " : in bit" - | VarBool v <- inps - ] ++ - [ "" - , " -- outputs" - ] ++ - [ " ; " ++ v ++ " : out bit" - | VarBool v <- outs' - ] ++ - [ " );" - , "end entity " ++ name ++ ";" - , "" - , "architecture" - , " structural" - , "of" - , " " ++ name - , "is" - ] - - hPutStr secondHandle $ unlines $ - [ "begin" - ] - - let new = - do n <- readIORef var - let n' = n+1; v = "w" ++ show n' - writeIORef var n' - hPutStr firstHandle (" signal " ++ v ++ " : bit;\n") - return v - - define v s = - case s of - Bool True -> port "vdd" [] - Bool False -> port "gnd" [] - Inv x -> port "inv" [x] - - And [] -> define v (Bool True) - And [x] -> port "id" [x] - And [x,y] -> port "and2" [x,y] - And (x:xs) -> define (w 0) (And xs) - >> define v (And [x,w 0]) - - Or [] -> define v (Bool False) - Or [x] -> port "id" [x] - Or [x,y] -> port "or2" [x,y] - Or (x:xs) -> define (w 0) (Or xs) - >> define v (Or [x,w 0]) - - Xor [] -> define v (Bool False) - Xor [x] -> port "id" [x] - Xor [x,y] -> port "xor2" [x,y] - Xor (x:xs) -> define (w 0) (Or xs) - >> define (w 1) (Inv (w 0)) - >> define (w 2) (And [x, w 1]) - - >> define (w 3) (Inv x) - >> define (w 4) (Xor xs) - >> define (w 5) (And [w 3, w 4]) - >> define v (Or [w 2, w 5]) - - VarBool s -> port "id" [s] - DelayBool x y -> port "delay" [x, y] - - _ -> wrong Lava2000.Error.NoArithmetic - where - w i = v ++ "_" ++ show i - - port name args = - do hPutStr secondHandle $ - " " - ++ make 9 ("c_" ++ v) - ++ " : entity " - ++ make 5 name - ++ " port map (" - ++ concat (intersperse ", " ("clk" : args ++ [v])) - ++ ");\n" - - outvs <- netlistIO new define (struct out) - hPutStr secondHandle $ unlines $ - [ "" - , " -- naming outputs" - ] - - sequence - [ define v' (VarBool v) - | (v,v') <- flatten outvs `zip` [ v' | VarBool v' <- outs' ] - ] - - hPutStr secondHandle $ unlines $ - [ "end structural;" - ] - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - sigs x = map unsymbol . flatten . struct $ x - - inps = sigs inp - outs' = sigs out' - - firstFile = file ++ "-1" - secondFile = file ++ "-2" - - make n s = take (n `max` length s) (s ++ repeat ' ') - - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Vis.hs b/Lava2000/Vis.hs deleted file mode 100644 --- a/Lava2000/Vis.hs +++ /dev/null @@ -1,265 +0,0 @@ -module Lava2000.Vis - ( vis - , writeVis - , writeVisInput - , writeVisInputOutput - , equivCheckVisInput - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- vis - -vis :: Checkable a => a -> IO ProofResult -vis a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile $ - writeDefinitions defsFile "circuit" - (Nothing :: Maybe ()) (delay high (andl props)) (var "good") - where - defsFile = verifyDir ++ "/circuit.mv" - ----------------------------------------------------------------- --- write Vis - -writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO () -writeVis name circ = - do writeVisInput name circ (var "inp") - -writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO () -writeVisInput name circ inp = - do writeVisInputOutput name circ inp (symbolize "outp" (circ inp)) - -writeVisInputOutput :: (Generic a, Generic b) - => String -> (a -> b) -> a -> b -> IO () -writeVisInputOutput name circ inp out = - do writeItAll name inp (circ inp) out - -writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO () -writeItAll name inp out out' = - do noBuffering - putStr ("Writing to file \"" ++ file ++ "\" ... ") - writeDefinitions file name (Just inp) out out' - putStrLn "Done." - where - file = name ++ ".mv" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: (Generic a, Generic b) - => FilePath -> String -> Maybe a -> b -> b -> IO () -writeDefinitions file name minp out out' = - do firstHandle <- openFile file1 WriteMode - secondHandle <- openFile file2 WriteMode - var <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ ".model " ++ name - ] ++ - [ ".inputs " ++ v - | VarBool v <- inps - ] - - hPutStr secondHandle $ unlines $ - [ ".outputs " ++ v - | VarBool v <- outs' - ] ++ - [ ".table -> low" - , "0" - , ".latch low initt" - , ".reset initt" - , "1" - ] - - let new = - do n <- readIORef var - let n' = n+1 - v = "w" ++ show n' - writeIORef var n' - return v - - define v s = - case s of - Bool True -> port (\_ -> True) [] - Bool False -> port (\_ -> False) [] - Inv x -> port (\[p] -> not p) [x] - - And [] -> define v (Bool True) - And [x] -> port (\[p] -> p) [x] - And [x,y] -> port (\[p,q] -> p && q) [x,y] - And (x:xs) -> define (w 0) (And xs) - >> define v (And [x,w 0]) - - Or [] -> define v (Bool False) - Or [x] -> port (\[p] -> p) [x] - Or [x,y] -> port (\[p,q] -> p || q) [x,y] - Or (x:xs) -> define (w 0) (Or xs) - >> define v (Or [x,w 0]) - - Xor [] -> define v (Bool False) - Xor [x] -> port (\[p] -> p) [x] - Xor [x,y] -> port (\[p,q] -> p /= q) [x,y] - Xor (x:xs) -> define (w 0) (Or xs) - >> define (w 1) (Inv (w 0)) - >> define (w 2) (And [x, w 1]) - - >> define (w 3) (Inv x) - >> define (w 4) (Xor xs) - >> define (w 5) (And [w 3, w 4]) - >> define v (Or [w 2, w 5]) - - VarBool s -> do port (\[p] -> p) [s] - case (minp,s) of - (Nothing, 'i':_) -> input s - _ -> return () - DelayBool x y -> delay x y - - _ -> wrong Lava2000.Error.NoArithmetic - where - w i = v ++ "_" ++ show i - - input s = - do hPutStr firstHandle $ - ".inputs " ++ s ++ "\n" - - port oper args = - do hPutStr secondHandle $ - ".table " - ++ unwords args - ++ " -> " - ++ v ++ "\n" - ++ unlines - [ line (xs ++ [oper xs]) - | xs <- binary (length args) - ] - where - line bs = - unwords (map (\b -> if b then "1" else "0") bs) - - binary 0 = [[]] - binary n = map (False:) xs ++ map (True:) xs - where - xs = binary (n-1) - - delay x y = - do hPutStr secondHandle $ unlines - [ ".latch " ++ y ++ " " ++ v ++ "_x" - , ".reset " ++ v ++ "_x" - , "0" - , ".table initt " ++ x ++ " " ++ v ++ "_x -> " ++ v - , "1 - - =" ++ x - , "0 - - =" ++ v ++ "_x" - ] - - outvs <- netlistIO new define (struct out) - - sequence - [ define v' (VarBool v) - | (v,v') <- flatten outvs `zip` [ v' | VarBool v' <- outs' ] - ] - - hPutStr secondHandle $ unlines $ - [ ".end" - ] - - hClose firstHandle - hClose secondHandle - system ("cat " ++ file1 ++ " " ++ file2 ++ " > " ++ file) - system ("rm " ++ file1 ++ " " ++ file2) - return () - where - file1 = file ++ "_1" - file2 = file ++ "_2" - - sigs x = map unsymbol . flatten . struct $ x - - inps = case minp of - Just inp -> sigs inp - Nothing -> [] - outs' = sigs out' - - make n s = take (n `max` length s) (s ++ repeat ' ') - ----------------------------------------------------------------- --- equivalence checking - -equivCheckVisInput circ1 circ2 inp = - do checkVerifyDir - noBuffering - writeVisInput name1 circ1 inp - writeVisInput name2 circ2 inp - putStr "Vis: ... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/vis.wrapper " - ++ name1 ++ " " ++ name2 - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - where - name = "Verify/circuit" - name1 = name ++ "_1" - name2 = name ++ "_2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Vis: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/vis-reach.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/Lava2000/Zchaff.hs b/Lava2000/Zchaff.hs deleted file mode 100644 --- a/Lava2000/Zchaff.hs +++ /dev/null @@ -1,150 +0,0 @@ -module Lava2000.Zchaff - ( zchaff - ) - where - -import Lava2000.Signal -import Lava2000.Netlist -import Lava2000.Generic -import Lava2000.Sequent -import Lava2000.Property -import Lava2000.Error -import Lava2000.LavaDir -import Lava2000.Verification - -import List - ( intersperse - , nub - ) - -import IO - ( openFile - , IOMode(..) - , hPutStr - , hClose - ) - -import Lava2000.IOBuffering - ( noBuffering - ) - -import Data.IORef - -import System.Cmd (system) -import System.Exit (ExitCode(..)) - ----------------------------------------------------------------- --- zchaff - -zchaff :: Checkable a => a -> IO ProofResult -zchaff a = - do checkVerifyDir - noBuffering - (props,_) <- properties a - proveFile defsFile (writeDefinitions defsFile props) - where - defsFile = verifyDir ++ "/circuit.cnf" - ----------------------------------------------------------------- --- definitions - -writeDefinitions :: FilePath -> [Signal Bool] -> IO () -writeDefinitions file props = - do firstHandle <- openFile firstFile WriteMode - secondHandle <- openFile secondFile WriteMode - var <- newIORef 0 - cls <- newIORef 0 - - hPutStr firstHandle $ unlines $ - [ "c Generated by Lava2000" - , "c " - ] - - let new = - do n <- readIORef var - let n' = n+1 - writeIORef var n' - return n' - - clause xs = - do n <- readIORef cls - let n' = n+1 in n' `seq` writeIORef cls n' - hPutStr secondHandle (unwords [ show x | x <- xs ] ++ " 0\n") - - define v s = - case s of - Bool True -> clause [ v ] - Bool False -> clause [ -v ] - Inv x -> clause [ -x, -v ] >> clause [ x, v ] - - And [] -> define v (Bool True) - And xs -> conjunction v xs - - Or [] -> define v (Bool False) - Or xs -> conjunction (-v) (map negate xs) - - Xor [] -> define v (Bool False) - Xor xs -> exactly1 v xs - - VarBool s -> hPutStr firstHandle ("c " ++ s ++ " : " ++ show v ++ "\n") - - DelayBool x y -> wrong Lava2000.Error.DelayEval - _ -> wrong Lava2000.Error.NoArithmetic - where - - conjunction v xs = - do clause (v : map negate xs) - sequence_ [ clause [ -v, x ] | x <- xs ] - - exactly1 v xs = - do clause (-v : xs) - sequence_ [ clause [ -v, -x, -y ] | (x,y) <- pairs xs ] - sequence_ [ clause ( v : -x : ys) | (x,ys) <- pick xs ] - - pairs [] = [] - pairs (x:xs) = [ (x,y) | y <- xs ] ++ pairs xs - - pick [] = [] - pick (x:xs) = (x,xs) : [ (y,x:ys) | (y,ys) <- pick xs ] - - outvs <- netlistIO new define (struct props) - clause (map negate (flatten outvs)) - - nvar <- readIORef var - ncls <- readIORef cls - hPutStr firstHandle ("p cnf " ++ show nvar ++ " " ++ show ncls ++ "\n") - - hClose firstHandle - hClose secondHandle - - system ("cat " ++ firstFile ++ " " ++ secondFile ++ " > " ++ file) - system ("rm " ++ firstFile ++ " " ++ secondFile) - return () - where - firstFile = file ++ "-1" - secondFile = file ++ "-2" - ----------------------------------------------------------------- --- primitive proving - -proveFile :: FilePath -> IO () -> IO ProofResult -proveFile file before = - do putStr "Zchaff: " - before - putStr "... " - lavadir <- getLavaDir - x <- system ( lavadir - ++ "/Scripts/zchaff.wrapper " - ++ file - ++ " -showTime" - ) - let res = case x of - ExitSuccess -> Valid - ExitFailure 1 -> Indeterminate - ExitFailure _ -> Falsifiable - putStrLn (show res ++ ".") - return res - ----------------------------------------------------------------- --- the end. - diff --git a/README b/README --- a/README +++ b/README @@ -1,6 +1,5 @@ -To get verification working (on Linux), change the path - - /home/emax/Program/chalmers-lava2000/ +To get verification working (on Linux), set the variables Lava2000_SMV and Lava2000_Satzoo to point to the binaries of the respective provers. -in Development/Lava2000/LavaDir.hs to the appropriate path, and change the wrapper scripts in the Scripts/ directory to point to the correct binaries. +Also make sure that the scripts smv.wrapper and satzoo.wrapper are executable. These scripts are possibly located in + $HOME/.cabal/share/chalmers-lava2000-1.1.0/Scripts diff --git a/Scripts/satzoo.wrapper b/Scripts/satzoo.wrapper --- a/Scripts/satzoo.wrapper +++ b/Scripts/satzoo.wrapper @@ -33,7 +33,6 @@ #- constants -Satzoo="/home/emax/Program/Satzoo/satzoo" Time="/tmp/lava-proof-time-$$" #---------------------------------------------------------------- @@ -41,7 +40,7 @@ satzoo_() { - time $Satzoo $Args $File 2> $Time + time $Lava2000_Satzoo $Args $File 2> $Time } satzoo_ > $Output diff --git a/Scripts/smv.wrapper b/Scripts/smv.wrapper --- a/Scripts/smv.wrapper +++ b/Scripts/smv.wrapper @@ -33,7 +33,6 @@ #- constants -Smv="/home/emax/Program/SMV/bin/smv" Time="/tmp/lava-proof-time-$$" #---------------------------------------------------------------- @@ -41,7 +40,7 @@ smv_() { - /usr/bin/time $Smv $File $Args 2> $Time + /usr/bin/time $Lava2000_SMV $File $Args 2> $Time } smv_ > $Output diff --git a/chalmers-lava2000.cabal b/chalmers-lava2000.cabal --- a/chalmers-lava2000.cabal +++ b/chalmers-lava2000.cabal @@ -1,5 +1,5 @@ name: chalmers-lava2000 -version: 1.0.2 +version: 1.1.0 homepage: http://www.cs.chalmers.se/~koen/Lava/ synopsis: Hardware description library description: Hardware description library @@ -11,52 +11,54 @@ maintainer: Emil Axelsson cabal-version: >= 1.2 build-type: Simple -data-files: README, INSTALL, Doc/tutorial.ps -extra-source-files: Vhdl/lava.vhd, Scripts/satzoo.wrapper, Scripts/smv.wrapper +data-files: README, INSTALL, Doc/tutorial.ps, Vhdl/lava.vhd, Scripts/satzoo.wrapper, Scripts/smv.wrapper library exposed-modules: - Lava2000 - Lava2000.Arithmetic - Lava2000.Captain - Lava2000.Combinational - Lava2000.ConstructiveAnalysis - Lava2000.Eprover - Lava2000.Error - Lava2000.Fixit - Lava2000.Generic - Lava2000.HeerHugo - Lava2000.IOBuffering - Lava2000.Isc - Lava2000.LavaDir - Lava2000.LavaRandom - Lava2000.Limmat - Lava2000.Modoc - Lava2000.MyST - Lava2000.Netlist - Lava2000.Operators - Lava2000.Patterns - Lava2000.Property - Lava2000.Ref - Lava2000.Retime - Lava2000.Satnik - Lava2000.Satzoo - Lava2000.Sequent - Lava2000.Sequential - Lava2000.SequentialCircuits - Lava2000.SequentialConstructive - Lava2000.Signal - Lava2000.SignalTry - Lava2000.Smv - Lava2000.Stable - Lava2000.Table - Lava2000.Test - Lava2000.Verification - Lava2000.Vhdl - Lava2000.Vis - Lava2000.Zchaff + Lava + Lava.Arithmetic + Lava.Captain + Lava.Combinational + Lava.ConstructiveAnalysis + Lava.Eprover + Lava.Error + Lava.Fixit + Lava.Generic + Lava.HeerHugo + Lava.IOBuffering + Lava.Isc + Lava.LavaDir + Lava.LavaRandom + Lava.Limmat + Lava.Modoc + Lava.MyST + Lava.Netlist + Lava.Operators + Lava.Patterns + Lava.Property + Lava.Ref + Lava.Retime + Lava.Satnik + Lava.Satzoo + Lava.Sequent + Lava.Sequential + Lava.SequentialCircuits + Lava.SequentialConstructive + Lava.Signal + Lava.SignalTry + Lava.Smv + Lava.Stable + Lava.Table + Lava.Test + Lava.Verification + Lava.Vhdl + Lava.Vis + Lava.Zchaff - build-Depends: base, haskell98, process + other-modules: + Paths_chalmers_lava2000 + + build-Depends: base >= 3 && < 4, haskell98 >= 1 && < 1.1, process >= 1 && < 1.1 extensions: Rank2Types, ExistentialQuantification ghc-options: -fno-warn-overlapping-patterns -fno-warn-missing-methods