module Language.Atom.Elaboration
(
Atom
, AtomDB (..)
, Global (..)
, Rule (..)
, StateHierarchy (..)
, buildAtom
, UID
, Name
, Phase (..)
, Path
, elaborate
, var
, var'
, array
, array'
, addName
, get
, put
, allUVs
, allUEs
) where
import Control.Monad.Trans
import Data.Function (on)
import Data.List
import Data.Char
import qualified Control.Monad.State.Strict as S
import Language.Atom.Expressions hiding (typeOf)
import Language.Atom.UeMap
type UID = Int
type Name = String
type Path = [Name]
data Phase = MinPhase Int | ExactPhase Int
data Global = Global
{ gRuleId :: Int
, gVarId :: Int
, gArrayId :: Int
, gState :: [StateHierarchy]
, gProbes :: [(String, Hash)]
, gPeriod :: Int
, gPhase :: Phase
}
data AtomDB = AtomDB
{ atomId :: Int
, atomName :: Name
, atomNames :: [Name]
, atomEnable :: Hash
, atomSubs :: [AtomDB]
, atomPeriod :: Int
, atomPhase :: Phase
, atomAssigns :: [(MUV, Hash)]
, atomActions :: [([String] -> String, [Hash])]
, atomAsserts :: [(Name, Hash)]
, atomCovers :: [(Name, Hash)]
}
data Rule
= Rule
{ ruleId :: Int
, ruleName :: Name
, ruleEnable :: Hash
, ruleAssigns :: [(MUV, Hash)]
, ruleActions :: [([String] -> String, [Hash])]
, rulePeriod :: Int
, rulePhase :: Phase
}
| Assert
{ ruleName :: Name
, ruleEnable :: Hash
, ruleAssert :: Hash
}
| Cover
{ ruleName :: Name
, ruleEnable :: Hash
, ruleCover :: Hash
}
data StateHierarchy
= StateHierarchy Name [StateHierarchy]
| StateVariable Name Const
| StateArray Name [Const]
instance Show AtomDB where show = atomName
instance Eq AtomDB where (==) = (==) `on` atomId
instance Ord AtomDB where compare a b = compare (atomId a) (atomId b)
instance Show Rule where show = ruleName
elaborateRules:: Hash -> AtomDB -> UeState [Rule]
elaborateRules parentEnable atom =
if isRule
then do r <- rule
rs <- rules
return $ r : rs
else rules
where
isRule = not $ null (atomAssigns atom) && null (atomActions atom)
enable :: UeState Hash
enable = do
st <- S.get
let (h,st') = newUE (uand (recoverUE st parentEnable)
(recoverUE st (atomEnable atom)))
st
S.put st'
return h
rule :: UeState Rule
rule = do
h <- enable
assigns <- S.foldM (\prs pr -> do pr' <- enableAssign pr
return $ pr' : prs) []
(atomAssigns atom)
return $ Rule
{ ruleId = atomId atom
, ruleName = atomName atom
, ruleEnable = h
, ruleAssigns = assigns
, ruleActions = atomActions atom
, rulePeriod = atomPeriod atom
, rulePhase = atomPhase atom
}
assert :: (Name, Hash) -> UeState Rule
assert (name, ue) = do
h <- enable
return $ Assert
{ ruleName = name
, ruleEnable = h
, ruleAssert = ue
}
cover :: (Name, Hash) -> UeState Rule
cover (name, ue) = do
h <- enable
return $ Cover
{ ruleName = name
, ruleEnable = h
, ruleCover = ue
}
rules :: UeState [Rule]
rules = do
asserts <- S.foldM (\rs e -> do r <- assert e
return $ r:rs
) [] (atomAsserts atom)
covers <- S.foldM (\rs e -> do r <- cover e
return $ r:rs
) [] (atomCovers atom)
rules' <- S.foldM (\rs db -> do en <- enable
r <- elaborateRules en db
return $ r:rs
) [] (atomSubs atom)
return $ asserts ++ covers ++ concat rules'
enableAssign :: (MUV, Hash) -> UeState (MUV, Hash)
enableAssign (uv, ue) = do
e <- enable
h <- maybeUpdate (MUVRef uv)
st <- S.get
let (h',st') = newUE (umux (recoverUE st e)
(recoverUE st ue)
(recoverUE st h))
st
S.put st'
return (uv, h')
reIdRules :: Int -> [Rule] -> [Rule]
reIdRules _ [] = []
reIdRules i (a:b) = case a of
Rule _ _ _ _ _ _ _ -> a { ruleId = i } : reIdRules (i + 1) b
_ -> a : reIdRules i b
buildAtom :: UeMap -> Global -> Name -> Atom a -> IO (a, AtomSt)
buildAtom st g name (Atom f) = do
let (h,st') = newUE (ubool True) st
f (st', (g { gRuleId = gRuleId g + 1 }, AtomDB
{ atomId = gRuleId g
, atomName = name
, atomNames = []
, atomEnable = h
, atomSubs = []
, atomPeriod = gPeriod g
, atomPhase = gPhase g
, atomAssigns = []
, atomActions = []
, atomAsserts = []
, atomCovers = []
}))
type AtomSt = (UeMap, (Global, AtomDB))
data Atom a = Atom (AtomSt -> IO (a, AtomSt))
instance Monad Atom where
return a = Atom (\ s -> return (a, s))
(Atom f1) >>= f2 = Atom f3
where
f3 s = do
(a, s) <- f1 s
let Atom f4 = f2 a
f4 s
instance MonadIO Atom where
liftIO io = Atom f
where
f s = do
a <- io
return (a, s)
get :: Atom AtomSt
get = Atom (\ s -> return (s, s))
put :: AtomSt -> Atom ()
put s = Atom (\ _ -> return ((), s))
elaborate :: UeMap -> Name -> Atom ()
-> IO (Maybe ( UeMap
, ( StateHierarchy, [Rule], [Name], [Name]
, [(Name, Type)])
))
elaborate st name atom = do
(_, (st0, (g, atomDB))) <- buildAtom st Global { gRuleId = 0
, gVarId = 0
, gArrayId = 0
, gState = []
, gProbes = []
, gPeriod = 1
, gPhase = MinPhase 0
}
name atom
let (h,st1) = newUE (ubool True) st0
(getRules,st2) = S.runState (elaborateRules h atomDB) st1
rules = reIdRules 0 (reverse getRules)
coverageNames = [ name | Cover name _ _ <- rules ]
assertionNames = [ name | Assert name _ _ <- rules ]
probeNames = [ (n, typeOf a st2) | (n, a) <- gProbes g ]
if (null rules)
then do
putStrLn "ERROR: Design contains no rules. Nothing to do."
return Nothing
else do
mapM_ (checkEnable st2) rules
ok <- mapM checkAssignConflicts rules
return (if and ok
then Just ( st2
, (trimState $ StateHierarchy name
$ gState g, rules, assertionNames
, coverageNames, probeNames))
else Nothing)
trimState :: StateHierarchy -> StateHierarchy
trimState a = case a of
StateHierarchy name items ->
StateHierarchy name $ filter f $ map trimState items
a -> a
where
f (StateHierarchy _ []) = False
f _ = True
checkEnable :: UeMap -> Rule -> IO ()
checkEnable st rule
| ruleEnable rule == (fst $ newUE (ubool False) st) =
putStrLn $ "WARNING: Rule will never execute: " ++ show rule
| otherwise = return ()
checkAssignConflicts :: Rule -> IO Bool
checkAssignConflicts rule@(Rule _ _ _ _ _ _ _) =
if length vars /= length vars'
then do
putStrLn $ "ERROR: Rule "
++ show rule
++ " contains multiple assignments to the same variable(s)."
return False
else do
return True
where
vars = fst $ unzip $ ruleAssigns rule
vars' = nub vars
checkAssignConflicts _ = return True
var :: Expr a => Name -> a -> Atom (V a)
var name init = do
name' <- addName name
(st, (g, atom)) <- get
let uv = UV (gVarId g) name' c
c = constant init
put (st, (g { gVarId = gVarId g + 1, gState = gState g ++ [StateVariable name c] }, atom))
return $ V uv
var' :: Name -> Type -> V a
var' name t = V $ UVExtern name t
array :: Expr a => Name -> [a] -> Atom (A a)
array name [] = error $ "ERROR: arrays can not be empty: " ++ name
array name init = do
name' <- addName name
(st, (g, atom)) <- get
let ua = UA (gArrayId g) name' c
c = map constant init
put (st, (g { gArrayId = gArrayId g + 1, gState = gState g ++ [StateArray name c] }, atom))
return $ A ua
array' :: Expr a => Name -> Type -> A a
array' name t = A $ UAExtern name t
addName :: Name -> Atom Name
addName name = do
(st, (g, atom)) <- get
checkName name
if elem name (atomNames atom)
then error $ "ERROR: Name \"" ++ name ++ "\" not unique in " ++ show atom ++ "."
else do
put (st, (g, atom { atomNames = name : atomNames atom }))
return $ atomName atom ++ "." ++ name
checkName :: Name -> Atom ()
checkName name =
if (\ x -> isAlpha x || x == '_') (head name) &&
and (map (\ x -> isAlphaNum x || x `elem` "._-[]") (tail name)) &&
and (map isAscii name)
then return ()
else error $ "ERROR: Name \"" ++ name ++ "\" is not a valid identifier."
allUVs :: UeMap -> [Rule] -> Hash -> [MUV]
allUVs st rules ue = fixedpoint next $ nearestUVs ue st
where
assigns = concat [ ruleAssigns r | r@(Rule _ _ _ _ _ _ _) <- rules ]
previousUVs :: MUV -> [MUV]
previousUVs uv = concat [ nearestUVs ue st | (uv', ue) <- assigns, uv == uv' ]
next :: [MUV] -> [MUV]
next uvs = sort $ nub $ uvs ++ concatMap previousUVs uvs
fixedpoint :: Eq a => (a -> a) -> a -> a
fixedpoint f a | a == f a = a
| otherwise = fixedpoint f $ f a
allUEs :: Rule -> [Hash]
allUEs rule = ruleEnable rule : ues
where
index :: MUV -> [Hash]
index (MUVArray _ ue) = [ue]
index _ = []
ues = case rule of
Rule _ _ _ _ _ _ _ ->
concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ]
++ concat (snd (unzip (ruleActions rule)))
Assert _ _ a -> [a]
Cover _ _ a -> [a]