Packages

o

chisel3

FormalContract

object FormalContract extends FormalContract$Intf

Create a contract block.

Outside of verification uses, the arguments passed to the contract are simply returned as contract results. During formal verification, the contract may act as a cutpoint by returning symbolic values for its results and using the contract body as constraint.

Within the contract body, RequireProperty and EnsureProperty can be used to describe the pre and post-conditions of the contract. During formal verification, contracts can be used to divide large formal checks into smaller pieces by first asserting some local properties hold, and then assuming those properties hold in the context of the larger proof.

Source
FormalContract.scala
Example:

  1. The following is a contract with no arguments.

    FormalContract {
  RequireProperty(a >= 1)
  EnsureProperty(a + a >= 2)
}

    The following is a contract with a single argument. It expresses the fact that the hardware implementation (a << 3) + a is equivalent to a * 9. During formal verification, this contract is interpreted as: - assert((a << 3) + a === a * 9) as a proof that the contract holds. - assume(b === a * 9) on a new symbolic value b as a simplification of other proofs.

    val b = FormalContract((a << 3) + a) { b =>
  EnsureProperty(b === a * 9)
}

    The following is a contract with multiple arguments. It expresses the fact that a carry-save adder with p, q, and r as inputs reduces the number of sum terms from p + q + r to c + s but doesn't change the sum of the terms. During formal verification, this contract is interpreted as: - assert(c + s === p + q + r) as a proof that the carry-save adder indeed compresses the three terms down to only two terms which have the same sum. - assume(u + v === p + q + r) on new symbolic values u and v as a simplification of other proofs.

    val s = p ^ q ^ r
val c = (p & q | (p ^ q) & r) << 1
val (u, v) = FormalContract(c, s) { case (u, v) =>
  EnsureProperty(u + v === p + q + r)
}
Linear Supertypes
FormalContract$Intf, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. FormalContract
  2. FormalContract$Intf
  3. AnyRef
  4. 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 apply(body: => Unit)(implicit sourceInfo: SourceInfo): Unit

    Create a contract block with no arguments and results.

  5. macro def apply(head: Data, tail: Data*): ((Any) => Unit) => Any

    Create a contract block with one or more arguments and results.

    Create a contract block with one or more arguments and results.

    Definition Classes
    FormalContract$Intf
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  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 finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable])
  11. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  13. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  14. def mapped[R](args: Seq[Data], mapping: (Seq[Data]) => R)(body: (R) => Unit)(implicit sourceInfo: SourceInfo): R

    Create a formal contract from a sequence of expressions.

    Create a formal contract from a sequence of expressions.

    The mapping function is used to convert the Seq[Data] to a user-defined type R, which is then passed to the contract body and returned as a result.

    This function is mainly intended for internal use, where the mapping function can be used to map the args sequence to a tuple that is more convenient for a user to work with.

    Example:

    1. Example with identity mapping. The Seq(a, b) is passed to withSeqArgs unmodified, and the contract returns a Seq[Data] result.

      def withSeqArgs(args: Seq[Data]): Unit = ...
val seqResult: Seq[Data] =
  FormalContract.mapping(Seq(a, b), _ => _)(withSeqArgs)

      Example with a mapping from sequence to a tuple. The Seq(a, b) is mapped to a (UInt, UInt) tuple through mapToTuple, which is then passed to withTupleArgs, and the contract returns a corresponding (UInt, UInt) result.

      def mapToTuple(args: Seq[Data]): (UInt, UInt) = {
  // check number of args and types, convert to tuple
}
def withTupleArgs(args: (UInt, UInt)): Unit = ...
val tupleResult: (UInt, UInt) =
  FormalContract.mapping(Seq(a, b), mapToTuple)(withTupleArgs)
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  19. def toString(): String
    Definition Classes
    AnyRef → Any
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()

Inherited from FormalContract$Intf

Inherited from AnyRef

Inherited from Any

Ungrouped