From 4a441dd47abfd72bc522ce37aafcf6220794db0c Mon Sep 17 00:00:00 2001 From: Jan Schiefer Date: Mon, 19 Feb 2024 01:42:59 +0100 Subject: [PATCH 1/2] Use multiclock mode in formal verification --- hw/spinal/projectname/MyTopLevelFormal.scala | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hw/spinal/projectname/MyTopLevelFormal.scala b/hw/spinal/projectname/MyTopLevelFormal.scala index 608bf8a..11c69f9 100644 --- a/hw/spinal/projectname/MyTopLevelFormal.scala +++ b/hw/spinal/projectname/MyTopLevelFormal.scala @@ -6,7 +6,7 @@ import spinal.core.formal._ // You need SymbiYosys to be installed. // See https://spinalhdl.github.io/SpinalDoc-RTD/master/SpinalHDL/Formal%20verification/index.html#installing-requirements object MyTopLevelFormal extends App { - FormalConfig + SpinalFormalConfig( _hasAsync = true ) .withBMC(10) .doVerify(new Component { val dut = FormalDut(MyTopLevel()) From 10dcbf0cf22c35239d9b3d6e0cb54efc290d2868 Mon Sep 17 00:00:00 2001 From: Jan Schiefer Date: Mon, 19 Feb 2024 03:42:39 +0100 Subject: [PATCH 2/2] Sync reset fixes --- build.sbt | 2 +- hw/spinal/projectname/Config.scala | 3 ++- hw/spinal/projectname/MyTopLevelFormal.scala | 3 ++- project/build.properties | 2 +- 4 files changed, 6 insertions(+), 4 deletions(-) diff --git a/build.sbt b/build.sbt index bee8024..1854991 100644 --- a/build.sbt +++ b/build.sbt @@ -2,7 +2,7 @@ ThisBuild / version := "1.0" ThisBuild / scalaVersion := "2.12.18" ThisBuild / organization := "org.example" -val spinalVersion = "1.10.1" +val spinalVersion = "dev" 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) diff --git a/hw/spinal/projectname/Config.scala b/hw/spinal/projectname/Config.scala index f3a2e3e..6115d71 100644 --- a/hw/spinal/projectname/Config.scala +++ b/hw/spinal/projectname/Config.scala @@ -7,7 +7,8 @@ object Config { def spinal = SpinalConfig( targetDirectory = "hw/gen", defaultConfigForClockDomains = ClockDomainConfig( - resetActiveLevel = HIGH + resetActiveLevel = HIGH, + resetKind = SYNC ), onlyStdLogicVectorAtTopLevelIo = true ) diff --git a/hw/spinal/projectname/MyTopLevelFormal.scala b/hw/spinal/projectname/MyTopLevelFormal.scala index 11c69f9..2704aef 100644 --- a/hw/spinal/projectname/MyTopLevelFormal.scala +++ b/hw/spinal/projectname/MyTopLevelFormal.scala @@ -6,7 +6,8 @@ import spinal.core.formal._ // You need SymbiYosys to be installed. // See https://spinalhdl.github.io/SpinalDoc-RTD/master/SpinalHDL/Formal%20verification/index.html#installing-requirements object MyTopLevelFormal extends App { - SpinalFormalConfig( _hasAsync = true ) + FormalConfig + .withConfig( Config.spinal ) .withBMC(10) .doVerify(new Component { val dut = FormalDut(MyTopLevel()) diff --git a/project/build.properties b/project/build.properties index 1e70b0c..abbbce5 100644 --- a/project/build.properties +++ b/project/build.properties @@ -1 +1 @@ -sbt.version=1.6.0 +sbt.version=1.9.8