module Language.Atom.Verify (verify) where
import Data.Char
import Data.Int
import Data.List
import Data.Ratio
import Data.Word
import System.Process
import Language.Atom.Elaboration
import Language.Atom.Expressions
verify :: Int -> [[[Rule]]] -> [UV] -> (String, UE) -> IO Bool
verify depth rules uvs (name, assert) = do
putStrLn $ "Checking assertion " ++ name ++ "..."
verify
where
verify | assert == ubool True = return True
| assert == ubool False = putStrLn ("Assertion failed trivially.") >> return False
| otherwise = do
out <- readProcess "yices" ["-e"] yices
case parseYices out of
S "unsat" : _ -> return True
S "sat" : vars' -> do
let vars = map (parseVar uvs) vars'
putStrLn ("Assertion failed. See counter example: " ++ name ++ ".vcd")
writeFile (name ++ ".vcd") $ vcd uvs vars
return False
_ -> error "Unexpected results from yices."
assertUE :: Int -> String
assertUE step = "(assert (not " ++ f ++ "))\n"
where
f = case assert of
UVRef uv -> uvName step uv
_ -> error "expressions not supported assertions yet"
asserts = concatMap assertUE [0..depth]
yices = initialize uvs ++ concatMap (transition rules uvs) [1..depth] ++ asserts ++ "(check)"
yicesType :: Type -> String
yicesType t = case t of
Bool -> "bool"
Int8 -> "(bitvector 8)"
Int16 -> "(bitvector 16)"
Int32 -> "(bitvector 32)"
Int64 -> "(bitvector 64)"
Word8 -> "(bitvector 8)"
Word16 -> "(bitvector 16)"
Word32 -> "(bitvector 32)"
Word64 -> "(bitvector 64)"
Float -> "real"
Double -> "real"
vars :: [UV] -> Int -> String
vars uvs step = concatMap (var step) uvs
where
var :: Int -> UV -> String
var step uv = "(define " ++ uvName step uv ++ "::" ++ yicesType (uvType uv) ++ ")\n"
uvName :: Int -> UV -> String
uvName step (UV i _ _) = "v" ++ show i ++ "_" ++ show step
initialize :: [UV] -> String
initialize uvs = vars uvs 0 ++ concatMap initialize uvs
where
initialize :: UV -> String
initialize uv@(UV _ _ (Local c)) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"
initialize (UV _ _ (External _)) = ""
const :: Const -> String
const c = case c of
CBool c -> if c then "true" else "false"
CInt8 c -> "0b" ++ bits 8 (fromIntegral c)
CInt16 c -> "0b" ++ bits 16 (fromIntegral c)
CInt32 c -> "0b" ++ bits 32 (fromIntegral c)
CInt64 c -> "0b" ++ bits 64 (fromIntegral c)
CWord8 c -> "0b" ++ bits 8 (fromIntegral c)
CWord16 c -> "0b" ++ bits 16 (fromIntegral c)
CWord32 c -> "0b" ++ bits 32 (fromIntegral c)
CWord64 c -> "0b" ++ bits 64 (fromIntegral c)
CFloat c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
CDouble c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"
bits :: Int -> Word64 -> String
bits 0 _ = ""
bits n a = bits (n 1) (div a 2) ++ show (mod a 2)
transition :: [[[Rule]]] -> [UV] -> Int -> String
transition _ uvs step = vars uvs step ++ transition
where
transition = "; transition " ++ show (step 1) ++ " to " ++ show step ++ "\n" --XXX
getUV :: [UV] -> Int -> UV
getUV [] _ = error "Verify.getUV"
getUV (uv@(UV i _ _):_) j | i == j = uv
getUV (_:a) i = getUV a i
parseVar :: [UV] -> Group -> (Int, UV, String)
parseVar uvs (G [S "=", S name, value]) = (t, getUV uvs i, parseValue value)
where
(i', t') = break (== '_') $ tail name
i = read i'
t = read $ tail t'
parseVar _ g = error $ "Verify.parseVar: " ++ show g
parseValue :: Group -> String
parseValue (S ('0':'b':a)) = "b" ++ a ++ " "
parseValue (S "true") = "1"
parseValue (S "false") = "0"
parseValue (S v) = "r" ++ v ++ " "
parseValue (G [S "/", S n, S d]) = "r" ++ show (fromRational (read n % read d)) ++ " "
parseValue a = error $ "Verify.parseValue: " ++ show a
data Group = G [Group] | S String deriving Show
parseYices :: String -> [Group]
parseYices = groups . tokens
groups :: [String] -> [Group]
groups [] = []
groups ("(":a) = G (groups x) : groups y where (x, y) = split 0 [] a
groups (a:b) = S a : groups b
split :: Int -> [String] -> [String] -> ([String], [String])
split 0 a (")":b) = (reverse a, b)
split n a ("(":b) = split (n + 1) ("(" : a) b
split n a (")":b) = split (n 1) (")" : a) b
split n a (b:c) = split n (b:a) c
split _ _ [] = error "Verify.split"
tokens :: String -> [String]
tokens [] = []
tokens (a:b) | isSpace a = tokens b
tokens ('(':b) = "(" : tokens b
tokens (')':b) = ")" : tokens b
tokens a = tokens' "" a
tokens' :: String -> String -> [String]
tokens' a [] = [reverse a]
tokens' a c@(b:_) | isSpace b || elem b "()" = reverse a : tokens c
tokens' a (b:c) = tokens' (b:a) c
data Heirarchy = Variable UV | Module String [Heirarchy]
vcd :: [UV] -> [(Int, UV, String)] -> String
vcd uvs signals' = header ++ samples ++ end
where
signals = sortBy (\ (a,_,_) (b,_,_) -> compare a b) signals'
header = "$timescale\n 1 ms\n$end\n" ++ concatMap decl (heirarchy 0 uvs) ++ "$enddefinitions $end\n"
(lastTime, _, _) = last signals
end = "#" ++ show (lastTime + 1) ++ "\n"
decl :: Heirarchy -> String
decl (Module name subs) = "$scope module " ++ name ++ " $end\n" ++ concatMap decl subs ++ "$upscope $end\n"
decl (Variable uv) = declVar uv
declVar :: UV -> String
declVar uv@(UV i n _) = case uvType uv of
Bool -> "$var wire 1 " ++ code ++ " " ++ name ++ " $end\n"
Int8 -> "$var integer 8 " ++ code ++ " " ++ name ++ " $end\n"
Int16 -> "$var integer 16 " ++ code ++ " " ++ name ++ " $end\n"
Int32 -> "$var integer 32 " ++ code ++ " " ++ name ++ " $end\n"
Int64 -> "$var integer 64 " ++ code ++ " " ++ name ++ " $end\n"
Word8 -> "$var wire 8 " ++ code ++ " " ++ name ++ " $end\n"
Word16 -> "$var wire 16 " ++ code ++ " " ++ name ++ " $end\n"
Word32 -> "$var wire 32 " ++ code ++ " " ++ name ++ " $end\n"
Word64 -> "$var wire 64 " ++ code ++ " " ++ name ++ " $end\n"
Float -> "$var real 32 " ++ code ++ " " ++ name ++ " $end\n"
Double -> "$var real 64 " ++ code ++ " " ++ name ++ " $end\n"
where
code = vcdCode i
name = reverse $ takeWhile (/= '.') $ reverse n
samples = concatMap sample signals
sample (t, (UV i _ _), v) = "#" ++ show t ++ "\n" ++ v ++ vcdCode i ++ "\n"
heirarchy :: Int -> [UV] -> [Heirarchy]
heirarchy _ [] = []
heirarchy depth uvs = heirarchy' depth notvars ++ map Variable vars
where
isVar :: UV -> Bool
isVar uv = length (path depth uv) == 1
(vars, notvars) = partition isVar uvs
heirarchy' :: Int -> [UV] -> [Heirarchy]
heirarchy' _ [] = []
heirarchy' depth uvs@(a:_) = Module n (heirarchy (depth + 1) yes) : heirarchy' depth no
where
n = head $ path depth a
isMod uv = n == head (path depth uv)
(yes, no) = partition isMod uvs
path :: Int -> UV -> [String]
path depth (UV _ n _) = drop depth $ words $ map (\ c -> if c == '.' then ' ' else c) n
vcdCode :: Int -> String
vcdCode i | i < 94 = [chr (33 + mod i 94)]
vcdCode i = vcdCode (div i 94) ++ [chr (33 + mod i 94)]