-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Using linear temporal logic (LTL) to verify embedded software and hardware.
--   
--   TODO
@package ltl
@version 0.0.0


-- | Using linear temporal logic (LTL) to verify embedded software and
--   hardware.
module Language.LTL
data N
data B
data R
data F

-- | LTL (and other) expressions.
data E a

-- | Verification directives.
data Directive

-- | Property must be true.
Assert :: String -> (E F) -> Directive

-- | Property is assumed to be true. Becomes an assertion in simulation.
Assume :: String -> (E F) -> Directive

-- | Sequence must be excited.
Cover :: String -> (E R) -> Directive

-- | Check VCD data against a set of verification directives. Returns a
--   list of violations with time of failure (Just: safety violation,
--   Nothing: liveness violation).
checkVCD :: String -> Int -> [Directive] -> [(Directive, Maybe Int)]
instance NB B
instance NB N
instance BR R
instance BR B
instance BF F
instance BF B