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
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*): 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): 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. def disable(prop: Property, cond: Disable): Property

    Disable the checking of a property if a condition is true.

    Disable the checking of a property if a condition is true. If the condition is true at any time during the evaluation of the property, the evaluation is aborted. Equivalent to disable iff (cond) prop in SVA.

  9. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  10. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  11. def eventually(prop: Property): 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.

  12. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable])
  13. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  15. def implication(seq: Sequence, prop: Property): 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.

  16. def implicationNonOverlapping(seq: Sequence, prop: Property): Property

    Non-overlapping variant of Property.implication.

    Non-overlapping variant of Property.implication. Equivalent to seq ##1 true |-> prop and seq |=> prop 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): 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*): 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. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  26. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  27. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped