diff --git a/Language/Atom/Code.hs b/Language/Atom/Code.hs --- a/Language/Atom/Code.hs +++ b/Language/Atom/Code.hs @@ -28,9 +28,8 @@ , cType :: Type -> String -- ^ C type naming rules. , cCode :: [Name] -> [Name] -> [(Name, Type)] -> (String, String) -- ^ Custom C code to insert above and below, given assertion names, coverage names, and probe names and types. , cRuleCoverage :: Bool -- ^ Enable rule coverage tracking. - , cAssert :: Bool -- ^ Enable assertion checking. + , cAssert :: Bool -- ^ Enable assertions and functional coverage. , cAssertName :: String -- ^ Name of assertion function. Type: void assert(int, cType Bool, cType Word64); - , cCover :: Bool -- ^ Enable functional coverage accumulation. , cCoverName :: String -- ^ Name of coverage function. Type: void cover(int, cType Bool, cType Word64); } @@ -43,7 +42,6 @@ , cRuleCoverage = True , cAssert = True , cAssertName = "assert" - , cCover = True , cCoverName = "cover" } @@ -129,10 +127,10 @@ type RuleCoverage = [(Name, Int, Int)] -writeC :: Name -> Config -> Schedule -> [UV] -> [UA] -> [Name] -> [Name] -> [(Name, Type)] -> IO RuleCoverage -writeC name config schedule uvs uas assertionNames coverageNames probeNames = do +writeC :: Name -> Config -> [Rule] -> Schedule -> [UV] -> [UA] -> [Name] -> [Name] -> [(Name, Type)] -> IO RuleCoverage +writeC name config rules schedule uvs uas assertionNames coverageNames probeNames = do writeFile (name ++ ".c") c - return [ (ruleName r, div (ruleId r) 32, mod (ruleId r) 32) | r <- rules ] + return [ (ruleName r, div (ruleId r) 32, mod (ruleId r) 32) | r <- rules' ] where (preCode, postCode) = cCode config assertionNames coverageNames probeNames c = unlines @@ -144,7 +142,8 @@ , codeIf (cRuleCoverage config) $ "static " ++ cType config Word32 ++ " __coverage_index = 0;" , concatMap (declUV config) uvs , concatMap (declUA config) uas - , concatMap (codeRule config assertionNames coverageNames) $ rules + , concatMap (codeRule config) rules' + , codeAssertionChecks config assertionNames coverageNames rules , "void " ++ (if null (cFuncName config) then name else cFuncName config) ++ "(void) {" , concatMap (codePeriodPhase config) schedule , " __global_clock = __global_clock + 1;" @@ -153,10 +152,10 @@ , postCode ] - rules :: [Rule] - rules = concat [ r | (_, _, r) <- schedule ] + rules' :: [Rule] + rules' = concat [ r | (_, _, r) <- schedule ] - covLen = 1 + div (maximum $ map ruleId rules) 32 + covLen = 1 + div (maximum $ map ruleId rules') 32 codeIf :: Bool -> String -> String codeIf a b = if a then b else "" @@ -191,16 +190,14 @@ doubleBits :: Double -> Word64 doubleBits = unsafeCoerce -codeRule :: Config -> [Name] -> [Name] -> Rule -> String -codeRule config assertionNames coverageNames rule = +codeRule :: Config -> Rule -> String +codeRule config rule@(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 ++ ", __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" @@ -208,12 +205,6 @@ ues = topo $ allUEs rule id ue = fromJust $ lookup ue ues - assertionId :: Name -> String - assertionId name = show $ fromJust $ elemIndex name assertionNames - - coverageId :: Name -> String - coverageId name = show $ fromJust $ elemIndex name coverageNames - codeAction :: (([String] -> String), [UE]) -> String codeAction (f, args) = " " ++ f (map id args) ++ ";\n" @@ -229,6 +220,23 @@ UVArray (UAExtern n _) index -> concat [n, "[", id index, "]"] UVExtern n _ -> n +codeRule _ _ = "" + +codeAssertionChecks :: Config -> [Name] -> [Name] -> [Rule] -> String +codeAssertionChecks config assertionNames coverageNames rules = codeIf (cAssert config) $ + "static void __assertion_checks(void) {\n" ++ + concatMap (codeUE config ues " ") ues ++ + concat [ " if (" ++ id enable ++ ") " ++ cAssertName config ++ "(" ++ assertionId name ++ ", " ++ id check ++ ", __global_clock);\n" | Assert name enable check <- rules ] ++ + concat [ " if (" ++ id enable ++ ") " ++ cCoverName config ++ "(" ++ coverageId name ++ ", " ++ id check ++ ", __global_clock);\n" | Cover name enable check <- rules ] ++ + "}\n\n" + where + ues = topo $ concat [ [a, b] | Assert _ a b <- rules ] ++ concat [ [a, b] | Cover _ a b <- rules ] + id ue = fromJust $ lookup ue ues + assertionId :: Name -> String + assertionId name = show $ fromJust $ elemIndex name assertionNames + coverageId :: Name -> String + coverageId name = show $ fromJust $ elemIndex name coverageNames + codePeriodPhase :: Config -> (Int, Int, [Rule]) -> String codePeriodPhase config (period, phase, rules) = unlines [ printf " {" @@ -246,5 +254,5 @@ clockType | period < 2 ^ 8 = Word8 | period < 2 ^ 16 = Word16 | otherwise = Word32 - callRule r = concat [" __r", show (ruleId r), "(); /* ", show r, " */"] + callRule r = concat [" ", codeIf (cAssert config) "__assertion_checks(); ", "__r", show (ruleId r), "(); /* ", show r, " */"] diff --git a/Language/Atom/Common.hs b/Language/Atom/Common.hs --- a/Language/Atom/Common.hs +++ b/Language/Atom/Common.hs @@ -14,6 +14,7 @@ , debounce -- * Lookup Tables , lookupTable + , linear -- * Hysteresis , hysteresis ) where @@ -87,6 +88,13 @@ slope = (y1 - y0) / (x1 - x0) interp = (x - x0) * slope + y0 +-- | Linear extrapolation and interpolation on a line with 2 points. +-- The two x points must be different to prevent a divide-by-zero. +linear :: FloatingE a => (E a, E a) -> (E a, E a) -> E a -> E a +linear (x1, y1) (x2, y2) a = slope * a + inter + where + slope = y2 - y1 / x2 - x1 + inter = y1 - slope * x1 -- | Hysteresis returns 'True' when the input exceeds @max@ and 'False' when -- the input is less than @min@. The state is held when the input is between diff --git a/Language/Atom/Compile.hs b/Language/Atom/Compile.hs --- a/Language/Atom/Compile.hs +++ b/Language/Atom/Compile.hs @@ -23,6 +23,6 @@ Nothing -> putStrLn "ERROR: Design rule checks failed." >> exitWith (ExitFailure 1) Just (rules, uvs, uas, assertionNames, coverageNames, probeNames) -> do let schedule' = schedule rules - ruleCoverage <- writeC name config schedule' uvs uas assertionNames coverageNames probeNames + ruleCoverage <- writeC name config rules schedule' uvs uas assertionNames coverageNames probeNames return (schedule', ruleCoverage, assertionNames, coverageNames, probeNames) diff --git a/Language/Atom/Elaboration.hs b/Language/Atom/Elaboration.hs --- a/Language/Atom/Elaboration.hs +++ b/Language/Atom/Elaboration.hs @@ -63,29 +63,36 @@ , atomCovers :: [(Name, UE)] } -data Rule = Rule - { ruleId :: Int - , ruleName :: Name - , ruleEnable :: UE - , ruleAssigns :: [(UV, UE)] - , ruleActions :: [([String] -> String, [UE])] - , rulePeriod :: Int - , rulePhase :: Int - , ruleAsserts :: [(Name, UE)] - , ruleCovers :: [(Name, UE)] - } +data Rule + = Rule + { ruleId :: Int + , ruleName :: Name + , ruleEnable :: UE + , ruleAssigns :: [(UV, UE)] + , ruleActions :: [([String] -> String, [UE])] + , rulePeriod :: Int + , rulePhase :: Int + } + | Assert + { ruleName :: Name + , ruleEnable :: UE + , ruleAssert :: UE + } + | Cover + { ruleName :: Name + , ruleEnable :: UE + , ruleCover :: UE + } 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 -instance Eq Rule where (==) = (==) `on` ruleId -instance Ord Rule where compare a b = compare (ruleId a) (ruleId b) elaborateRules:: UE -> AtomDB -> [Rule] elaborateRules parentEnable atom = if isRule then rule : rules else rules where - isRule = not $ null (atomAssigns atom) && null (atomActions atom) && null (atomAsserts atom) && null (atomCovers atom) + isRule = not $ null (atomAssigns atom) && null (atomActions atom) enable = uand parentEnable $ atomEnable atom rule = Rule { ruleId = atomId atom @@ -95,17 +102,26 @@ , ruleActions = atomActions atom , rulePeriod = atomPeriod atom , rulePhase = atomPhase atom - , ruleAsserts = atomAsserts atom - , ruleCovers = atomCovers atom } - rules = concatMap (elaborateRules enable) (atomSubs 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 :: [Rule] -> [Rule] -reIdRules rules = map (\ r -> r { ruleId = fromJust $ lookup (ruleId r) ids } ) rules - where - ids = zip (map ruleId rules) [0..] +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 @@ -154,9 +170,9 @@ 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, gPhase = 0 } name atom - let rules = reIdRules $ elaborateRules (ubool True) atomDB - coverageNames = concatMap (fst . unzip . ruleCovers ) rules - assertionNames = concatMap (fst . unzip . ruleAsserts) rules + 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 @@ -177,7 +193,7 @@ -- | 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 = +checkAssignConflicts rule@(Rule _ _ _ _ _ _ _) = if length vars /= length vars' then do putStrLn $ "ERROR: Rule " ++ show rule ++ " contains multiple assignments to the same variable(s)." @@ -187,6 +203,7 @@ where vars = fst $ unzip $ ruleAssigns rule vars' = nub vars +checkAssignConflicts _ = return True {- -- | Checks that all array indices are not a function of array variables. @@ -280,7 +297,7 @@ allUVs :: [Rule] -> UE -> [UV] allUVs rules ue = fixedpoint next $ nearestUVs ue where - assigns = concatMap ruleAssigns rules + assigns = concat [ ruleAssigns r | r@(Rule _ _ _ _ _ _ _) <- rules ] previousUVs :: UV -> [UV] previousUVs uv = concat [ nearestUVs ue | (uv', ue) <- assigns, uv == uv' ] next :: [UV] -> [UV] @@ -292,9 +309,13 @@ -- | All primary expressions used in a rule. allUEs :: Rule -> [UE] -allUEs rule = ruleEnable rule : concat [ ue : index uv | (uv, ue) <- ruleAssigns rule ] ++ concat (snd (unzip (ruleActions rule))) ++ snd (unzip (ruleAsserts rule)) ++ snd (unzip (ruleCovers rule)) +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] diff --git a/Language/Atom/Language.hs b/Language/Atom/Language.hs --- a/Language/Atom/Language.hs +++ b/Language/Atom/Language.hs @@ -287,7 +287,9 @@ return (value $ V $ UVExtern "__coverage_index" Word32, value $ V $ UVExtern "__coverage[__coverage_index]" Word32) --- | Assertion that checks an E Bool. Assertions are only checked if the containing rule is enabled and executed. +-- | An assertions checks that an E Bool is true. Assertions are checked between the execution of every rule. +-- Parent enabling conditions can disable assertions, but period and phase constraints do not. +-- Assertion names should be globally unique. assert :: Name -> E Bool -> Atom () assert name check = do (g, atom) <- get @@ -301,11 +303,13 @@ assert name $ imply a b cover (name ++ "Precondition") a --- | Adds a functional coverage point. +-- | A functional coverage point tracks if an event has occured (true). +-- Coverage points are checked at the same time as assertions. +-- Coverage names should be globally unique. cover :: Name -> E Bool -> Atom () cover name check = do (g, atom) <- get - let names = fst $ unzip $ atomAsserts atom - when (elem name names) (liftIO $ putStrLn $ "WARNING: Assertion name already used: " ++ name) + let names = fst $ unzip $ atomCovers atom + when (elem name names) (liftIO $ putStrLn $ "WARNING: Coverage name already used: " ++ name) put (g, atom { atomCovers = (name, ue check) : atomCovers atom }) diff --git a/Language/Atom/Scheduling.hs b/Language/Atom/Scheduling.hs --- a/Language/Atom/Scheduling.hs +++ b/Language/Atom/Scheduling.hs @@ -13,8 +13,9 @@ type Schedule = [(Int, Int, [Rule])] -- (period, phase, rules) schedule :: [Rule] -> Schedule -schedule rules = concatMap spread periods +schedule rules' = concatMap spread periods where + rules = [ r | r@(Rule _ _ _ _ _ _ _) <- rules' ] -- Algorithm for assigning rules to phases for a given period: diff --git a/Language/Atom/Unit.hs b/Language/Atom/Unit.hs --- a/Language/Atom/Unit.hs +++ b/Language/Atom/Unit.hs @@ -88,6 +88,8 @@ runTest :: Int -> IO Test -> IO (Name, Bool, Int, [Name], [Name]) runTest seed test = do test <- test + putStrLn $ "running test " ++ name test ++ " ..." + hFlush stdout (_, _, _, coverageNames, _) <- compile "atom_unit_test" defaults { cCode = prePostCode test, cRuleCoverage = False } $ testbench test (exit, out, err) <- readProcessWithExitCode "gcc" (["-Wall", "-g", "-o", "atom_unit_test"] ++ [ "-i" ++ i | i <- includes test ] ++ modules test ++ ["atom_unit_test.c"]) "" let file = name test ++ ".log" @@ -110,11 +112,15 @@ , "#include " , "void assert (int id, unsigned char check, unsigned long long clock) {" , " static unsigned char failed[" ++ show (length assertionNames) ++ "] = {" ++ intercalate "," (replicate (length assertionNames) "0") ++ "};" - , " " ++ intercalate "\n else " [ "if (id == " ++ show id ++ ") { if (! check && ! failed[id]) { printf(\"ASSERTION FAILURE: " ++ name ++ " at time %lli\\n\", clock); failed[id] = 1; } }" | (name, id) <- zip assertionNames [0..] ] + , " if (! check) {" + , " " ++ intercalate "\n else " [ "if (id == " ++ show id ++ ") { if (! failed[id]) { printf(\"ASSERTION FAILURE: " ++ name ++ " at time %lli\\n\", clock); failed[id] = 1; } }" | (name, id) <- zip assertionNames [0..] ] + , " }" , "}" , "void cover (int id, unsigned char check, unsigned long long clock) {" , " static unsigned char covered[" ++ show (length coverageNames) ++ "] = {" ++ intercalate "," (replicate (length coverageNames) "0") ++ "};" - , " " ++ intercalate "\n else " [ "if (id == " ++ show id ++ ") { if (check && ! covered[id]) { printf(\"covered: " ++ name ++ " at time %lli\\n\", clock); covered[id] = 1; } }" | (name, id) <- zip coverageNames [0..] ] + , " if (check) {" + , " " ++ intercalate "\n else " [ "if (id == " ++ show id ++ ") { if (! covered[id]) { printf(\"covered: " ++ name ++ " at time %lli\\n\", clock); covered[id] = 1; } }" | (name, id) <- zip coverageNames [0..] ] + , " }" , "}" ] ++ declCode test diff --git a/RELEASE-NOTES b/RELEASE-NOTES --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,3 +1,9 @@ +atom 0.1.3 12/03/2009 + +- Added linear lookup (Common). +- Assertions and coverage points are checked between the execution of every rule, not just once per cycle. +- Removed cCover code configuration. Assertions and coverage are enabled by cAssert. + atom 0.1.2 11/25/2009 - Added div0_ and mod0_ functions, that instrument runtime checks for divide-by-zero (Lee Pike). diff --git a/atom.cabal b/atom.cabal --- a/atom.cabal +++ b/atom.cabal @@ -1,15 +1,21 @@ name: atom -version: 0.1.2 +version: 0.1.3 category: Language synopsis: A DSL for embedded hard realtime applications. description: - Atom is a Haskell DSL for designing hard realtime embedded programs. Based - on conditional term rewriting, atom will compile a collection of atomic - state transition rules to a C program with constant memory use and - deterministic execution time. + Atom is a Haskell DSL for designing hard realtime embedded software. + Based on guarded atomic actions (similar to STM), Atom enables + highly concurrent programming without the need for mutex locking. + + In addition, Atom performs compile-time task scheduling and generates code + with deterministic execution time and constant memory use, simplifying the + process of timing verification and memory consumption in hard realtime applications. + + Without mutex locking and run-time task scheduling, Atom eliminates + the need and overhead of RTOSs for many embedded applications. author: Tom Hawkins maintainer: Tom Hawkins