ltl-0.0.0: Using linear temporal logic (LTL) to verify embedded software and hardware.
Using linear temporal logic (LTL) to verify embedded software and hardware.
data N Source
data B Source
data R Source
data F Source
data E a Source
LTL (and other) expressions.
data Directive Source
Property must be true.
Property is assumed to be true. Becomes an assertion in simulation.
Sequence must be excited.
checkVCD :: String -> Int -> [Directive] -> [(Directive, Maybe Int)]Source
Check VCD data against a set of verification directives. Returns a list of violations with time of failure (Just: safety violation, Nothing: liveness violation).
Produced by Haddock version 2.8.0