chisel
7.9.0+2-5294dafe-SNAPSHOT
API
Generated with
chisel/chisel3/chisel3.ltl/RequireProperty

RequireProperty

chisel3.ltl.RequireProperty
object RequireProperty extends AssertPropertyLike

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.

Attributes

Source
LTL.scala
Graph
Supertypes
class Object
trait Matchable
class Any
Self type

Members list

Value members

Inherited methods

protected def _applyCondClockDisableLabelImpl(cond: Bool, clock: Clock, disable: Disable, label: String)(implicit sourceInfo: SourceInfo): Unit

Attributes

Inherited from:
AssertPropertyLike
Source
LTL.scala
protected def _applyCondImpl(cond: Bool)(implicit sourceInfo: SourceInfo): Unit

Attributes

Inherited from:
AssertPropertyLike
Source
LTL.scala
protected def _applyCondLabelImpl(cond: Bool, label: String)(implicit sourceInfo: SourceInfo): Unit

Attributes

Inherited from:
AssertPropertyLike
Source
LTL.scala
protected def _applyImpl(prop: => Property, clock: Option[Clock] = ..., disable: Option[Disable] = ..., label: Option[String] = ...)(implicit sourceInfo: SourceInfo): Unit

Attributes

Inherited from:
AssertPropertyLike
Source
LTL.scala
def apply(cond: Bool, clock: Clock, disable: Disable, label: String)(using SourceInfo): Unit

Assert, assume, or cover that a boolean predicate holds.

Assert, assume, or cover that a boolean predicate holds.

Value parameters

clock:

specifies a clock with respect to which all cycle delays in the property are expressed. This is a shorthand for prop.clock(clock).

cond:

a boolean predicate that should be checked.

disable:

specifies a condition under which the evaluation of the property is disabled. This is a shorthand for prop.disable(disable).

label:

is used to assign a name to the assert, assume, or cover construct in the output language. In SystemVerilog, this is emitted as label: assert(...). This will generate a boolean property that is clocked using the implicit clock and disabled in the case where the design has not yet been reset.

Attributes

Inherited from:
AssertPropertyLikeIntf (hidden)
Source
LTLIntf.scala
def apply(cond: Bool, label: String)(using SourceInfo): Unit

Assert, assume, or cover that a boolean predicate holds.

Assert, assume, or cover that a boolean predicate holds.

Value parameters

cond:

a boolean predicate that should be checked.

label:

is used to assign a name to the assert, assume, or cover construct in the output language. In SystemVerilog, this is emitted as label: assert(...). This will generate a boolean property that is clocked using the implicit clock and disabled in the case where the design has not yet been reset.

Attributes

Inherited from:
AssertPropertyLikeIntf (hidden)
Source
LTLIntf.scala
def apply(cond: Bool)(using SourceInfo): Unit

Assert, assume, or cover that a boolean predicate holds.

Assert, assume, or cover that a boolean predicate holds.

Value parameters

cond:

a boolean predicate that should be checked. This will generate a boolean property that is clocked using the implicit clock and disabled in the case where the design has not yet been reset.

Attributes

Inherited from:
AssertPropertyLikeIntf (hidden)
Source
LTLIntf.scala
def apply(prop: => Property, clock: Option[Clock] = ..., disable: Option[Disable] = ..., label: Option[String] = ...)(using SourceInfo): Unit

Assert, assume, or cover that a property holds.

Assert, assume, or cover that a property holds.

Value parameters

clock

[optional]: specifies a clock with respect to which all cycle delays in the property are expressed. This is a shorthand for prop.clock(clock).

disable

[optional]: specifies a condition under which the evaluation of the property is disabled. This is a shorthand for prop.disable(disable).

label

[optional]: is used to assign a name to the assert, assume, or cover construct in the output language. In SystemVerilog, this is emitted as label: assert(...).

prop:

parameter can be a Property, Sequence, or simple Bool.

Attributes

Inherited from:
AssertPropertyLikeIntf (hidden)
Source
LTLIntf.scala
Generated with