Merge pull request #1422 from freechipsproject/revert-inline-nots-only

Revert inline nots

6 files changed, 10 insertions, 209 deletions

diff --git a/.travis.yml b/.travis.yml
index 2065cb56..9e552319 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -77,11 +77,12 @@ jobs:
         - "travis_wait 30 sleep 1800 &"
         - ./.run_formal_checks.sh ICache
     - stage: test
-      name: "Formal equivalence: Ops"
+      name: "Formal equivalence: small expression-tree stress tests"
       script:
         - yosys -V
         - "travis_wait 30 sleep 1800 &"
         - ./.run_formal_checks.sh Ops
+        - ./.run_formal_checks.sh AddNot
     - stage: test
       script:
         - benchmark/scripts/benchmark_cold_compile.py -N 2 --designs regress/ICache.fir --versions HEAD
diff --git a/regress/AddNot.fir b/regress/AddNot.fir
new file mode 100644
index 00000000..38c72a16
--- /dev/null
+++ b/regress/AddNot.fir
@@ -0,0 +1,6 @@
+circuit AddNot:
+  module AddNot:
+    input a: UInt<8>
+    input b: UInt<8>
+    output o: UInt<9>
+    o <= add(a, not(b))
diff --git a/src/main/scala/firrtl/Emitter.scala b/src/main/scala/firrtl/Emitter.scala
index 7ee652af..12ef17c2 100644
--- a/src/main/scala/firrtl/Emitter.scala
+++ b/src/main/scala/firrtl/Emitter.scala
@@ -237,10 +237,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
         if (e.tpe == AsyncResetType) {
           throw EmitterException("Cannot emit async reset muxes directly")
         }
-        e.cond match {
-          case DoPrim(Not, Seq(sel), _,_) => emit(Seq(sel," ? ",cast(e.fval)," : ",cast(e.tval)),top + 1)
-          case _ => emit(Seq(e.cond," ? ",cast(e.tval)," : ",cast(e.fval)),top + 1)
-        }
+        emit(Seq(e.cond," ? ",cast(e.tval)," : ",cast(e.fval)),top + 1)
       }
       case (e: ValidIf) => emit(Seq(cast(e.value)),top + 1)
       case (e: WRef) => w write e.serialize
@@ -980,8 +977,7 @@ class VerilogEmitter extends SeqTransform with Emitter {
     new BlackBoxSourceHelper,
     new FixAddingNegativeLiterals,
     new ReplaceTruncatingArithmetic,
-    new InlineNotsTransform,
-    new InlineBitExtractionsTransform,  // here after InlineNots to clean up not(not(...)) rename
+    new InlineBitExtractionsTransform,
     new InlineCastsTransform,
     new LegalizeClocksTransform,
     new FlattenRegUpdate,
diff --git a/src/main/scala/firrtl/transforms/InlineNots.scala b/src/main/scala/firrtl/transforms/InlineNots.scala
deleted file mode 100644
index 299c130a..00000000
--- a/src/main/scala/firrtl/transforms/InlineNots.scala
+++ /dev/null
@@ -1,92 +0,0 @@
-package firrtl
-package transforms
-
-import firrtl.ir._
-import firrtl.Mappers._
-import firrtl.PrimOps.{Bits, Not}
-import firrtl.Utils.{isBitExtract, isTemp}
-import firrtl.WrappedExpression._
-
-import scala.collection.mutable
-
-object InlineNotsTransform {
-
-  /** Returns true if Expression is a Not PrimOp, false otherwise */
-  private def isNot(expr: Expression): Boolean = expr match {
-    case DoPrim(Not, args,_,_) => args.forall(isSimpleExpr)
-    case _ => false
-  }
-
-  // Checks if an Expression is made up of only Nots terminated by a Literal or Reference.
-  // private because it's not clear if this definition of "Simple Expression" would be useful elsewhere.
-  // Note that this can have false negatives but MUST NOT have false positives.
-  private def isSimpleExpr(expr: Expression): Boolean = expr match {
-    case _: WRef | _: Literal | _: WSubField => true
-    case DoPrim(Not, args, _,_) => args.forall(isSimpleExpr)
-    case _ => false
-  }
-
-  /** Mapping from references to the [[firrtl.ir.Expression Expression]]s that drive them */
-  type Netlist = mutable.HashMap[WrappedExpression, Expression]
-
-  /** Recursively replace [[WRef]]s with new [[Expression]]s
-    *
-    * @param netlist a '''mutable''' HashMap mapping references to [[firrtl.ir.DefNode DefNode]]s to their connected
-    * [[firrtl.ir.Expression Expression]]s. It is '''not''' mutated in this function
-    * @param expr the Expression being transformed
-    * @return Returns expr with Nots inlined
-    */
-  def onExpr(netlist: Netlist)(expr: Expression): Expression = {
-    expr.map(onExpr(netlist)) match {
-      case e @ WRef(name, _,_,_) =>
-        netlist.get(we(e))
-               .filter(isNot)
-               .getOrElse(e)
-      // replace bits-of-not with not-of-bits to enable later bit extraction transform
-      case lhs @ DoPrim(op, Seq(lval), lcons, ltpe) if isBitExtract(op) && isSimpleExpr(lval) =>
-        netlist.getOrElse(we(lval), lval) match {
-          case DoPrim(Not, Seq(rhs), rcons, rtpe) =>
-            DoPrim(Not, Seq(DoPrim(op, Seq(rhs), lcons, ltpe)), rcons, ltpe)
-          case _ => lhs  // Not a candiate
-        }
-      // replace back-to-back inversions with a straight rename
-      case lhs @ DoPrim(Not, Seq(inv), _, invtpe) if isSimpleExpr(lhs) && isSimpleExpr(inv) && (lhs.tpe == invtpe) && (bitWidth(lhs.tpe) == bitWidth(inv.tpe)) =>
-        netlist.getOrElse(we(inv), inv) match {
-          case DoPrim(Not, Seq(rhs), _, rtpe) if (invtpe == rtpe) && (bitWidth(inv.tpe) == bitWidth(rhs.tpe)) =>
-            DoPrim(Bits, Seq(rhs), Seq(bitWidth(lhs.tpe)-1,0), rtpe)
-          case _ => lhs  // Not a candiate
-        }
-      case other => other // Not a candidate
-    }
-  }
-
-  /** Inline nots in a Statement
-    *
-    * @param netlist a '''mutable''' HashMap mapping references to [[firrtl.ir.DefNode DefNode]]s to their connected
-    * [[firrtl.ir.Expression Expression]]s. This function '''will''' mutate it if stmt is a [[firrtl.ir.DefNode
-    * DefNode]] with a Temporary name and a value that is a [[PrimOp]] Not
-    * @param stmt the Statement being searched for nodes and transformed
-    * @return Returns stmt with nots inlined
-    */
-  def onStmt(netlist: Netlist)(stmt: Statement): Statement =
-    stmt.map(onStmt(netlist)).map(onExpr(netlist)) match {
-      case node @ DefNode(_, name, value) if isTemp(name) =>
-        netlist(we(WRef(name))) = value
-        node
-      case other => other
-    }
-
-  /** Inline nots in a Module */
-  def onMod(mod: DefModule): DefModule = mod.map(onStmt(new Netlist))
-}
-
-/** Inline nodes that are simple nots */
-class InlineNotsTransform extends Transform {
-  def inputForm = UnknownForm
-  def outputForm = UnknownForm
-
-  def execute(state: CircuitState): CircuitState = {
-    val modulesx = state.circuit.modules.map(InlineNotsTransform.onMod(_))
-    state.copy(circuit = state.circuit.copy(modules = modulesx))
-  }
-}
diff --git a/src/test/scala/firrtlTests/ConstantPropagationTests.scala b/src/test/scala/firrtlTests/ConstantPropagationTests.scala
index cc7a5e32..18579ca8 100644
--- a/src/test/scala/firrtlTests/ConstantPropagationTests.scala
+++ b/src/test/scala/firrtlTests/ConstantPropagationTests.scala
@@ -733,78 +733,6 @@ class ConstantPropagationSingleModule extends ConstantPropagationSpec {
     (parse(exec(input))) should be(parse(check))
   }
 
-   "ConstProp" should "propagate boolean equality with true" in {
-    val input =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= eq(x, UInt<1>("h1"))
-      """.stripMargin
-    val check =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= x
-      """.stripMargin
-    (parse(exec(input))) should be(parse(check))
-  }
-
-   "ConstProp" should "propagate boolean equality with false" in {
-    val input =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= eq(x, UInt<1>("h0"))
-      """.stripMargin
-    val check =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= not(x)
-      """.stripMargin
-    (parse(exec(input))) should be(parse(check))
-  }
-
-   "ConstProp" should "propagate boolean non-equality with true" in {
-    val input =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= neq(x, UInt<1>("h1"))
-      """.stripMargin
-    val check =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= not(x)
-      """.stripMargin
-    (parse(exec(input))) should be(parse(check))
-  }
-
-   "ConstProp" should "propagate boolean non-equality with false" in {
-    val input =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= neq(x, UInt<1>("h0"))
-      """.stripMargin
-    val check =
-      """circuit Top :
-        |  module Top :
-        |    input x : UInt<1>
-        |    output z : UInt<1>
-        |    z <= x
-      """.stripMargin
-    (parse(exec(input))) should be(parse(check))
-  }
-
   // Optimizing this mux gives: z <= pad(UInt<2>(0), 4)
   // Thus this checks that we then optimize that pad
   "ConstProp" should "optimize nested Expressions" in {
diff --git a/src/test/scala/firrtlTests/VerilogEmitterTests.scala b/src/test/scala/firrtlTests/VerilogEmitterTests.scala
index ad8b8bf9..c5d0eacc 100644
--- a/src/test/scala/firrtlTests/VerilogEmitterTests.scala
+++ b/src/test/scala/firrtlTests/VerilogEmitterTests.scala
@@ -176,44 +176,6 @@ class DoPrimVerilog extends FirrtlFlatSpec {
         |""".stripMargin.split("\n") map normalized
     executeTest(input, check, compiler)
   }
-  "inline Not" should "emit correctly" in {
-    val compiler = new VerilogCompiler
-    val input =
-      """circuit InlineNot :
-        |  module InlineNot :
-        |    input a: UInt<1>
-        |    input b: UInt<1>
-        |    input c: UInt<4>
-        |    output d: UInt<1>
-        |    output e: UInt<1>
-        |    output f: UInt<1>
-        |    output g: UInt<1>
-        |    output h: UInt<1>
-        |    d <= and(a, not(b))
-        |    e <= or(a, not(b))
-        |    f <= not(not(not(bits(c, 2, 2))))
-        |    g <= mux(not(bits(c, 2, 2)), a, b)
-        |    h <= shr(not(bits(c, 2, 1)), 1)""".stripMargin
-    val check =
-      """module InlineNot(
-        |  input   a,
-        |  input   b,
-        |  input  [3:0] c,
-        |  output  d,
-        |  output  e,
-        |  output  f,
-        |  output  g,
-        |  output  h
-        |);
-        |  assign d = a & ~b;
-        |  assign e = a | ~b;
-        |  assign f = ~c[2];
-        |  assign g = c[2] ? b : a;
-        |  assign h = ~c[2];
-        |endmodule
-        |""".stripMargin.split("\n") map normalized
-    executeTest(input, check, compiler)
-  }
   "Rem" should "emit correctly" in {
     val compiler = new VerilogCompiler
     val input =