Add a separate flag for partitioning method

README.md

@@ -46,7 +46,7 @@ Use `--help` to get an overview of all the options the compiler has:
 
 ```
 $ eqmap --help
-Technology Mapping Optimization with E-Graphs
+EqMap: FPGA Technology Mapping w/ E-Graphs
 
 Usage: eqmap_fpga [OPTIONS] [INPUT] [OUTPUT]
 
@@ -61,11 +61,13 @@ Options:
   -c, --no-canonicalize            Do not canonicalize the input into LUTs
   -d, --decomp                     Find new decompositions at runtime
       --disassemble <DISASSEMBLE>  Comma separated list of cell types to decompose into
-  -r, --no-retime                  Do not use register retiming
+      --partition <PARTITION>      Netlist partitioning method for re-synthesis
+                           [default: arc-set] [possible values: r2r, arc-set, delay-paths]
   -v, --verbose                    Print explanations (generates a proof and runs slower)
       --min-depth                  Extract for minimum circuit depth
-  -k, --k <K>                      Max fan in size allowed for extracted LUTs
-  -w, --reg-weight <REG_WEIGHT>    Ratio of register cost to LUT cost
+      --random                     Extract randomly
+  -k, --k <K>                      Max fan in size allowed for extracted LUTs [default: 6]
+  -w, --reg-weight <REG_WEIGHT>    Ratio of register cost to LUT cost [default: 1]
   -t, --timeout <TIMEOUT>          Build/extraction timeout in seconds
   -s, --node-limit <NODE_LIMIT>    Maximum number of nodes in graph
   -n, --iter-limit <ITER_LIMIT>    Maximum number of rewrite iterations

src/bin/eqmap_asic.rs

@@ -1,5 +1,4 @@
 use clap::Parser;
-#[cfg(any(feature = "exact_cbc", feature = "exact_highs"))]
 use clap::ValueEnum;
 use eqmap::{
     asic::{CellAnalysis, CellLang, CellRpt, expansion_rewrites, expr_is_mapped},
@@ -24,6 +23,13 @@ enum Solver {
     Highs,
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, ValueEnum)]
+enum PartitionMethod {
+    R2R,
+    ArcSet,
+    DelayPaths,
+}
+
 /// ASIC Technology Mapping Optimization with E-Graphs
 #[derive(Parser, Debug)]
 #[command(version, long_about = None)]
@@ -64,6 +70,10 @@ struct Args {
     #[arg(long, value_enum)]
     exact: Option<Solver>,
 
+    /// Netlist partitioning method for re-synthesis
+    #[arg(long, value_enum, default_value_t = PartitionMethod::ArcSet)]
+    partition: PartitionMethod,
+
     /// Print explanations (generates a proof and runs slower)
     #[arg(short = 'v', long, default_value_t = false)]
     verbose: bool,
@@ -242,7 +252,17 @@ fn main() -> std::io::Result<()> {
     let mut mapper = f
         .get_analysis::<LogicMapper<CellLang, PrimitiveCell>>()
         .map_err(std::io::Error::other)?;
-    mapper.insert_all_r2r().map_err(std::io::Error::other)?;
+
+    match args.partition {
+        PartitionMethod::R2R => {
+            mapper.insert_all_r2r().map_err(std::io::Error::other)?;
+        }
+        PartitionMethod::ArcSet => {
+            mapper.insert_partitioned().map_err(std::io::Error::other)?;
+        }
+        PartitionMethod::DelayPaths => todo!("Implement delay-based partitioning"),
+    }
+
     let mut mapping = mapper.mappings();
     let mapping = mapping.pop().unwrap();
     let expr = mapping.get_expr();

src/bin/eqmap_fpga.rs

@@ -1,5 +1,4 @@
 use clap::Parser;
-#[cfg(any(feature = "exact_cbc", feature = "exact_highs"))]
 use clap::ValueEnum;
 #[cfg(feature = "dyn_decomp")]
 use eqmap::rewrite::dyn_decompositions;
@@ -27,6 +26,13 @@ enum Solver {
     Highs,
 }
 
+#[derive(Debug, Clone, PartialEq, Eq, ValueEnum)]
+enum PartitionMethod {
+    R2R,
+    ArcSet,
+    DelayPaths,
+}
+
 /// EqMap: FPGA Technology Mapping w/ E-Graphs
 #[derive(Parser, Debug)]
 #[command(version, long_about = None)]
@@ -73,9 +79,9 @@ struct Args {
     #[arg(long, value_enum)]
     exact: Option<Solver>,
 
-    /// Do not use register retiming
-    #[arg(short = 'r', long, default_value_t = false)]
-    no_retime: bool,
+    /// Netlist partitioning method for re-synthesis
+    #[arg(long, value_enum, default_value_t = PartitionMethod::ArcSet)]
+    partition: PartitionMethod,
 
     /// Print explanations (generates a proof and runs slower)
     #[arg(short = 'v', long, default_value_t = false)]
@@ -174,7 +180,8 @@ fn main() -> std::io::Result<()> {
         rules.append(&mut dyn_decompositions(true));
     }
 
-    if !args.no_retime {
+    // Cannot retime broken up paths
+    if args.partition != PartitionMethod::R2R {
         rules.append(&mut register_retiming());
     }
 
@@ -186,7 +193,11 @@ fn main() -> std::io::Result<()> {
     );
     debug!(
         "Retiming rewrites {}",
-        if args.no_retime { "OFF" } else { "ON" }
+        if args.partition == PartitionMethod::R2R {
+            "OFF"
+        } else {
+            "ON"
+        }
     );
 
     let req = SynthRequest::default().with_rules(rules);
@@ -271,11 +282,17 @@ fn main() -> std::io::Result<()> {
     let mut mapper = f
         .get_analysis::<LogicMapper<LutLang, PrimitiveCell>>()
         .map_err(std::io::Error::other)?;
-    if args.no_retime {
-        mapper.insert_all_r2r().map_err(std::io::Error::other)?;
-    } else {
-        mapper.insert_partitioned().map_err(std::io::Error::other)?;
+
+    match args.partition {
+        PartitionMethod::R2R => {
+            mapper.insert_all_r2r().map_err(std::io::Error::other)?;
+        }
+        PartitionMethod::ArcSet => {
+            mapper.insert_partitioned().map_err(std::io::Error::other)?;
+        }
+        PartitionMethod::DelayPaths => todo!("Implement delay-based partitioning"),
     }
+
     let mut mapping = mapper.mappings();
     let mapping = mapping.pop().unwrap();
     let expr = mapping.get_expr();

src/lib.rs

@@ -4,15 +4,15 @@
 
 `eqmap`: FPGA LUT Remapping using E-Graphs
 
-This Verilog-to-Verilog tool seeks to evaluate the use of logic rewriting and equality saturation for improving FPGA technology mapping.
+This Verilog-to-Verilog tool uses logic rewriting and equality saturation for improving FPGA technology mapping.
 
 The LUT representation can be found in the [lut] module, whereas a lot of the bit-twiddling of truth tables happens in [rewrite]. [driver] has all the code related to tooling and end-to-end integration.
 
 `eqmap_fpga` is the main CLI tool, and you can see how it is used in some of the CI [tests](https://github.com/matth2k/eqmap/tree/main/tests/verilog). Lastly, eqmap is bundled together with yosys in the [eqmap](https://github.com/matth2k/eqmap/blob/main/bin/eqmap) script. This is the script that should be used to process your own verilog:
 
 ```bash
 $ eqmap --help
-Technology Mapping Optimization with E-Graphs
+EqMap: FPGA Technology Mapping w/ E-Graphs
 
 Usage: eqmap_fpga [OPTIONS] [INPUT] [OUTPUT]
 
@@ -27,9 +27,11 @@ Options:
   -c, --no-canonicalize            Do not canonicalize the input into LUTs
   -d, --decomp                     Find new decompositions at runtime
       --disassemble <DISASSEMBLE>  Comma separated list of cell types to decompose into
-  -r, --no-retime                  Do not use register retiming
+      --partition <PARTITION>      Netlist partitioning method for re-synthesis
+                           [default: arc-set] [possible values: r2r, arc-set, delay-paths]
   -v, --verbose                    Print explanations (generates a proof and runs slower)
       --min-depth                  Extract for minimum circuit depth
+      --random                     Extract randomly
   -k, --k <K>                      Max fan in size allowed for extracted LUTs [default: 6]
   -w, --reg-weight <REG_WEIGHT>    Ratio of register cost to LUT cost [default: 1]
   -t, --timeout <TIMEOUT>          Build/extraction timeout in seconds

tests/driver/rewrite_bug.v

@@ -1,4 +1,4 @@
-// RUN: eqmap_fpga %s --assert-sat --no-retime -k 4 | FileCheck %s
+// RUN: eqmap_fpga %s --assert-sat --partition r2r -k 4 | FileCheck %s
 
 module rewrite_bug (
     clk,