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 Language.Atom.Expressions
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, UE)]
, gPeriod :: Int
, gPhase :: Phase
}
data AtomDB = AtomDB
{ atomId :: Int
, atomName :: Name
, atomNames :: [Name]
, atomEnable :: UE
, atomSubs :: [AtomDB]
, atomPeriod :: Int
, atomPhase :: Phase
, atomAssigns :: [(UV, UE)]
, atomActions :: [([String] -> String, [UE])]
, atomAsserts :: [(Name, UE)]
, atomCovers :: [(Name, UE)]
}
data Rule
= Rule
{ ruleId :: Int
, ruleName :: Name
, ruleEnable :: UE
, ruleAssigns :: [(UV, UE)]
, ruleActions :: [([String] -> String, [UE])]
, rulePeriod :: Int
, rulePhase :: Phase
}
| Assert
{ ruleName :: Name
, ruleEnable :: UE
, ruleAssert :: UE
}
| Cover
{ ruleName :: Name
, ruleEnable :: UE
, ruleCover :: UE
}
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:: UE -> AtomDB -> [Rule]
elaborateRules parentEnable atom = if isRule then rule : rules else rules
where
isRule = not $ null (atomAssigns atom) && null (atomActions atom)
enable = uand parentEnable $ atomEnable atom
rule = Rule
{ ruleId = atomId atom
, ruleName = atomName atom
, ruleEnable = enable
, ruleAssigns = map enableAssign $ atomAssigns atom
, ruleActions = atomActions atom
, rulePeriod = atomPeriod atom
, rulePhase = atomPhase atom
}
assert (name, ue) = Assert
{ ruleName = name
, ruleEnable = enable
, ruleAssert = ue
}
cover (name, ue) = Cover
{ ruleName = name
, ruleEnable = enable
, ruleCover = ue
}
rules = map assert (atomAsserts atom) ++ map cover (atomCovers atom) ++ concatMap (elaborateRules enable) (atomSubs atom)
enableAssign :: (UV, UE) -> (UV, UE)
enableAssign (uv, ue) = (uv, umux enable ue $ UVRef uv)
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 :: Global -> Name -> Atom a -> IO (a, (Global, AtomDB))
buildAtom g name (Atom f) = f (g { gRuleId = gRuleId g + 1 }, AtomDB
{ atomId = gRuleId g
, atomName = name
, atomNames = []
, atomEnable = ubool True
, atomSubs = []
, atomPeriod = gPeriod g
, atomPhase = gPhase g
, atomAssigns = []
, atomActions = []
, atomAsserts = []
, atomCovers = []
})
data Atom a = Atom ((Global, AtomDB) -> IO (a, (Global, AtomDB)))
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 (Global, AtomDB)
get = Atom (\ s -> return (s, s))
put :: (Global, AtomDB) -> Atom ()
put s = Atom (\ _ -> return ((), s))
elaborate :: Name -> Atom () -> IO (Maybe (StateHierarchy, [Rule], [Name], [Name], [(Name, Type)]))
elaborate name atom = do
(_, (g, atomDB)) <- buildAtom Global { gRuleId = 0, gVarId = 0, gArrayId = 0, gState = [], gProbes = [], gPeriod = 1, gPhase = MinPhase 0 } name atom
let rules = reIdRules 0 $ elaborateRules (ubool True) atomDB
coverageNames = [ name | Cover name _ _ <- rules ]
assertionNames = [ name | Assert name _ _ <- rules ]
probeNames = [ (n, typeOf a) | (n, a) <- gProbes g ]
if (null rules)
then do
putStrLn "ERROR: Design contains no rules. Nothing to do."
return Nothing
else do
mapM_ checkEnable rules
ok <- mapM checkAssignConflicts rules
return (if and ok then Just (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 :: Rule -> IO ()
checkEnable rule | ruleEnable rule == ubool False = 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
(g, atom) <- get
let uv = UV (gVarId g) name' c
c = constant init
put (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
(g, atom) <- get
let ua = UA (gArrayId g) name' c
c = map constant init
put (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
(g, atom) <- get
checkName name
if elem name (atomNames atom)
then error $ "ERROR: Name \"" ++ name ++ "\" not unique in " ++ show atom ++ "."
else do
put (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 :: [Rule] -> UE -> [UV]
allUVs rules ue = fixedpoint next $ nearestUVs ue
where
assigns = concat [ ruleAssigns r | r@(Rule _ _ _ _ _ _ _) <- rules ]
previousUVs :: UV -> [UV]
previousUVs uv = concat [ nearestUVs ue | (uv', ue) <- assigns, uv == uv' ]
next :: [UV] -> [UV]
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 -> [UE]
allUEs rule = ruleEnable rule : ues
where
index :: UV -> [UE]
index (UVArray _ 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]