package ltl
- Alphabetic
- Public
- Protected
Type Members
- sealed abstract class AssertPropertyLike extends AnyRef
The base class for the
AssertProperty
,AssumeProperty
, andCoverProperty
verification 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 beSequence
s themselves, likea
ora 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.apply
for 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.apply
for 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.apply
for 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(...)
. SeeSequenceAtom
for 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
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 toEnsureProperty
is assumed to hold.Use like
EnsureProperty(p)
. SeeAssertPropertyLike.apply
for 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
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 toRequireProperty
is asserted to hold.Use like
RequireProperty(p)
. SeeAssertPropertyLike.apply
for 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 typesBundle
andVec
.The Chisel package is a compatibility layer that attempts to provide chisel2 compatibility in chisel3.
Utility objects and methods are found in the
util
package.The
testers
package defines the basic interface for chisel testers.