diff --git a/AGENTS.md b/AGENTS.md index d3b9c396..ed9cf3ea 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -19,7 +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` +- Equivalent NOR netlists from an e-graph (egg) with exact SAT extraction, an experiment record (the code was removed for exact synthesis) that also explains why wide-NOR construction steps time out: `docs/egraph_netlists.md` - Exact synthesis of NOR netlists that windowed construction can build (`exact::synthesize`, `nor_synthesis.rsdsl`): `docs/nor_synthesis.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`) diff --git a/Cargo.lock b/Cargo.lock index 5e783232..533acd1b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8,17 +8,6 @@ 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" @@ -232,24 +221,6 @@ 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" @@ -262,15 +233,6 @@ 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" @@ -332,15 +294,6 @@ 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" @@ -359,9 +312,6 @@ name = "hashbrown" version = "0.12.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" -dependencies = [ - "ahash", -] [[package]] name = "hashbrown" @@ -447,15 +397,6 @@ 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" @@ -791,7 +732,6 @@ dependencies = [ "cadical", "derive_more", "disjoint-set", - "egg", "eyre", "fastanvil", "fastnbt", @@ -968,22 +908,6 @@ 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" @@ -1015,33 +939,13 @@ 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 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", + "thiserror-impl", ] [[package]] @@ -1394,7 +1298,7 @@ dependencies = [ "flate2", "indexmap 2.0.0", "memchr", - "thiserror 2.0.18", + "thiserror", "zopfli", ] diff --git a/Cargo.toml b/Cargo.toml index dd791783..447389f8 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -35,7 +35,6 @@ 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/docs/egraph_netlists.md b/docs/egraph_netlists.md index 5332aa73..c44c90c2 100644 --- a/docs/egraph_netlists.md +++ b/docs/egraph_netlists.md @@ -1,5 +1,16 @@ # Equivalent NOR netlists from an e-graph (2026-10-05) +> **Status (2026-10-10): the e-graph code is removed.** Exact synthesis +> (`nor_synthesis.md`) took its place. Synthesis designs a netlist and its +> construction order together, proves minimum torch counts, and gave the +> improvements (the 2-bit adder about a fifth smaller, the 4:1 mux built for +> the first time). The e-graph's netlists were mostly unbuildable. Its lasting +> results are the diagnosis below ("Why the steps fail") and the +> `or_cost` 1 netlist, which synthesis found again. The measurements here +> were taken at commit `600ad6d`, which still has `exact/egraph.rs`, +> `exact/egraph_extract.rsdsl`, and the harness's `CIRCUIT=egraph-full-adder` +> mode. The 8-gate netlist survives as `WIDE_FULL_ADDER` in `exact/tests.rs`. + 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` @@ -366,6 +377,8 @@ For the full adder in a 2-wide box: ## Running +At commit `600ad6d` (the code is gone since): + ```sh cargo test --release --lib egraph_netlists_compute_the_full_adder cargo test --release --lib explore_egraph_netlists -- --ignored --nocapture @@ -373,24 +386,18 @@ CIRCUIT=egraph-full-adder CIRCUIT_COMPACT_SECONDS=600 \ cargo test --release --lib diagnose_construct_circuit -- --ignored --nocapture ``` -`explore_egraph_netlists` takes these knobs: +`explore_egraph_netlists` took 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`, -`EGRAPH_BINARY`, `EGRAPH_SPLIT`, `EGRAPH_CHAIN`, and -`CIRCUIT_ORDER=min-live`, besides the box and step knobs -(`CIRCUIT_HEIGHT`, `CIRCUIT_MAX_WINDOW`, `CIRCUIT_STEP_SECONDS`, -`CIRCUIT_RESTART_SECONDS`). `CIRCUIT_NETLIST_ONLY=1` prints the netlist, -its live nets and its continuing inputs, and stops. The harness also prints -each construction step: the gate, the input cases it is on in, its -continuing inputs, and the nets alive after it. - -To see why a step times out, set `EXACT_DIAGNOSE_UNKNOWN=1` (with -`EXACT_DIAGNOSE_VARIANT_SECONDS`, default 20). To solve that step again -for longer and write it as DIMACS, set -`EXACT_DIAGNOSE_FAILED_STEP=` (with `EXACT_DIAGNOSE_SECONDS`). +- `EGRAPH_GREEDY=1` also printed greedy extractions. + +The circuit harness took `EGRAPH_DEPTH`, `EGRAPH_OR_COST`, +`EGRAPH_BINARY`, `EGRAPH_SPLIT` and `EGRAPH_CHAIN`. + +Still available: any netlist runs through the harness as text +(`CIRCUIT=netlist CIRCUIT_NETLIST=...`, `CIRCUIT_CHAIN=` for the support +block stages), with `CIRCUIT_ORDER=min-live`, the box and step knobs, the +per-step printout and the step diagnostics (`nor_synthesis.md`, "Running"). diff --git a/docs/nor_synthesis.md b/docs/nor_synthesis.md index 363303fd..9515ddff 100644 --- a/docs/nor_synthesis.md +++ b/docs/nor_synthesis.md @@ -182,3 +182,20 @@ CIRCUIT=netlist CIRCUIT_ORDER=index CIRCUIT_NETLIST='g3=NOR(cin); ...' \ `CIRCUIT_NETLIST` takes `NorNetlist::to_text`'s form. A name read before it is defined is an input, and a net nothing reads is an output. +`CIRCUIT_CHAIN=` builds NORs of more than `n` signals in stages on one +support block (`NorNetlist::chain_wide_gates`); a synthesized netlist has its +OR stages already. Targets are expressions over the inputs (`~ & ^ |`, +tightest first; `synthesis::truth_table`). + +The harness knobs: `CIRCUIT_HEIGHT`, `CIRCUIT_MAX_WINDOW`, +`CIRCUIT_STEP_SECONDS`, `CIRCUIT_RESTART_SECONDS`, `CIRCUIT_ORDER` +(`index`, `min-live`, smallest cone first otherwise). `CIRCUIT_NETLIST_ONLY=1` +prints the netlist, its live nets and continuing inputs per gate order, and +each construction step (the gate, the input cases it is on in, its +continuing inputs, the nets alive after it), then stops. + +To see why a step times out, set `EXACT_DIAGNOSE_UNKNOWN=1` (with +`EXACT_DIAGNOSE_VARIANT_SECONDS`, default 20): the first timed-out step is +solved again with one requirement dropped at a time. To solve that step +again for longer and write it as DIMACS, set +`EXACT_DIAGNOSE_FAILED_STEP=` (with `EXACT_DIAGNOSE_SECONDS`). diff --git a/src/transform/place_and_route/local_placer/exact/egraph.rs b/src/transform/place_and_route/local_placer/exact/egraph.rs deleted file mode 100644 index f47b315e..00000000 --- a/src/transform/place_and_route/local_placer/exact/egraph.rs +++ /dev/null @@ -1,799 +0,0 @@ -//! 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, Objective}; - -use super::cnf::{Cnf, Lit}; -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, - /// Only NORs of at most two signals. - pub binary: bool, - /// Build a NOR of more than two signals from OR nets: the two halves of - /// its OR, each an OR net if wider than one signal, so construction - /// places the merges as steps of their own before the torch. - pub split_wide: bool, - pub time_limit: Duration, -} - -impl Default for ExtractOptions { - fn default() -> Self { - Self { - max_depth: None, - or_cost: 0, - binary: false, - split_wide: false, - 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, -} - -/// The extraction model on a solver, with what reads its answers back. -struct GroundedExtraction { - nodes: Vec<(Id, Bool)>, - picks: Vec, - objective: Objective, - /// `-at_least[b]` requires cost `<= offset + b` (`objective_counter`). - at_least: Vec, - solver: SatSolver, -} - -impl GroundedExtraction { - /// Assumptions for a cost of at most `cost`; `None` if none is that low. - fn at_most(&self, cost: i64) -> Option> { - let bound = cost - self.objective.offset; - if bound < 0 { - return None; - } - Some( - self.at_least - .get(bound as usize) - .map(|&lit| vec![-lit]) - .unwrap_or_default(), - ) - } - - fn cost(&self) -> i64 { - self.objective.cost(|lit| self.solver.value(lit)) - } - - /// The picked nodes by class. - fn chosen(&self) -> HashMap { - self.nodes - .iter() - .zip(&self.picks) - .filter(|(_, &lit)| self.solver.value(lit)) - .map(|((class, node), _)| { - let choice = Choice { - node: node.clone(), - gates: BTreeSet::new(), - depth: 0, - }; - (*class, choice) - }) - .collect() - } -} - -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, false) - } - - /// 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 mut grounded = self.ground_extraction(options)?; - let stop = AtomicBool::new(false); - let signal = StopSignal { - stop: &stop, - deadline: Some(Instant::now() + options.time_limit), - restart: None, - }; - let mut best = None::<(i64, HashMap)>; - let mut proven = false; - loop { - let assumptions = match &best { - None => Vec::new(), - Some((cost, _)) => match grounded.at_most(cost - 1) { - Some(assumptions) => assumptions, - None => { - proven = true; - break; - } - }, - }; - match grounded.solver.solve(&assumptions, &signal) { - SolveResult::Sat => best = Some((grounded.cost(), grounded.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, options.split_wide)?, - cost: cost as usize, - proven, - })) - } - - /// `egraph_extract.rsdsl` grounded over this e-graph, on a solver. - fn ground_extraction(&self, options: &ExtractOptions) -> eyre::Result { - let ExtractOptions { - max_depth, - or_cost, - binary, - .. - } = *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) - .param("binary", binary); - 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 ground = GroundOptions { - guards: false, - provenance: false, - positive_or_aux: false, - no_fold: false, - }; - let mut program = extract_model() - .ground(&instance, ground) - .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); - Ok(GroundedExtraction { - nodes, - picks, - objective, - at_least, - solver, - }) - } - - 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, split: bool) -> eyre::Result { - let mut builder = Builder { - exploration: self, - best, - split, - 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(), - net_of_class: HashMap::new(), - }; - let mut outputs = Vec::new(); - for (name, root) in &self.outputs { - let (root, node) = builder.choice(*root)?; - let output = match node { - Bool::Var(_) => bail!("output `{name}` is an input"), - Bool::Not(_) => builder.net(root, 0)?, - // An OR output needs a driver: a NOT over the NOR of its terms. - _ => { - let inputs = builder.sources(root, 0)?; - let nor = builder.push(NetDriver::Gate, inputs); - builder.nets[nor].name = format!("{name}_n"); - builder.push(NetDriver::Gate, BTreeSet::from([nor])) - } - }; - outputs.push((name.clone(), output)); - } - let mut nets = builder.nets; - 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) - } -} - -/// Turns one chosen node per class into nets. -struct Builder<'a> { - exploration: &'a Exploration, - best: &'a HashMap, - /// NORs of more than two signals read OR nets instead (see `ExtractOptions::split_wide`). - split: bool, - nets: Vec, - net_of_class: HashMap, -} - -impl Builder<'_> { - fn choice(&self, class: Id) -> eyre::Result<(Id, Bool)> { - let class = self.exploration.egraph.find(class); - let choice = self - .best - .get(&class) - .ok_or_else(|| eyre!("class {class} has no buildable form"))?; - Ok((class, choice.node.clone())) - } - - fn push(&mut self, driver: NetDriver, inputs: BTreeSet) -> NetId { - let index = self.nets.len(); - let prefix = if driver == NetDriver::Or { "o" } else { "g" }; - self.nets.push(Net { - name: format!("{prefix}{index}"), - node_id: index, - driver, - gate_inputs: inputs.into_iter().collect(), - }); - index - } - - /// The nets whose OR a class is (one net unless it chose an OR). - fn sources(&mut self, class: Id, depth: usize) -> eyre::Result> { - ensure!(depth < 256, "extraction recursed too deep"); - let (class, node) = self.choice(class)?; - match node { - Bool::Or([a, b]) => { - let mut set = self.sources(a, depth + 1)?; - set.extend(self.sources(b, depth + 1)?); - Ok(set) - } - _ => Ok(BTreeSet::from([self.net(class, depth + 1)?])), - } - } - - /// The net of a class that chose an input or a NOT. - fn net(&mut self, class: Id, depth: usize) -> eyre::Result { - ensure!(depth < 256, "extraction recursed too deep"); - if let Some(&net) = self.net_of_class.get(&class) { - return Ok(net); - } - let net = match self.choice(class)?.1 { - Bool::Var(symbol) => self - .nets - .iter() - .position(|net| net.driver == NetDriver::Input(symbol.to_string())) - .ok_or_else(|| eyre!("unknown input {symbol}"))?, - Bool::Not(a) => { - let inputs = self.gate_inputs(a, depth + 1)?; - self.push(NetDriver::Gate, inputs) - } - other => bail!("class {class} chose {other} as a net"), - }; - self.net_of_class.insert(class, net); - Ok(net) - } - - /// What a NOT of `class` reads: the leaves of its OR, or, with `split` - /// and more than two leaves, the OR's two halves, each an OR net if it - /// is an OR itself. - fn gate_inputs(&mut self, class: Id, depth: usize) -> eyre::Result> { - let leaves = self.sources(class, depth)?; - if !self.split || leaves.len() <= 2 { - return Ok(leaves); - } - match self.choice(class)?.1 { - Bool::Or([a, b]) => Ok(BTreeSet::from([ - self.term(a, depth + 1)?, - self.term(b, depth + 1)?, - ])), - _ => Ok(leaves), - } - } - - /// The net of a class, an OR net if it chose an OR. - fn term(&mut self, class: Id, depth: usize) -> eyre::Result { - ensure!(depth < 256, "extraction recursed too deep"); - let (class, node) = self.choice(class)?; - let Bool::Or([a, b]) = node else { - return self.net(class, depth + 1); - }; - if let Some(&net) = self.net_of_class.get(&class) { - return Ok(net); - } - let inputs = BTreeSet::from([self.term(a, depth + 1)?, self.term(b, depth + 1)?]); - let net = self.push(NetDriver::Or, inputs); - self.net_of_class.insert(class, net); - Ok(net) - } -} - -/// The truth table of `expression` over `inputs`: bit `k` is its value in -/// case `k`, where bit `i` of `k` is `inputs[i]`. -pub fn truth_table(inputs: &[&str], expression: &str) -> eyre::Result { - let mut egraph = EGraph::new(TruthTable::new(inputs)?); - let id = egraph.add_expr(&parse(expression)?); - Ok(egraph[id].data) -} - -/// Gates on the slowest path to each output (OR nets free, NOT one). -pub fn netlist_depths(netlist: &NorNetlist) -> BTreeMap { - let mut depth = vec![0usize; netlist.nets.len()]; - for net in netlist.topological_order() { - let latest = netlist.nets[net] - .gate_inputs - .iter() - .map(|&input| depth[input]) - .max() - .unwrap_or(0); - depth[net] = match netlist.nets[net].driver { - NetDriver::Input(_) => 0, - NetDriver::Gate => latest + 1, - NetDriver::Or => latest, - }; - } - 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 deleted file mode 100644 index 9e1fc448..00000000 --- a/src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl +++ /dev/null @@ -1,86 +0,0 @@ -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; -// 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]; - -// 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 "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) { - 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 29942049..88030fd8 100644 --- a/src/transform/place_and_route/local_placer/exact/mod.rs +++ b/src/transform/place_and_route/local_placer/exact/mod.rs @@ -21,7 +21,6 @@ mod compact; mod construct; mod dimacs; mod dsl; -mod egraph; mod encode; mod layout; mod netlist; @@ -42,9 +41,6 @@ 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}; 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 94391cfb..c50ecfc4 100644 --- a/src/transform/place_and_route/local_placer/exact/netlist.rs +++ b/src/transform/place_and_route/local_placer/exact/netlist.rs @@ -324,6 +324,28 @@ impl NorNetlist { Ok(netlist) } + /// Torches on the slowest path to each output (OR nets add none). + pub fn output_depths(&self) -> BTreeMap { + let mut depth = vec![0usize; self.nets.len()]; + for net in self.topological_order() { + let latest = self.nets[net] + .gate_inputs + .iter() + .map(|&input| depth[input]) + .max() + .unwrap_or(0); + depth[net] = match self.nets[net].driver { + NetDriver::Input(_) => 0, + NetDriver::Gate => latest + 1, + NetDriver::Or => latest, + }; + } + self.outputs + .iter() + .map(|(name, net)| (name.clone(), depth[*net])) + .collect() + } + pub fn input_names(&self) -> Vec { let mut names = self .nets diff --git a/src/transform/place_and_route/local_placer/exact/synthesis.rs b/src/transform/place_and_route/local_placer/exact/synthesis.rs index 02d1dc65..eff21f6e 100644 --- a/src/transform/place_and_route/local_placer/exact/synthesis.rs +++ b/src/transform/place_and_route/local_placer/exact/synthesis.rs @@ -18,7 +18,6 @@ use eyre::{ensure, eyre}; use rsdsl::{GroundOptions, IValue, Instance, Model}; use super::cnf::Cnf; -use super::egraph::truth_table; use super::netlist::{Net, NetDriver, NorNetlist}; use super::solver::{SatSolver, SolveResult, StopSignal}; @@ -75,7 +74,7 @@ pub enum SynthesisOutcome { } /// The netlist of `options.steps` steps computing `outputs` (expressions over -/// `inputs`, as in `Exploration::new`) with the fewest torches, within the +/// `inputs`, see `truth_table`) with the fewest torches, within the /// live and depth bounds. Construction should take its nets in index order /// (`GateOrder::NetIndex`), the order the bound holds for. pub fn synthesize( @@ -281,3 +280,107 @@ fn check_outputs( } Ok(()) } + +/// The truth table of `expression` over `inputs`: bit `k` is its value in +/// case `k`, where bit `i` of `k` is `inputs[i]`. The expression uses input +/// names, parentheses, and `~ & ^ |`, tightest first. +pub fn truth_table(inputs: &[&str], expression: &str) -> eyre::Result { + ensure!(inputs.len() <= 6, "a truth table holds at most 6 inputs"); + let cases = 1usize << inputs.len(); + let mut parser = Parser { + text: expression.as_bytes(), + at: 0, + inputs, + cases, + full: if cases == 64 { + u64::MAX + } else { + (1u64 << cases) - 1 + }, + }; + let table = parser.binary(0)?; + parser.skip(); + ensure!( + parser.at == parser.text.len(), + "unexpected `{}` in `{expression}`", + &expression[parser.at..] + ); + Ok(table) +} + +/// Recursive descent over `truth_table`'s expressions, one table per term. +struct Parser<'a> { + text: &'a [u8], + at: usize, + inputs: &'a [&'a str], + cases: usize, + full: u64, +} + +impl Parser<'_> { + /// Binary operators from the loosest: `|`, `^`, `&`. + const LEVELS: [u8; 3] = [b'|', b'^', b'&']; + + fn skip(&mut self) { + while self.text.get(self.at).is_some_and(u8::is_ascii_whitespace) { + self.at += 1; + } + } + + fn binary(&mut self, level: usize) -> eyre::Result { + if level == Self::LEVELS.len() { + return self.unary(); + } + let mut table = self.binary(level + 1)?; + loop { + self.skip(); + if self.text.get(self.at) != Some(&Self::LEVELS[level]) { + return Ok(table); + } + self.at += 1; + let right = self.binary(level + 1)?; + table = match Self::LEVELS[level] { + b'|' => table | right, + b'^' => table ^ right, + _ => table & right, + }; + } + } + + fn unary(&mut self) -> eyre::Result { + self.skip(); + match self.text.get(self.at) { + Some(b'~') => { + self.at += 1; + Ok(!self.unary()? & self.full) + } + Some(b'(') => { + self.at += 1; + let table = self.binary(0)?; + self.skip(); + ensure!(self.text.get(self.at) == Some(&b')'), "missing `)`"); + self.at += 1; + Ok(table) + } + _ => { + let start = self.at; + while self + .text + .get(self.at) + .is_some_and(|&c| c.is_ascii_alphanumeric() || c == b'_') + { + self.at += 1; + } + let name = std::str::from_utf8(&self.text[start..self.at])?; + let index = self + .inputs + .iter() + .position(|&input| input == name) + .ok_or_else(|| eyre!("unknown input `{name}`"))?; + Ok((0..self.cases) + .filter(|case| case >> index & 1 == 1) + .fold(0, |table, case| table | 1 << case)) + } + } + } +} 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 78fb5623..b1442904 100644 --- a/src/transform/place_and_route/local_placer/exact/tests.rs +++ b/src/transform/place_and_route/local_placer/exact/tests.rs @@ -278,10 +278,10 @@ fn gate_order_from_env(name: &str) -> GateOrder { } } -/// With `EGRAPH_CHAIN=`, NORs of more than `n` signals are built in +/// With `CIRCUIT_CHAIN=`, NORs of more than `n` signals are built in /// stages on one support block (`NorNetlist::chain_wide_gates`). fn chain_from_env(netlist: NorNetlist) -> eyre::Result { - match std::env::var("EGRAPH_CHAIN") { + match std::env::var("CIRCUIT_CHAIN") { Ok(fan_in) => netlist.chain_wide_gates(fan_in.parse()?), Err(_) => Ok(netlist), } @@ -2137,7 +2137,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|egraph-full-adder CIRCUIT_WIDTH=2 +/// `CIRCUIT=mux2|half-adder|adder2|adder2-nor|mux4|full-adder|netlist CIRCUIT_WIDTH=2 /// CIRCUIT_HEIGHT=10 CIRCUIT_MAX_WINDOW=4 CIRCUIT_STEP_SECONDS=60 CIRCUIT_RESTART_SECONDS=600 /// CIRCUIT_COMPACT_SECONDS=300 /// CIRCUIT_SEED=1 CIRCUIT_WORKERS=8 CIRCUIT_WRITE=`; `CIRCUIT_NETLIST_ONLY=1` stops @@ -2155,33 +2155,10 @@ fn diagnose_construct_circuit() -> eyre::Result<()> { .with_test_writer() .try_init(); 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, only 2-input NORs with - // `EGRAPH_BINARY=1`, wide NORs built from OR nets with `EGRAPH_SPLIT=1`, - // and NORs of more than `EGRAPH_CHAIN` signals built in stages on one - // support block (`NorNetlist::chain_wide_gates`). 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), - binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), - split_wide: std::env::var("EGRAPH_SPLIT").as_deref() == Ok("1"), - ..Default::default() - }; - let extraction = exploration - .extract_exact(&options)? - .ok_or_else(|| eyre::eyre!("no netlist for {options:?}"))?; - ExactLocalPlacer::from_netlist(chain_from_env(extraction.netlist)?) - } // `netlist`: the netlist in `CIRCUIT_NETLIST`, in `NorNetlist::to_text`'s - // form (`screen_egraph_netlists` prints them so), with `EGRAPH_CHAIN`. + // form (`synthesize_buildable_circuits` prints them so), with + // `CIRCUIT_CHAIN`. "netlist" => { let text = std::env::var("CIRCUIT_NETLIST") .map_err(|_| eyre::eyre!("CIRCUIT=netlist needs CIRCUIT_NETLIST"))?; @@ -3707,7 +3684,7 @@ fn report_rcell_timing() -> eyre::Result<()> { Ok(()) } -/// The full adder as functions for the e-graph: `(inputs, outputs)`. +/// The full adder as output expressions over its inputs: `(inputs, outputs)`. fn full_adder_functions() -> (Vec<&'static str>, Vec<(&'static str, &'static str)>) { ( vec!["a", "b", "cin"], @@ -3725,62 +3702,6 @@ fn output_functions(netlist: &NorNetlist) -> BTreeMap> { .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()); - // Split, the 8 gates read at most two signals each, OR nets included. - let split = exploration - .extract_exact(&ExtractOptions { - split_wide: true, - ..Default::default() - })? - .expect("a netlist"); - assert_eq!(output_functions(&split.netlist), expected); - assert_eq!(split.netlist.gates().count(), fewest.cost); - assert!(split - .netlist - .nets - .iter() - .all(|net| net.gate_inputs.len() <= 2)); - assert!(split - .netlist - .nets - .iter() - .any(|net| net.driver == NetDriver::Or)); - Ok(()) -} - /// The circuits `synthesize_buildable_circuits` takes, as output expressions /// over the inputs. `adder2` is the 2-bit adder without carry in, the /// function of the harness's `adder2` and hand-written `adder2-nor`. @@ -3832,7 +3753,7 @@ fn synthesized_full_adders_stay_buildable() -> eyre::Result<()> { assert_eq!(order.len(), steps); let live = live_after_each_step(netlist, &order, &BTreeSet::new()); assert!(live.iter().all(|&live| live <= 4), "{live:?}"); - let found_depths = netlist_depths(netlist); + let found_depths = netlist.output_depths(); assert!(found_depths["cout"] <= depths[0], "{found_depths:?}"); assert!(found_depths["s"] <= depths[1], "{found_depths:?}"); } @@ -3862,17 +3783,43 @@ fn synthesized_small_circuits_need_fewer_torches() -> eyre::Result<()> { Ok(()) } +/// Synthesis reads its targets as expressions: `~` binds tightest, then +/// `&`, `^` and `|`; bit `k` of a table is case `k`, bit `i` of `k` input `i`. +#[test] +fn synthesis_truth_tables_follow_precedence() -> eyre::Result<()> { + use super::synthesis::truth_table; + let inputs = ["a", "b", "c"]; + let table = |expression| truth_table(&inputs, expression); + let bit = |case: usize, index: usize| case >> index & 1 == 1; + let expected = |f: fn(bool, bool, bool) -> bool| { + (0..8usize) + .filter(|&case| f(bit(case, 0), bit(case, 1), bit(case, 2))) + .fold(0u64, |table, case| table | 1 << case) + }; + assert_eq!(table("a^b^c")?, expected(|a, b, c| a ^ b ^ c)); + assert_eq!(table("a|b&c")?, expected(|a, b, c| a | (b & c))); + assert_eq!(table("~a&b")?, expected(|a, b, _| !a & b)); + assert_eq!(table("~(a|b) ^ c")?, expected(|a, b, c| !(a | b) ^ c)); + assert!(table("a&d").is_err()); + assert!(table("(a|b").is_err()); + Ok(()) +} + +/// The 8-gate full adder an e-graph found (`docs/egraph_netlists.md`), with +/// NORs of up to four signals. +const WIDE_FULL_ADDER: &str = "g3=NOR(a,b); g4=NOR(a,cin,g3); g5=NOR(b,cin,g3); \ + g6=NOR(a,g3,g4,g5); g7=NOR(cin,g4,g5); g8=NOR(b,g3,g5); s=NOR(g6,g7,g8); \ + cout=NOR(g3,g4,g5)"; + /// Chaining wide NORs keeps every function, leaves no NOR wider than two /// signals, and construction places each chain's stages consecutively, /// right before the NOR they end in. #[test] fn chained_wide_gates_keep_functions_and_stay_together() -> eyre::Result<()> { - let (inputs, outputs) = full_adder_functions(); - let exploration = Exploration::new(&inputs, &outputs, Limits::default())?; - let wide = exploration - .extract_exact(&ExtractOptions::default())? - .expect("a netlist") - .netlist; + let wide = NorNetlist::from_text(WIDE_FULL_ADDER)?; + let nor9 = NorNetlist::from_logic_graph(&full_adder_graph("nor9"))?; + assert_eq!(output_functions(&wide), output_functions(&nor9)); + assert_eq!(wide.gates().count(), 8); assert!(wide .gates() .any(|gate| wide.nets[gate].gate_inputs.len() > 2)); @@ -3912,123 +3859,6 @@ fn chained_wide_gates_keep_functions_and_stay_together() -> eyre::Result<()> { 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 min_live = live_after_each_step( - netlist, - &construct::gate_order(netlist, GateOrder::MinLive), - &BTreeSet::new(), - ); - println!( - "EGRAPH {label}: min-live order live_max={} live={min_live:?}", - min_live.iter().max().unwrap_or(&0) - ); - 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); - let ors = netlist - .nets - .iter() - .filter(|net| net.driver == NetDriver::Or) - .count(); - println!( - "EGRAPH {label}: gates={} or_nets={ors} depths={:?} max_fan_in={fan_in} live_max={} live={live:?}", - netlist.gates().count(), - netlist_depths(netlist), - live.iter().max().unwrap_or(&0) - ); - for net in gates { - let inputs = netlist.nets[net] - .gate_inputs - .iter() - .map(|&input| netlist.nets[input].name.as_str()) - .collect::>(); - let kind = if netlist.nets[net].driver == NetDriver::Or { - "OR" - } else { - "NOR" - }; - println!("EGRAPH {} = {kind}{inputs:?}", netlist.nets[net].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, - binary: std::env::var("EGRAPH_BINARY").as_deref() == Ok("1"), - split_wide: std::env::var("EGRAPH_SPLIT").as_deref() == Ok("1"), - 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(()) -} - /// Synthesizes circuits that construction can build (`exact::synthesize`): /// `SYNTH_CIRCUIT` (`full-adder`; see `synthesis_functions`), for each step /// count in `SYNTH_STEPS` (`9..=13`, as `lo..=hi`), the fewest torches with @@ -4077,7 +3907,7 @@ fn synthesize_buildable_circuits() -> eyre::Result<()> { "SYNTH steps={steps} torches={} proven={} depths={:?} live={:?} continuing={:?} ({seconds:.1}s)\n {}", found.torches, found.proven, - netlist_depths(netlist), + netlist.output_depths(), live_after_each_step(netlist, &order, &none), continuing_inputs_each_step(netlist, &order, &none), netlist.to_text()