Merge pull request #1454 from Readon/fix_for_yosys0.41

Fix for yosys0.41
SpinalHDL · Jun 20, 2024 · d11eabf · d11eabf
2 parents 42b22b3 + 09bca4a
commit d11eabf
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 18 deletions.
diff --git a/tester/src/test/scala/spinal/core/BitVectorTests.scala b/tester/src/test/scala/spinal/core/BitVectorTests.scala
@@ -1,6 +1,6 @@
 package spinal.core
 
-import spinal.core.formal.{FormalConfig, SpinalFormalConfig}
+import spinal.core.formal.{FormalConfig, SpinalFormalConfig, FormalDut}
 import spinal.lib.formal.SpinalFormalFunSuite
 import spinal.tester.SpinalAnyFunSuite
 
@@ -30,41 +30,54 @@ class SubdivideInTestErrors extends SpinalAnyFunSuite {
 
 class SubdivideInTest extends SpinalFormalFunSuite {
   case class SliceDutBits(width: Int, sliceWidth: BitCount) extends Component {
-    val i = Bits(width bit)
-    val o = Bits(width bit)
+    val i = in Bits(width bit)
+    val o = out Bits(width bit)
     val split = i.subdivideIn(sliceWidth, strict = false)
 
     if (width % sliceWidth.value == 0)
       split.foreach(s => assert(s.getWidth == sliceWidth.value))
     else
       split.dropRight(1).foreach(s => assert(s.getWidth == sliceWidth.value))
-
-    o := Cat(split.asInstanceOf[Iterable[Data]])
-    assert(i === o)
+
+    o := Cat(split.asInstanceOf[Iterable[Data]])    
+    def formalAsserts() ={
+      i <> in(cloneOf(i))
+      assert(i === o)
+    }
   }
 
   case class SliceDutSlices(width: Int, slicesCount: SlicesCount) extends Component {
-    val i = Bits(width bit)
-    val o = Bits(width bit)
-    val split = i.subdivideIn(slicesCount, strict = false)
+    val i = in Bits(width bit)
+    val o = out Bits(width bit)
+    val split = i.subdivideIn(slicesCount, strict = false)    
     assert(split.size == slicesCount.value, s"split into ${split.size} slices, not ${slicesCount.value}")
 
     o := Cat(split.asInstanceOf[Iterable[Data]])
-    assert(i === o)
+    def formalAsserts() = {
+      i <> in(cloneOf(i))
+      assert(i === o)
+    }
   }
 
   test("mix of slicing operations") {
     SpinalFormalConfig(_keepDebugInfo = true)
       .withBMC(5)
       .withProve(5)
       .doVerify(new Component {
-        val dut_8_2bit = SliceDutBits(8, 2 bit) // default case
-        val dut_8_5bit = SliceDutBits(8, 5 bit) // uneven case, https://github.com/SpinalHDL/SpinalHDL/issues/1049
-        val dut_9_4bit = SliceDutBits(9, 4 bit) // odd width
-        val dut_2_3bit = SliceDutBits(2, 3 bit) // width smaller than sliceWidth
-        val dut_8_2slices = SliceDutSlices(8, 2 slices) // default case
-        val dut_8_3slices = SliceDutSlices(8, 3 slices) // uneven case
-        val dut_9_4slices = SliceDutSlices(9, 4 slices) // odd width
+        val dut_8_2bit = FormalDut(SliceDutBits(8, 2 bit)) // default case
+        dut_8_2bit.formalAsserts()
+        val dut_8_5bit = FormalDut(SliceDutBits(8, 5 bit)) // uneven case, https://github.com/SpinalHDL/SpinalHDL/issues/1049
+        dut_8_5bit.formalAsserts()
+        val dut_9_4bit = FormalDut(SliceDutBits(9, 4 bit)) // odd width
+        dut_9_4bit.formalAsserts()
+        val dut_2_3bit = FormalDut(SliceDutBits(2, 3 bit)) // width smaller than sliceWidth
+        dut_2_3bit.formalAsserts()
+        val dut_8_2slices = FormalDut(SliceDutSlices(8, 2 slices)) // default case
+        dut_8_2slices.formalAsserts()
+        val dut_8_3slices = FormalDut(SliceDutSlices(8, 3 slices)) // uneven case
+        dut_8_3slices.formalAsserts()
+        val dut_9_4slices = FormalDut(SliceDutSlices(9, 4 slices)) // odd width
+        dut_9_4slices.formalAsserts()
       }.setDefinitionName("BitVectorTests_SubdivideInTest"))
   }
 }
diff --git a/tester/src/test/scala/spinal/lib/UtilsChecker.scala b/tester/src/test/scala/spinal/lib/UtilsChecker.scala
@@ -5,6 +5,17 @@ import spinal.core.formal._
 // import spinal.lib.{StreamFifo, History, OHToUInt}
 import spinal.lib.formal._
 
+case class PriorityMuxFixture(width: Int, msbFirst: Boolean) extends Component{
+  val inputWidth = log2Up(width)
+  val io = new Bundle {
+    val sel = in Bits(width bits)
+    val inputs = in Vec(Bits(inputWidth bits), width)
+    val output = out(Bits(inputWidth bits))
+  }
+  val output = PriorityMux(io.sel, io.inputs, msbFirst)
+  io.output <> output
+}
+
 class PriorityMuxChecker extends SpinalFormalFunSuite {
   def testMain(width: Int, msbFirst: Boolean){
     FormalConfig
@@ -14,7 +25,12 @@ class PriorityMuxChecker extends SpinalFormalFunSuite {
         val sel = in Bits(width bits)
         val inputWidth = log2Up(width)
         val inputs = in Vec(Bits(inputWidth bits), width)
-        val output = out(PriorityMux(sel, inputs, msbFirst))
+        val output = out(Bits(inputWidth bits))
+
+        val dut = FormalDut(PriorityMuxFixture(width, msbFirst))
+        sel <> dut.io.sel
+        inputs <> dut.io.inputs
+        output <> dut.io.output
 
         for(id <- 0 until inputs.size){
           assume(inputs(id) === id)