From 18b9a987552492928aa1199d8cf498fe561c2f03 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Wed, 10 Nov 2021 06:33:39 -0800
Subject: smt: fix handling of div primitive in formal backend (#2409)

We never tested the case where the width of the
numerator was less than the denominator.
This should fix any issue with this combination.---
 .../backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala       | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/test')

diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
index c9c1c943..7476b20c 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
@@ -113,6 +113,8 @@ class FirrtlExpressionSemanticsSpec extends AnyFlatSpec {
     assert(primop(false, "div", 8, List(8, 4), modelUndef = false) == "udiv(i0, zext(i1, 4))")
     assert(primop(true, "div", 8, List(7, 7), modelUndef = false) == "sdiv(sext(i0, 1), sext(i1, 1))")
     assert(primop(true, "div", 8, List(7, 4), modelUndef = false) == "sdiv(sext(i0, 1), sext(i1, 4))")
+    // result width is always the width of the numerator, even if the denominator is larger
+    assert(primop(false, "div", 1, List(1, 2), modelUndef = false) == "udiv(zext(i0, 1), i1)[0]")
   }
 
   it should "correctly translate the `rem` primitive operation" in {
-- 
cgit v1.2.3