atom 0.1.1 → 0.1.2

raw patch · 12 files changed

+377/−41 lines, 12 filesdep +yicesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: yices

API changes (from Hackage documentation)

Files

• LICENSE +1/−1
• Language/Atom.hs +2/−0
• Language/Atom/Analysis.hs +4/−3
• Language/Atom/Code.hs +11/−12
• Language/Atom/Common.hs +1/−1
• Language/Atom/Elaboration.hs +15/−6
• Language/Atom/Expressions.hs +38/−6
• Language/Atom/Language.hs +25/−3
• Language/Atom/Scheduling.hs +47/−5
• Language/Atom/Verification.hs +219/−0
• RELEASE-NOTES +8/−0
• atom.cabal +6/−4

@@ -1,6 +1,6 @@ Copyright (c) Tom Hawkins 2007-2009 -Contributions from John Van Enk, Brian Lewis+Contributions from John Van Enk, Brian Lewis, Lee Pike  All rights reserved. 

@@ -11,6 +11,7 @@   , module Language.Atom.Common   , module Language.Atom.Language   , module Language.Atom.Unit+  , module Language.Atom.Verification   ) where  import Language.Atom.Code@@ -18,3 +19,4 @@ import Language.Atom.Common import Language.Atom.Language import Language.Atom.Unit+import Language.Atom.Verification

@@ -7,9 +7,10 @@ import Language.Atom.Expressions  -- | Topologically sorts a list of expressions and subexpressions.-topo :: Int -> [UE] -> [(UE, String)]-topo start ues = reverse ues'+topo :: [UE] -> [(UE, String)]+topo ues = reverse ues'   where+  start = 0   (_, ues') = foldl collect (start, []) ues   collect :: (Int, [(UE, String)]) -> UE -> (Int, [(UE, String)])   collect (n, ues) ue | any ((== ue) . fst) ues = (n, ues)@@ -20,5 +21,5 @@  -- | Number of UE's computed in rule. ruleComplexity :: Rule -> Int-ruleComplexity = length . topo 0 . allUEs+ruleComplexity = length . topo . allUEs 

@@ -138,16 +138,16 @@   c = unlines     [ preCode     , ""-    , "static " ++ cType config Word64 ++ " __clock = 0;"+    , "static " ++ cType config Word64 ++ " __global_clock = 0;"     , codeIf (cRuleCoverage config) $ "static const " ++ cType config Word32 ++ " __coverage_len = " ++ show covLen ++ ";"     , codeIf (cRuleCoverage config) $ "static " ++ cType config Word32 ++ " __coverage[" ++ show covLen ++ "] = {" ++ (concat $ intersperse ", " $ replicate covLen "0") ++ "};"     , codeIf (cRuleCoverage config) $ "static " ++ cType config Word32 ++ " __coverage_index = 0;"     , concatMap (declUV config) uvs     , concatMap (declUA config) uas-    , concatMap (codeRule config assertionNames coverageNames topo') $ rules+    , concatMap (codeRule config assertionNames coverageNames) $ rules     , "void " ++ (if null (cFuncName config) then name else cFuncName config) ++ "(void) {"     , concatMap (codePeriodPhase config) schedule-    , "  __clock = __clock + 1;"+    , "  __global_clock = __global_clock + 1;"     , "}"     , ""     , postCode@@ -156,7 +156,6 @@   rules :: [Rule]   rules = concat [ r | (_, _, r) <- schedule ] -  topo' = topo 0   covLen = 1 + div (maximum $ map ruleId rules) 32  codeIf :: Bool -> String -> String@@ -192,16 +191,16 @@ doubleBits :: Double -> Word64 doubleBits = unsafeCoerce -codeRule :: Config -> [Name] -> [Name] -> ([UE] -> [(UE, String)]) -> Rule -> String-codeRule config assertionNames coverageNames topo rule =+codeRule :: Config -> [Name] -> [Name] -> Rule -> String+codeRule config assertionNames coverageNames rule =   "/* " ++ show rule ++ " */\n" ++   "static void __r" ++ show (ruleId rule) ++ "(void) {\n" ++   concatMap (codeUE    config ues "  ") ues ++   "  if (" ++ id (ruleEnable rule) ++ ") {\n" ++   concatMap codeAction (ruleActions rule) ++   codeIf (cRuleCoverage config) ("    __coverage[" ++ covWord ++ "] = __coverage[" ++ covWord ++ "] | (1 << " ++ covBit ++ ");\n") ++-  concat [ codeIf (cAssert config) ("    " ++ cAssertName config ++ "(" ++ assertionId name ++ ", " ++ id check ++ ", __clock);\n") | (name, check) <- ruleAsserts rule ] ++-  concat [ codeIf (cCover  config) ("    " ++ cCoverName  config ++ "(" ++ coverageId  name ++ ", " ++ id check ++ ", __clock);\n") | (name, check) <- ruleCovers  rule ] +++  concat [ codeIf (cAssert config) ("    " ++ cAssertName config ++ "(" ++ assertionId name ++ ", " ++ id check ++ ", __global_clock);\n") | (name, check) <- ruleAsserts rule ] +++  concat [ codeIf (cCover  config) ("    " ++ cCoverName  config ++ "(" ++ coverageId  name ++ ", " ++ id check ++ ", __global_clock);\n") | (name, check) <- ruleCovers  rule ] ++   "  }\n" ++   concatMap codeAssign (ruleAssigns rule) ++   "}\n\n"@@ -233,13 +232,13 @@ codePeriodPhase :: Config -> (Int, Int, [Rule]) -> String codePeriodPhase config (period, phase, rules) = unlines   [ printf "  {"-  , printf "    static %s __clock = %i;" (cType config clockType) phase-  , printf "    if (__clock == 0) {"+  , printf "    static %s __scheduling_clock = %i;" (cType config clockType) phase+  , printf "    if (__scheduling_clock == 0) {"   , intercalate "\n" $ map callRule rules-  , printf "      __clock = %i;" (period - 1)+  , printf "      __scheduling_clock = %i;" (period - 1)   , printf "    }"   , printf "    else {"-  , printf "      __clock = __clock - 1;"+  , printf "      __scheduling_clock = __scheduling_clock - 1;"   , printf "    }"   , printf "  }"   ]

@@ -31,7 +31,7 @@   timer <- word64 name 0   return $ Timer timer --- | Starts a Timer.  A Timer can be restarted at any time.+-- | Starts a Timer.  A timer can be restarted at any time. startTimer :: Timer -> E Word64 -> Atom () startTimer t = startTimerIf t true 

@@ -22,6 +22,7 @@   , allUEs   ) where +import Control.Monad import Control.Monad.Trans import Data.Function (on) import Data.List@@ -45,6 +46,7 @@   , gArrays  :: [UA]   , gProbes  :: [(String, UE)]   , gPeriod  :: Int+  , gPhase   :: Int   }  data AtomDB = AtomDB@@ -54,6 +56,7 @@   , atomEnable      :: UE          -- Enabling condition.   , atomSubs        :: [AtomDB]    -- Sub atoms.   , atomPeriod      :: Int+  , atomPhase       :: Int   , atomAssigns     :: [(UV, UE)]   , atomActions     :: [([String] -> String, [UE])]   , atomAsserts     :: [(Name, UE)]@@ -67,6 +70,7 @@   , ruleAssigns   :: [(UV, UE)]   , ruleActions   :: [([String] -> String, [UE])]   , rulePeriod    :: Int+  , rulePhase     :: Int   , ruleAsserts   :: [(Name, UE)]   , ruleCovers    :: [(Name, UE)]   }@@ -90,6 +94,7 @@     , ruleAssigns   = map enableAssign $ atomAssigns atom     , ruleActions   = atomActions atom     , rulePeriod    = atomPeriod  atom+    , rulePhase     = atomPhase   atom     , ruleAsserts   = atomAsserts atom     , ruleCovers    = atomCovers  atom     }@@ -110,6 +115,7 @@   , atomEnable    = ubool True   , atomSubs      = []   , atomPeriod    = gPeriod g+  , atomPhase     = gPhase  g   , atomAssigns   = []   , atomActions   = []   , atomAsserts   = []@@ -147,16 +153,19 @@ -- | Given a top level name and design, elaborates design and returns a design database. elaborate :: Name -> Atom () -> IO (Maybe ([Rule], [UV], [UA], [Name], [Name], [(Name, Type)])) elaborate name atom = do-  (_, (g, atomDB)) <- buildAtom Global { gRuleId = 0, gVarId = 0, gArrayId = 0, gVars = [], gArrays = [], gProbes = [], gPeriod = 1 } name atom+  (_, (g, atomDB)) <- buildAtom Global { gRuleId = 0, gVarId = 0, gArrayId = 0, gVars = [], gArrays = [], gProbes = [], gPeriod = 1, gPhase  = 0 } name atom   let rules = reIdRules $ elaborateRules (ubool True) atomDB       coverageNames  = concatMap (fst . unzip . ruleCovers ) rules       assertionNames = concatMap (fst . unzip . ruleAsserts) rules       probeNames = [ (n, typeOf a) | (n, a) <- gProbes g ]-  mapM_ checkEnable rules-  ok <- mapM checkAssignConflicts rules-  if not $ and ok-    then return Nothing-    else return $ Just (rules, gVars g, gArrays g, assertionNames, coverageNames, probeNames)+  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 (rules, gVars g, gArrays g, assertionNames, coverageNames, probeNames) else Nothing)   

@@ -53,7 +53,9 @@   , limit   -- * Arithmetic Operations   , div_+  , div0_   , mod_+  , mod0_   -- * Conditional Operator   , mux   -- * Array Indexing@@ -506,7 +508,14 @@   xor a b = (a .&. complement b) .|. (complement a .&. b)   shift (Const a) n = Const $ shift a n   shift a n = Shift a n-  rotate = error "E rotate not supported."+  rotate a n | n >= width a = error "E rotates too far."+  rotate (Const a) n = Const $ rotate a n+  rotate a n | n > 0     = shift a n .|. shift a (width a - n) .&. Const (mask n)+             | n < 0     = shift a n .&. Const (mask $ width a + n) .|. shift a (width a + n)+             | otherwise = a+    where+    mask 0 = 0+    mask n = shiftL (mask $ n - 1) 1 + 1   bitSize = width   isSigned = signed @@ -597,21 +606,43 @@   min = min_ a b   max = max_ a b --- | Division.+-- | Division.  If both the dividend and divisor are constants, a compile-time+-- check is made for divide-by-zero.  Otherwise, if the divisor ever evaluates+-- to @0@, a runtime exception will occur, even if the division occurs within+-- the scope of a 'cond' or 'mux' that tests for @0@ (because Atom generates+-- deterministic-time code, every branch of a 'cond' or 'mux' is executed). div_ :: IntegralE a => E a -> E a -> E a div_ (Const a) (Const b) = Const $ a `div` b div_ a b = Div a b --- | Modulo.+-- | Division, where the C code is instrumented with a runtime check to ensure+-- the divisor does not equal @0@.  If it is equal to @0@, the 3rd argument is a+-- user-supplied non-zero divsor.+div0_ :: IntegralE a => E a -> E a -> a -> E a+div0_ _ _ 0 = error "The third argument to div0_ must be non-zero."+div0_ a b c = div_ a $ mux (b ==. 0) (Const c) b++-- | Modulo.  If both the dividend and modulus are constants, a compile-time+-- check is made for divide-by-zero.  Otherwise, if the modulus ever evaluates+-- to @0@, a runtime exception will occur, even if the division occurs within+-- the scope of a 'cond' or 'mux' that tests for @0@ (because Atom generates+-- deterministic-time code, every branch of a 'cond' or 'mux' is executed). mod_ :: IntegralE a => E a -> E a -> E a mod_ (Const a) (Const b) = Const $ a `mod` b mod_ a b = Mod a b +-- | Modulus, where the C code is instrumented with a runtime check to ensure+-- the modulus does not equal @0@.  If it is equal to @0@, the 3rd argument is+-- a user-supplied non-zero divsor.+mod0_ :: IntegralE a => E a -> E a -> a -> E a+mod0_ _ _ 0 = error "The third argument to mod0_ must be non-zero."+mod0_ a b c = mod_ a $ mux (b ==. 0) (Const c) b+ -- | Returns the value of a 'V'. value :: V a -> E a value = VRef --- | Conditional expression.+-- | Conditional expression.  Note, both branches are evaluated! -- -- > mux test onTrue onFalse mux :: Expr a => E Bool -> E a -> E a -> E a@@ -659,8 +690,9 @@ nearestUVs = nub . f   where   f :: UE -> [UV]-  f (UVRef uv) = [uv]-  f ue = concatMap f $ ueUpstream ue+  f (UVRef uv@(UVArray _ i)) = [uv] ++ f i+  f (UVRef uv)               = [uv]+  f ue                       = concatMap f $ ueUpstream ue  -- | All array indexing subexpressions. arrayIndices :: UE -> [(UA, UE)]

@@ -8,6 +8,8 @@   , atom   , period   , getPeriod+  , phase+  , getPhase   -- * Action Directives   , cond   , Assign (..)@@ -102,6 +104,26 @@   (g, _) <- get   return $ gPeriod g +-- | Defines the earliest phase within the period at which the rule should+-- execute.  The 'phase' must be at least zero and less than the current 'period'.+phase :: Int -> Atom a -> Atom a+phase n _ | n < 0 = error "ERROR: phase must be at least 0."+phase n atom = do+  (g, a) <- get+  if (n >= gPeriod g) +    then error "ERROR: phase must be less than the current phase."+    else do put (g { gPhase = n }, a)+            r <- atom+            (g', a) <- get+            put (g' { gPhase = gPhase g }, a)+            return r++-- | Returns the phase of the current scope.+getPhase :: Atom Int+getPhase = do+  (g, _) <- get+  return $ gPhase g+ -- | Returns the current atom hierarchical path. path :: Atom String path = do@@ -256,7 +278,7 @@  -- | Reference to the 64-bit free running clock. clock :: E Word64-clock = value $ V $ UVExtern "__clock" Word64+clock = value $ V $ UVExtern "__global_clock" Word64  -- | Rule coverage information.  (current coverage index, coverage data) nextCoverage :: Atom (E Word32, E Word32)@@ -265,7 +287,7 @@   return (value $ V $ UVExtern "__coverage_index" Word32, value $ V $ UVExtern "__coverage[__coverage_index]" Word32)  --- | Assertion that checks an E Bool.  Assertions are only check if containing rule is enabled and executed.+-- | Assertion that checks an E Bool.  Assertions are only checked if the containing rule is enabled and executed. assert :: Name -> E Bool -> Atom () assert name check = do   (g, atom) <- get@@ -279,7 +301,7 @@   assert name $ imply a b   cover (name ++ "Precondition") a --- | Addes a functional coverage point.+-- | Adds a functional coverage point. cover :: Name -> E Bool -> Atom () cover name check = do   (g, atom) <- get

@@ -16,11 +16,55 @@ schedule rules = concatMap spread periods   where +  -- Algorithm for assigning rules to phases for a given period:++    -- 1. List the rules by their offsets, highest first.++    -- 2. If the list is empty, stop.++    -- 3. Otherwise, take the head of the list and assign its phase as follows:+    -- find the set of phases containing the minimum number of rules such that+    -- they are at least as large as the rule's offset.  Then take the smallest+    -- of those phases.++    -- 4. Go to (2).++  -- Algorithm properties: for each period, ++    -- A. Each rule is scheduled no earlier than its offset.++    -- B. The phase with the most rules is the minimum of all possible schedules+    -- that satisfy (A).++    -- XXX Check if this is true.+    -- C. The sum of the difference between between each rule's offset and it's+    -- scheduled phase is the minimum of all schedules satisfying (A) and (B).+       spread :: (Int, [Rule]) -> Schedule-  spread (period, rules) = [ (period, phase, rules) | (phase, rules) <- zip [0..] $ unconcat rulesPerPhase rules ]+  spread (period, rules) = +    placeRules (replicate period []) orderedByPhase +     where-    rulesPerPhase = (length rules `div` period) + (if length rules `mod` period > 0 then 1 else 0)+    orderedByPhase :: [Rule]+    orderedByPhase = +        sortBy (\r0 r1 -> compare (rulePhase r1) (rulePhase r0)) rules +    placeRules :: [[Rule]] -> [Rule] -> [(Int, Int, [Rule])]+    placeRules ls [] = +      filter (\(_,_,rls) -> not (null rls)) $ zip3 (repeat period) [0..(period-1)] ls+    placeRules ls (r:rst) = placeRules (insertAt (lub r ls) r ls) rst ++    lub :: Rule -> [[Rule]] -> Int+    lub r ls = let minI = rulePhase r+                   lub' i [] = i -- unreachable.  Included to prevent missing+                                 -- cases ghc warnings.+                   lub' i ls | (head ls) == minimum ls = i+                             | otherwise = lub' (i+1) (tail ls)+               in  lub' minI (drop minI $ map length ls)++    insertAt :: Int -> Rule -> [[Rule]] -> [[Rule]]+    insertAt i r ls = (take i ls) ++ ((r:(ls !! i)):(drop (i+1) ls))+   periods = foldl grow [] [ (rulePeriod r, r) | r <- rules ]    grow :: [(Int, [Rule])] -> (Int, Rule) -> [(Int, [Rule])]@@ -28,9 +72,7 @@   grow ((a, bs):rest) (a', b) | a' == a   = (a, b : bs) : rest                               | otherwise = (a, bs) : grow rest (a', b) -unconcat :: Int -> [a] -> [[a]]-unconcat _ [] = []-unconcat n a  = take n a : unconcat n (drop n a)+  reportSchedule :: Schedule -> String reportSchedule schedule = concat

@@ -0,0 +1,219 @@+module Language.Atom.Verification+  ( Model+  , model+  -- , verify+  -- , kInduction+  -- , boundedModelChecking+  , test+  ) where++import Data.Char ()+import Data.Function ()+import Data.Int ()+import Data.List ()+import Data.Ratio ()+import Data.Word ()+import Math.SMT.Yices.Pipe+import Math.SMT.Yices.Syntax+import System.Process ()++import Language.Atom.Elaboration ()+import Language.Atom.Expressions+import Language.Atom.Scheduling++-- | A model of a scheduled program for model checking.+data Model = Model+  --{ transition :: Int -> [Name] -> ([CmdY], [CmdY])+  --, names :: [(Name, Int)]+  --, +  --}++-- | Create a model from a scheduled program.+model :: Schedule -> [UV] -> [UA] -> Model +model _ _ _ = Model++-- | A list of assertions captured by a model.+--assertions :: Model -> [Name]++-- | Bounded model checking starting from the initial state.+--boundedModelChecking :: Model -> Int -> Name -> IO (Maybe Witness)++-- | K-induction model checking given a min and a max k-depth.+--kInduction :: Model -> Int -> Int -> Name -> IO ()+++test :: IO ()+test = do+  print test+  result <- runY test+  print result+  where+  test =+    [ DEFINE ("a", VarT "int") Nothing+    , DEFINE ("b", VarT "int") Nothing+    , ASSERT (VarE "a" := VarE "b")+    -- , ASSERT (YNe (YVar "a") (YVar "b"))+    ]+  +-- | Runs a Yices program.  Returns a list of variable values if satisfiable.+runY :: [CmdY] -> IO ResY+runY a = do+  p <- createYicesPipe "yices" []+  runCmdsY p a+  r <- checkY p+  exitY p+  return r++++{-+yType :: Type -> YT+yType t = case t of+  Bool   -> YBool+  Int8   -> YInt+  Int16  -> YInt+  Int32  -> YInt+  Int64  -> YInt+  Word8  -> YNat+  Word16 -> YNat+  Word32 -> YNat+  Word64 -> YNat+  Float  -> YReal+  Double -> YReal+-}++{-+vars :: [UV] -> Int -> String+vars uvs step = concatMap (var step) uvs+  where+  var :: Int -> UV -> String+  var step uv = "(define " ++ uvName step uv ++ "::" ++ yicesType (uvType uv) ++ ")\n"++uvName :: Int -> UV -> String+uvName step (UV i _ _) = "v" ++ show i ++ "_" ++ show step++initialize :: [UV] -> String+initialize uvs = vars uvs 0 ++ concatMap initialize uvs+  where+  initialize :: UV -> String+  initialize uv@(UV _ _ (Local c)) = "(assert (= " ++ uvName 0 uv ++ " " ++ const c ++ "))\n"+  initialize (UV _ _ (External _)) = ""+  const :: Const -> String+  const c = case c of+    CBool   c -> if c then "true" else "false"+    CInt8   c -> "0b" ++ bits  8 (fromIntegral c)+    CInt16  c -> "0b" ++ bits 16 (fromIntegral c)+    CInt32  c -> "0b" ++ bits 32 (fromIntegral c)+    CInt64  c -> "0b" ++ bits 64 (fromIntegral c)+    CWord8  c -> "0b" ++ bits  8 (fromIntegral c)+    CWord16 c -> "0b" ++ bits 16 (fromIntegral c)+    CWord32 c -> "0b" ++ bits 32 (fromIntegral c)+    CWord64 c -> "0b" ++ bits 64 (fromIntegral c)+    CFloat  c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"+    CDouble c -> "(/ " ++ show (numerator $ toRational c) ++ " " ++ show (denominator $ toRational c) ++ ")"++  bits :: Int -> Word64 -> String+  bits 0 _ = ""+  bits n a = bits (n - 1) (div a 2) ++ show (mod a 2)++-- Time 0 to 1 is step 1.+transition :: [[[Rule]]] -> [UV] -> Int -> String+transition _ {-schedule-} uvs step = vars uvs step ++ transition+  where+  transition = "; transition " ++ show (step - 1) ++ " to " ++ show step ++ "\n"  --XXX++getUV :: [UV] -> Int -> UV+getUV [] _ = error "Verify.getUV"+getUV (uv@(UV i _ _):_) j | i == j = uv+getUV (_:a) i = getUV a i+++parseVar :: [UV] -> Group -> (Int, UV, String)+parseVar uvs (G [S "=", S name, value]) = (t, getUV uvs i, parseValue value)+  where+  (i', t') = break (== '_') $ tail name+  i = read i'+  t = read $ tail t'+parseVar _ g = error $ "Verify.parseVar: " ++ show g++parseValue :: Group -> String+parseValue (S ('0':'b':a)) = "b" ++ a ++ " "+parseValue (S "true")      = "1"+parseValue (S "false")     = "0"+parseValue (S v)           = "r" ++ v ++ " "+parseValue (G [S "/", S n, S d]) = "r" ++ show (fromRational (read n % read d)) ++ " "+parseValue a               = error $ "Verify.parseValue: " ++ show a+++data Heirarchy = Variable UV | Module String [Heirarchy]++vcd :: [UV] -> [(Int, UV, String)] -> String+vcd uvs signals' = header ++ samples ++ end+  where+  signals = sortBy (\ (a,_,_) (b,_,_) -> compare a b) signals'++  header = "$timescale\n  1 ms\n$end\n" ++ concatMap decl (heirarchy 0 uvs) ++ "$enddefinitions $end\n"+  (lastTime, _, _) = last signals+  end = "#" ++ show (lastTime + 1) ++ "\n"++  decl :: Heirarchy -> String+  decl (Module name subs) = "$scope module " ++ name ++ " $end\n" ++ concatMap decl subs ++ "$upscope $end\n"+  decl (Variable uv)      = declVar uv++  declVar :: UV -> String+  declVar uv@(UV i n _) = case uvType uv of+    Bool   -> "$var wire 1 "     ++ code ++ " " ++ name ++ " $end\n"+    Int8   -> "$var integer 8 "  ++ code ++ " " ++ name ++ " $end\n"+    Int16  -> "$var integer 16 " ++ code ++ " " ++ name ++ " $end\n"+    Int32  -> "$var integer 32 " ++ code ++ " " ++ name ++ " $end\n"+    Int64  -> "$var integer 64 " ++ code ++ " " ++ name ++ " $end\n"+    Word8  -> "$var wire 8 "     ++ code ++ " " ++ name ++ " $end\n"+    Word16 -> "$var wire 16 "    ++ code ++ " " ++ name ++ " $end\n"+    Word32 -> "$var wire 32 "    ++ code ++ " " ++ name ++ " $end\n"+    Word64 -> "$var wire 64 "    ++ code ++ " " ++ name ++ " $end\n"+    Float  -> "$var real 32 "    ++ code ++ " " ++ name ++ " $end\n"+    Double -> "$var real 64 "    ++ code ++ " " ++ name ++ " $end\n"+    where+    code = vcdCode i+    name = reverse $ takeWhile (/= '.') $ reverse n++  samples = concatMap sample signals++  sample (t, (UV i _ _), v) = "#" ++ show t ++ "\n" ++ v ++ vcdCode i ++ "\n"++heirarchy :: Int -> [UV] -> [Heirarchy]+heirarchy _ [] = []+heirarchy depth uvs = heirarchy' depth notvars ++ map Variable vars+  where+  isVar :: UV -> Bool+  isVar uv = length (path depth uv) == 1+  (vars, notvars) = partition isVar uvs++heirarchy' :: Int -> [UV] -> [Heirarchy]+heirarchy' _ [] = []+heirarchy' depth uvs@(a:_) = Module n (heirarchy (depth + 1) yes) : heirarchy' depth no+  where+  n = head $ path depth a+  isMod uv = n == head (path depth uv)+  (yes, no) = partition isMod uvs++path :: Int -> UV -> [String]+path depth (UV _ n _) = drop depth $ words $ map (\ c -> if c == '.' then ' ' else c) n++vcdCode :: Int -> String+vcdCode i | i < 94 =              [chr (33 + mod i 94)]+vcdCode i = vcdCode (div i 94) ++ [chr (33 + mod i 94)]++{-+bitString :: Int -> String+bitString n = if null bits then "0" else bits+  where+  bit :: Int -> Char+  bit i = if testBit n i then '1' else '0'+  bits = dropWhile (== '0') $ map bit $ reverse [0..31]+-}++-}+++

@@ -1,3 +1,11 @@+atom 0.1.2    11/25/2009++- Added div0_ and mod0_ functions, that instrument runtime checks for divide-by-zero (Lee Pike).+- Added a phase function that specifies the earliest phase into a period a rule should execute (Lee Pike). +- New scheduling algorithm to balance when rules fire across the period.+- Added support for Bits.rotate.+- Added check for empty design.+ atom 0.1.1    09/29/2009  - Added ULL C constant annotations for rule scheduling.

@@ -1,5 +1,5 @@ name:    atom-version: 0.1.1+version: 0.1.2  category: Language @@ -17,7 +17,7 @@ license:      BSD3 license-file: LICENSE -homepage: http://patch-tag.com/r/tomahawkins/atom+homepage: http://tomahawkins.org  build-type:    Simple cabal-version: >= 1.6@@ -29,7 +29,8 @@     build-depends:         base       >= 4       && < 5,         mtl        >= 1.1.0.1 && < 1.2,-        process    >= 1.0.1.1 && < 1.2+        process    >= 1.0.1.1 && < 1.2,+        yices      >= 0.0.0.4      exposed-modules:         Language.Atom@@ -43,6 +44,7 @@         Language.Atom.Language         Language.Atom.Scheduling         Language.Atom.Unit+        Language.Atom.Verification      extensions: GADTs @@ -52,4 +54,4 @@  source-repository head     type:     darcs-    location: http://patch-tag.com/r/atom/pullrepo+    location: http://patch-tag.com/r/tomahawkins/atom/pullrepo