module Language.Atom.Language
(
module Language.Atom.Expressions
, Atom
, atom
, period
, getPeriod
, phase
, exactPhase
, getPhase
, cond
, Assign (..)
, incr
, decr
, var
, var'
, array
, array'
, bool
, bool'
, int8
, int8'
, int16
, int16'
, int32
, int32'
, int64
, int64'
, word8
, word8'
, word16
, word16'
, word32
, word32'
, word64
, word64'
, float
, float'
, double
, double'
, action
, call
, probe
, probes
, assert
, cover
, assertImply
, Name
, liftIO
, path
, clock
, nextCoverage
) where
import Control.Monad
import Control.Monad.Trans
import Data.Int
import Data.Word
import Data.List (foldl')
import Language.Atom.Elaboration hiding (Atom)
import qualified Language.Atom.Elaboration as E
import Language.Atom.Expressions
import Language.Atom.UeMap hiding (typeOf)
infixr 1 <==
type Atom = E.Atom
atom :: Name -> Atom a -> Atom a
atom name design = do
name' <- addName name
(st1, (g1, parent)) <- get
(a, (st2, (g2, child))) <- liftIO $ buildAtom st1 g1 { gState = [] } name' design
put (st2, ( g2 { gState = gState g1 ++ [StateHierarchy name $ gState g2] }
, parent { atomSubs = atomSubs parent ++ [child] }))
return a
period :: Int -> Atom a -> Atom a
period n _ | n <= 0 = error "ERROR: Execution period must be greater than 0."
period n atom = do
(st, (g, a)) <- get
put (st, (g { gPeriod = n }, a))
r <- atom
(st', (g', a)) <- get
put (st', (g' { gPeriod = gPeriod g }, a))
return r
getPeriod :: Atom Int
getPeriod = do
(_, (g, _)) <- get
return $ gPeriod g
phase' :: (Int -> Phase) -> Int -> Atom a -> Atom a
phase' _ n _ | n < 0 = error $ "ERROR: phase " ++ show n ++ " must be at least 0."
phase' phType n atom = do
(st, (g, a)) <- get
if (n >= gPeriod g)
then error $ "ERROR: phase " ++ show n ++ " must be less than the current period "
++ show (gPeriod g) ++ "."
else do put (st, (g { gPhase = phType n }, a))
r <- atom
(st', (g', a)) <- get
put (st', (g' { gPhase = gPhase g }, a))
return r
phase :: Int -> Atom a -> Atom a
phase n a = phase' MinPhase n a
exactPhase :: Int -> Atom a -> Atom a
exactPhase n a = phase' ExactPhase n a
getPhase :: Atom Int
getPhase = do
(_, (g, _)) <- get
return $ case gPhase g of
MinPhase ph -> ph
ExactPhase ph -> ph
path :: Atom String
path = do
(_, (_, atom)) <- get
return $ atomName atom
bool :: Name -> Bool -> Atom (V Bool)
bool = var
bool' :: Name -> V Bool
bool' name = var' name Bool
int8 :: Name -> Int8 -> Atom (V Int8)
int8 = var
int8' :: Name -> V Int8
int8' name = var' name Int8
int16 :: Name -> Int16 -> Atom (V Int16)
int16 = var
int16' :: Name -> V Int16
int16' name = var' name Int16
int32 :: Name -> Int32 -> Atom (V Int32)
int32 = var
int32' :: Name -> V Int32
int32' name = var' name Int32
int64 :: Name -> Int64 -> Atom (V Int64)
int64 = var
int64' :: Name -> V Int64
int64' name = var' name Int64
word8 :: Name -> Word8 -> Atom (V Word8)
word8 = var
word8' :: Name -> V Word8
word8' name = var' name Word8
word16 :: Name -> Word16 -> Atom (V Word16)
word16 = var
word16' :: Name -> V Word16
word16' name = var' name Word16
word32 :: Name -> Word32 -> Atom (V Word32)
word32 = var
word32' :: Name -> V Word32
word32' name = var' name Word32
word64 :: Name -> Word64 -> Atom (V Word64)
word64 = var
word64' :: Name -> V Word64
word64' name = var' name Word64
float :: Name -> Float -> Atom (V Float)
float = var
float' :: Name -> V Float
float' name = var' name Float
double :: Name -> Double -> Atom (V Double)
double = var
double' :: Name -> V Double
double' name = var' name Double
action :: ([String] -> String) -> [UE] -> Atom ()
action f ues = do
(st, (g, a)) <- get
let (st', hashes) = foldl' (\(accSt,hs) ue -> let (h,accSt') = newUE ue accSt in
(accSt',h:hs))
(st,[]) ues
put (st', (g, a { atomActions = atomActions a ++ [(f, hashes)] }))
call :: Name -> Atom ()
call n = action (\ _ -> n ++ "()") []
probe :: Expr a => Name -> E a -> Atom ()
probe name a = do
(st, (g, atom)) <- get
let (h,st') = newUE (ue a) st
if any (\ (n, _) -> name == n) $ gProbes g
then error $ "ERROR: Duplicated probe name: " ++ name
else put (st', (g { gProbes = (name, h) : gProbes g }, atom))
probes :: Atom [(String, UE)]
probes = do
(st, (g, _)) <- get
let (strs,hs) = unzip (gProbes g)
let g' = zip strs (map (recoverUE st) hs)
return g'
incr :: (Assign a, NumE a) => V a -> Atom ()
incr a = a <== value a + 1
decr :: (Assign a, NumE a) => V a -> Atom ()
decr a = a <== value a 1
class Expr a => Assign a where
(<==) :: V a -> E a -> Atom ()
v <== e = do
(st, (g, atom)) <- get
let (h,st0) = newUE (ue e) st
let (muv,st1) = newUV (uv v) st0
put (st1, (g, atom { atomAssigns = (muv, h) : atomAssigns atom }))
instance Assign Bool
instance Assign Int8
instance Assign Int16
instance Assign Int32
instance Assign Int64
instance Assign Word8
instance Assign Word16
instance Assign Word32
instance Assign Word64
instance Assign Float
instance Assign Double
cond :: E Bool -> Atom ()
cond c = do
(st, (g, atom)) <- get
let ae = recoverUE st (atomEnable atom)
let (h,st') = newUE (uand ae (ue c)) st
put (st', (g, atom { atomEnable = h}))
clock :: E Word64
clock = value $ word64' "__global_clock"
nextCoverage :: Atom (E Word32, E Word32)
nextCoverage = do
action (const "__coverage_index = (__coverage_index + 1) % __coverage_len") []
return (value $ word32' "__coverage_index", value $ word32' "__coverage[__coverage_index]")
assert :: Name -> E Bool -> Atom ()
assert name check = do
(st, (g, atom)) <- get
let names = fst $ unzip $ atomAsserts atom
when (elem name names) (liftIO $ putStrLn $ "WARNING: Assertion name already used: " ++ name)
let (chk,st') = newUE (ue check) st
put (st', (g, atom { atomAsserts = (name, chk) : atomAsserts atom }))
assertImply :: Name -> E Bool -> E Bool -> Atom ()
assertImply name a b = do
assert name $ imply a b
cover (name ++ "Precondition") a
cover :: Name -> E Bool -> Atom ()
cover name check = do
(st, (g, atom)) <- get
let names = fst $ unzip $ atomCovers atom
when (elem name names) (liftIO $ putStrLn $ "WARNING: Coverage name already used: " ++ name)
let (chk,st') = newUE (ue check) st
put (st', (g, atom { atomCovers = (name, chk) : atomCovers atom }))