-
Notifications
You must be signed in to change notification settings - Fork 19
/
Elaboration.hs
433 lines (386 loc) · 13.3 KB
/
Elaboration.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
module Language.Atom.Elaboration
(
-- UeStateT
-- * Atom monad and container.
Atom
, AtomDB (..)
, Global (..)
, Rule (..)
, StateHierarchy (..)
, buildAtom
-- * Type Aliases and Utilities
, 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
-- | A name.
type Name = String
-- | A hierarchical name.
type Path = [Name]
-- | A phase is either the minimum phase or the exact phase.
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] -- Names used at this level.
, atomEnable :: Hash -- Enabling condition.
, atomSubs :: [AtomDB] -- Sub atoms.
, 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
-- , mathH :: Bool -- Contains a math.h call?
}
| 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)
-- st <- S.get
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
-- S.put 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 = []
}))
-- S.return db
type AtomSt = (UeMap, (Global, AtomDB))
-- | The Atom monad holds variable and rule declarations.
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))
-- | A Relation is used for relative performance constraints between 'Action's.
-- data Relation = Higher UID | Lower UID deriving (Show, Eq)
-- XXX elaborate is a bit hacky since we're threading state through this
-- function, but I don't want to go change all the UeState monads to UeStateT
-- monads.
-- | Given a top level name and design, elaborates design and returns a design database.
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
-- | Checks that a rule will not be trivially disabled.
checkEnable :: UeMap -> Rule -> IO ()
checkEnable st rule
| ruleEnable rule == (fst $ newUE (ubool False) st) =
putStrLn $ "WARNING: Rule will never execute: " ++ show rule
| otherwise = return ()
-- | Check that a variable is assigned more than once in a rule. Will
-- eventually be replaced consistent assignment checking.
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
{-
-- | Checks that all array indices are not a function of array variables.
checkArrayIndices :: [Rule] -> Rule -> IO Bool
checkArrayIndices rules rule =
where
ues = allUEs rule
arrayIndices' = concatMap arrayIndices ues
[ (name, ) | (UA _ name _, index) <- concatMap arrayIndices ues, UV (Array (UA _ name' init)) <- allUVs rules index, length init /= 1 ]
data UA = UA Int String [Const] deriving (Show, Eq, Ord)
data UV = UV UVLocality deriving (Show, Eq, Ord)
data UVLocality = Array UA UE | External String Type deriving (Show, Eq, Ord)
allUVs :: [Rule] -> UE -> [UV]
arrayIndices :: UE -> [(UA, UE)]
, ruleEnable :: UE
, ruleAssigns :: [(UV, UE)]
, ruleActions :: [([String] -> String, [UE])]
-}
-- | Generic local variable declaration.
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
-- | Generic external variable declaration.
var' :: Name -> Type -> V a
var' name t = V $ UVExtern name t
-- | Generic array declaration.
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
-- | Generic external array declaration.
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
-- still accepts some misformed names, like "_.." or "_]["
checkName :: Name -> Atom ()
checkName name =
if (\ x -> isAlpha x || x == '_') (head name) &&
and (map (\ x -> isAlphaNum x || x `elem` "._[]") (tail name))
then return ()
else error $ "ERROR: Name \"" ++ name ++ "\" is not a valid identifier."
{-
ruleGraph :: Name -> [Rule] -> [UV] -> IO ()
ruleGraph name rules uvs = do
putStrLn $ "Writing rule graph (" ++ name ++ ".dot)..."
writeFile (name ++ ".dot") g
--system $ "dot -o " ++ name ++ ".png -Tpng " ++ name ++ ".dot"
return ()
where
adminUVs =
[ UV (-1) "__clock" (External Word64)
, UV (-2) "__coverage_index" (External Word32)
, UV (-3) "__coverage[__coverage_index]" (External Word32)
]
g = unlines
[ "digraph " ++ name ++ "{"
, concat [ " r" ++ show (ruleId r) ++ " [label = \"" ++ show r ++ "\" shape = ellipse];\n" | r <- rules ]
, concat [ " v" ++ show i ++ " [label = \"" ++ n ++ "\" shape = box];\n" | (UV i n _) <- adminUVs ++ uvs ]
, concat [ " r" ++ show (ruleId r) ++ " -> v" ++ show i ++ "\n" | r <- rules, (UV i _ _, _) <- ruleAssigns r ]
, concat [ " v" ++ show i ++ " -> r" ++ show (ruleId r) ++ "\n" | r <- rules, (UV i _ _) <- ruleUVRefs r ]
, "}"
]
ruleUVRefs r = nub $ concatMap uvSet ues
where
ues = ruleEnable r : snd (unzip (ruleAssigns r)) ++ concat (snd (unzip (ruleActions r)))
-}
-- | All the variables that directly and indirectly control the value of an expression.
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
-- | All primary expressions used in a rule.
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]