module Lava.Isc
( IscMethod(..)
, isc
, iscWith
) where
import Lava.Ref
import Lava.Signal
import Lava.Generic
import Lava.Property
import Lava.LavaDir
import Lava.Sequent
import Lava.Netlist
import Lava.Verification
import Lava.IOBuffering
import Data.Array
import Lava.MyST
import Data.List(intersperse)
import System.Process (system)
import System.Exit (ExitCode(..))
data IscMethod
= StepMin
| StepMax
| Mixed
| Bmc
isc :: Checkable a => a -> IO ProofResult
isc :: a -> IO ProofResult
isc = IscMethod -> Int -> a -> IO ProofResult
forall a. Checkable a => IscMethod -> Int -> a -> IO ProofResult
iscWith IscMethod
Mixed 10
iscWith :: Checkable a => IscMethod -> Int -> a -> IO ProofResult
iscWith :: IscMethod -> Int -> a -> IO ProofResult
iscWith m :: IscMethod
m n :: Int
n a :: a
a =
do IO ()
checkVerifyDir
IO ()
noBuffering
String -> a -> IO ()
forall a. Checkable a => String -> a -> IO ()
net_ String
netfile a
a
String
lavadir <- IO String
getLavaDir
ExitCode
r <- String -> IO ExitCode
system (String
execute)
ProofResult -> IO ProofResult
forall (m :: * -> *) a. Monad m => a -> m a
return (ProofResult -> IO ProofResult) -> ProofResult -> IO ProofResult
forall a b. (a -> b) -> a -> b
$ case ExitCode
r of
ExitSuccess -> ProofResult
Valid
ExitFailure 1 -> ProofResult
Indeterminate
ExitFailure _ -> ProofResult
Falsifiable
where
execute :: String
execute = "isc "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
netfile String -> String -> String
forall a. [a] -> [a] -> [a]
++ " "
String -> String -> String
forall a. [a] -> [a] -> [a]
++ (IscMethod -> String
m2par IscMethod
m) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n
netfile :: String
netfile = String
verifyDir String -> String -> String
forall a. [a] -> [a] -> [a]
++ "/circuit.net"
m2par :: IscMethod -> String
m2par StepMin = "-smin"
m2par StepMax = "-smax"
m2par Mixed = "-mix"
m2par Bmc = "-bmc"
data Sign a = Pos a | Not a deriving (Int -> Sign a -> String -> String
[Sign a] -> String -> String
Sign a -> String
(Int -> Sign a -> String -> String)
-> (Sign a -> String)
-> ([Sign a] -> String -> String)
-> Show (Sign a)
forall a. Show a => Int -> Sign a -> String -> String
forall a. Show a => [Sign a] -> String -> String
forall a. Show a => Sign a -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Sign a] -> String -> String
$cshowList :: forall a. Show a => [Sign a] -> String -> String
show :: Sign a -> String
$cshow :: forall a. Show a => Sign a -> String
showsPrec :: Int -> Sign a -> String -> String
$cshowsPrec :: forall a. Show a => Int -> Sign a -> String -> String
Show, ReadPrec [Sign a]
ReadPrec (Sign a)
Int -> ReadS (Sign a)
ReadS [Sign a]
(Int -> ReadS (Sign a))
-> ReadS [Sign a]
-> ReadPrec (Sign a)
-> ReadPrec [Sign a]
-> Read (Sign a)
forall a. Read a => ReadPrec [Sign a]
forall a. Read a => ReadPrec (Sign a)
forall a. Read a => Int -> ReadS (Sign a)
forall a. Read a => ReadS [Sign a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Sign a]
$creadListPrec :: forall a. Read a => ReadPrec [Sign a]
readPrec :: ReadPrec (Sign a)
$creadPrec :: forall a. Read a => ReadPrec (Sign a)
readList :: ReadS [Sign a]
$creadList :: forall a. Read a => ReadS [Sign a]
readsPrec :: Int -> ReadS (Sign a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Sign a)
Read)
sneg :: Sign a -> Sign a
sneg (Pos x :: a
x) = a -> Sign a
forall a. a -> Sign a
Not a
x
sneg (Not x :: a
x) = a -> Sign a
forall a. a -> Sign a
Pos a
x
type NetList = Array Int (S (Sign Int))
instance Functor Sign where
fmap :: (a -> b) -> Sign a -> Sign b
fmap f :: a -> b
f (Pos x :: a
x) = b -> Sign b
forall a. a -> Sign a
Pos (a -> b
f a
x)
fmap f :: a -> b
f (Not x :: a
x) = b -> Sign b
forall a. a -> Sign a
Not (a -> b
f a
x)
showS :: S String -> String
showS :: S String -> String
showS (Bool b :: Bool
b) = "Bool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Bool -> String
forall a. Show a => a -> String
show Bool
b
showS (Or [x :: String
x,y :: String
y]) = "Or " String -> String -> String
forall a. [a] -> [a] -> [a]
++ "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ',' Char -> String -> String
forall a. a -> [a] -> [a]
: String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
showS (Xor [x :: String
x,y :: String
y]) = "Xor " String -> String -> String
forall a. [a] -> [a] -> [a]
++ "[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ ',' Char -> String -> String
forall a. a -> [a] -> [a]
: String
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
showS (VarBool v :: String
v) = "VarBool " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
forall a. Show a => a -> String
show String
v
showS (DelayBool x :: String
x y :: String
y) = "DelayBool (" 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
y String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
showS _ = String -> String
forall a. HasCallStack => String -> a
error "showS"
showN :: NetList -> String
showN :: NetList -> String
showN = Array Int String -> String
showA (Array Int String -> String)
-> (NetList -> Array Int String) -> NetList -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S (Sign Int) -> String) -> NetList -> Array Int String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (S String -> String
showS (S String -> String)
-> (S (Sign Int) -> S String) -> S (Sign Int) -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sign Int -> String) -> S (Sign Int) -> S String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Sign Int -> String
forall a. Show a => a -> String
show)
showA :: Array Int String -> String
showA :: Array Int String -> String
showA a :: Array Int String
a = "array " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Int, Int) -> String
forall a. Show a => a -> String
show (Array Int String -> (Int, Int)
forall i e. Array i e -> (i, i)
bounds Array Int String
a) String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [" String -> String -> String
forall a. [a] -> [a] -> [a]
++
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String] -> [String]
forall a. a -> [a] -> [a]
intersperse "," (((Int, String) -> String) -> [(Int, String)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (\ (i :: Int
i,s :: String
s) -> "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ "," String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")")
(Array Int String -> [(Int, String)]
forall i e. Ix i => Array i e -> [(i, e)]
assocs Array Int String
a)))
String -> String -> String
forall a. [a] -> [a] -> [a]
++ "]"
showAll :: (NetList, a) -> String
showAll (n :: NetList
n,p :: a
p) = "(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NetList -> String
showN NetList
n 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
p String -> String -> String
forall a. [a] -> [a] -> [a]
++ ")"
net_ :: Checkable a => String -> a -> IO ()
net_ :: String -> a -> IO ()
net_ file :: String
file a :: a
a = do
(NetList, Sign Int)
p <- a -> IO (NetList, Sign Int)
forall a. Checkable a => a -> IO (NetList, Sign Int)
net a
a
String -> String -> IO ()
writeFile String
file ((NetList, Sign Int) -> String
forall a. Show a => (NetList, a) -> String
showAll (NetList, Sign Int)
p)
net :: Checkable a => a -> IO (NetList, Sign Int)
net :: a -> IO (NetList, Sign Int)
net a :: a
a =
do (props :: [Signal Bool]
props,_) <- a -> IO ([Signal Bool], Model -> [[String]])
forall a.
Checkable a =>
a -> IO ([Signal Bool], Model -> [[String]])
properties a
a
let top :: Signal Bool
top = case [Signal Bool]
props of
[x :: Signal Bool
x] -> Signal Bool
x
xs :: [Signal Bool]
xs -> [Signal Bool] -> Signal Bool
andl [Signal Bool]
xs
let (tab :: [(Int, S (Sign Int))]
tab, Object top' :: Sign Int
top') = Struct Symbol -> ([(Int, S (Sign Int))], Struct (Sign Int))
forall (f :: * -> *).
Sequent f =>
f Symbol -> ([(Int, S (Sign Int))], f (Sign Int))
table (Signal Bool -> Struct Symbol
forall a. Generic a => a -> Struct Symbol
struct Signal Bool
top)
(NetList, Sign Int) -> IO (NetList, Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, Int) -> [(Int, S (Sign Int))] -> NetList
forall i e. Ix i => (i, i) -> [(i, e)] -> Array i e
array (0, [(Int, S (Sign Int))] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Int, S (Sign Int))]
tabInt -> Int -> Int
forall a. Num a => a -> a -> a
-1) [(Int, S (Sign Int))]
tab, Sign Int
top')
table :: Sequent f => f Symbol -> ([(Int,S (Sign Int))], f (Sign Int))
table :: f Symbol -> ([(Int, S (Sign Int))], f (Sign Int))
table str :: f Symbol
str =
(forall s. ST s ([(Int, S (Sign Int))], f (Sign Int)))
-> ([(Int, S (Sign Int))], f (Sign Int))
forall a. (forall s. ST s a) -> a
runST
( do STRef s Int
ref <- Int -> ST s (STRef s Int)
forall a s. a -> ST s (STRef s a)
newSTRef 0
STRef s [(Int, S (Sign Int))]
table <- [(Int, S (Sign Int))] -> ST s (STRef s [(Int, S (Sign Int))])
forall a s. a -> ST s (STRef s a)
newSTRef []
let define :: S (Sign Int) -> ST s (Sign Int)
define sym :: S (Sign Int)
sym = do
[(Int, S (Sign Int))]
tab <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
case S (Sign Int)
sym of
And xs :: [Sign Int]
xs -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Or ((Sign Int -> Sign Int) -> [Sign Int] -> [Sign Int]
forall a b. (a -> b) -> [a] -> [b]
map Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg [Sign Int]
xs) ST s (Sign Int) -> (Sign Int -> ST s (Sign Int)) -> ST s (Sign Int)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign Int -> ST s (Sign Int))
-> (Sign Int -> Sign Int) -> Sign Int -> ST s (Sign Int)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg
Or xs :: [Sign Int]
xs -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Or [Sign Int]
xs
Xor xs :: [Sign Int]
xs -> ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
forall s. [s] -> S s
Xor [Sign Int]
xs
Inv x :: Sign Int
x -> Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign Int -> Sign Int
forall a. Sign a -> Sign a
sneg Sign Int
x)
x :: S (Sign Int)
x -> do Int
v <- ST s Int
new
STRef s [(Int, S (Sign Int))] -> [(Int, S (Sign Int))] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [(Int, S (Sign Int))]
table ((Int
v,S (Sign Int)
x)(Int, S (Sign Int))
-> [(Int, S (Sign Int))] -> [(Int, S (Sign Int))]
forall a. a -> [a] -> [a]
:[(Int, S (Sign Int))]
tab)
Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Sign Int
forall a. a -> Sign a
Pos Int
v)
bin :: ([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin f :: [Sign Int] -> S (Sign Int)
f [x :: Sign Int
x] = Sign Int -> ST s (Sign Int)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign Int
x
bin f :: [Sign Int] -> S (Sign Int)
f (x :: Sign Int
x:y :: Sign Int
y:xs :: [Sign Int]
xs) = do
Int
v <- ST s Int
new
[(Int, S (Sign Int))]
tab <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
STRef s [(Int, S (Sign Int))] -> [(Int, S (Sign Int))] -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s [(Int, S (Sign Int))]
table ((Int
v, [Sign Int] -> S (Sign Int)
f [Sign Int
x,Sign Int
y]) (Int, S (Sign Int))
-> [(Int, S (Sign Int))] -> [(Int, S (Sign Int))]
forall a. a -> [a] -> [a]
: [(Int, S (Sign Int))]
tab)
([Sign Int] -> S (Sign Int)) -> [Sign Int] -> ST s (Sign Int)
bin [Sign Int] -> S (Sign Int)
f (Int -> Sign Int
forall a. a -> Sign a
Pos Int
vSign Int -> [Sign Int] -> [Sign Int]
forall a. a -> [a] -> [a]
:[Sign Int]
xs)
new :: ST s Int
new = do
Int
n <- STRef s Int -> ST s Int
forall s a. STRef s a -> ST s a
readSTRef STRef s Int
ref
STRef s Int -> Int -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s Int
ref (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+1)
Int -> ST s Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
n
f (Sign Int)
str' <- (S (Sign Int) -> ST s (Sign Int))
-> f Symbol -> ST s (f (Sign Int))
forall (f :: * -> *) v s.
Sequent f =>
(S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ S (Sign Int) -> ST s (Sign Int)
define f Symbol
str
[(Int, S (Sign Int))]
tab <- STRef s [(Int, S (Sign Int))] -> ST s [(Int, S (Sign Int))]
forall s a. STRef s a -> ST s a
readSTRef STRef s [(Int, S (Sign Int))]
table
([(Int, S (Sign Int))], f (Sign Int))
-> ST s ([(Int, S (Sign Int))], f (Sign Int))
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, S (Sign Int))]
tab, f (Sign Int)
str')
)
netlistST_ :: Sequent f => (S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ :: (S v -> ST s v) -> f Symbol -> ST s (f v)
netlistST_ define :: S v -> ST s v
define symbols :: f Symbol
symbols =
do TableST s (S Symbol) v
tab <- ST s (TableST s (S Symbol) v)
forall s a b. ST s (TableST s a b)
tableST
let gather :: Symbol -> ST s v
gather (Symbol sym :: Ref (S Symbol)
sym) =
do Maybe v
visited <- TableST s (S Symbol) v -> Ref (S Symbol) -> ST s (Maybe v)
forall s a b. TableST s a b -> Ref a -> ST s (Maybe b)
findST TableST s (S Symbol) v
tab Ref (S Symbol)
sym
case Maybe v
visited of
Just v :: v
v -> do v -> ST s v
forall (m :: * -> *) a. Monad m => a -> m a
return v
v
Nothing -> (v -> ST s v) -> ST s v
forall a s. (a -> ST s a) -> ST s a
fixST ((v -> ST s v) -> ST s v) -> (v -> ST s v) -> ST s v
forall a b. (a -> b) -> a -> b
$ \v :: v
v -> do
TableST s (S Symbol) v -> Ref (S Symbol) -> v -> ST s ()
forall s a b. TableST s a b -> Ref a -> b -> ST s ()
extendST TableST s (S Symbol) v
tab Ref (S Symbol)
sym v
v
S v
s <- (Symbol -> ST s v) -> S Symbol -> ST s (S v)
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap Symbol -> ST s v
gather (Ref (S Symbol) -> S Symbol
forall a. Ref a -> a
deref Ref (S Symbol)
sym)
S v -> ST s v
define S v
s
in (Symbol -> ST s v) -> f Symbol -> ST s (f v)
forall (m :: * -> *) (s :: * -> *) a b.
(Monad m, Sequent s) =>
(a -> m b) -> s a -> m (s b)
mmap Symbol -> ST s v
gather f Symbol
symbols