diff options
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala | 4 | ||||
| -rw-r--r-- | src/test/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemanticsSpec.scala | 31 |
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") + } } |