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 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(..))
vis :: Checkable a => a -> IO ProofResult
vis :: a -> IO ProofResult
vis a :: a
a =
do IO ()
checkVerifyDir
IO ()
noBuffering
(props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
String -> IO () -> IO ProofResult
proveFile String
defsFile (IO () -> IO ProofResult) -> IO () -> IO ProofResult
forall a b. (a -> b) -> a -> b
$
String -> String -> Maybe () -> Signal Bool -> Signal Bool -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions String
defsFile "circuit"
(Maybe ()
forall a. Maybe a
Nothing :: Maybe ()) (Signal Bool -> Signal Bool -> Signal Bool
forall a. Generic a => a -> a -> a
delay Signal Bool
high ([Signal Bool] -> Signal Bool
andl [Signal Bool]
props)) (String -> Signal Bool
forall a. Constructive a => String -> a
var "good")
where
defsFile :: String
defsFile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.mv"
writeVis :: (Constructive a, Generic b) => String -> (a -> b) -> IO ()
writeVis :: String -> (a -> b) -> IO ()
writeVis name :: String
name circ :: a -> b
circ =
do String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name a -> b
circ (String -> a
forall a. Constructive a => String -> a
var "inp")
writeVisInput :: (Generic a, Generic b) => String -> (a -> b) -> a -> IO ()
writeVisInput :: String -> (a -> b) -> a -> IO ()
writeVisInput name :: String
name circ :: a -> b
circ inp :: a
inp =
do String -> (a -> b) -> a -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput String
name a -> b
circ a
inp (String -> b -> b
forall a. Generic a => String -> a -> a
symbolize "outp" (a -> b
circ a
inp))
writeVisInputOutput :: (Generic a, Generic b)
=> String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput :: String -> (a -> b) -> a -> b -> IO ()
writeVisInputOutput name :: String
name circ :: a -> b
circ inp :: a
inp out :: b
out =
do String -> a -> b -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> a -> b -> b -> IO ()
writeItAll String
name a
inp (a -> b
circ a
inp) b
out
writeItAll :: (Generic a, Generic b) => String -> a -> b -> b -> IO ()
writeItAll :: String -> a -> b -> b -> IO ()
writeItAll name :: String
name inp :: a
inp out :: b
out out' :: b
out' =
do IO ()
noBuffering
String -> IO ()
putStr ("Writing to file \"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\" ... ")
String -> String -> Maybe a -> b -> b -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions String
file String
name (a -> Maybe a
forall a. a -> Maybe a
Just a
inp) b
out b
out'
String -> IO ()
putStrLn "Done."
where
file :: String
file = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".mv"
writeDefinitions :: (Generic a, Generic b)
=> FilePath -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions :: String -> String -> Maybe a -> b -> b -> IO ()
writeDefinitions file :: String
file name :: String
name minp :: Maybe a
minp out :: b
out out' :: b
out' =
do Handle
firstHandle <- String -> IOMode -> IO Handle
openFile String
file1 IOMode
WriteMode
Handle
secondHandle <- String -> IOMode -> IO Handle
openFile String
file2 IOMode
WriteMode
IORef Integer
var <- Integer -> IO (IORef Integer)
forall a. a -> IO (IORef a)
newIORef 0
Handle -> String -> IO ()
hPutStr Handle
firstHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ ".model " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name
] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ ".inputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
| VarBool v :: String
v <- [S Symbol]
inps
]
Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ ".outputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
| VarBool v :: String
v <- [S Symbol]
outs'
] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
[ ".table -> low"
, "0"
, ".latch low initt"
, ".reset initt"
, "1"
]
let new :: IO String
new =
do Integer
n <- IORef Integer -> IO Integer
forall a. IORef a -> IO a
readIORef IORef Integer
var
let n' :: Integer
n' = Integer
nInteger -> Integer -> Integer
forall a. Num a => a -> a -> a
+1
v :: String
v = "w" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n'
IORef Integer -> Integer -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef Integer
var Integer
n'
String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return String
v
define :: String -> S String -> IO ()
define v :: String
v s :: S String
s =
case S String
s of
Bool True -> ([Bool] -> Bool) -> [String] -> IO ()
port (\_ -> Bool
True) []
Bool False -> ([Bool] -> Bool) -> [String] -> IO ()
port (\_ -> Bool
False) []
Inv x :: String
x -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool -> Bool
not Bool
p) [String
x]
And [] -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
True)
And [x :: String
x] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool
p) [String
x]
And [x :: String
x,y :: String
y] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
&& Bool
q) [String
x,String
y]
And (x :: String
x:xs :: [String]
xs) -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
And [String]
xs)
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v ([String] -> S String
forall s. [s] -> S s
And [String
x,Integer -> String
forall a. Show a => a -> String
w 0])
Or [] -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
Or [x :: String
x] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool
p) [String
x]
Or [x :: String
x,y :: String
y] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
|| Bool
q) [String
x,String
y]
Or (x :: String
x:xs :: [String]
xs) -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
Or [String]
xs)
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v ([String] -> S String
forall s. [s] -> S s
Or [String
x,Integer -> String
forall a. Show a => a -> String
w 0])
Xor [] -> String -> S String -> IO ()
define String
v (Bool -> S String
forall s. Bool -> S s
Bool Bool
False)
Xor [x :: String
x] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool
p) [String
x]
Xor [x :: String
x,y :: String
y] -> ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p,q :: Bool
q] -> Bool
p Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Bool
q) [String
x,String
y]
Xor (x :: String
x:xs :: [String]
xs) -> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 0) ([String] -> S String
forall s. [s] -> S s
Or [String]
xs)
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 1) (String -> S String
forall s. s -> S s
Inv (Integer -> String
forall a. Show a => a -> String
w 0))
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 2) ([String] -> S String
forall s. [s] -> S s
And [String
x, Integer -> String
forall a. Show a => a -> String
w 1])
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 3) (String -> S String
forall s. s -> S s
Inv String
x)
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 4) ([String] -> S String
forall s. [s] -> S s
Xor [String]
xs)
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define (Integer -> String
forall a. Show a => a -> String
w 5) ([String] -> S String
forall s. [s] -> S s
And [Integer -> String
forall a. Show a => a -> String
w 3, Integer -> String
forall a. Show a => a -> String
w 4])
IO () -> IO () -> IO ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> S String -> IO ()
define String
v ([String] -> S String
forall s. [s] -> S s
Or [Integer -> String
forall a. Show a => a -> String
w 2, Integer -> String
forall a. Show a => a -> String
w 5])
VarBool s :: String
s -> do ([Bool] -> Bool) -> [String] -> IO ()
port (\[p :: Bool
p] -> Bool
p) [String
s]
case (Maybe a
minp,String
s) of
(Nothing, 'i':_) -> String -> IO ()
input String
s
_ -> () -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
DelayBool x :: String
x y :: String
y -> String -> String -> IO ()
delay String
x String
y
_ -> Error -> IO ()
forall a. Error -> a
wrong Error
Lava.Error.NoArithmetic
where
w :: a -> String
w i :: a
i = String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
i
input :: String -> IO ()
input s :: String
s =
do Handle -> String -> IO ()
hPutStr Handle
firstHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
".inputs " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
port :: ([Bool] -> Bool) -> [String] -> IO ()
port oper :: [Bool] -> Bool
oper args :: [String]
args =
do Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$
".table "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unwords [String]
args
String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -> "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
String -> String -> String
forall a. [a] -> [a] -> [a]
++ [String] -> String
unlines
[ [Bool] -> String
line ([Bool]
xs [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [[Bool] -> Bool
oper [Bool]
xs])
| [Bool]
xs <- Int -> [[Bool]]
forall a. (Eq a, Num a) => a -> [[Bool]]
binary ([String] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [String]
args)
]
where
line :: [Bool] -> String
line bs :: [Bool]
bs =
[String] -> String
unwords ((Bool -> String) -> [Bool] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\b :: Bool
b -> if Bool
b then "1" else "0") [Bool]
bs)
binary :: a -> [[Bool]]
binary 0 = [[]]
binary n :: a
n = ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
FalseBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) [[Bool]]
xs [[Bool]] -> [[Bool]] -> [[Bool]]
forall a. [a] -> [a] -> [a]
++ ([Bool] -> [Bool]) -> [[Bool]] -> [[Bool]]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
TrueBool -> [Bool] -> [Bool]
forall a. a -> [a] -> [a]
:) [[Bool]]
xs
where
xs :: [[Bool]]
xs = a -> [[Bool]]
binary (a
na -> a -> a
forall a. Num a => a -> a -> a
-1)
delay :: String -> String -> IO ()
delay x :: String
x y :: String
y =
do Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
[ ".latch " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
, ".reset " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
, "0"
, ".table initt " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x -> " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v
, "1 - - =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x
, "0 - - =" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
v String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_x"
]
Struct String
outvs <- IO String
-> (String -> S String -> IO ())
-> Struct Symbol
-> IO (Struct String)
forall (f :: * -> *) v.
Sequent f =>
IO v -> (v -> S v -> IO ()) -> f Symbol -> IO (f v)
netlistIO IO String
new String -> S String -> IO ()
define (b -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct b
out)
[IO ()] -> IO [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence
[ String -> S String -> IO ()
define String
v' (String -> S String
forall s. String -> S s
VarBool String
v)
| (v :: String
v,v' :: String
v') <- Struct String -> [String]
forall a. Struct a -> [a]
flatten Struct String
outvs [String] -> [String] -> [(String, String)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [ String
v' | VarBool v' :: String
v' <- [S Symbol]
outs' ]
]
Handle -> String -> IO ()
hPutStr Handle
secondHandle (String -> IO ()) -> String -> IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
[ ".end"
]
Handle -> IO ()
hClose Handle
firstHandle
Handle -> IO ()
hClose Handle
secondHandle
String -> IO ExitCode
system ("cat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file2 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " > " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file)
String -> IO ExitCode
system ("rm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file2)
() -> IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
where
file1 :: String
file1 = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_1"
file2 :: String
file2 = String
file String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_2"
sigs :: a -> [S Symbol]
sigs x :: a
x = (Symbol -> S Symbol) -> [Symbol] -> [S Symbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> S Symbol
unsymbol ([Symbol] -> [S Symbol]) -> (a -> [Symbol]) -> a -> [S Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Struct Symbol -> [Symbol]
forall a. Struct a -> [a]
flatten (Struct Symbol -> [Symbol])
-> (a -> Struct Symbol) -> a -> [Symbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct (a -> [S Symbol]) -> a -> [S Symbol]
forall a b. (a -> b) -> a -> b
$ a
x
inps :: [S Symbol]
inps = case Maybe a
minp of
Just inp :: a
inp -> a -> [S Symbol]
forall a. Generic a => a -> [S Symbol]
sigs a
inp
Nothing -> []
outs' :: [S Symbol]
outs' = b -> [S Symbol]
forall a. Generic a => a -> [S Symbol]
sigs b
out'
make :: Int -> String -> String
make n :: Int
n s :: String
s = Int -> String -> String
forall a. Int -> [a] -> [a]
take (Int
n Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) (String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
forall a. a -> [a]
repeat ' ')
equivCheckVisInput :: (a -> b) -> (a -> b) -> a -> IO ProofResult
equivCheckVisInput circ1 :: a -> b
circ1 circ2 :: a -> b
circ2 inp :: a
inp =
do IO ()
checkVerifyDir
IO ()
noBuffering
String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name1 a -> b
circ1 a
inp
String -> (a -> b) -> a -> IO ()
forall a b.
(Generic a, Generic b) =>
String -> (a -> b) -> a -> IO ()
writeVisInput String
name2 a -> b
circ2 a
inp
String -> IO ()
putStr "Vis: ... "
String
lavadir <- IO String
getLavaDir
ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/vis.wrapper "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
name2
String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime"
)
let res :: ProofResult
res = case ExitCode
x of
ExitSuccess -> ProofResult
Valid
ExitFailure 1 -> ProofResult
Indeterminate
ExitFailure _ -> ProofResult
Falsifiable
String -> IO ()
putStrLn (ProofResult -> String
forall a. Show a => a -> String
show ProofResult
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".")
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res
where
name :: String
name = "Verify/circuit"
name1 :: String
name1 = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_1"
name2 :: String
name2 = String
name String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_2"
proveFile :: FilePath -> IO () -> IO ProofResult
proveFile :: String -> IO () -> IO ProofResult
proveFile file :: String
file before :: IO ()
before =
do String -> IO ()
putStr "Vis: "
IO ()
before
String -> IO ()
putStr "... "
String
lavadir <- IO String
getLavaDir
ExitCode
x <- String -> IO ExitCode
system ( String
lavadir
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/Scripts/vis-reach.wrapper "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
file
String -> String -> String
forall a. [a] -> [a] -> [a]
++ " -showTime"
)
let res :: ProofResult
res = case ExitCode
x of
ExitSuccess -> ProofResult
Valid
ExitFailure 1 -> ProofResult
Indeterminate
ExitFailure _ -> ProofResult
Falsifiable
String -> IO ()
putStrLn (ProofResult -> String
forall a. Show a => a -> String
show ProofResult
res String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".")
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return ProofResult
res