c

spinal.core.formal

SpinalFormalConfig

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: FormalBackend = SymbiYosysFormalBackend, _keepDebugInfo: Boolean = false, _skipWireReduce: Boolean = false, _hasAsync: Boolean = false, _timeout: Option[Int] = None, _engines: ArrayBuffer[FormalEngin] = ArrayBuffer()) extends Product with Serializable

SpinalSim configuration

Linear Supertypes
Serializable, Serializable, Product, Equals, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. SpinalFormalConfig
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. AnyRef
  7. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new 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: FormalBackend = SymbiYosysFormalBackend, _keepDebugInfo: Boolean = false, _skipWireReduce: Boolean = false, _hasAsync: Boolean = false, _timeout: Option[Int] = None, _engines: ArrayBuffer[FormalEngin] = ArrayBuffer())

Value Members

  1. var _additionalIncludeDir: ArrayBuffer[String]
  2. var _additionalRtlPath: ArrayBuffer[String]
  3. var _backend: FormalBackend
  4. var _engines: ArrayBuffer[FormalEngin]
  5. var _hasAsync: Boolean
  6. var _keepDebugInfo: Boolean
  7. var _modesWithDepths: LinkedHashMap[String, Int]
  8. var _skipWireReduce: Boolean
  9. var _spinalConfig: SpinalConfig
  10. var _timeout: Option[Int]
  11. var _workspaceName: String
  12. var _workspacePath: String
  13. def addEngin(engin: FormalEngin): SpinalFormalConfig.this.type
  14. def addIncludeDir(that: String): SpinalFormalConfig.this.type
  15. def addRtl(that: String): SpinalFormalConfig.this.type
  16. def compile[T <: Component](report: SpinalReport[T]): SpinalFormalBackend
  17. def compile[T <: Component](rtl: ⇒ T): SpinalFormalBackend
  18. def compileCloned[T <: Component](rtl: ⇒ T): SpinalFormalBackend
  19. def doVerify[T <: Component](rtl: ⇒ T, name: String)(implicit className: String): Unit
  20. def doVerify[T <: Component](rtl: ⇒ T)(implicit className: String): Unit
  21. def doVerify[T <: Component](report: SpinalReport[T], name: String)(implicit className: String): Unit
  22. def doVerify[T <: Component](report: SpinalReport[T])(implicit className: String): Unit
  23. def withAsync: SpinalFormalConfig.this.type
  24. def withBMC(depth: Int = 100): SpinalFormalConfig.this.type
  25. def withBackend(backend: FormalBackend): SpinalFormalConfig.this.type
  26. def withConfig(config: SpinalConfig): SpinalFormalConfig.this.type
  27. def withCover(depth: Int = 100): SpinalFormalConfig.this.type
  28. def withDebug: SpinalFormalConfig.this.type
  29. def withEngies(engins: Seq[FormalEngin]): SpinalFormalConfig.this.type
  30. def withGhdl: SpinalFormalConfig.this.type
  31. def withOutWireReduce: SpinalFormalConfig.this.type
  32. def withProve(depth: Int = 100): SpinalFormalConfig.this.type
  33. def withSymbiYosys: SpinalFormalConfig.this.type
  34. def withSyncOnly: SpinalFormalConfig.this.type
  35. def withSyncResetDefault: SpinalFormalConfig.this.type
  36. def withTimeout(timeout: Int): SpinalFormalConfig.this.type
  37. def workspaceName(name: String): SpinalFormalConfig.this.type
  38. def workspacePath(path: String): SpinalFormalConfig.this.type