From 2d197c841c5400c6deaa1592525be6a1d81dc1e2 Mon Sep 17 00:00:00 2001
From: Kevin Laeufer
Date: Tue, 21 Dec 2021 12:07:30 -0500
Subject: smt: deal correctly with negative SInt literals (#2447)

---
 .../smt/FirrtlExpressionSemanticsSpec.scala        | 31 ++++++++++++++++++++++
 1 file changed, 31 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 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")
+  }
 }
-- 
cgit v1.2.3