From 89669089044c836137c3fb5b2952fdf35eaafa34 Mon Sep 17 00:00:00 2001 From: rollrat Date: Sat, 10 Oct 2026 09:00:53 +0900 Subject: [PATCH] Remove the e-graph search now that synthesis replaces it The e-graph experiment (#61) found full adders with fewer gates or less depth, but nearly all of them were unbuildable. Its lasting results were the diagnosis of why construction steps time out and the exact synthesis built on it. Synthesis designs netlists that are buildable by construction, proves minimum torch counts, and gave the actual gains: a 2-bit adder about a fifth smaller and a 4:1 mux built for the first time. The e-graph code had no remaining use but cost about 900 lines and the egg dependency (9 crates). - egraph.rs and egraph_extract.rsdsl are deleted, along with egg. - Synthesis gets its own expression evaluator (synthesis::truth_table), with a precedence test. - The output-depth helper moves to NorNetlist::output_depths. - The e-graph's 8-gate full adder stays as WIDE_FULL_ADDER text. The chaining test uses it. - The harness drops CIRCUIT=egraph-full-adder. Any netlist still runs as CIRCUIT=netlist, and EGRAPH_CHAIN is now CIRCUIT_CHAIN. - docs/egraph_netlists.md is kept as the experiment record. It notes that its measurements come from commit 600ad6d. The live harness knobs are documented in docs/nor_synthesis.md. Co-Authored-By: Claude Opus 5.5 --- AGENTS.md | 2 +- Cargo.lock | 100 +-- Cargo.toml | 1 - docs/egraph_netlists.md | 39 +- docs/nor_synthesis.md | 17 + .../local_placer/exact/egraph.rs | 799 ------------------ .../local_placer/exact/egraph_extract.rsdsl | 86 -- .../place_and_route/local_placer/exact/mod.rs | 4 - .../local_placer/exact/netlist.rs | 22 + .../local_placer/exact/synthesis.rs | 107 ++- .../local_placer/exact/tests.rs | 250 +----- 11 files changed, 210 insertions(+), 1217 deletions(-) delete mode 100644 src/transform/place_and_route/local_placer/exact/egraph.rs delete mode 100644 src/transform/place_and_route/local_placer/exact/egraph_extract.rsdsl 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()