Formula Combinators

data N Source

Instances

NB N

data B Source

Instances

NB B
BR B
BF B

data R Source

Instances

BR R

data F Source

Instances

BF F

data E a Source

LTL (and other) expressions.

Verification Directives

data Directive Source

Verification directives.

Constructors

Assert String (E F)	Property must be true.
Assume String (E F)	Property is assumed to be true. Becomes an assertion in simulation.
Cover String (E R)	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).