chalmers-lava2000 1.5.1 → 1.6
raw patch · 4 files changed
+237/−5 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
+ Lava.Minisat: minisat :: Checkable a => a -> IO ProofResult
Files
- INSTALL +4/−3
- Lava/Minisat.hs +150/−0
- Scripts/minisat.wrapper +80/−0
- chalmers-lava2000.cabal +3/−2
INSTALL view
@@ -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: <http://www.cs.cmu.edu/~modelcheck/smv.html>- * There is (as of 2015-10-23) a cached version of Satzoo available here: <http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.cs.chalmers.se/~een/Satzoo/>+ * MiniSAT can be obtained from here: <http://minisat.se/MiniSat.html>+ - (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.
+ Lava/Minisat.hs view
@@ -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.+
+ Scripts/minisat.wrapper view
@@ -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.
chalmers-lava2000.cabal view
@@ -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: <http://projects.haskell.org/chalmers-lava2000/Doc/tutorial.pdf> 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