diff --git a/INSTALL b/INSTALL --- a/INSTALL +++ b/INSTALL @@ -14,9 +14,10 @@ # Verification -In order to use verification, make sure that the binaries `smv` and/or `satzoo` are visible in your path. +In order to use verification, make sure that the binaries `smv` and/or `minisat` are visible in your path. * SMV can be obtained from here: - * There is (as of 2015-10-23) a cached version of Satzoo available here: + * MiniSAT can be obtained from here: + - (We have tested with the pre-compiled Linux version 1.14.) -If verification gives ".../smv.wrapper Permission denied" (or similarly for `satzoo`), you need to mark the problematic files as executable. (That is, not the files in the `Scripts` directory, but the copy of those files that Cabal made during installation. +If verification gives ".../smv.wrapper Permission denied" (or similarly for `minisat`), you need to mark the problematic files as executable. (That is, not the files in the `Scripts` directory, but the copy of those files that Cabal made during installation. diff --git a/Lava/Minisat.hs b/Lava/Minisat.hs new file mode 100644 --- /dev/null +++ b/Lava/Minisat.hs @@ -0,0 +1,150 @@ +module Lava.Minisat + ( minisat + ) + 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 Data.List + ( intersperse + , nub + ) + +import System.IO + ( openFile + , IOMode(..) + , hPutStr + , hClose + ) + +import Lava.IOBuffering + ( noBuffering + ) + +import Data.IORef + +import System.Process (system) +import System.Exit (ExitCode(..)) + +---------------------------------------------------------------- +-- minisat + +minisat :: Checkable a => a -> IO ProofResult +minisat 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 "Minisat: " + before + putStr "... " + lavadir <- getLavaDir + x <- system ( lavadir + ++ "/Scripts/minisat.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/Scripts/minisat.wrapper b/Scripts/minisat.wrapper new file mode 100644 --- /dev/null +++ b/Scripts/minisat.wrapper @@ -0,0 +1,80 @@ +#!/bin/sh +#---------------------------------------------------------------- +#- Wrapper for minisat +#- to be used by the Lava system +#---------------------------------------------------------------- + +#- This file gets `File' as an argument, and produces the file +#- File.out, containing the output of prover. + +trap 'echo "(^C) \c"' INT + +#---------------------------------------------------------------- +#- Variables + +#- options + +cd "`dirname $1`" +File="`echo $1 | sed s!.*/!!`" +shift +ShowTime="no" + +if [ "$1" = "-showTime" ] +then + ShowTime="yes" + shift +fi + +Args="$*" + +#- derived + +Output="$File.out" + +#- constants + +Time="/tmp/lava-proof-time-$$" + +#---------------------------------------------------------------- +#- Running Minisat + +minisat_() +{ + time minisat $Args $File 2> $Time +} + +minisat_ > $Output + +#---------------------------------------------------------------- +#- Time + +seconds() +{ + if [ "$ShowTime" = "yes" ] + then + echo "(t=$2) \c" + fi +} + +seconds `tail -3 $Time` +cat $Time >> $Output +rm $Time 2> /dev/null + +#---------------------------------------------------------------- +#- Check Output + +if grep "UNSATISFIABLE" $Output > /dev/null +then + #- VALID + exit 0 +else if grep "SATISFIABLE" $Output > /dev/null +then + #- FALSIFIABLE + exit 2 +else + #- INDETERMINATE + exit 1 +fi; fi + +#---------------------------------------------------------------- +#- the end. diff --git a/chalmers-lava2000.cabal b/chalmers-lava2000.cabal --- a/chalmers-lava2000.cabal +++ b/chalmers-lava2000.cabal @@ -1,5 +1,5 @@ name: chalmers-lava2000 -version: 1.5.1 +version: 1.6 synopsis: Hardware description EDSL description: For more info, see the tutorial: category: Language, Hardware @@ -11,7 +11,7 @@ homepage: http://projects.haskell.org/chalmers-lava2000/Doc/tutorial.pdf cabal-version: >= 1.6 build-type: Simple -data-files: README, INSTALL, Doc/tutorial.pdf, Vhdl/lava.vhd, Scripts/satzoo.wrapper, Scripts/smv.wrapper +data-files: README, INSTALL, Doc/tutorial.pdf, Vhdl/lava.vhd, Scripts/*.wrapper source-repository head type: darcs @@ -34,6 +34,7 @@ Lava.LavaDir Lava.LavaRandom Lava.Limmat + Lava.Minisat Lava.Modoc Lava.MyST Lava.Netlist