Packages

p

spinal.core

formal

package formal

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. formal
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. case class Abc() extends SbyEngine with Product with Serializable
  2. case class Aiger() extends SbyEngine with Product with Serializable
  3. trait FormalBackend extends AnyRef
  4. trait FormalEngin extends AnyRef
  5. sealed trait SbyEngine extends FormalEngin
  6. case class SmtBmc(nomem: Boolean = false, syn: Boolean = false, stbv: Boolean = false, stdt: Boolean = false, nopresat: Boolean = false, unroll: Option[Boolean] = None, dumpsmt2: Boolean = false, progress: Boolean = true, solver: SmtBmcSolver.SmtBmcSolver = SmtBmcSolver.Yices) extends SbyEngine with Product with Serializable
  7. class SpinalFormalBackendSel extends AnyRef
  8. case class SpinalFormalConfig(_workspacePath: String = ..., _workspaceName: String = null, _spinalConfig: SpinalConfig = SpinalConfig().includeFormal, _additionalRtlPath: ArrayBuffer[String] = ArrayBuffer[String](), _additionalIncludeDir: ArrayBuffer[String] = ArrayBuffer[String](), _modesWithDepths: LinkedHashMap[String, Int] = LinkedHashMap[String, Int](), _backend: SpinalFormalBackendSel = SpinalFormalBackendSel.SYMBIYOSYS, _keepDebugInfo: Boolean = false, _skipWireReduce: Boolean = false, _hasAsync: Boolean = false, _timeout: Option[Int] = None, _engines: ArrayBuffer[FormalEngin] = ArrayBuffer()) extends Product with Serializable

    SpinalSim configuration

  9. class SpinalSbyException extends Exception
  10. class SymbiYosysBackend extends FormalBackend
  11. class SymbiYosysBackendConfig extends AnyRef

Value Members

  1. def FormalConfig: SpinalFormalConfig
  2. def allconst[T <: Data](that: T): T
  3. def allseq[T <: Data](that: T): T
  4. def anyconst[T <: Data](that: T): T
  5. def anyseq[T <: Data](that: T): T
  6. def changed[T <: Data](that: T, init: T = null.asInstanceOf[T]): Bool
  7. implicit val className: String
  8. def fell(that: Bool): Bool
  9. def initstate(): Bool
  10. def past[T <: Data](that: T): T
  11. def past[T <: Data](that: T, delay: Int): T
  12. def pastValid(): Bool
  13. def pastValidAfterReset(): Bool
  14. def rose(that: Bool): Bool
  15. def stable[T <: Data](that: T, init: T = null.asInstanceOf[T]): Bool
  16. object FormalDut
  17. object FormalWorkspace

    Formal verify Workspace

  18. object SbyMode extends Enumeration
  19. object SmtBmcSolver extends Enumeration
  20. object SpinalFormalBackendSel

Inherited from AnyRef

Inherited from Any

Ungrouped