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
label "startNew" $ if_ (a /=. ref a0 ||. b /=. ref b0) $ do
a0 <== a
b0 <== b
a1 <== a
b1 <== b
label "reduceA" $ if_ (ref a1 >. ref b1) $ do
a1 <== ref a1 ref b1
label "reduceB" $ if_ (ref b1 >. ref a1) $ do
b1 <== ref b1 ref a1
return (ref a1 ==. ref b1, ref a1)
gcdMain :: Stmt ()
gcdMain = do
a <- input int "a"
b <- input int "b"
done <- bool "done" False
result <- int "result" 0
(done', result') <- scope "gcd" $ gcd' a b
done <== done'
result <== result'
buildGCD :: IO ()
buildGCD = code "gcd" gcdMain
counter :: Stmt ()
counter = do
counter <- int "counter" 0
label "GreaterThanOrEqualTo0" $ assert $ ref counter >=. 0
label "LessThan10" $ assert $ ref counter <. 10
ifelse (ref counter ==. 10) (counter <== 0) (counter <== ref counter + 1)
verifyCounter :: IO ()
verifyCounter = verify "yices" 20 counter
arbiterSpec :: (E Bool, E Bool, E Bool) -> (E Bool, E Bool, E Bool) -> Stmt ()
arbiterSpec (requestA, requestB, requestC) (grantA, grantB, grantC) = do
label "OneHot" $ assert $ grantA &&. not_ grantB &&. not_ grantC
||. not_ grantA &&. grantB &&. not_ grantC
||. not_ grantA &&. not_ grantB &&. grantC
||. not_ grantA &&. not_ grantB &&. not_ grantC
label "NotRequestedA" $ assert $ imply (not_ requestA) (not_ grantA)
label "NotRequestedB" $ assert $ imply (not_ requestB) (not_ grantB)
label "NotRequestedC" $ assert $ imply (not_ requestC) (not_ grantC)
label "OnlyRequestA" $ assert $ imply ( requestA &&. not_ requestB &&. not_ requestC) grantA
label "OnlyRequestB" $ assert $ imply (not_ requestA &&. requestB &&. not_ requestC) grantB
label "OnlyRequestC" $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC
label "Highest" $ assert $ imply requestA grantA
label "Medium" $ assert $ imply (not_ requestA &&. requestB) grantB
label "Lowest" $ assert $ imply (not_ requestA &&. not_ requestB &&. requestC) grantC
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
label "GrantA" $ if_ (requestA) (grantA <== true)
label "GrantB" $ if_ (not_ requestA &&. requestB) (grantB <== true)
label "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 = scope name $ do
requestA <- input bool "requestA"
requestB <- input bool "requestB"
requestC <- input bool "requestC"
let requests = (requestA, requestB, requestC)
grants@(grantA, grantB, grantC) <- scope "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" 20 $ arbiter "arbiter1" arbiter1
putStrLn "\nVerifying arbiter2 ..."
verify "yices" 20 $ arbiter "arbiter2" arbiter2
putStrLn "\nVerifying arbiter2 ..."
verify "yices" 20 $ 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