SpinalHDL 1.7.0 + formal example

build.sbt

@@ -2,7 +2,7 @@ ThisBuild / version := "1.0"
 ThisBuild / scalaVersion := "2.11.12"
 ThisBuild / organization := "org.example"
 
-val spinalVersion = "1.6.4"
+val spinalVersion = "1.7.0"
 val spinalCore = "com.github.spinalhdl" %% "spinalhdl-core" % spinalVersion
 val spinalLib = "com.github.spinalhdl" %% "spinalhdl-lib" % spinalVersion
 val spinalIdslPlugin = compilerPlugin("com.github.spinalhdl" %% "spinalhdl-idsl-plugin" % spinalVersion)

src/main/scala/mylib/MyTopLevelFormal.scala

@@ -0,0 +1,23 @@
+package mylib
+
+import spinal.core._
+import spinal.core.formal._
+
+//MyTopLevel's testbench
+object MyTopLevelFormal {
+  def main(args: Array[String]) {
+    FormalConfig.withBMC(10).doVerify(new Component {
+      val dut = FormalDut(new MyTopLevel)
+
+      // Ensure the formal test start with a reset
+      assumeInitial(clockDomain.isResetActive)
+
+      // Provide some stimulus
+      anyseq(dut.io.cond0)
+      anyseq(dut.io.cond1)
+
+      // Check the state initial value and increment
+      assert(dut.io.state === past(dut.io.state + U(dut.io.cond0)).init(0))
+    })
+  }
+}