Module Verify


module Verify: sig .. end
Digital verification.


Verification Types


type sequence = Circuit.sequence 
Sequences are analogous to PSL's SEREs.
type property = Circuit.property 
Properties are analogous to PSL's formulas.

Common Helpers


val rigid : string -> int -> Design.signal
Creates a non-deterministic, rigid signal for verification.

Sequences


val seq : Design.signal -> sequence
Creates a sequence from a single bit signal.
val ($) : sequence -> sequence -> sequence
Sequence concatenation. (PSL: s1 ; s2)
val (-$) : sequence -> sequence -> sequence
Sequence infusion. (PSL: s1 : s2)
val (|$) : sequence -> sequence -> sequence
Sequence alternation. (PSL: s1 | s2)
val (&$) : sequence -> sequence -> sequence
Sequence AND (non-length matching). (PSL: s1 & s2)
val (&&$) : sequence -> sequence -> sequence
Sequence AND (length matching). (PSL: s1 && s2)
val within : sequence -> sequence -> sequence
(PSL s1 within s2)
val star : sequence
Anything (0 or more). PSL: [*]
val plus : sequence
Anything 1 or more. (PSL: [+])
val any_n : int -> sequence
Anything for n cycles. (PSL: [*n])
val any_n_to_m : int -> int -> sequence
Anything for n to m cycles. (PSL: [*n:m])
val any_n_to_inf : int -> sequence
Anything for n to inf cycles. (PSL: [*n:inf])
val repeat_star : sequence -> sequence
Sequence repetion (0 or more). (PSL: s[*])
val repeat_plus : sequence -> sequence
Sequence repetion (1 or more). (PSL: s[+])
val repeat_n : sequence -> int -> sequence
Consecutive repetition. (PSL: s[*n])
val repeat_n_to_m : sequence -> int -> int -> sequence
Consecutive repetition. (PSL: s[*n:m])
val repeat_n_to_inf : sequence -> int -> sequence
Consecutive repetition. (PSL: s[*n:inf])

Properties


val prop : Design.signal -> property
Creates a property from a single bit signal.
val (!?) : property -> property
Property NOT. PSL: ! a
val (&&?) : property -> property -> property
Property AND. PSL: a && b
val (||?) : property -> property -> property
Property OR. PSL: a || b
val (->?) : property -> property -> property
Property implication. PSL: a -> b
val (<->?) : property -> property -> property
Property equivalence. PSL: a <-> b
val always : property -> property
Property is always true. PSL: always a
val never : property -> property
Property is never true. PSL: never p
val eventually : property -> property
Eventually. PSL: eventually! a
val propseq : sequence -> property
Creates a property from a sequence. PSL: sequence !
val propseq_w : sequence -> property
Creates a property from a weak sequence. PSL: sequence
val until : property -> property -> property
Strong until. PSL: a until! b
val until_w : property -> property -> property
Weak until. PSL: a until b
val (|->) : sequence -> property -> property
Suffix implication, overlapping. (PSL: s |-> p)
val (|=>) : sequence -> property -> property
Suffix implication, non-overlapping. (PSL: s |=> p)

Verification Directives


val assertion : string -> property -> unit
Asserts a property.
val assert_always : string -> property -> unit
Asserts always a property.
val assert_always_signal : string -> Design.signal -> unit
Asserts always a signal.
val assume : string -> property -> unit
Assumes a property.
val assume_always : string -> property -> unit
Assumes always a property.
val assume_always_signal : string -> Design.signal -> unit
Assumes always a signal.
val cover : string -> sequence -> unit
Sets a cover point.