2 files changed, 34 insertions, 1 deletions
diff --git a/src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala b/src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala
index 6f454a22..865382c9 100644
--- a/src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala
+++ b/src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala
@@ -13,7 +13,9 @@ private object FirrtlExpressionSemantics {
       case ir.DoPrim(op, args, consts, _) => onPrim(op, args, consts)
       case r: ir.RefLikeExpression => BVSymbol(r.serialize, getWidth(r))
       case ir.UIntLiteral(value, ir.IntWidth(width)) => BVLiteral(value, width.toInt)
-      case ir.SIntLiteral(value, ir.IntWidth(width)) => BVLiteral(value, width.toInt)
+      case ir.SIntLiteral(value, ir.IntWidth(width)) =>
+        val twosComplementValue = value & ((BigInt(1) << width.toInt) - 1)
+        BVLiteral(twosComplementValue, width.toInt)
       case ir.Mux(cond, tval, fval, _) =>
         val width = List(tval, fval).map(getWidth).max
         BVIte(toSMT(cond), toSMT(tval, width), toSMT(fval, width))
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")
+  }
 }