[circt-synth] Add an option to disable WordsToBits, remove verification code from design (#8733)

This modifies circt-synth to make it more practical.
* Remove verification code from synthesis parts. ExtarctTestCode is currently used, but eventually it must be replaced with something cleaner. 
* Add an option to disable wordsToBits.

include/circt/Synthesis/SynthesisPipeline.h

@@ -38,6 +38,10 @@ struct AIGOptimizationPipelineOptions
       *this, "ignore-abc-failures",
       llvm::cl::desc("Continue on ABC failure instead of aborting"),
       llvm::cl::init(false)};
+
+  PassOptions::Option<bool> disableWordToBits{
+      *this, "disable-word-to-bits",
+      llvm::cl::desc("Disable LowerWordToBits pass"), llvm::cl::init(false)};
 };
 
 //===----------------------------------------------------------------------===//

lib/Synthesis/SynthesisPipeline.cpp

@@ -62,10 +62,11 @@ void circt::synthesis::buildAIGOptimizationPipeline(
 
   pm.addPass(aig::createLowerVariadic());
 
-  // TODO: LowerWordToBits is not scalable for large designs. Change to
-  // conditionally enable the pass once the rest of the pipeline was able
-  // to handle multibit operands properly.
-  pm.addPass(aig::createLowerWordToBits());
+  // LowerWordToBits may not be scalable for large designs so conditionally
+  // disable it. It's also worth considering keeping word-level representation
+  // for faster synthesis.
+  if (!options.disableWordToBits)
+    pm.addPass(aig::createLowerWordToBits());
   pm.addPass(createCSEPass());
   pm.addPass(createSimpleCanonicalizerPass());
 

test/circt-synth/basic.mlir

@@ -3,12 +3,14 @@
 // RUN: circt-synth %s --top and --emit-bytecode -f | circt-opt | FileCheck %s --check-prefix=CHECK
 // RUN: circt-synth %s --until-before aig-lowering | FileCheck %s --check-prefix=AIG
 // RUN: circt-synth %s --until-before aig-lowering --convert-to-comb | FileCheck %s --check-prefix=COMB
+// RUN: circt-synth %s --top and --disable-word-to-bits | FileCheck %s --check-prefix=DISABLE_WORD
 
 // TOP-LABEL: module attributes {"aig.longest-path-analysis-top" = @and}
-// AIG-LABEL: @and
-// CHECK-LABEL: @and
-// COMB-LABEL: @and
-hw.module @and(in %a: i2, in %b: i2, in %c: i2, out and: i2) {
+// AIG-LABEL: @and(
+// CHECK-LABEL: @and(
+// COMB-LABEL: @and(
+// DISABLE_WORD-LABEL: @and(
+hw.module @and(in %a: i2, in %b: i2, in %c: i2, in %d: i1, out and: i2) {
   // AIG-NEXT:  %[[AND_INV:.+]] = aig.and_inv %a, %b, %c : i2
   // AIG-NEXT: dbg.variable
   // AIG-NEXT: hw.output %[[AND_INV]] : i2
@@ -26,11 +28,22 @@ hw.module @and(in %a: i2, in %b: i2, in %c: i2, out and: i2) {
   // CHECK-NEXT: dbg.variable
   // CHECK-NEXT: hw.output %[[CONCAT]] : i2
   // COMB-NOT: aig.and_inv
+  // DISABLE_WORD-NOT: comb.extract
+  // DISABLE_WORD-NOT: comb.concat
   %0 = comb.and %a, %b, %c : i2
   dbg.variable "test", %0 : i2
   hw.output %0 : i2
 }
 
+// CHECK-LABEL: @verification(
+// CHECK-NOT: sv.assert
+hw.module @verification(in %a: i1, out result: i1) {
+  sv.initial {
+    sv.assert %a, immediate
+  }
+  hw.output %a : i1
+}
+
 // TOP-LABEL: hw.module @unrelated
 // TOP-NEXT: comb.add %a, %b
 hw.module @unrelated(in %a: i2, in %b: i2, out and: i2) {

tools/circt-synth/CMakeLists.txt

@@ -13,6 +13,7 @@ target_link_libraries(circt-synth
   CIRCTSeq
   CIRCTSim
   CIRCTSV
+  CIRCTSVTransforms
   CIRCTSynthesis
   CIRCTTransforms
   CIRCTVerif

tools/circt-synth/circt-synth.cpp

@@ -24,6 +24,7 @@
 #include "circt/Dialect/LTL/LTLDialect.h"
 #include "circt/Dialect/OM/OMDialect.h"
 #include "circt/Dialect/SV/SVDialect.h"
+#include "circt/Dialect/SV/SVPasses.h"
 #include "circt/Dialect/Seq/SeqDialect.h"
 #include "circt/Dialect/Sim/SimDialect.h"
 #include "circt/Dialect/Verif/VerifDialect.h"
@@ -144,6 +145,10 @@ static cl::opt<bool>
                       cl::desc("Continue on ABC failure instead of aborting"),
                       cl::init(false), cl::cat(mainCategory));
 
+static cl::opt<bool> disableWordToBits("disable-word-to-bits",
+                                       cl::desc("Disable LowerWordToBits pass"),
+                                       cl::init(false), cl::cat(mainCategory));
+
 //===----------------------------------------------------------------------===//
 // Main Tool Logic
 //===----------------------------------------------------------------------===//
@@ -174,6 +179,11 @@ static void partiallyLegalizeCombToAIG(SmallVectorImpl<std::string> &ops) {
 
 // Add a default synthesis pipeline and analysis.
 static void populateCIRCTSynthPipeline(PassManager &pm) {
+  // ExtractTestCode is used to move verification code from design to
+  // remove registers/logic used only for verification.
+  pm.addPass(sv::createSVExtractTestCodePass(
+      /*disableInstanceExtraction=*/false, /*disableRegisterExtraction=*/false,
+      /*disableModuleInlining=*/false));
   auto pipeline = [](OpPassManager &pm) {
     circt::synthesis::buildAIGLoweringPipeline(pm);
     if (untilReached(UntilAIGLowering))
@@ -183,6 +193,7 @@ static void populateCIRCTSynthPipeline(PassManager &pm) {
     options.abcCommands = abcCommands;
     options.abcPath.setValue(abcPath);
     options.ignoreAbcFailures.setValue(ignoreAbcFailures);
+    options.disableWordToBits.setValue(disableWordToBits);
 
     circt::synthesis::buildAIGOptimizationPipeline(pm, options);
   };