Fix equivalence tests (#853)

* - modify firrtlEquivalenceTest to use yosys equiv_simple/equiv_induct instead of miter
- add RemoveValidIf pass to MinimumLowFirrtlOptimization

* add EquivalenceTest to FirrtlSpec.scala, make classes in IntegrationSpec.scala abstract

* change types of inputForm/outputForm to CircuitForm

* change EquivalenceTest message

* remove ICache equivalence tests

* fix rebase errors

* Add Ops scalatests to LEC suite

* Only run compiler-path-comparison LEC tests on Ops design

* Fixup issues with merge

Co-authored-by: Albert Magyar <albert.magyar@gmail.com>

3 files changed, 53 insertions, 30 deletions

diff --git a/src/main/scala/firrtl/util/BackendCompilationUtilities.scala b/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
index 3bbef814..93ce4df8 100644
--- a/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
+++ b/src/main/scala/firrtl/util/BackendCompilationUtilities.scala
@@ -198,14 +198,14 @@ object BackendCompilationUtilities extends LazyLogging {
     * @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)
+    * @param timesteps    the maximum number of timesteps for Yosys equivalence
+    *                     checking to consider
     */
   def yosysExpectSuccess(customTop: String,
                          referenceTop: String,
                          testDir: File,
-                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
-    !yosysExpectFailure(customTop, referenceTop, testDir, resets)
+                         timesteps: Int = 1): Boolean = {
+    !yosysExpectFailure(customTop, referenceTop, testDir, timesteps)
   }
 
   /** Creates and runs a Yosys script that creates and runs SAT on a miter
@@ -219,27 +219,33 @@ object BackendCompilationUtilities extends LazyLogging {
     * @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)
+    * @param timesteps    the maximum number of timesteps for Yosys equivalence
+    *                     checking to consider
     */
   def yosysExpectFailure(customTop: String,
                          referenceTop: String,
                          testDir: File,
-                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
+                         timesteps: Int = 1): 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
+         |prep -flatten -top $customTop; proc; opt; memory
+         |design -stash custom
          |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"""
+         |prep -flatten -top $referenceTop; proc; opt; memory
+         |design -stash reference
+         |design -copy-from custom -as custom $customTop
+         |design -copy-from reference -as reference $referenceTop
+         |equiv_make custom reference equiv
+         |hierarchy -top equiv
+         |prep -flatten -top equiv
+         |clean -purge
+         |equiv_simple -seq $timesteps
+         |equiv_induct -seq $timesteps
+         |equiv_status -assert
+         """
         .stripMargin)
     yosysScriptWriter.close()
 
@@ -276,16 +282,4 @@ trait BackendCompilationUtilities extends LazyLogging {
     BackendCompilationUtilities.executeExpectingFailure(prefix, dir, assertionMsg)
   }
   def executeExpectingSuccess(prefix: String, dir: File): Boolean = BackendCompilationUtilities.executeExpectingSuccess(prefix, dir)
-  def yosysExpectSuccess(customTop: String,
-                         referenceTop: String,
-                         testDir: File,
-                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
-    BackendCompilationUtilities.yosysExpectSuccess(customTop, referenceTop, testDir, resets)
-  }
-  def yosysExpectFailure(customTop: String,
-                         referenceTop: String,
-                         testDir: File,
-                         resets: Seq[(Int, String, Int)] = Seq.empty): Boolean = {
-    BackendCompilationUtilities.yosysExpectFailure(customTop, referenceTop, testDir, resets)
-  }
 }
diff --git a/src/test/scala/firrtl/testutils/FirrtlSpec.scala b/src/test/scala/firrtl/testutils/FirrtlSpec.scala
index 8f0241fe..c9cd1ecd 100644
--- a/src/test/scala/firrtl/testutils/FirrtlSpec.scala
+++ b/src/test/scala/firrtl/testutils/FirrtlSpec.scala
@@ -77,12 +77,12 @@ trait FirrtlRunners extends BackendCompilationUtilities {
     * @param input string containing Firrtl source
     * @param customTransforms Firrtl transforms to test for equivalence
     * @param customAnnotations Optional Firrtl annotations
-    * @param resets tell yosys which signals to set for SAT, format is (timestep, signal, value)
+    * @param timesteps the maximum number of timesteps to consider
     */
   def firrtlEquivalenceTest(input: String,
                             customTransforms: Seq[Transform] = Seq.empty,
                             customAnnotations: AnnotationSeq = Seq.empty,
-                            resets: Seq[(Int, String, Int)] = Seq.empty): Unit = {
+                            timesteps: Int = 1): Unit = {
     val circuit = Parser.parse(input.split("\n").toIterator)
     val prefix = circuit.main
     val testDir = createTestDirectory(prefix + "_equivalence_test")
@@ -112,7 +112,7 @@ trait FirrtlRunners extends BackendCompilationUtilities {
     val refResult = (new firrtl.stage.FirrtlStage).run(refAnnos)
     val refName = refResult.collectFirst({ case stage.FirrtlCircuitAnnotation(c) => c.main }).getOrElse(refSuggestedName)
 
-    assert(yosysExpectSuccess(customName, refName, testDir, resets))
+    assert(BackendCompilationUtilities.yosysExpectSuccess(customName, refName, testDir, timesteps))
   }
 
   /** Compiles input Firrtl to Verilog */
@@ -430,5 +430,20 @@ trait Utils {
       System.setSecurityManager(null)
     }
   }
+}
+
+/** Super class for equivalence driven Firrtl tests */
+abstract class EquivalenceTest(transforms: Seq[Transform], name: String, dir: String) extends FirrtlFlatSpec {
+  val fileName = s"$dir/$name.fir"
+  val in = getClass.getResourceAsStream(fileName)
+  if (in == null) {
+    throw new FileNotFoundException(s"Resource '$fileName'")
+  }
+  val source = scala.io.Source.fromInputStream(in)
+  val input = try source.mkString finally source.close()
 
+  s"$name with ${transforms.map(_.name).mkString(", ")}" should
+    s"be equivalent to $name without ${transforms.map(_.name).mkString(", ")}" in {
+    firrtlEquivalenceTest(input, transforms)
+  }
 }
diff --git a/src/test/scala/firrtlTests/IntegrationSpec.scala b/src/test/scala/firrtlTests/IntegrationSpec.scala
index 352a5e52..b399923f 100644
--- a/src/test/scala/firrtlTests/IntegrationSpec.scala
+++ b/src/test/scala/firrtlTests/IntegrationSpec.scala
@@ -52,3 +52,17 @@ class RocketCoreCompilationTest extends CompilationTest("RocketCore", "/regress"
 class ICacheCompilationTest extends CompilationTest("ICache", "/regress")
 class FPUCompilationTest extends CompilationTest("FPU", "/regress")
 class HwachaSequencerCompilationTest extends CompilationTest("HwachaSequencer", "/regress")
+
+abstract class CommonSubexprEliminationEquivTest(name: String, dir: String) extends
+  EquivalenceTest(Seq(firrtl.passes.CommonSubexpressionElimination), name, dir)
+abstract class DeadCodeEliminationEquivTest(name: String, dir: String) extends
+  EquivalenceTest(Seq(new firrtl.transforms.DeadCodeElimination), name, dir)
+abstract class ConstantPropagationEquivTest(name: String, dir: String) extends
+  EquivalenceTest(Seq(new firrtl.transforms.ConstantPropagation), name, dir)
+abstract class LowFirrtlOptimizationEquivTest(name: String, dir: String) extends
+  EquivalenceTest(Seq(new LowFirrtlOptimization), name, dir)
+
+class OpsCommonSubexprEliminationTest extends CommonSubexprEliminationEquivTest("Ops", "/regress")
+class OpsDeadCodeEliminationTest extends DeadCodeEliminationEquivTest("Ops", "/regress")
+class OpsConstantPropagationTest extends ConstantPropagationEquivTest("Ops", "/regress")
+class OpsLowFirrtlOptimizationTest extends LowFirrtlOptimizationEquivTest("Ops", "/regress")