Constant prop add (#849)

* add FoldADD to const prop, add yosys miter tests

* add option for verilog compiler without optimizations

* rename FoldLogicalOp to FoldCommutativeOp

* add GetNamespace and RenameModules, GetNamespace stores namespace as a ModuleNamespaceAnnotation

* add constant propagation for Tail DoPrims

* add scaladocs for MinimumLowFirrtlOptimization and yosysExpectFalure/Success, add constant propagation for Head DoPrim

* add legalize pass to MinimumLowFirrtlOptimizations, use constPropBitExtract in legalize pass

1 files changed, 61 insertions, 0 deletions

diff --git a/src/main/scala/firrtl/util/BackendCompilationUtilities.scala b/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
index 0c5ab12f..d3d34e87 100644
--- a/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
+++ b/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
@@ -152,4 +152,65 @@ trait BackendCompilationUtilities {
   def executeExpectingSuccess(prefix: String, dir: File): Boolean = {
     !executeExpectingFailure(prefix, dir)
   }
+
+  /** Creates and runs a Yosys script that creates and runs SAT on a miter
+    * circuit. Returns true if SAT succeeds, false otherwise
+    *
+    * The custom and reference Verilog files must not contain any modules with
+    * the same name otherwise Yosys will not be able to create a miter circuit
+    *
+    * @param customTop    name of the DUT with custom transforms without the .v
+    *                     extension
+    * @param referenceTop name of the DUT without custom transforms without the
+    *                     .v extension
+    * @param testDir      directory containing verilog files
+    * @param resets       signals to set for SAT, format is
+    *                     (timestep, signal, value)
+    */
+  def yosysExpectSuccess(customTop: String,
+                         referenceTop: String,
+                         testDir: File,
+                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
+    !yosysExpectFailure(customTop, referenceTop, testDir, resets)
+  }
+
+  /** Creates and runs a Yosys script that creates and runs SAT on a miter
+    * circuit. Returns false if SAT succeeds, true otherwise
+    *
+    * The custom and reference Verilog files must not contain any modules with
+    * the same name otherwise Yosys will not be able to create a miter circuit
+    *
+    * @param customTop    name of the DUT with custom transforms without the .v
+    *                     extension
+    * @param referenceTop name of the DUT without custom transforms without the
+    *                     .v extension
+    * @param testDir      directory containing verilog files
+    * @param resets       signals to set for SAT, format is
+    *                     (timestep, signal, value)
+    */
+  def yosysExpectFailure(customTop: String,
+                         referenceTop: String,
+                         testDir: File,
+                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
+
+    val setSignals = resets.map(_._2).toSet[String].map(s => s"-set in_$s 0").mkString(" ")
+    val setAtSignals = resets.map {
+      case (timestep, signal, value) => s"-set-at $timestep in_$signal $value"
+    }.mkString(" ")
+    val scriptFileName = s"${testDir.getAbsolutePath}/yosys_script"
+    val yosysScriptWriter = new PrintWriter(scriptFileName)
+    yosysScriptWriter.write(
+      s"""read_verilog ${testDir.getAbsolutePath}/$customTop.v
+         |read_verilog ${testDir.getAbsolutePath}/$referenceTop.v
+         |prep; proc; opt; memory
+         |miter -equiv -flatten $customTop $referenceTop miter
+         |hierarchy -top miter
+         |sat -verify -tempinduct -prove trigger 0 $setSignals $setAtSignals -seq 1 miter"""
+        .stripMargin)
+    yosysScriptWriter.close()
+
+    val resultFileName = testDir.getAbsolutePath + "/yosys_results"
+    val command = s"yosys -s $scriptFileName" #> new File(resultFileName)
+    command.! != 0
+  }
 }