diff --git a/LICENSE b/LICENSE --- a/LICENSE +++ b/LICENSE @@ -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. diff --git a/Language/Atom.hs b/Language/Atom.hs --- a/Language/Atom.hs +++ b/Language/Atom.hs @@ -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 diff --git a/Language/Atom/Analysis.hs b/Language/Atom/Analysis.hs --- a/Language/Atom/Analysis.hs +++ b/Language/Atom/Analysis.hs @@ -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 diff --git a/Language/Atom/Code.hs b/Language/Atom/Code.hs --- a/Language/Atom/Code.hs +++ b/Language/Atom/Code.hs @@ -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 " }" ] diff --git a/Language/Atom/Common.hs b/Language/Atom/Common.hs --- a/Language/Atom/Common.hs +++ b/Language/Atom/Common.hs @@ -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 diff --git a/Language/Atom/Elaboration.hs b/Language/Atom/Elaboration.hs --- a/Language/Atom/Elaboration.hs +++ b/Language/Atom/Elaboration.hs @@ -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) diff --git a/Language/Atom/Expressions.hs b/Language/Atom/Expressions.hs --- a/Language/Atom/Expressions.hs +++ b/Language/Atom/Expressions.hs @@ -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)] diff --git a/Language/Atom/Language.hs b/Language/Atom/Language.hs --- a/Language/Atom/Language.hs +++ b/Language/Atom/Language.hs @@ -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 diff --git a/Language/Atom/Scheduling.hs b/Language/Atom/Scheduling.hs --- a/Language/Atom/Scheduling.hs +++ b/Language/Atom/Scheduling.hs @@ -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 diff --git a/Language/Atom/Verification.hs b/Language/Atom/Verification.hs new file mode 100644 --- /dev/null +++ b/Language/Atom/Verification.hs @@ -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] +-} + +-} + + + diff --git a/RELEASE-NOTES b/RELEASE-NOTES --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -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. diff --git a/atom.cabal b/atom.cabal --- a/atom.cabal +++ b/atom.cabal @@ -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