From 6c973e94c60e743d63cb004f7f9cc43a3294d4ea Mon Sep 17 00:00:00 2001 From: rollrat Date: Mon, 5 Oct 2026 16:21:15 +0900 Subject: [PATCH 1/2] Search equivalent NOR netlists with an e-graph The exact placer builds whatever NOR netlist it is handed, so a hand-written netlist such as the full adder's nor9 fixes its torch count and logic depth before placement starts. egraph.rs explores the equivalent netlists with egg and extracts ones worth placing. Saturation runs De Morgan, double negation, commutativity and associativity, distribution and factoring both ways, absorption, and XOR and XNOR expansions. Each e-class carries its truth table, and classes with equal tables are unioned in modify, so different forms of one function always meet. The full adder reaches 230 of the 256 three-input functions in 73 ms. Greedy extraction decides class by class and missed the shared NORs (13 gates against nor9's 9), so extraction is exact: egraph_extract.rsdsl, grounded with rsdsl and solved with the placer's CaDiCaL binding, picks one node per needed class (outputs are torches, a NOT adds a tick, an OR none) and minimizes gates, plus or_cost per OR node since every NOR input is a signal to route, within an optional depth bound. Each extraction is proven optimal for its e-graph in 0.1-10 s. On the full adder: - fewest gates: 8 (nor9 has 9), depth 3/4, but NORs of up to 4 inputs; - depth 3: 9 gates, depth 2/3; - or_cost 1: 9 gates, depth 4/5 against nor9's 5/6, fan-in 3, and the same 4 nets alive at once as nor9. The circuit harness places them (CIRCUIT=egraph-full-adder with EGRAPH_DEPTH and EGRAPH_OR_COST); explore_egraph_netlists sweeps depth bounds and OR costs. ExactLocalPlacer::from_netlist takes a netlist built elsewhere. Co-Authored-By: Claude Opus 5.5 --- Cargo.lock | 100 ++- Cargo.toml | 1 + .../local_placer/exact/egraph.rs | 713 ++++++++++++++++++ .../local_placer/exact/egraph_extract.rsdsl | 75 ++ .../place_and_route/local_placer/exact/mod.rs | 10 + .../local_placer/exact/netlist.rs | 2 +- .../local_placer/exact/tests.rs | 178 ++++- 7 files changed, 1073 insertions(+), 6 deletions(-) create mode 100644 src/transform/place_and_route/local_placer/exact/egraph.rs create mode 100644 src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl diff --git a/Cargo.lock b/Cargo.lock index 533acd1b..5e783232 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,6 +8,17 @@ version = "1.0.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "f26201604c87b1e01bd3d98f8d5d9a8fcbb815e8cedb41ffccbeb4bf593a35fe" +[[package]] +name = "ahash" +version = "0.7.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "891477e0c6a8957309ee5c45a6368af3ae14bb510732d2684ffa19af310920f9" +dependencies = [ + "getrandom", + "once_cell", + "version_check", +] + [[package]] name = "ansi_term" version = "0.12.1" @@ -221,6 +232,24 @@ dependencies = [ "syn 2.0.87", ] +[[package]] +name = "egg" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "96beaf9d35dbc4686bc86a4ecb851fd6a406f0bf32d9f646b1225a5c5cf5b5d7" +dependencies = [ + "env_logger", + "fxhash", + "hashbrown 0.12.3", + "indexmap 1.9.3", + "instant", + "log", + "smallvec", + "symbol_table", + "symbolic_expressions", + "thiserror 1.0.69", +] + [[package]] name = "either" version = "1.8.1" @@ -233,6 +262,15 @@ version = "1.0.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0" +[[package]] +name = "env_logger" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a12e6657c4c97ebab115a42dcee77225f7f482cdd841cf7088c657a42e9e00e7" +dependencies = [ + "log", +] + [[package]] name = "equivalent" version = "1.0.1" @@ -294,6 +332,15 @@ dependencies = [ "miniz_oxide", ] +[[package]] +name = "fxhash" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c31b6d751ae2c7f11320402d34e41349dd1016f8d5d45e48c4312bc8625af50c" +dependencies = [ + "byteorder", +] + [[package]] name = "getrandom" version = "0.2.15" @@ -312,6 +359,9 @@ name = "hashbrown" version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" +dependencies = [ + "ahash", +] [[package]] name = "hashbrown" @@ -397,6 +447,15 @@ dependencies = [ "web-time", ] +[[package]] +name = "instant" +version = "0.1.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e0242819d153cba4b4b05a5a8f2a7e9bbf97b6055b2a002b395c96b5ff3c0222" +dependencies = [ + "cfg-if", +] + [[package]] name = "itertools" version = "0.11.0" @@ -732,6 +791,7 @@ dependencies = [ "cadical", "derive_more", "disjoint-set", + "egg", "eyre", "fastanvil", "fastnbt", @@ -908,6 +968,22 @@ dependencies = [ "syn 2.0.87", ] +[[package]] +name = "symbol_table" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32bf088d1d7df2b2b6711b06da3471bc86677383c57b27251e18c56df8deac14" +dependencies = [ + "ahash", + "hashbrown 0.12.3", +] + +[[package]] +name = "symbolic_expressions" +version = "5.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7c68d531d83ec6c531150584c42a4290911964d5f0d79132b193b67252a23b71" + [[package]] name = "syn" version = "1.0.109" @@ -939,13 +1015,33 @@ dependencies = [ "unicode-width 0.1.10", ] +[[package]] +name = "thiserror" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +dependencies = [ + "thiserror-impl 1.0.69", +] + [[package]] name = "thiserror" version = "2.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4" dependencies = [ - "thiserror-impl", + "thiserror-impl 2.0.18", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.69" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.87", ] [[package]] @@ -1298,7 +1394,7 @@ dependencies = [ "flate2", "indexmap 2.0.0", "memchr", - "thiserror", + "thiserror 2.0.18", "zopfli", ] diff --git a/Cargo.toml b/Cargo.toml index 447389f8..dd791783 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -35,6 +35,7 @@ tracing-subscriber = "0.3.17" flate2 = "1.0.26" serde = "1.0.183" zip = { version = "2.2", default-features = false, features = ["deflate"] } +egg = "0.9" [target.'cfg(not(target_arch = "wasm32"))'.dependencies] mimalloc = "0.1.43" diff --git a/src/transform/place_and_route/local_placer/exact/egraph.rs b/src/transform/place_and_route/local_placer/exact/egraph.rs new file mode 100644 index 00000000..7749269c --- /dev/null +++ b/src/transform/place_and_route/local_placer/exact/egraph.rs @@ -0,0 +1,713 @@ +//! Equivalent NOR netlists from an e-graph (egg). +//! +//! A hand-written netlist (`nor9`, say) fixes which gates the placer builds. +//! Equality saturation explores other expressions of the same functions: De +//! Morgan, double negation, commutativity and associativity, distribution and +//! factoring, absorption, and XOR expansions. Every e-class carries its truth +//! table, and classes with the same table are merged as soon as they appear, +//! so two forms of one function always meet, whichever rules produced them. +//! +//! Extraction then picks NOR netlists in the placer's terms. A NOT is a torch +//! (one gate and one redstone tick), an OR is free (dust and blocks), and a +//! shared subterm is built once. `Weights` trade gates against depth, so a few +//! weightings give a small set of distinct netlists to place. + +use std::collections::{BTreeMap, BTreeSet, HashMap}; +use std::sync::atomic::AtomicBool; +use std::sync::OnceLock; +use std::time::{Duration, Instant}; + +use egg::{ + define_language, rewrite as rw, Analysis, DidMerge, EGraph, Id, RecExpr, Rewrite, Runner, + StopReason, Symbol, +}; +use eyre::{bail, ensure, eyre}; +use rsdsl::{GroundOptions, IValue, Instance, Model}; + +use super::cnf::Cnf; +use super::netlist::{Net, NetDriver, NetId, NorNetlist}; +use super::solver::{SatSolver, SolveResult, StopSignal}; + +const EXTRACT_SOURCE: &str = include_str!("egraph_extract.rsdsl"); + +fn extract_model() -> &'static Model { + static MODEL: OnceLock = OnceLock::new(); + MODEL.get_or_init(|| { + Model::parse("egraph_extract.rsdsl", EXTRACT_SOURCE) + .unwrap_or_else(|error| panic!("{error}")) + }) +} + +/// What `Exploration::extract_exact` minimizes, and within what. +#[derive(Debug, Clone, Copy)] +pub struct ExtractOptions { + /// Gates on the slowest path to an output, at most. + pub max_depth: Option, + /// Weight of each OR node (one more input on a NOR) against a gate's 1. + pub or_cost: usize, + pub time_limit: Duration, +} + +impl Default for ExtractOptions { + fn default() -> Self { + Self { + max_depth: None, + or_cost: 0, + time_limit: Duration::from_secs(60), + } + } +} + +/// A netlist picked by `Exploration::extract_exact`. +#[derive(Debug, Clone)] +pub struct Extraction { + pub netlist: NorNetlist, + /// The minimized cost: gates, plus `or_cost` per OR node. + pub cost: usize, + /// No netlist in the e-graph within the depth costs less. + pub proven: bool, +} + +define_language! { + /// Boolean expressions over named inputs. Only `~` and `|` are built: a + /// NOT is a torch, an OR is dust and blocks. `&` and `^` state functions + /// and give the rewrites something to go through. + pub enum Bool { + "~" = Not(Id), + "|" = Or([Id; 2]), + "&" = And([Id; 2]), + "^" = Xor([Id; 2]), + Var(Symbol), + } +} + +/// The truth table of every e-class: bit `k` is the value in input case `k`, +/// where bit `i` of `k` is input `i`. Classes with the same table are merged. +#[derive(Debug, Clone, Default)] +pub struct TruthTable { + inputs: Vec, + full: u64, + by_table: HashMap, +} + +impl TruthTable { + fn new(inputs: &[&str]) -> eyre::Result { + ensure!(inputs.len() <= 6, "truth tables hold at most 6 inputs"); + let cases = 1u32 << inputs.len(); + Ok(Self { + inputs: inputs.iter().map(|&name| Symbol::from(name)).collect(), + full: if cases == 64 { + u64::MAX + } else { + (1u64 << cases) - 1 + }, + by_table: HashMap::new(), + }) + } + + fn input(&self, symbol: Symbol) -> u64 { + let index = self + .inputs + .iter() + .position(|&input| input == symbol) + .unwrap_or_else(|| panic!("unknown input {symbol}")); + (0..self.full.count_ones()) + .filter(|case| case & (1 << index) != 0) + .fold(0, |table, case| table | (1 << case)) + } +} + +impl Analysis for TruthTable { + type Data = u64; + + fn make(egraph: &EGraph, enode: &Bool) -> u64 { + let table = |id: &Id| egraph[*id].data; + let analysis = &egraph.analysis; + match enode { + Bool::Not(a) => !table(a) & analysis.full, + Bool::Or([a, b]) => table(a) | table(b), + Bool::And([a, b]) => table(a) & table(b), + Bool::Xor([a, b]) => table(a) ^ table(b), + Bool::Var(symbol) => analysis.input(*symbol), + } + } + + fn merge(&mut self, a: &mut u64, b: u64) -> DidMerge { + assert_eq!(*a, b, "merged e-classes compute different functions"); + DidMerge(false, false) + } + + fn modify(egraph: &mut EGraph, id: Id) { + let table = egraph[id].data; + match egraph.analysis.by_table.get(&table) { + Some(&other) => { + egraph.union(other, id); + } + None => { + egraph.analysis.by_table.insert(table, id); + } + } + } +} + +fn rules() -> Vec> { + let mut rules = vec![ + rw!("or-comm"; "(| ?a ?b)" => "(| ?b ?a)"), + rw!("and-comm"; "(& ?a ?b)" => "(& ?b ?a)"), + rw!("xor-comm"; "(^ ?a ?b)" => "(^ ?b ?a)"), + rw!("or-assoc"; "(| ?a (| ?b ?c))" => "(| (| ?a ?b) ?c)"), + rw!("and-assoc"; "(& ?a (& ?b ?c))" => "(& (& ?a ?b) ?c)"), + rw!("xor-assoc"; "(^ ?a (^ ?b ?c))" => "(^ (^ ?a ?b) ?c)"), + rw!("not-not"; "(~ (~ ?a))" => "?a"), + rw!("or-absorb"; "(| ?a (& ?a ?b))" => "?a"), + rw!("and-absorb"; "(& ?a (| ?a ?b))" => "?a"), + rw!("or-idem"; "(| ?a ?a)" => "?a"), + rw!("and-idem"; "(& ?a ?a)" => "?a"), + ]; + rules.extend(rw!("and-de-morgan"; "(& ?a ?b)" <=> "(~ (| (~ ?a) (~ ?b)))")); + rules.extend(rw!("or-de-morgan"; "(~ (| ?a ?b))" <=> "(& (~ ?a) (~ ?b))")); + rules.extend(rw!("and-over-or"; "(& ?a (| ?b ?c))" <=> "(| (& ?a ?b) (& ?a ?c))")); + rules.extend(rw!("or-over-and"; "(| ?a (& ?b ?c))" <=> "(& (| ?a ?b) (| ?a ?c))")); + rules.extend(rw!("xor-sop"; "(^ ?a ?b)" <=> "(| (& ?a (~ ?b)) (& (~ ?a) ?b))")); + rules.extend(rw!("xor-pos"; "(^ ?a ?b)" <=> "(& (| ?a ?b) (~ (& ?a ?b)))")); + rules.extend(rw!("xnor"; "(~ (^ ?a ?b))" <=> "(^ (~ ?a) ?b)")); + rules +} + +/// Limits of one saturation run. +#[derive(Debug, Clone, Copy)] +pub struct Limits { + pub iterations: usize, + pub nodes: usize, + pub time: std::time::Duration, +} + +impl Default for Limits { + fn default() -> Self { + Self { + iterations: 12, + nodes: 50_000, + time: std::time::Duration::from_secs(20), + } + } +} + +/// A saturated e-graph and its output classes. +pub struct Exploration { + egraph: EGraph, + inputs: Vec, + outputs: Vec<(String, Id)>, + pub iterations: usize, + pub stop_reason: Option, +} + +/// How to weigh an extracted netlist: torches and ticks on its slowest path. +#[derive(Debug, Clone, Copy)] +pub struct Weights { + pub gates: f64, + pub depth: f64, +} + +#[derive(Debug, Clone)] +struct Choice { + node: Bool, + gates: BTreeSet, + depth: usize, +} + +impl Exploration { + /// Saturates `outputs` (infix expressions over `inputs` with `~ & ^ |`) + /// within `limits`. + pub fn new(inputs: &[&str], outputs: &[(&str, &str)], limits: Limits) -> eyre::Result { + let mut egraph = EGraph::new(TruthTable::new(inputs)?); + let mut roots = Vec::new(); + for &(name, expression) in outputs { + let expression = parse(expression)?; + roots.push((name.to_owned(), egraph.add_expr(&expression))); + } + let runner = Runner::default() + .with_egraph(egraph) + .with_iter_limit(limits.iterations) + .with_node_limit(limits.nodes) + .with_time_limit(limits.time) + .run(&rules()); + let iterations = runner.iterations.len(); + let stop_reason = runner.stop_reason.clone(); + let egraph = runner.egraph; + let outputs = roots + .into_iter() + .map(|(name, id)| (name, egraph.find(id))) + .collect(); + Ok(Self { + egraph, + inputs: inputs.iter().map(|&name| name.to_owned()).collect(), + outputs, + iterations, + stop_reason, + }) + } + + pub fn classes(&self) -> usize { + self.egraph.number_of_classes() + } + + pub fn nodes(&self) -> usize { + self.egraph.total_number_of_nodes() + } + + /// The netlist with the least weighted cost, greedily: each class takes + /// the NOT, OR, or input node whose own and inputs' gates (shared ones + /// counted once) and depth weigh least, until no class changes. + pub fn extract(&self, weights: Weights) -> eyre::Result { + let egraph = &self.egraph; + let score = |choice: &Choice| { + weights.gates * choice.gates.len() as f64 + weights.depth * choice.depth as f64 + }; + let mut best = HashMap::::new(); + for _ in 0..256 { + let mut changed = false; + for class in egraph.classes() { + for node in &class.nodes { + let Some(candidate) = self.candidate(class.id, node, &best) else { + continue; + }; + let better = match best.get(&class.id) { + None => true, + Some(current) => { + let (new, old) = (score(&candidate), score(current)); + new < old - 1e-9 + || ((new - old).abs() <= 1e-9 + && (candidate.gates.len(), candidate.depth) + < (current.gates.len(), current.depth)) + } + }; + if better { + best.insert(class.id, candidate); + changed = true; + } + } + } + if !changed { + break; + } + } + self.netlist(&best) + } + + /// The netlist with the fewest NOT gates (plus `or_cost` per OR node) + /// whose outputs are at most `max_depth` gates deep, picked exactly by + /// SAT over the e-graph (`egraph_extract.rsdsl`): one node per needed + /// class, shared classes built once. Lowers the bound until it is proven + /// or `time_limit` runs out; `None` when no netlist of the e-graph fits. + pub fn extract_exact(&self, options: &ExtractOptions) -> eyre::Result> { + let ExtractOptions { + max_depth, + or_cost, + time_limit, + } = *options; + let egraph = &self.egraph; + let classes = egraph.classes().map(|class| class.id).collect::>(); + let index = classes + .iter() + .enumerate() + .map(|(index, &id)| (id, index)) + .collect::>(); + let mut nodes = Vec::<(Id, Bool)>::new(); + let mut rows = Vec::new(); + for class in egraph.classes() { + let own = class.id; + for node in &class.nodes { + let children = match node { + Bool::Var(_) => Vec::new(), + Bool::Not(a) => vec![egraph.find(*a)], + Bool::Or([a, b]) => vec![egraph.find(*a), egraph.find(*b)], + Bool::And(_) | Bool::Xor(_) => continue, + }; + if children.contains(&own) { + continue; + } + let n = nodes.len(); + nodes.push((own, node.clone())); + rows.push(("node_class", vec![n.into(), index[&own].into()])); + match node { + Bool::Not(_) => rows.push(("gate", vec![n.into()])), + Bool::Or(_) => rows.push(("or_node", vec![n.into()])), + _ => {} + } + for child in children.into_iter().collect::>() { + rows.push(( + "edge", + vec![n.into(), index[&own].into(), index[&child].into()], + )); + } + } + } + let levels = max_depth.unwrap_or(24); + let mut instance = Instance::new("egraph"); + instance + .domain("Class", (0..classes.len()).map(IValue::from)) + .domain("Node", (0..nodes.len()).map(IValue::from)) + .domain("Tick", (0..=levels).map(IValue::from)) + .param("levels", levels) + .param("or_cost", or_cost); + if let Some(depth) = max_depth { + instance.param("max_depth", depth); + } + for fact in ["node_class", "edge", "gate", "or_node", "root"] { + instance.fact(fact); + } + for (fact, row) in rows { + instance.row(fact, row); + } + for (_, root) in &self.outputs { + instance.row("root", vec![index[&egraph.find(*root)].into()]); + } + let options = GroundOptions { + guards: false, + provenance: false, + positive_or_aux: false, + no_fold: false, + }; + let mut program = extract_model() + .ground(&instance, options) + .map_err(|error| eyre!("grounding egraph_extract failed:\n{error}"))?; + let objective = program + .objective() + .ok_or_else(|| eyre!("egraph_extract has no objective"))?; + let at_least = program.objective_counter(objective.total_weight()); + let picks = (0..nodes.len()) + .map(|n| program.var_lit("Pick", &[n.into()])) + .collect::>>() + .ok_or_else(|| eyre!("egraph_extract has no Pick for every node"))?; + let cnf = Cnf::from_literals( + program.num_vars(), + program.literals().to_vec(), + program.clause_count(), + ); + let mut solver = SatSolver::new(1); + solver.add_cnf(&cnf); + let stop = AtomicBool::new(false); + let signal = StopSignal { + stop: &stop, + deadline: Some(Instant::now() + time_limit), + restart: None, + }; + let mut best = None::<(i64, HashMap)>; + let mut proven = false; + loop { + let assumptions = match &best { + None => Vec::new(), + Some((cost, _)) => { + let bound = cost - 1 - objective.offset; + if bound < 0 { + proven = true; + break; + } + vec![-at_least[bound as usize]] + } + }; + match solver.solve(&assumptions, &signal) { + SolveResult::Sat => { + let cost = objective.cost(|lit| solver.value(lit)); + let chosen = nodes + .iter() + .zip(&picks) + .filter(|(_, &lit)| solver.value(lit)) + .map(|((class, node), _)| { + let choice = Choice { + node: node.clone(), + gates: BTreeSet::new(), + depth: 0, + }; + (*class, choice) + }) + .collect(); + best = Some((cost, chosen)); + } + SolveResult::Unsat => { + proven = best.is_some(); + break; + } + SolveResult::Interrupted => break, + } + } + let Some((cost, chosen)) = best else { + return Ok(None); + }; + Ok(Some(Extraction { + netlist: self.netlist(&chosen)?, + cost: cost as usize, + proven, + })) + } + + fn candidate(&self, class: Id, node: &Bool, best: &HashMap) -> Option { + let child = |id: &Id| best.get(&self.egraph.find(*id)); + match node { + Bool::Var(_) => Some(Choice { + node: node.clone(), + gates: BTreeSet::new(), + depth: 0, + }), + Bool::Or([a, b]) => { + let (a, b) = (child(a)?, child(b)?); + Some(Choice { + node: node.clone(), + gates: a.gates.union(&b.gates).copied().collect(), + depth: a.depth.max(b.depth), + }) + } + Bool::Not(a) => { + let a = child(a)?; + // A NOT of its own class (through rewrites) builds nothing. + if a.gates.contains(&class) { + return None; + } + let mut gates = a.gates.clone(); + gates.insert(class); + Some(Choice { + node: node.clone(), + gates, + depth: a.depth + 1, + }) + } + Bool::And(_) | Bool::Xor(_) => None, + } + } + + fn netlist(&self, best: &HashMap) -> eyre::Result { + let egraph = &self.egraph; + let mut nets = self + .inputs + .iter() + .enumerate() + .map(|(index, name)| Net { + name: name.clone(), + node_id: index, + driver: NetDriver::Input(name.clone()), + gate_inputs: Vec::new(), + }) + .collect::>(); + let mut net_of_class = HashMap::::new(); + + // The nets whose OR a class is (one net unless it chose an OR). + fn sources( + exploration: &Exploration, + best: &HashMap, + nets: &mut Vec, + net_of_class: &mut HashMap, + class: Id, + depth: usize, + ) -> eyre::Result> { + ensure!(depth < 256, "extraction recursed too deep"); + let class = exploration.egraph.find(class); + let choice = best + .get(&class) + .ok_or_else(|| eyre!("class {class} has no buildable form"))?; + match &choice.node { + Bool::Or([a, b]) => { + let mut set = sources(exploration, best, nets, net_of_class, *a, depth + 1)?; + set.extend(sources( + exploration, + best, + nets, + net_of_class, + *b, + depth + 1, + )?); + Ok(set) + } + _ => Ok(BTreeSet::from([net( + exploration, + best, + nets, + net_of_class, + class, + depth + 1, + )?])), + } + } + + fn net( + exploration: &Exploration, + best: &HashMap, + nets: &mut Vec, + net_of_class: &mut HashMap, + class: Id, + depth: usize, + ) -> eyre::Result { + if let Some(&net) = net_of_class.get(&class) { + return Ok(net); + } + let net = match &best[&class].node { + Bool::Var(symbol) => nets + .iter() + .position(|net| net.driver == NetDriver::Input(symbol.to_string())) + .ok_or_else(|| eyre!("unknown input {symbol}"))?, + Bool::Not(a) => { + let inputs = sources(exploration, best, nets, net_of_class, *a, depth + 1)?; + nets.push(Net { + name: format!("g{}", nets.len()), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: inputs.into_iter().collect(), + }); + nets.len() - 1 + } + other => bail!("class {class} chose {other} as a net"), + }; + net_of_class.insert(class, net); + Ok(net) + } + + let mut outputs = Vec::new(); + for (name, root) in &self.outputs { + let root = egraph.find(*root); + let choice = best + .get(&root) + .ok_or_else(|| eyre!("output `{name}` has no buildable form"))?; + let output = match choice.node { + Bool::Var(_) => bail!("output `{name}` is an input"), + Bool::Not(_) => net(self, best, &mut nets, &mut net_of_class, root, 0)?, + // An OR output needs a driver: a NOT over the NOR of its terms. + _ => { + let inputs = sources(self, best, &mut nets, &mut net_of_class, root, 0)?; + nets.push(Net { + name: format!("{name}_n"), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: inputs.into_iter().collect(), + }); + nets.push(Net { + name: format!("g{}", nets.len()), + node_id: nets.len(), + driver: NetDriver::Gate, + gate_inputs: vec![nets.len() - 1], + }); + nets.len() - 1 + } + }; + outputs.push((name.clone(), output)); + } + for (name, output) in &outputs { + if nets[*output].driver == NetDriver::Gate { + nets[*output].name = name.clone(); + } + } + outputs.sort(); + let netlist = NorNetlist { nets, outputs }; + netlist.check_acyclic()?; + Ok(netlist) + } +} + +/// Gates on the slowest path to each output (OR free, NOT one). +pub fn netlist_depths(netlist: &NorNetlist) -> BTreeMap { + let mut depth = vec![0usize; netlist.nets.len()]; + for net in netlist.topological_order() { + if netlist.nets[net].driver == NetDriver::Gate { + depth[net] = 1 + netlist.nets[net] + .gate_inputs + .iter() + .map(|&input| depth[input]) + .max() + .unwrap_or(0); + } + } + netlist + .outputs + .iter() + .map(|(name, net)| (name.clone(), depth[*net])) + .collect() +} + +/// The gates as functions of the inputs: two netlists with the same gate +/// functions and gate inputs build the same circuit. +pub fn signature(netlist: &NorNetlist) -> BTreeSet<(Vec, Vec>)> { + let values = netlist.net_values(); + netlist + .gates() + .map(|gate| { + let mut inputs = netlist.nets[gate] + .gate_inputs + .iter() + .map(|&input| values[input].clone()) + .collect::>(); + inputs.sort(); + (values[gate].clone(), inputs) + }) + .collect() +} + +/// Parses `~ & ^ |` (tightest first) over names and parentheses. +fn parse(text: &str) -> eyre::Result> { + struct Parser<'a> { + chars: std::iter::Peekable>, + expression: RecExpr, + } + impl Parser<'_> { + fn skip(&mut self) { + while self.chars.peek().is_some_and(|c| c.is_whitespace()) { + self.chars.next(); + } + } + fn binary(&mut self, level: usize) -> eyre::Result { + const OPERATORS: [char; 3] = ['|', '^', '&']; + if level == OPERATORS.len() { + return self.unary(); + } + let mut left = self.binary(level + 1)?; + loop { + self.skip(); + if self.chars.peek() != Some(&OPERATORS[level]) { + return Ok(left); + } + self.chars.next(); + let right = self.binary(level + 1)?; + let node = match OPERATORS[level] { + '|' => Bool::Or([left, right]), + '^' => Bool::Xor([left, right]), + _ => Bool::And([left, right]), + }; + left = self.expression.add(node); + } + } + fn unary(&mut self) -> eyre::Result { + self.skip(); + match self.chars.peek() { + Some('~') => { + self.chars.next(); + let inner = self.unary()?; + Ok(self.expression.add(Bool::Not(inner))) + } + Some('(') => { + self.chars.next(); + let inner = self.binary(0)?; + self.skip(); + ensure!(self.chars.next() == Some(')'), "missing `)`"); + Ok(inner) + } + Some(c) if c.is_alphanumeric() || *c == '_' => { + let mut name = String::new(); + while let Some(&c) = self.chars.peek() { + if !(c.is_alphanumeric() || c == '_') { + break; + } + name.push(c); + self.chars.next(); + } + Ok(self.expression.add(Bool::Var(Symbol::from(name)))) + } + other => bail!("unexpected {other:?}"), + } + } + } + let mut parser = Parser { + chars: text.chars().peekable(), + expression: RecExpr::default(), + }; + parser.binary(0)?; + parser.skip(); + ensure!(parser.chars.next().is_none(), "trailing text in `{text}`"); + Ok(parser.expression) +} diff --git a/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl new file mode 100644 index 00000000..9ba8054b --- /dev/null +++ b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl @@ -0,0 +1,75 @@ +rsdsl 2; +model egraph_extract; + +// Exact extraction of a NOR netlist from a saturated Boolean e-graph +// (egraph.rs). Every e-class is a function of the inputs; its nodes are the +// ways to build it from other classes: an input, a NOT of one class (a +// torch), or an OR of two (dust and blocks, free). Picking one node in every +// class the outputs need gives a netlist; shared classes are built once. + +domain Class: int; +domain Node: int; +domain Tick: int; // 0..=levels + +fact node_class(Node, Class); // every buildable node and its class +fact edge(Node, Class, Class); // a node, its class, and a child class +fact gate(Node); // a NOT: one torch, one tick +fact or_node(Node); // an OR: one more input on a NOR +fact root(Class); // an output + +param levels: int = 16; +param max_depth: int? = none; +param gate_cost: int = 1; +param depth_cost: int = 0; +// Wide NORs are hard to build in a narrow box: every input is a signal that +// has to reach the torch's block, so `or_cost` charges each OR node. +param or_cost: int = 0; + +var Pick[n: Node]; +var Need[c: Class]; + +// Ticks from the inputs: a NOT adds one, an OR none. Children come strictly +// before a NOT, so picks cannot loop through torches; an OR loop would join +// classes with the same function, which the e-graph already merged (self +// loops are left out of `edge`). +@encoding(order) +int Depth[c: Class] in 0..=levels; + +// An output is a torch: the netlist names a gate for it (an OR output would +// become a NOR and a NOT there, two torches the count would miss). +rule "출력은 만들어야 하고, 토치임" { + forall c: Class where root(c) { + require Need[c]; + require any(Pick[n] for (n, k) in node_class where k == c and gate(n)); + } +} + +rule "만들 클래스는 노드 하나를 고름" { + forall c: Class { + require Need[c] -> any(Pick[n] for (n, k) in node_class where k == c); + require at_most_one(Pick[n] for (n, k) in node_class where k == c); + } +} + +rule "고른 노드의 자식도 만들고, 더 먼저 도착함" { + forall (n, k, c) in edge { + require Pick[n] -> Need[c]; + if gate(n) { + require Pick[n] -> Depth[c] < Depth[k]; + } else { + require Pick[n] -> Depth[c] <= Depth[k]; + } + } +} + +rule "출력 깊이 상한" { + if has(max_depth) { + forall c: Class where root(c) { + require Depth[c] <= max_depth; + } + } +} + +minimize gate_cost * count(Pick[n] for n: Node where gate(n)) + + or_cost * count(Pick[n] for n: Node where or_node(n)) + + depth_cost * count(Depth[c] >= t for c: Class, t: Tick where root(c) and t >= 1); diff --git a/src/transform/place_and_route/local_placer/exact/mod.rs b/src/transform/place_and_route/local_placer/exact/mod.rs index 0e4d4092..0507088f 100644 --- a/src/transform/place_and_route/local_placer/exact/mod.rs +++ b/src/transform/place_and_route/local_placer/exact/mod.rs @@ -21,6 +21,7 @@ mod compact; mod construct; mod dimacs; mod dsl; +mod egraph; mod encode; mod layout; mod netlist; @@ -40,6 +41,7 @@ use std::time::{Duration, Instant}; pub use compact::{AttemptTime, CompactionConfig, CompactionReport}; pub use construct::{ConstructionConfig, ConstructionReport, GateOrder}; pub use dimacs::DimacsComments; +pub use egraph::{netlist_depths, signature, Exploration, ExtractOptions, Extraction, Limits, Weights}; pub use encode::CellKind; pub use layout::{ExactLayout, InputPolicy, OutputPolicy}; pub use netlist::{Net, NetDriver, NetId, NorNetlist}; @@ -394,6 +396,14 @@ impl ExactLocalPlacer { }) } + /// A placer for a netlist built elsewhere (an e-graph extraction, say). + pub fn from_netlist(netlist: NorNetlist) -> Self { + Self { + netlist, + name: "exact-local-cell".to_owned(), + } + } + pub fn with_name(mut self, name: impl Into) -> Self { self.name = name.into(); self diff --git a/src/transform/place_and_route/local_placer/exact/netlist.rs b/src/transform/place_and_route/local_placer/exact/netlist.rs index 84d2aacc..50772beb 100644 --- a/src/transform/place_and_route/local_placer/exact/netlist.rs +++ b/src/transform/place_and_route/local_placer/exact/netlist.rs @@ -151,7 +151,7 @@ impl NorNetlist { Ok(netlist) } - fn check_acyclic(&self) -> eyre::Result<()> { + pub(super) fn check_acyclic(&self) -> eyre::Result<()> { let mut state = vec![0u8; self.nets.len()]; fn visit(netlist: &NorNetlist, net: NetId, state: &mut [u8]) -> eyre::Result<()> { match state[net] { diff --git a/src/transform/place_and_route/local_placer/exact/tests.rs b/src/transform/place_and_route/local_placer/exact/tests.rs index 6ab12c06..b90b8b79 100644 --- a/src/transform/place_and_route/local_placer/exact/tests.rs +++ b/src/transform/place_and_route/local_placer/exact/tests.rs @@ -2030,7 +2030,7 @@ fn print_attempt_times(prefix: &str, report: &CompactionReport) { } /// Construction plus compaction for small circuits: -/// `CIRCUIT=mux2|half-adder|adder2|adder2-nor|mux4|full-adder CIRCUIT_WIDTH=2 +/// `CIRCUIT=mux2|half-adder|adder2|adder2-nor|mux4|full-adder|egraph-full-adder CIRCUIT_WIDTH=2 /// CIRCUIT_HEIGHT=10 CIRCUIT_STEP_SECONDS=60 CIRCUIT_COMPACT_SECONDS=300 /// CIRCUIT_SEED=1 CIRCUIT_WORKERS=8 CIRCUIT_WRITE=`; `CIRCUIT_NETLIST_ONLY=1` stops /// after printing the NOR netlist and its live-net counts; @@ -2047,8 +2047,29 @@ fn diagnose_construct_circuit() -> eyre::Result<()> { .with_test_writer() .try_init(); let circuit = std::env::var("CIRCUIT").unwrap_or_else(|_| "mux2".to_owned()); - let graph = circuit_graph(&circuit)?; - let placer = ExactLocalPlacer::new(&graph)?.with_name(format!("exact-{circuit}")); + // `egraph-full-adder`: the cheapest netlist the e-graph holds + // (`Exploration::extract_exact`) within `EGRAPH_DEPTH` (any), with + // `EGRAPH_OR_COST` (0) per OR node. + let placer = match circuit.as_str() { + "egraph-full-adder" => { + let (inputs, outputs) = full_adder_functions(); + let exploration = Exploration::new(&inputs, &outputs, Limits::default())?; + let options = ExtractOptions { + max_depth: std::env::var("EGRAPH_DEPTH") + .ok() + .map(|depth| depth.parse::()) + .transpose()?, + or_cost: env_usize("EGRAPH_OR_COST", 0), + ..Default::default() + }; + let extraction = exploration + .extract_exact(&options)? + .ok_or_else(|| eyre::eyre!("no netlist for {options:?}"))?; + ExactLocalPlacer::from_netlist(extraction.netlist) + } + _ => ExactLocalPlacer::new(&circuit_graph(&circuit)?)?, + } + .with_name(format!("exact-{circuit}")); let netlist = placer.netlist(); if circuit.starts_with("adder2") { // Both adder netlists must add: {c1, s1, s0} = a1a0 + b1b0. @@ -3519,3 +3540,154 @@ fn report_rcell_timing() -> eyre::Result<()> { } Ok(()) } + +/// The full adder as functions for the e-graph: `(inputs, outputs)`. +fn full_adder_functions() -> (Vec<&'static str>, Vec<(&'static str, &'static str)>) { + ( + vec!["a", "b", "cin"], + vec![("s", "a^b^cin"), ("cout", "(a&b)|(a&cin)|(b&cin)")], + ) +} + +/// Output functions of a netlist by name, as truth-table rows. +fn output_functions(netlist: &NorNetlist) -> BTreeMap> { + let values = netlist.net_values(); + netlist + .outputs + .iter() + .map(|(name, net)| (name.clone(), values[*net].clone())) + .collect() +} + +/// Netlists extracted from the saturated full adder compute the full adder. +/// Exact extraction needs fewer gates than the hand-written `nor9` (8, proven +/// for this e-graph, against 9) and, at the same 9 gates, half its depth; +/// greedy extraction misses the shared NORs and needs more. +#[test] +fn egraph_netlists_compute_the_full_adder() -> eyre::Result<()> { + let (inputs, outputs) = full_adder_functions(); + let exploration = Exploration::new(&inputs, &outputs, Limits::default())?; + let nor9 = NorNetlist::from_logic_graph(&full_adder_graph("nor9"))?; + let expected = output_functions(&nor9); + let greedy = exploration.extract(Weights { + gates: 1.0, + depth: 0.0, + })?; + assert_eq!(output_functions(&greedy), expected); + let fewest = exploration + .extract_exact(&ExtractOptions::default())? + .expect("a netlist"); + assert_eq!(output_functions(&fewest.netlist), expected); + assert!(fewest.proven); + assert_eq!(fewest.netlist.gates().count(), fewest.cost); + assert!(fewest.cost < nor9.gates().count()); + let within = |depth| ExtractOptions { + max_depth: Some(depth), + ..Default::default() + }; + let shallow = exploration + .extract_exact(&within(3))? + .expect("a netlist within 3 gates"); + assert_eq!(output_functions(&shallow.netlist), expected); + assert!(netlist_depths(&shallow.netlist) + .values() + .all(|&depth| depth <= 3)); + assert!(exploration.extract_exact(&within(2))?.is_none()); + Ok(()) +} + +/// Saturates `EGRAPH_CIRCUIT` (`full-adder`) and prints the e-graph's size +/// and, per weighting, the extracted netlist's gates, depths, and live nets +/// beside `nor9`'s: +/// `cargo test --release --lib explore_egraph_netlists -- --ignored --nocapture`. +#[test] +#[ignore = "experiment; run explicitly with --nocapture"] +fn explore_egraph_netlists() -> eyre::Result<()> { + let (inputs, outputs) = full_adder_functions(); + let limits = Limits { + iterations: env_usize("EGRAPH_ITERATIONS", 12), + nodes: env_usize("EGRAPH_NODES", 50_000), + time: Duration::from_secs(env_usize("EGRAPH_SECONDS", 20) as u64), + }; + let started = std::time::Instant::now(); + let exploration = Exploration::new(&inputs, &outputs, limits)?; + println!( + "EGRAPH classes={} nodes={} iterations={} stop={:?} in {:?}", + exploration.classes(), + exploration.nodes(), + exploration.iterations, + exploration.stop_reason, + started.elapsed() + ); + let describe = |label: &str, netlist: &NorNetlist| { + let gates = construct::gate_order(netlist, GateOrder::SmallestConeFirst); + let live = live_after_each_step(netlist, &gates, &BTreeSet::new()); + let fan_in = netlist + .gates() + .map(|gate| netlist.nets[gate].gate_inputs.len()) + .max() + .unwrap_or(0); + println!( + "EGRAPH {label}: gates={} depths={:?} max_fan_in={fan_in} live_max={} live={live:?}", + netlist.gates().count(), + netlist_depths(netlist), + live.iter().max().unwrap_or(&0) + ); + for gate in netlist.gates() { + let inputs = netlist.nets[gate] + .gate_inputs + .iter() + .map(|&input| netlist.nets[input].name.as_str()) + .collect::>(); + println!("EGRAPH {} = NOR{inputs:?}", netlist.nets[gate].name); + } + }; + describe( + "nor9", + &NorNetlist::from_logic_graph(&full_adder_graph("nor9"))?, + ); + if std::env::var("EGRAPH_GREEDY").is_ok() { + for (gates, depth) in [(1.0, 0.0), (1.0, 1.0), (0.01, 1.0)] { + let netlist = exploration.extract(Weights { gates, depth })?; + describe(&format!("greedy gates*{gates}+depth*{depth}"), &netlist); + } + } + // Exact: the cheapest netlist within each depth, shallowest first, for + // each OR cost (`EGRAPH_OR_COSTS`, `0`). + let seconds = Duration::from_secs(env_usize("EGRAPH_EXTRACT_SECONDS", 60) as u64); + let or_costs = std::env::var("EGRAPH_OR_COSTS") + .unwrap_or_else(|_| "0".to_owned()) + .split(',') + .map(str::parse::) + .collect::, _>>()?; + for or_cost in or_costs { + for depth in (2..=env_usize("EGRAPH_MAX_DEPTH", 8)) + .map(Some) + .chain([None]) + { + let started = std::time::Instant::now(); + let options = ExtractOptions { + max_depth: depth, + or_cost, + time_limit: seconds, + }; + match exploration.extract_exact(&options)? { + Some(extraction) => describe( + &format!( + "exact or_cost={or_cost} depth<={} cost={} proven={} in {:.1?}", + depth.map_or("any".to_owned(), |depth| depth.to_string()), + extraction.cost, + extraction.proven, + started.elapsed() + ), + &extraction.netlist, + ), + None => println!( + "EGRAPH exact or_cost={or_cost} depth<={depth:?}: none in {:.1?}", + started.elapsed() + ), + } + } + } + Ok(()) +} From 0aeff7569b0a04490b41fd488e450a82c80bc2d1 Mon Sep 17 00:00:00 2001 From: rollrat Date: Mon, 5 Oct 2026 16:47:52 +0900 Subject: [PATCH 2/2] Measure e-graph netlists in placement; allow only two-input NORs The e-graph finds full adders with fewer gates (8) or less depth than nor9, so the question was whether placement gains from them. Placed with the same settings, the wide NORs they rely on are what construction cannot handle: steps with a 3- or 4-input NOR ran out of their 60 s repeatedly. The 8-gate and depth-3 netlists found no layout in 3 and 5 restarts; the or_cost 1 netlist (9 gates, depths 4/5, fan-in 3) took 15-16 minutes to construct against nor9's 1-1.5, and then compacted to the best cell of the runs on one seed (88 blocks, 11 ticks) and a poor one on the other. A `binary` extraction option allows only two-input NORs (an OR may not join classes built as ORs). Under it the minimum is nor9 itself, 9 gates at depth 5/6, proven optimal for the e-graph, so every gain over nor9 needs wider NORs and therefore a construction that can build them. docs/egraph_netlists.md records the method, the extractions, the placements, and that as the next step. Co-Authored-By: Claude Opus 5.5 --- AGENTS.md | 1 + docs/egraph_netlists.md | 166 ++++++++++++++++++ .../local_placer/exact/egraph.rs | 7 +- .../local_placer/exact/egraph_extract.rsdsl | 11 ++ .../local_placer/exact/tests.rs | 5 +- 5 files changed, 188 insertions(+), 2 deletions(-) create mode 100644 docs/egraph_netlists.md diff --git a/AGENTS.md b/AGENTS.md index 5c6ae541..68b0828d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -19,6 +19,7 @@ - Exact SAT-based local placer, survey, and construct/compact pipeline: `docs/exact_local_placer.md` - Full-adder tiles that chain into n-bit ripple-carry adders (`CarryTiling`): `docs/carry_tiles.md` - Critical paths in redstone ticks: static timing, delay bounds, and timing-first construction and compaction: `docs/timing_driven_placement.md` +- Equivalent NOR netlists from an e-graph (egg) with exact SAT extraction: `docs/egraph_netlists.md` - Solver modeling DSL (rsdsl v2, crate `crates/rsdsl`): design and parity measurements `docs/solver_dsl_design.md`; grammar and language spec `docs/solver_dsl_grammar.md`; the exact placer's model is `src/transform/place_and_route/local_placer/exact/exact_placer.rsdsl` (grounded by `exact/dsl.rs`) When asked to create or preserve project documentation, add an appropriate file under `docs/` and link it from this file when it is useful for future agents. diff --git a/docs/egraph_netlists.md b/docs/egraph_netlists.md new file mode 100644 index 00000000..b9d3263d --- /dev/null +++ b/docs/egraph_netlists.md @@ -0,0 +1,166 @@ +# Equivalent NOR netlists from an e-graph (2026-10-05) + +The exact placer builds the NOR netlist it is given. Construction places one +gate per step, and the signal vocabulary is the netlist's net functions and +their complements. A hand-written netlist such as the full adder's `nor9` +therefore fixes how many torches there are and how deep the logic runs. +`exact/egraph.rs` searches the equivalent netlists with an e-graph (the `egg` +crate) and extracts the ones worth placing. + +## Saturation + +The language has `~`, `|`, `&`, `^`, and inputs. Only `~` (a torch: one gate, +one redstone tick) and `|` (dust and blocks: free) are built; `&` and `^` +state functions and give the rewrites something to pass through. + +The rules are: + +- commutativity and associativity; +- double negation, idempotence, and absorption; +- De Morgan in both directions; +- AND over OR and OR over AND, both ways; +- XOR as a sum of products and as a product of sums; +- XNOR as XOR with one input negated. + +The analysis gives every e-class its truth table (up to 6 inputs). `modify` +unions any two classes with the same table as soon as the second appears. +Two forms of one function thus always meet, whichever rules produced them, +and the classes are the functions the rules have reached. + +The full adder (`s = a^b^cin`, `cout = ab|a·cin|b·cin`) reaches 230 of the +256 three-input functions: 6,187 nodes, 12 iterations, 73 ms. + +## Extraction + +**Greedy extraction** (`Exploration::extract`) gives each class the node +whose own and inputs' gates (shared ones counted once) and depth weigh +least, until no class changes. It decides class by class, so it misses +NORs that pay off only when several gates share them. On the full adder +every weighting gave the same 13-gate netlist, against `nor9`'s 9. + +**Exact extraction** (`Exploration::extract_exact`) solves the choice with +SAT, from a second rsdsl model, `exact/egraph_extract.rsdsl`: + +- the outputs are needed and are torches (an OR output would become a NOR + and a NOT in the netlist); +- a needed class picks one node, and the classes that node reads are needed + too; +- `Depth` adds a tick per NOT and none per OR, which also rules out loops; + `max_depth` bounds the outputs; +- the objective is the number of picked NOTs, plus `or_cost` per picked + OR (every input of a NOR is a signal to route to its block); +- `binary` allows only NORs of two signals. + +The same CaDiCaL binding as the placer lowers the bound until the minimum +is proven. On the full adder each depth bound took 0.1-0.4 s: + +| Depth bound | Fewest gates (proven) | Depths cout / s | Most nets live at once | +| --- | --- | --- | --- | +| 2 | none | | | +| 3 | 9 | 2 / 3 | 7 | +| 4 and up | 8 | 3 / 4 | 6 | +| `nor9` (by hand) | 9 | 5 / 6 | 4 | + +The 8-gate full adder: + +``` +g3 = NOR(a, b) +g4 = NOR(a, cin, g3) +g5 = NOR(b, cin, g3) +g6 = NOR(a, g3, g4, g5) +g7 = NOR(b, g3, g4, g5) +g8 = NOR(cin, g4, g5) +s = NOR(g6, g7, g8) +cout = NOR(g3, g4, g5) +``` + +With `or_cost` 1 or more, the cheapest netlist has 9 gates and depths 4/5, +one tick faster than `nor9`. Its widest NOR reads 3 signals, and as with +`nor9` at most 4 nets are alive at once: + +``` +g3 = NOR(a, b) +g4 = NOR(a) +g5 = NOR(b) +g6 = NOR(g4, g5) +g7 = NOR(cin, g3, g6) +g8 = NOR(g3, g6, g7) +g9 = NOR(cin, g7) +s = NOR(g8, g9) +cout = NOR(g3, g7) +``` + +With `binary` (two-input NORs only), the minimum is 9 gates at depth 5/6: +`nor9` itself, proven optimal for this e-graph. Depth 5/5 needs 12 gates, +and nothing reaches depth 4. Every gain the e-graph finds over `nor9` uses +wider NORs. + +The minimum holds within this e-graph. A netlist the rules never reach can +still be smaller. + +## Placement + +The circuit harness places the extracted netlists: + +- `CIRCUIT=egraph-full-adder` uses the fewest gates overall; +- `EGRAPH_DEPTH=` uses the fewest gates within depth `n`; +- `EGRAPH_OR_COST=` charges each OR node `w`; +- `EGRAPH_BINARY=1` allows only two-input NORs. + +Full adder, 5 workers, 600 s of compaction, no timing: + +| Netlist | Seed | Construction | Compacted | +| --- | --- | --- | --- | +| `nor9`, fan-in 2 | 1 | 64 s | 2x12x9, 146 blocks, cout 13, s 18 | +| `nor9` | 2 | 96 s | 2x11x10, 148 blocks, cout 11, s 17 | +| `or_cost` 1, 9 gates, fan-in 3 | 1 | 995 s, 3 restarts | 2x15x7, 121 blocks, cout 12, s 19 | +| `or_cost` 1 | 2 | 937 s, 4 restarts | 2x11x9, 88 blocks, cout 7, s 11 | +| 8 gates, fan-in 4 | 1 | no layout in 3 restarts | | +| depth 3, 9 gates, fan-in 4 | 1 | no layout in 5 restarts | | + +- Construction is where wide NORs cost. + - Steps with a 3- or 4-input NOR ran out of their 60 s again and again: + `g4 = NOR(a, cin, g3)`, `cout = NOR(g4, g5, g7)`, and the `or_cost` 1 + netlist's `g7 = NOR(cin, g3, g6)`. + - Every input of such a NOR has to reach one block within a window two + cells wide. + - `nor9`'s two-input NORs construct on the first try in 1-1.5 minutes. +- Once built, the `or_cost` 1 netlist gave the smallest and fastest cell + of these runs (seed 2: 88 blocks, 11 ticks). +- Compaction varies too much from run to run (the 600 s runs did not + converge) to rank the netlists on two seeds. + +Two placement steps had failed as infeasible within 0.1 s, the first time +a new input was placed. Construction offered the new input the cell of a +switch kept from an earlier step, and the fixed switch was read as the new +input's. That is fixed: new inputs skip placed switches, and a fixed +switch belongs to the input whose only site it is. With +`EXACT_DIAGNOSE_INFEASIBLE`, an infeasible step is re-solved with one +requirement dropped at a time, which is how it was found. + +## Next + +- Let construction build a wide NOR in parts, its OR terms first, so + narrow windows can place the netlists with fewer gates. +- Constrain extraction for carry tiles: the carry needs monotone signals + (`carry_tiles.md`). + +## Running + +```sh +cargo test --release --lib egraph_netlists_compute_the_full_adder +cargo test --release --lib explore_egraph_netlists -- --ignored --nocapture +CIRCUIT=egraph-full-adder CIRCUIT_COMPACT_SECONDS=600 \ + cargo test --release --lib diagnose_construct_circuit -- --ignored --nocapture +``` + +`explore_egraph_netlists` takes these knobs: + +- saturation: `EGRAPH_ITERATIONS`, `EGRAPH_NODES`, `EGRAPH_SECONDS`; +- the sweep: `EGRAPH_MAX_DEPTH`, `EGRAPH_OR_COSTS` (comma-separated), + `EGRAPH_BINARY=1`; +- `EGRAPH_EXTRACT_SECONDS`; +- `EGRAPH_GREEDY=1` also prints greedy extractions. + +The circuit harness takes `EGRAPH_DEPTH`, `EGRAPH_OR_COST`, and +`EGRAPH_BINARY`. diff --git a/src/transform/place_and_route/local_placer/exact/egraph.rs b/src/transform/place_and_route/local_placer/exact/egraph.rs index 7749269c..dfa0d9ca 100644 --- a/src/transform/place_and_route/local_placer/exact/egraph.rs +++ b/src/transform/place_and_route/local_placer/exact/egraph.rs @@ -45,6 +45,8 @@ pub struct ExtractOptions { pub max_depth: Option, /// Weight of each OR node (one more input on a NOR) against a gate's 1. pub or_cost: usize, + /// Only NORs of at most two signals. + pub binary: bool, pub time_limit: Duration, } @@ -53,6 +55,7 @@ impl Default for ExtractOptions { Self { max_depth: None, or_cost: 0, + binary: false, time_limit: Duration::from_secs(60), } } @@ -303,6 +306,7 @@ impl Exploration { let ExtractOptions { max_depth, or_cost, + binary, time_limit, } = *options; let egraph = &self.egraph; @@ -349,7 +353,8 @@ impl Exploration { .domain("Node", (0..nodes.len()).map(IValue::from)) .domain("Tick", (0..=levels).map(IValue::from)) .param("levels", levels) - .param("or_cost", or_cost); + .param("or_cost", or_cost) + .param("binary", binary); if let Some(depth) = max_depth { instance.param("max_depth", depth); } diff --git a/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl index 9ba8054b..9e1fc448 100644 --- a/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl +++ b/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl @@ -24,6 +24,9 @@ param depth_cost: int = 0; // Wide NORs are hard to build in a narrow box: every input is a signal that // has to reach the torch's block, so `or_cost` charges each OR node. param or_cost: int = 0; +// Every NOR reads at most two signals: an OR node may only join classes that +// are not themselves built as ORs. +param binary: bool = false; var Pick[n: Node]; var Need[c: Class]; @@ -62,6 +65,14 @@ rule "고른 노드의 자식도 만들고, 더 먼저 도착함" { } } +rule "2입력 NOR만" { + if binary { + forall (n, k, c) in edge where or_node(n) { + require Pick[n] -> not any(Pick[m] for (m, j) in node_class where j == c and or_node(m)); + } + } +} + rule "출력 깊이 상한" { if has(max_depth) { forall c: Class where root(c) { diff --git a/src/transform/place_and_route/local_placer/exact/tests.rs b/src/transform/place_and_route/local_placer/exact/tests.rs index b90b8b79..d820552d 100644 --- a/src/transform/place_and_route/local_placer/exact/tests.rs +++ b/src/transform/place_and_route/local_placer/exact/tests.rs @@ -2049,7 +2049,8 @@ fn diagnose_construct_circuit() -> eyre::Result<()> { let circuit = std::env::var("CIRCUIT").unwrap_or_else(|_| "mux2".to_owned()); // `egraph-full-adder`: the cheapest netlist the e-graph holds // (`Exploration::extract_exact`) within `EGRAPH_DEPTH` (any), with - // `EGRAPH_OR_COST` (0) per OR node. + // `EGRAPH_OR_COST` (0) per OR node, and only 2-input NORs with + // `EGRAPH_BINARY=1`. let placer = match circuit.as_str() { "egraph-full-adder" => { let (inputs, outputs) = full_adder_functions(); @@ -2060,6 +2061,7 @@ fn diagnose_construct_circuit() -> eyre::Result<()> { .map(|depth| depth.parse::()) .transpose()?, or_cost: env_usize("EGRAPH_OR_COST", 0), + binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), ..Default::default() }; let extraction = exploration @@ -3669,6 +3671,7 @@ fn explore_egraph_netlists() -> eyre::Result<()> { let options = ExtractOptions { max_depth: depth, or_cost, + binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), time_limit: seconds, }; match exploration.extract_exact(&options)? {