module Language.ImProve.Examples
( buildGCD
, counter
, verifyCounter
, arbiterSpec
, arbiter
, arbiter1
, arbiter2
, arbiter3
, verifyArbiters
, buildArbiters
, runAll
) where
import Language.ImProve
gcd' :: E Int -> E Int -> Stmt (E Bool, E Int)
gcd' a b = do
a0 <- int "a0" 0
b0 <- int "b0" 0
a1 <- int "a1" 0
b1 <- int "b1" 0
"startNew" -| if_ (a /=. ref a0 ||. b /=. ref b0) $ do
a0 <== a
b0 <== b
a1 <== a
b1 <== b
"reduceA" -| if_ (ref a1 >. ref b1) $ do
a1 <== ref a1 ref b1
"reduceB" -| if_ (ref b1 >. ref a1) $ do
b1 <== ref b1 ref a1
return (ref a1 ==. ref b1, ref a1)
gcdMain :: Stmt ()
gcdMain = do
let a = input int ["a"]
b = input int ["b"]
done <- bool "done" False
result <- int "result" 0
(done', result') <- "gcd" -| gcd' a b
done <== done'
result <== result'
buildGCD :: IO ()
buildGCD = code "gcd" gcdMain
counter :: Stmt ()
counter = do
counter <- int "counter" 0
theorem "GreaterThanOrEqualTo0" 1 [] $ ref counter >=. 0
theorem "LessThan10" 1 [] $ ref counter <=. 9
ifelse (ref counter ==. 9) (counter <== 0) (counter <== ref counter + 1)
verifyCounter :: IO ()
verifyCounter = verify "yices" counter
arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
theorem "OneHot" 1 [] $ grantA &&. not_ grantB &&. not_ grantC
||. not_ grantA &&. grantB &&. not_ grantC
||. not_ grantA &&. not_ grantB &&. grantC
||. not_ grantA &&. not_ grantB &&. not_ grantC
theorem "NotRequestedA" 1 [] $ not_ requestA --> not_ grantA
theorem "NotRequestedB" 1 [] $ not_ requestB --> not_ grantB
theorem "NotRequestedC" 1 [] $ not_ requestC --> not_ grantC
theorem "OnlyRequestA" 1 [] $ ( requestA &&. not_ requestB &&. not_ requestC) --> grantA
theorem "OnlyRequestB" 1 [] $ (not_ requestA &&. requestB &&. not_ requestC) --> grantB
theorem "OnlyRequestC" 1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
theorem "Highest" 1 [] $ requestA --> grantA
theorem "Medium" 1 [] $ (not_ requestA &&. requestB) --> grantB
theorem "Lowest" 1 [] $ (not_ requestA &&. not_ requestB &&. requestC) --> grantC
return ()
arbiter1 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
arbiter1 (requestA, requestB, requestC) = do
let grantA = requestA
grantB = requestB
grantC = requestC
return (grantA, grantB, grantC)
arbiter2 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
arbiter2 (requestA, requestB, requestC) = do
grantA <- bool "grantA" False
grantB <- bool "grantB" False
grantC <- bool "grantC" False
"GrantA" -| if_ (requestA) (grantA <== true)
"GrantB" -| if_ (not_ requestA &&. requestB) (grantB <== true)
"GrantC" -| if_ (not_ requestA &&. not_ requestB &&. requestC) (grantC <== true)
return (ref grantA, ref grantB, ref grantC)
arbiter3 :: (E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)
arbiter3 (requestA, requestB, requestC) = do
let grantA = requestA
grantB = not_ requestA &&. requestB
grantC = not_ requestA &&. not_ requestB &&. requestC
return (grantA, grantB, grantC)
arbiter :: Name -> ((E Bool, E Bool, E Bool) -> Stmt (E Bool, E Bool, E Bool)) -> Stmt ()
arbiter name implementation = name -| do
let requestA = input bool ["requestA"]
requestB = input bool ["requestB"]
requestC = input bool ["requestC"]
let requests = (requestA, requestB, requestC)
grants@(grantA, grantB, grantC) <- "impl" -| implementation requests
arbiterSpec requests grants
bool' "grantA" grantA
bool' "grantB" grantB
bool' "grantC" grantC
return ()
verifyArbiters :: IO ()
verifyArbiters = do
putStrLn "\nVerifying arbiter1 ..."
verify "yices" $ arbiter "arbiter1" arbiter1
putStrLn "\nVerifying arbiter2 ..."
verify "yices" $ arbiter "arbiter2" arbiter2
putStrLn "\nVerifying arbiter2 ..."
verify "yices" $ arbiter "arbiter3" arbiter3
buildArbiters :: IO ()
buildArbiters = do
putStrLn "\nBuilding arbiter1 (arbiter1.c/h) ..."
code "arbiter1" $ arbiter "arbiter1" arbiter1
putStrLn "\nBuilding arbiter2 (arbiter2.c/h) ..."
code "arbiter2" $ arbiter "arbiter2" arbiter2
putStrLn "\nBuilding arbiter3 (arbiter3.c/h) ..."
code "arbiter3" $ arbiter "arbiter3" arbiter3
runAll :: IO ()
runAll = do
putStrLn "\nBuilding GCD (gcd.c, gcd.h) ..."
buildGCD
putStrLn "\nVerifying counter ..."
verifyCounter
putStrLn "\nVerifying arbiters ..."
verifyArbiters
putStrLn "\nBuilding arbiters ..."
buildArbiters