chiseltest.formal
package chiseltest.formal
Formal compatibility API placeholders.
Formal verification is currently unsupported in this compatibility layer. Any usage should fail at compile time to avoid vacuously passing tests.
Attributes
Members list
Type members
Classlikes
Result of a Bounded Model Checking run
Result of a Bounded Model Checking run
Attributes
- Source
- package.scala
- Supertypes
-
class Objecttrait Matchableclass Any
- Known subtypes
case object BTORMCBackend extends FormalBackendAnnotation
Attributes
- Source
- package.scala
- Supertypes
-
trait Singletontrait Producttrait Mirrortrait Serializabletrait Producttrait Equalsclass FormalBackendAnnotationclass Objecttrait Matchableclass AnyShow all
- Self type
-
BTORMCBackend.type
case class BasicWitness(body: String) extends Witness
Most basic type of witness: simply dumps the ouput from the BMC tool
Most basic type of witness: simply dumps the ouput from the BMC tool
Attributes
- Source
- package.scala
- Supertypes
-
trait Serializabletrait Producttrait Equalsclass Witnessclass Objecttrait Matchableclass AnyShow all
Annotation placeholder for source compatibility only.
Annotation placeholder for source compatibility only.
Attributes
- Source
- package.scala
- Supertypes
-
trait Serializabletrait Producttrait Equalsclass Objecttrait Matchableclass AnyShow all
trait Formal
Attributes
- Source
- package.scala
- Supertypes
-
class Objecttrait Matchableclass Any
abstract class FormalBackendAnnotation(val name: String, val kmaxFlag: String, val UnsatOutput: String, val SatOutput: String)
Bounded Model Checking Backends supported by Formal. Currently only BTORMC is supported.
Bounded Model Checking Backends supported by Formal. Currently only BTORMC is supported.
Attributes
- Source
- package.scala
- Supertypes
-
class Objecttrait Matchableclass Any
- Known subtypes
-
object BTORMCBackend
Attributes
- Source
- package.scala
- Supertypes
-
trait Serializabletrait Producttrait Equalsclass BMCResultclass Objecttrait Matchableclass AnyShow all
Attributes
- Source
- package.scala
- Supertypes
-
trait Singletontrait Producttrait Mirrortrait Serializabletrait Producttrait Equalsclass BMCResultclass Objecttrait Matchableclass AnyShow all
- Self type
-
Unsat.type
counterexample object for a BMC run
counterexample object for a BMC run
Attributes
- Source
- package.scala
- Supertypes
-
class Objecttrait Matchableclass Any
- Known subtypes
-
class BasicWitness
Value members
Concrete methods
Attributes
- Source
- package.scala
In this article