diff options
| author | Kevin Laeufer | 2021-12-21 12:07:30 -0500 |
|---|---|---|
| committer | GitHub | 2021-12-21 09:07:30 -0800 |
| commit | 2d197c841c5400c6deaa1592525be6a1d81dc1e2 (patch) | |
| tree | 70c27ea58339cb1cfbc6abbe016295f869a9298b /src/main | |
| parent | c00a4ebb0608f9ef98729e9b610a2678be2bc4fd (diff) | |
smt: deal correctly with negative SInt literals (#2447)
Diffstat (limited to 'src/main')
| -rw-r--r-- | src/main/scala/firrtl/backends/experimental/smt/FirrtlExpressionSemantics.scala | 4 |
1 files changed, 3 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)) |