chisel3.ltl

Assert that a property holds.

Use like AssertProperty(p). See AssertPropertyLike.apply for optional clock, disable_iff, and label parameters.

The base class for the AssertProperty, AssumeProperty, and CoverProperty verification constructs.

Assume that a property holds.

Use like AssumeProperty(p). See AssertPropertyLike.apply for optional clock, disable_iff, and label parameters.

Cover that a property holds.

Use like CoverProperty(p). See AssertPropertyLike.apply for optional clock, disable_iff, and label parameters.

The delay atoms available to users. Can be interleaved with actual sequences in Sequence(...). See SequenceAtom for details.

Ensure that a property holds as a post-condition of a contract. Behaves like an AssertProperty if used outside of a contract. When used inside of a contract, the behavior differs depending on how the contract is used in a formal proof:

• During a proof that the contract is upheld by the surrounding circuit, the property given to EnsureProperty is asserted to hold.
• During a larger proof where the contract is already assumed to be proven, the property given to EnsureProperty is assumed to hold.

Use like EnsureProperty(p). See AssertPropertyLike.apply for optional clock, disable_iff, and label parameters.

A Linear Temporal Logic (LTL) property.

Prefix-style utilities to work with properties.

This object exposes the primary API to create and compose properties from booleans, sequences, and other properties.

Require that a property holds as a pre-condition of a contract. Behaves like an AssertProperty if used outside of a contract. When used inside of a contract, the behavior differs depending on how the contract is used in a formal proof:

• During a proof that the contract is upheld by the surrounding circuit, the property given to RequireProperty is assumed to hold.
• During a larger proof where the contract is already assumed to be proven, the property given to RequireProperty is asserted to hold.

Use like RequireProperty(p). See AssertPropertyLike.apply for optional clock, disable_iff, and label parameters.

A Linear Temporal Logic (LTL) sequence.

Prefix-style utilities to work with sequences.

This object exposes the primary API to create and compose sequences from booleans and shorter sequences.

A single item that may be used in the Sequence(...) convenience constructor for sequences. These atoms may either be Sequences themselves, like a or a and b, or a DelayAtom, like Delay. Together they enable a shorthand notation for sequences like:

Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e).