Packages

object 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.

Source
LTL.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. Property
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def and(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property

    Form the conjunction of two properties.

    Form the conjunction of two properties. Equivalent to arg0 and arg1 and ... and argN in SVA.

  5. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  6. def clock(prop: Property, clock: Clock)(implicit sourceInfo: SourceInfo): Property

    Specify a clock relative to which all cycle delays within prop are specified.

    Specify a clock relative to which all cycle delays within prop are specified. Equivalent to @(posedge clock) prop in SVA.

  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  10. def eventually(prop: Property)(implicit sourceInfo: SourceInfo): Property

    Indicate that a property will eventually hold at a future point in time.

    Indicate that a property will eventually hold at a future point in time. This is a *strong* eventually, so the property has to hold within a finite number of cycles. The property does not trivially hold by waiting an infinite number of cycles.

    Equivalent to s_eventually prop in SVA.

  11. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable])
  12. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def implication(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property

    Precondition the checking of a property (the consequent) on a sequence (the antecedent).

    Precondition the checking of a property (the consequent) on a sequence (the antecedent). Equivalent to the overlapping implication seq |-> prop in SVA.

  15. def implicationNonOverlapping(seq: Sequence, prop: Property)(implicit sourceInfo: SourceInfo): Property

    Non-overlapping variant of Property.implication.

    Non-overlapping variant of Property.implication. Equivalent to seq ##1 true |-> prop and seq |=> prop in SVA.

  16. def intersect(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property

    Form the conjunction of two properties, where the start and end times of both sequences must be identical.

    Form the conjunction of two properties, where the start and end times of both sequences must be identical. Equivalent to arg0 intersect arg1 intersect ... intersect argN in SVA.

  17. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  18. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  19. def not(prop: Property)(implicit sourceInfo: SourceInfo): Property

    Negate a property.

    Negate a property. Equivalent to not prop in SVA.

  20. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  21. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  22. def or(arg0: Property, argN: Property*)(implicit sourceInfo: SourceInfo): Property

    Form the disjunction of two properties.

    Form the disjunction of two properties. Equivalent to arg0 or arg1 or ... or argN in SVA.

  23. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  24. def toString(): String
    Definition Classes
    AnyRef → Any
  25. def until(arg0: Property, arg1: Property)(implicit sourceInfo: SourceInfo): Property

    Check that a property holds untile another property holds.

    Check that a property holds untile another property holds. This operator is weak: the property will hold even if input always holds and condition never holds.

  26. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  27. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  28. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped