smt: deal correctly with negative SInt literals (#2447)

1 files changed, 31 insertions, 0 deletions

diff --git a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
index 7476b20c..52021625 100644
--- a/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
+++ b/src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala
@@ -278,4 +278,35 @@ class FirrtlExpressionSemanticsSpec extends AnyFlatSpec {
     assert(primop(false, "tail", 4, List(5), List(1)) == "i0[3:0]")
     assert(primop(false, "tail", 2, List(5), List(3)) == "i0[1:0]")
   }
+
+  private def literalSource(resTpe: String, lit: String) =
+    s"""circuit m:
+       |  module m:
+       |    output res: $resTpe
+       |    res <= $lit
+       |
+       |""".stripMargin
+  private def literalExpr(resTpe: String, lit: String) = {
+    val src = literalSource(resTpe, lit)
+    val sys = SMTBackendHelpers.toSys(src, modelUndef = true)
+    sys.signals.last.e.toString
+  }
+
+  private def uIntLit(lit: String) = literalExpr("UInt", lit)
+  it should "correctly translate unsigned integer literals" in {
+    assert(uIntLit("UInt(5)") == "3'b101")
+    assert(uIntLit("UInt<4>(5)") == "4'b101")
+    assert(uIntLit("UInt(0)") == "1'b0")
+  }
+
+  private def sIntLit(lit: String) = literalExpr("SInt", lit)
+  it should "correctly translate signed integer literals" in {
+    assert(sIntLit("SInt(5)") == "4'b101")
+    assert(sIntLit("SInt<4>(5)") == "4'b101")
+    assert(sIntLit("SInt(0)") == "1'b0")
+    assert(sIntLit("SInt(-1)") == "1'b1")
+    assert(sIntLit("SInt(-2)") == "2'b10")
+    assert(sIntLit("SInt(-5)") == "4'b1011")
+    assert(sIntLit("SInt<4>(-5)") == "4'b1011")
+  }
 }