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