package ltl
- Alphabetic
- Public
- Protected
Type Members
- sealed abstract class AssertPropertyLike extends AnyRef
The base class for the
AssertProperty,AssumeProperty, andCoverPropertyverification constructs. - sealed trait Property extends AnyRef
A Linear Temporal Logic (LTL) property.
- sealed trait Sequence extends Property
A Linear Temporal Logic (LTL) sequence.
- sealed trait SequenceAtom extends AnyRef
A single item that may be used in the
Sequence(...)convenience constructor for sequences.A single item that may be used in the
Sequence(...)convenience constructor for sequences. These atoms may either beSequences themselves, likeaora and b, or aDelayAtom, likeDelay. Together they enable a shorthand notation for sequences like:Sequence(a, Delay(), b, Delay(2), c, Delay(3, 9), d, Delay(4, None), e).
Value Members
- object AssertProperty extends AssertPropertyLike
Assert that a property holds.
Assert that a property holds.
Use like
AssertProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object AssumeProperty extends AssertPropertyLike
Assume that a property holds.
Assume that a property holds.
Use like
AssumeProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object CoverProperty extends AssertPropertyLike
Cover that a property holds.
Cover that a property holds.
Use like
CoverProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object Delay
The delay atoms available to users.
The delay atoms available to users. Can be interleaved with actual sequences in
Sequence(...). SeeSequenceAtomfor details. - object EnsureProperty extends AssertPropertyLike
Ensure that a property holds as a post-condition of a contract.
Ensure that a property holds as a post-condition of a contract. Behaves like an
AssertPropertyif 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
EnsurePropertyis asserted to hold. - During a larger proof where the contract is already assumed to be proven, the property given toEnsurePropertyis assumed to hold.Use like
EnsureProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object Property
Prefix-style utilities to work with properties.
Prefix-style utilities to work with properties.
This object exposes the primary API to create and compose properties from booleans, sequences, and other properties.
- object RequireProperty extends AssertPropertyLike
Require that a property holds as a pre-condition of a contract.
Require that a property holds as a pre-condition of a contract. Behaves like an
AssertPropertyif 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
RequirePropertyis assumed to hold. - During a larger proof where the contract is already assumed to be proven, the property given toRequirePropertyis asserted to hold.Use like
RequireProperty(p). SeeAssertPropertyLike.applyfor optional clock, disable_iff, and label parameters. - object Sequence
Prefix-style utilities to work with sequences.
Prefix-style utilities to work with sequences.
This object exposes the primary API to create and compose sequences from booleans and shorter sequences.
This is the documentation for Chisel.
Package structure
The chisel3 package presents the public API of Chisel. It contains the concrete core types
UInt,SInt,Bool,Clock, andReg, the abstract typesBits,Aggregate, andData, and the aggregate typesBundleandVec.The Chisel package is a compatibility layer that attempts to provide chisel2 compatibility in chisel3.
Utility objects and methods are found in the
utilpackage.The
testerspackage defines the basic interface for chisel testers.