Upstream intervals (#870)

Major features:

- Added Interval type, as well as PrimOps asInterval, clip, wrap, and sqz.
- Changed PrimOp names: bpset -> setp, bpshl -> incp, bpshr -> decp
- Refactored width/bound inferencer into a separate constraint solver
- Added transforms to infer, trim, and remove interval bounds
- Tests for said features

Plan to be released with 1.3

1 files changed, 135 insertions, 351 deletions

diff --git a/src/main/scala/firrtl/passes/InferWidths.scala b/src/main/scala/firrtl/passes/InferWidths.scala
index 9c58da2c..2211d238 100644
--- a/src/main/scala/firrtl/passes/InferWidths.scala
+++ b/src/main/scala/firrtl/passes/InferWidths.scala
@@ -3,15 +3,20 @@
 package firrtl.passes
 
 // Datastructures
-import scala.collection.mutable.ArrayBuffer
-import scala.collection.immutable.ListMap
-
 import firrtl._
 import firrtl.annotations.{Annotation, ReferenceTarget}
 import firrtl.ir._
 import firrtl.Utils._
 import firrtl.Mappers._
-import firrtl.traversals.Foreachers._
+import firrtl.Implicits.width2constraint
+import firrtl.annotations.{CircuitTarget, ModuleTarget, ReferenceTarget, Target}
+import firrtl.constraint.{ConstraintSolver, IsMax}
+
+object InferWidths {
+  def apply(): InferWidths = new InferWidths()
+  def run(c: Circuit): Circuit = new InferWidths().run(c)
+  def execute(state: CircuitState): CircuitState = new InferWidths().execute(state)
+}
 
 case class WidthGeqConstraintAnnotation(loc: ReferenceTarget, exp: ReferenceTarget) extends Annotation {
   def update(renameMap: RenameMap): Seq[WidthGeqConstraintAnnotation] = {
@@ -33,369 +38,146 @@ case class WidthGeqConstraintAnnotation(loc: ReferenceTarget, exp: ReferenceTarg
   }
 }
 
+/** Infers the widths of all signals with unknown widths
+  *
+  * Is a global width inference algorithm
+  * - Instances of the same module with unknown input port widths will be assigned the
+  *   largest width of all assignments to each of its instance ports
+  * - If you don't want the global inference behavior, then be sure to define all your input widths
+  *
+  * Infers the smallest width is larger than all assigned widths to a signal
+  * - Note that this means that dummy assignments that are overwritten by last-connect-semantics
+  *   can still influence width inference
+  * - E.g.
+  *   wire x: UInt
+  *   x <= UInt<5>(15)
+  *   x <= UInt<1>(1)
+  *
+  *   Since width inference occurs before lowering, it infers x's width to be 5 but with an assignment of UInt(1):
+  *
+  *   wire x: UInt<5>
+  *   x <= UInt<1>(1)
+  *
+  * Uses firrtl.constraint package to infer widths
+  */
 class InferWidths extends Transform with ResolvedAnnotationPaths {
   def inputForm: CircuitForm = UnknownForm
   def outputForm: CircuitForm = UnknownForm
 
-  val annotationClasses = Seq(classOf[WidthGeqConstraintAnnotation])
+  private val constraintSolver = new ConstraintSolver()
 
-  type ConstraintMap = collection.mutable.LinkedHashMap[String, Width]
-
-  def solve_constraints(l: Seq[WGeq]): ConstraintMap = {
-    def unique(ls: Seq[Width]) : Seq[Width] =
-      (ls map (new WrappedWidth(_))).distinct map (_.w)
-    // Combines constraints on the same VarWidth into the same constraint
-    def make_unique(ls: Seq[WGeq]): ListMap[String,Width] = {
-      ls.foldLeft(ListMap.empty[String, Width])((acc, wgeq) => wgeq.loc match {
-        case VarWidth(name) => acc.get(name) match {
-          case None => acc + (name -> wgeq.exp)
-          // Avoid constructing massive MaxWidth chains
-          case Some(MaxWidth(args)) => acc + (name -> MaxWidth(wgeq.exp +: args))
-          case Some(width) => acc + (name -> MaxWidth(Seq(wgeq.exp, width)))
-        }
-        case _ => acc
-      })
-    }
-    def pullMinMax(w: Width): Width = w map pullMinMax match {
-      case PlusWidth(MaxWidth(maxs), IntWidth(i)) => MaxWidth(maxs.map(m => PlusWidth(m, IntWidth(i))))
-      case PlusWidth(IntWidth(i), MaxWidth(maxs)) => MaxWidth(maxs.map(m => PlusWidth(m, IntWidth(i))))
-      case MinusWidth(MaxWidth(maxs), IntWidth(i)) => MaxWidth(maxs.map(m => MinusWidth(m, IntWidth(i))))
-      case MinusWidth(IntWidth(i), MaxWidth(maxs)) => MaxWidth(maxs.map(m => MinusWidth(IntWidth(i), m)))
-      case PlusWidth(MinWidth(mins), IntWidth(i)) => MinWidth(mins.map(m => PlusWidth(m, IntWidth(i))))
-      case PlusWidth(IntWidth(i), MinWidth(mins)) => MinWidth(mins.map(m => PlusWidth(m, IntWidth(i))))
-      case MinusWidth(MinWidth(mins), IntWidth(i)) => MinWidth(mins.map(m => MinusWidth(m, IntWidth(i))))
-      case MinusWidth(IntWidth(i), MinWidth(mins)) => MinWidth(mins.map(m => MinusWidth(IntWidth(i), m)))
-      case wx => wx
-    }
-    def collectMinMax(w: Width): Width = w map collectMinMax match {
-      case MinWidth(args) => MinWidth(unique(args.foldLeft(List[Width]()) {
-        case (res, wxx: MinWidth) => wxx.args ++: res
-        case (res, wxx) => wxx +: res
-      }))
-      case MaxWidth(args) => MaxWidth(unique(args.foldLeft(List[Width]()) {
-        case (res, wxx: MaxWidth) => wxx.args ++: res
-        case (res, wxx) => wxx +: res
-      }))
-      case wx => wx
-    }
-    def mergePlusMinus(w: Width): Width = w map mergePlusMinus match {
-      case wx: PlusWidth => (wx.arg1, wx.arg2) match {
-        case (w1: IntWidth, w2: IntWidth) => IntWidth(w1.width + w2.width)
-        case (PlusWidth(IntWidth(x), w1), IntWidth(y)) =>  PlusWidth(IntWidth(x + y), w1)
-        case (PlusWidth(w1, IntWidth(x)), IntWidth(y)) =>  PlusWidth(IntWidth(x + y), w1)
-        case (IntWidth(y), PlusWidth(w1, IntWidth(x))) =>  PlusWidth(IntWidth(x + y), w1)
-        case (IntWidth(y), PlusWidth(IntWidth(x), w1)) =>  PlusWidth(IntWidth(x + y), w1)
-        case (MinusWidth(w1, IntWidth(x)), IntWidth(y)) => PlusWidth(IntWidth(y - x), w1)
-        case (IntWidth(y), MinusWidth(w1, IntWidth(x))) => PlusWidth(IntWidth(y - x), w1)
-        case _ => wx
-      }
-      case wx: MinusWidth => (wx.arg1, wx.arg2) match {
-        case (w1: IntWidth, w2: IntWidth) => IntWidth(w1.width - w2.width)
-        case (PlusWidth(IntWidth(x), w1), IntWidth(y)) =>  PlusWidth(IntWidth(x - y), w1)
-        case (PlusWidth(w1, IntWidth(x)), IntWidth(y)) =>  PlusWidth(IntWidth(x - y), w1)
-        case (MinusWidth(w1, IntWidth(x)), IntWidth(y)) => PlusWidth(IntWidth(x - y), w1)
-        case _ => wx
-      }
-      case wx: ExpWidth => wx.arg1 match {
-        case w1: IntWidth => IntWidth(BigInt((math.pow(2, w1.width.toDouble) - 1).toLong))
-        case _ => wx
-      }
-      case wx => wx
-    }
-    def removeZeros(w: Width): Width = w map removeZeros match {
-      case wx: PlusWidth => (wx.arg1, wx.arg2) match {
-        case (w1, IntWidth(x)) if x == 0 => w1
-        case (IntWidth(x), w1) if x == 0 => w1
-        case _ => wx
-      }
-      case wx: MinusWidth => (wx.arg1, wx.arg2) match {
-        case (w1: IntWidth, w2: IntWidth) => IntWidth(w1.width - w2.width)
-        case (w1, IntWidth(x)) if x == 0 => w1
-        case _ => wx
-      }
-      case wx => wx
-    }
-    def simplify(w: Width): Width = {
-      val opts = Seq(
-        pullMinMax _,
-        collectMinMax _,
-        mergePlusMinus _,
-        removeZeros _
-      )
-      opts.foldLeft(w) { (width, opt) => opt(width) }
-    }
-
-    def substitute(h: ConstraintMap)(w: Width): Width = {
-      //;println-all-debug(["Substituting for [" w "]"])
-      val wx = simplify(w)
-      //;println-all-debug(["After Simplify: [" wx "]"])
-      wx map substitute(h) match {
-        //;("matched  println-debugvarwidth!")
-        case wxx: VarWidth => h get wxx.name match {
-          case None => wxx
-          case Some(p) =>
-            //;println-debug("Contained!")
-            //;println-all-debug(["Width: " wxx])
-            //;println-all-debug(["Accessed: " h[name(wxx)]])
-            val t = simplify(substitute(h)(p))
-            h(wxx.name) = t
-            t
-        }
-        case wxx => wxx
-        //;println-all-debug(["not varwidth!" w])
-      }
-    }
-
-    def b_sub(h: ConstraintMap)(w: Width): Width = {
-      w map b_sub(h) match {
-        case wx: VarWidth => h getOrElse (wx.name, wx)
-        case wx => wx
-      }
-    }
-
-    def remove_cycle(n: String)(w: Width): Width = {
-      //;println-all-debug(["Removing cycle for " n " inside " w])
-      w match {
-        case wx: MaxWidth => MaxWidth(wx.args filter {
-          case wxx: VarWidth => !(n equals wxx.name)
-          case MinusWidth(VarWidth(name), IntWidth(i)) if ((i >= 0) && (n == name)) => false
-          case _ => true
-        })
-        case wx: MinusWidth => wx.arg1 match {
-          case v: VarWidth if n == v.name => v
-          case v => wx
-        }
-        case wx => wx
-      }
-      //;println-all-debug(["After removing cycle for " n ", returning " wx])
-    }
+  val annotationClasses = Seq(classOf[WidthGeqConstraintAnnotation])
 
-    def hasVarWidth(n: String)(w: Width): Boolean = {
-      var has = false
-      def rec(w: Width): Width = {
-        w match {
-          case wx: VarWidth if wx.name == n => has = true
-          case _ =>
+  private def addTypeConstraints(r1: ReferenceTarget, r2: ReferenceTarget)(t1: Type, t2: Type): Unit = (t1,t2) match {
+    case (UIntType(w1), UIntType(w2)) => constraintSolver.addGeq(w1, w2, r1.prettyPrint(""), r2.prettyPrint(""))
+    case (SIntType(w1), SIntType(w2)) => constraintSolver.addGeq(w1, w2, r1.prettyPrint(""), r2.prettyPrint(""))
+    case (ClockType, ClockType) =>
+    case (FixedType(w1, p1), FixedType(w2, p2)) =>
+      constraintSolver.addGeq(p1, p2, r1.prettyPrint(""), r2.prettyPrint(""))
+      constraintSolver.addGeq(w1, w2, r1.prettyPrint(""), r2.prettyPrint(""))
+    case (IntervalType(l1, u1, p1), IntervalType(l2, u2, p2)) =>
+      constraintSolver.addGeq(p1, p2, r1.prettyPrint(""), r2.prettyPrint(""))
+      constraintSolver.addLeq(l1, l2, r1.prettyPrint(""), r2.prettyPrint(""))
+      constraintSolver.addGeq(u1, u2, r1.prettyPrint(""), r2.prettyPrint(""))
+    case (AnalogType(w1), AnalogType(w2)) =>
+      constraintSolver.addGeq(w1, w2, r1.prettyPrint(""), r2.prettyPrint(""))
+      constraintSolver.addGeq(w2, w1, r1.prettyPrint(""), r2.prettyPrint(""))
+    case (t1: BundleType, t2: BundleType) =>
+      (t1.fields zip t2.fields) foreach { case (f1, f2) =>
+        (f1.flip, f2.flip) match {
+          case (Default, Default) => addTypeConstraints(r1.field(f1.name), r2.field(f2.name))(f1.tpe, f2.tpe)
+          case (Flip, Flip) => addTypeConstraints(r2.field(f2.name), r1.field(f1.name))(f2.tpe, f1.tpe)
+          case _ => sys.error("Shouldn't be here")
         }
-        w map rec
-      }
-      rec(w)
-      has
-    }
-
-    //; Forward solve
-    //; Returns a solved list where each constraint undergoes:
-    //;  1) Continuous Solving (using triangular solving)
-    //;  2) Remove Cycles
-    //;  3) Move to solved if not self-recursive
-    val u = make_unique(l)
-
-    //println("======== UNIQUE CONSTRAINTS ========")
-    //for (x <- u) { println(x) }
-    //println("====================================")
-
-    val f = new ConstraintMap
-    val o = ArrayBuffer[String]()
-    for ((n, e) <- u) {
-      //println("==== SOLUTIONS TABLE ====")
-      //for (x <- f) println(x)
-      //println("=========================")
-
-      val e_sub = simplify(substitute(f)(e))
-
-      //println("Solving " + n + " => " + e)
-      //println("After Substitute: " + n + " => " + e_sub)
-      //println("==== SOLUTIONS TABLE (Post Substitute) ====")
-      //for (x <- f) println(x)
-      //println("=========================")
-
-      val ex = remove_cycle(n)(e_sub)
-
-      //println("After Remove Cycle: " + n + " => " + ex)
-      if (!hasVarWidth(n)(ex)) {
-        //println("Not rec!: " + n + " => " + ex)
-        //println("Adding [" + n + "=>" + ex + "] to Solutions Table")
-        f(n) = ex
-        o += n
       }
-    }
-
-    //println("Forward Solved Constraints")
-    //for (x <- f) println(x)
-
-    //; Backwards Solve
-    val b = new ConstraintMap
-    for (i <- (o.size - 1) to 0 by -1) {
-      val n = o(i) // Should visit `o` backward
-      /*
-      println("SOLVE BACK: [" + n + " => " + f(n) + "]")
-      println("==== SOLUTIONS TABLE ====")
-      for (x <- b) println(x)
-      println("=========================")
-      */
-      val ex = simplify(b_sub(b)(f(n)))
-      /*
-      println("BACK RETURN: [" + n + " => " + ex + "]")
-      */
-      b(n) = ex
-      /*
-      println("==== SOLUTIONS TABLE (Post backsolve) ====")
-      for (x <- b) println(x)
-      println("=========================")
-      */
-    }
-    b
-  }
-
-  def get_constraints_t(t1: Type, t2: Type): Seq[WGeq] = (t1,t2) match {
-    case (t1: UIntType, t2: UIntType) => Seq(WGeq(t1.width, t2.width))
-    case (t1: SIntType, t2: SIntType) => Seq(WGeq(t1.width, t2.width))
-    case (ClockType, ClockType) => Nil
+    case (t1: VectorType, t2: VectorType) => addTypeConstraints(r1.index(0), r2.index(0))(t1.tpe, t2.tpe)
     case (AsyncResetType, AsyncResetType) => Nil
-    case (FixedType(w1, p1), FixedType(w2, p2)) => Seq(WGeq(w1,w2), WGeq(p1,p2))
-    case (AnalogType(w1), AnalogType(w2)) => Seq(WGeq(w1,w2), WGeq(w2,w1))
-    case (t1: BundleType, t2: BundleType) =>
-      (t1.fields zip t2.fields foldLeft Seq[WGeq]()){case (res, (f1, f2)) =>
-        res ++ (f1.flip match {
-          case Default => get_constraints_t(f1.tpe, f2.tpe)
-          case Flip => get_constraints_t(f2.tpe, f1.tpe)
-        })
-      }
-    case (t1: VectorType, t2: VectorType) => get_constraints_t(t1.tpe, t2.tpe)
     case (ResetType, _) => Nil
     case (_, ResetType) => Nil
   }
 
-  def run(c: Circuit, extra: Seq[WGeq]): Circuit = {
-    val v = ArrayBuffer[WGeq]() ++ extra
+  private def addExpConstraints(e: Expression): Expression = e map addExpConstraints match {
+    case m@Mux(p, tVal, fVal, t) =>
+      constraintSolver.addGeq(getWidth(p), Closed(1), "mux predicate", "1.W")
+      m
+    case other => other
+  }
 
-    def get_constraints_e(e: Expression): Unit = {
-      e match {
-        case (e: Mux) => v ++= Seq(
-          WGeq(getWidth(e.cond), IntWidth(1)),
-          WGeq(IntWidth(1), getWidth(e.cond))
-        )
-        case _ =>
+  private def addStmtConstraints(mt: ModuleTarget)(s: Statement): Statement = s map addExpConstraints match {
+    case c: Connect =>
+      val n = get_size(c.loc.tpe)
+      val locs = create_exps(c.loc)
+      val exps = create_exps(c.expr)
+      (locs zip exps).foreach { case (loc, exp) =>
+        to_flip(flow(loc)) match {
+          case Default => addTypeConstraints(Target.asTarget(mt)(loc), Target.asTarget(mt)(exp))(loc.tpe, exp.tpe)
+          case Flip => addTypeConstraints(Target.asTarget(mt)(exp), Target.asTarget(mt)(loc))(exp.tpe, loc.tpe)
+        }
       }
-      e.foreach(get_constraints_e)
-    }
-
-    def get_constraints_declared_type (t: Type): Type = t match {
-      case FixedType(_, p) =>
-        v += WGeq(p,IntWidth(0))
-        t
-      case _ => t map get_constraints_declared_type
-    }
-
-    def get_constraints_s(s: Statement): Unit = {
-      s map get_constraints_declared_type match {
-        case (s: Connect) =>
-          val locs = create_exps(s.loc)
-          val exps = create_exps(s.expr)
-          v ++= locs.zip(exps).flatMap { case (locx, expx) =>
-            to_flip(flow(locx)) match {
-              case Default => get_constraints_t(locx.tpe, expx.tpe)//WGeq(getWidth(locx), getWidth(expx))
-              case Flip => get_constraints_t(expx.tpe, locx.tpe)//WGeq(getWidth(expx), getWidth(locx))
-            }
-          }
-        case (s: PartialConnect) =>
-          val ls = get_valid_points(s.loc.tpe, s.expr.tpe, Default, Default)
-          val locs = create_exps(s.loc)
-          val exps = create_exps(s.expr)
-          v ++= (ls flatMap {case (x, y) =>
-            val locx = locs(x)
-            val expx = exps(y)
-            to_flip(flow(locx)) match {
-              case Default => get_constraints_t(locx.tpe, expx.tpe)//WGeq(getWidth(locx), getWidth(expx))
-              case Flip => get_constraints_t(expx.tpe, locx.tpe)//WGeq(getWidth(expx), getWidth(locx))
-            }
-          })
-        case (s: DefRegister) =>
-          if (s.reset.tpe != AsyncResetType ) {
-            v ++= (
-               get_constraints_t(s.reset.tpe, UIntType(IntWidth(1))) ++
-               get_constraints_t(UIntType(IntWidth(1)), s.reset.tpe))
-           }
-          v ++= get_constraints_t(s.tpe, s.init.tpe)
-        case (s:Conditionally) => v ++=
-           get_constraints_t(s.pred.tpe, UIntType(IntWidth(1))) ++
-           get_constraints_t(UIntType(IntWidth(1)), s.pred.tpe)
-        case Attach(_, exprs) =>
-          // All widths must be equal
-          val widths = exprs map (e => getWidth(e.tpe))
-          v ++= widths.tail map (WGeq(widths.head, _))
-        case _ =>
+      c
+    case pc: PartialConnect =>
+      val ls = get_valid_points(pc.loc.tpe, pc.expr.tpe, Default, Default)
+      val locs = create_exps(pc.loc)
+      val exps = create_exps(pc.expr)
+      ls foreach { case (x, y) =>
+        val loc = locs(x)
+        val exp = exps(y)
+        to_flip(flow(loc)) match {
+          case Default => addTypeConstraints(Target.asTarget(mt)(loc), Target.asTarget(mt)(exp))(loc.tpe, exp.tpe)
+          case Flip => addTypeConstraints(Target.asTarget(mt)(exp), Target.asTarget(mt)(loc))(exp.tpe, loc.tpe)
+        }
       }
-      s.foreach(get_constraints_e)
-      s.foreach(get_constraints_s)
-    }
-
-    c.modules.foreach(_.foreach(get_constraints_s))
-    c.modules.foreach(_.ports.foreach({p => get_constraints_declared_type(p.tpe)}))
-
-    //println("======== ALL CONSTRAINTS ========")
-    //for(x <- v) println(x)
-    //println("=================================")
-    val h = solve_constraints(v)
-    //println("======== SOLVED CONSTRAINTS ========")
-    //for(x <- h) println(x)
-    //println("====================================")
-
-    def evaluate(w: Width): Width = {
-      def map2(a: Option[BigInt], b: Option[BigInt], f: (BigInt,BigInt) => BigInt): Option[BigInt] =
-         for (a_num <- a; b_num <- b) yield f(a_num, b_num)
-      def reduceOptions(l: Seq[Option[BigInt]], f: (BigInt,BigInt) => BigInt): Option[BigInt] =
-         l.reduce(map2(_, _, f))
+      pc
+    case r: DefRegister =>
+      if (r.reset.tpe != AsyncResetType ) {
+        addTypeConstraints(Target.asTarget(mt)(r.reset), mt.ref("1"))(r.reset.tpe, UIntType(IntWidth(1)))
+      }
+      addTypeConstraints(mt.ref(r.name), Target.asTarget(mt)(r.init))(r.tpe, r.init.tpe)
+      r
+    case a@Attach(_, exprs) =>
+      val widths = exprs map (e => (e, getWidth(e.tpe)))
+      val maxWidth = IsMax(widths.map(x => width2constraint(x._2)))
+      widths.foreach { case (e, w) =>
+        constraintSolver.addGeq(w, CalcWidth(maxWidth), Target.asTarget(mt)(e).prettyPrint(""), mt.ref(a.serialize).prettyPrint(""))
+      }
+      a
+    case c: Conditionally =>
+       addTypeConstraints(Target.asTarget(mt)(c.pred), mt.ref("1.W"))(c.pred.tpe, UIntType(IntWidth(1)))
+       c map addStmtConstraints(mt)
+    case x => x map addStmtConstraints(mt)
+  }
+  private def fixWidth(w: Width): Width = constraintSolver.get(w) match {
+    case Some(Closed(x)) if trim(x).isWhole => IntWidth(x.toBigInt)
+    case None => w
+    case _ => sys.error("Shouldn't be here")
+  }
+  private def fixType(t: Type): Type = t map fixType map fixWidth match {
+    case IntervalType(l, u, p) => 
+      val (lx, ux) = (constraintSolver.get(l), constraintSolver.get(u)) match {
+        case (Some(x: Bound), Some(y: Bound)) => (x, y)
+        case (None, None) => (l, u)
+        case x => sys.error(s"Shouldn't be here: $x")
 
-      // This function shouldn't be necessary
-      // Added as protection in case a constraint accidentally uses MinWidth/MaxWidth
-      // without any actual Widths. This should be elevated to an earlier error
-      def forceNonEmpty(in: Seq[Option[BigInt]], default: Option[BigInt]): Seq[Option[BigInt]] =
-        if (in.isEmpty) Seq(default)
-        else in
 
-      def solve(w: Width): Option[BigInt] = w match {
-        case wx: VarWidth =>
-          for{
-            v <- h.get(wx.name) if !v.isInstanceOf[VarWidth]
-            result <- solve(v)
-          } yield result
-        case wx: MaxWidth => reduceOptions(forceNonEmpty(wx.args.map(solve), Some(BigInt(0))), max)
-        case wx: MinWidth => reduceOptions(forceNonEmpty(wx.args.map(solve), None), min)
-        case wx: PlusWidth => map2(solve(wx.arg1), solve(wx.arg2), {_ + _})
-        case wx: MinusWidth => map2(solve(wx.arg1), solve(wx.arg2), {_ - _})
-        case wx: ExpWidth => map2(Some(BigInt(2)), solve(wx.arg1), pow_minus_one)
-        case wx: IntWidth => Some(wx.width)
-        case wx => throwInternalError(s"solve: shouldn't be here - %$wx")
       }
+      IntervalType(lx, ux, fixWidth(p))
+    case FixedType(w, p) => FixedType(w, fixWidth(p))
+    case x => x
+  }
+  private def fixStmt(s: Statement): Statement = s map fixStmt map fixType
+  private def fixPort(p: Port): Port = {
+    Port(p.info, p.name, p.direction, fixType(p.tpe))
+  }
 
-      solve(w) match {
-        case None => w
-        case Some(s) => IntWidth(s)
-      }
-    }
-
-    def reduce_var_widths_w(w: Width): Width = {
-      //println-all-debug(["REPLACE: " w])
-      evaluate(w)
-      //println-all-debug(["WITH: " wx])
-    }
-
-    def reduce_var_widths_t(t: Type): Type = {
-      t map reduce_var_widths_t map reduce_var_widths_w
-    }
-
-    def reduce_var_widths_s(s: Statement): Statement = {
-      s map reduce_var_widths_s map reduce_var_widths_t
-    }
-
-    def reduce_var_widths_p(p: Port): Port = {
-      Port(p.info, p.name, p.direction, reduce_var_widths_t(p.tpe))
-    }
-
-    InferTypes.run(c.copy(modules = c.modules map (_
-      map reduce_var_widths_p
-      map reduce_var_widths_s)))
+  def run (c: Circuit): Circuit = {
+    val ct = CircuitTarget(c.main)
+    c.modules foreach ( m => m map addStmtConstraints(ct.module(m.name)))
+    constraintSolver.solve()
+    val ret = InferTypes.run(c.copy(modules = c.modules map (_
+      map fixPort
+      map fixStmt)))
+    constraintSolver.clear()
+    ret
   }
 
   def execute(state: CircuitState): CircuitState = {
@@ -426,7 +208,7 @@ class InferWidths extends Transform with ResolvedAnnotationPaths {
       }
     }
 
-    val extraConstraints = state.annotations.flatMap {
+    state.annotations.foreach {
       case anno: WidthGeqConstraintAnnotation if anno.loc.isLocal && anno.exp.isLocal  =>
         val locType :: expType :: Nil = Seq(anno.loc, anno.exp) map { target =>
           val baseType = typeMap.getOrElse(target.copy(component = Seq.empty),
@@ -440,10 +222,12 @@ class InferWidths extends Transform with ResolvedAnnotationPaths {
           leafType
         }
 
-        get_constraints_t(locType, expType)
-      case other => Seq.empty
+        //get_constraints_t(locType, expType)
+        addTypeConstraints(anno.loc, anno.exp)(locType, expType)
+      case other =>
     }
 
-    state.copy(circuit = run(state.circuit, extraConstraints))
+    state.copy(circuit = run(state.circuit))
   }
+
 }