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 :: Checkable a => a -> IO ProofResult
smv a =
do checkVerifyDir
noBuffering
(props,_) <- properties a
proveFile defsFile (writeDefinitions defsFile props)
where
defsFile = verifyDir ++ "/circuit.smv"
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"
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