diff --git a/TASK_DETAILS.md b/TASK_DETAILS.md index b331f7d8..0b6cae08 100644 --- a/TASK_DETAILS.md +++ b/TASK_DETAILS.md @@ -203,6 +203,11 @@ We welcome new engineering problem ideas — even without complete verification holographic_polarization_multiplexing Polarization-multiplexed holography + + ElectronicDesignAutomation + CertifiedAIGResynthesis + Proof-carrying, DAG-aware Boolean resynthesis with exact local equivalence checking and area/depth optimization + ComputerSystems MallocLab diff --git a/TASK_DETAILS_zh-CN.md b/TASK_DETAILS_zh-CN.md index 44d1b1fa..e5f84a22 100644 --- a/TASK_DETAILS_zh-CN.md +++ b/TASK_DETAILS_zh-CN.md @@ -203,6 +203,11 @@ Frontier-Eng 目前已覆盖以下领域的任务。每个任务均配有可运 holographic_polarization_multiplexing 偏振复用全息 + + ElectronicDesignAutomation + CertifiedAIGResynthesis + 带证明证书的 DAG 感知布尔重综合，精确验证局部等价性并优化面积与深度 + ComputerSystems MallocLab diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md new file mode 100644 index 00000000..7e5b8d76 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/README.md @@ -0,0 +1,67 @@ +# Certified AIG Resynthesis + +This benchmark asks an optimization policy to rewrite real combinational Boolean +networks represented as and-inverter graphs (AIGs). Each proposed small-cut +replacement is accepted only after exact truth-table equivalence checking and is +recorded as a replayable certificate. The score rewards fewer reachable AND nodes +and lower logic depth. + +This is a synthesis benchmark, not a timing or traffic simulator: candidate code +directly changes the Boolean DAG that is measured. The independent Python checker +reconstructs every accepted transformation from the original AIG and certificate. + +## Files + +- `Task.md`: complete API, proof format, workloads, limits, and score. +- `references/problem_config.json`: frozen workload and resource configuration. +- `references/README.md`: standards and research context. +- `scripts/init.cpp`: compact editable C++ starter policy. +- `verification/rewrite_runtime.hpp`: immutable graph API and certificate runtime. +- `baseline/solution.cpp`: frozen starter used for score normalization. +- `baseline/result_log.txt`: measured reference run. +- `verification/evaluator.py`: workload construction, compilation, independent + certificate replay, and scoring. +- `frontier_eval/`: unified-task metadata and its argument-safe evaluator wrapper. + +## Requirements + +- Linux or another POSIX environment with Python 3.10+; +- `g++` with C++17 support; and +- one CPU core and less than 2 GiB RAM. + +There are no Python packages, containers, external solvers, downloads, GPUs, or +vendor EDA tools. The complete starter evaluation takes about 3.3 seconds on the +repository's current AMD EPYC host, including two C++ compilations and ten circuit +runs. + +## Direct evaluation + +From this task directory: + +```bash +python verification/evaluator.py scripts/init.cpp +``` + +The starter must report `valid=1.0` and `combined_score=1.0`. A score above 1.0 is +an improvement over the frozen starter. + +## Unified evaluation + +From the repository root: + +```bash +python -m frontier_eval \ + task=unified \ + task.benchmark=ElectronicDesignAutomation/CertifiedAIGResynthesis \ + algorithm=openevolve \ + algorithm.iterations=0 +``` + +No runtime override is required; the default process isolation and +`frontier-eval-driver` environment are sufficient. + +## Editing contract + +Only change code between `EVOLVE-BLOCK-START` and `EVOLVE-BLOCK-END` in +`scripts/init.cpp`. The evaluator byte-compares both immutable portions against +the frozen baseline before compiling a candidate. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md new file mode 100644 index 00000000..8a079704 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/Task.md @@ -0,0 +1,168 @@ +# Certified, Budgeted AIG Resynthesis + +## Engineering problem + +Logic synthesis repeatedly replaces a subgraph with a cheaper equivalent one. +The hard part is not merely discovering Boolean identities: useful flows must +coordinate local choices on a shared DAG, reuse existing divisors, trade area +against depth, and never change any output function. A rewrite that looks good as +a tree can lose once fanout and reconvergence are considered. + +This task exposes that problem directly. A C++ policy receives a mutable +and-inverter graph (AIG), proposes arbitrary local replacement AIGs, and obtains a +Boolean proof obligation for each proposal. The immutable runtime emits only +accepted transformations. A separate Python implementation then replays the +certificate and exhaustively checks each obligation before measuring the final +DAG. No probabilistic simulation is used for correctness. + +The central open engineering question is how to search a large space of locally +equivalent expressions while making globally beneficial, DAG-aware decisions +under a strict rewrite budget. Equality-saturation scheduling, cut enumeration, +NPN-aware libraries, exact small-function synthesis, divisor selection, and +learned rewrite orchestration can all be explored inside the same interface. + +## Boolean representation + +Inputs are dense, combinational ASCII AIGER (`aag`) networks: + +- node 0 is constant false and literal 1 is constant true; +- positive literal `2 * id` denotes a node; +- xor with 1 denotes complemented polarity; and +- every non-input node is a two-input AND. + +The frozen evaluator deterministically constructs five engineering circuit +families from `references/problem_config.json`: + +1. a 96-bit ripple-carry adder; +2. a 64-bit logical barrel shifter; +3. a 128-request fixed-priority arbiter; +4. a 48-rule, 12-bit-per-rule packet classifier; and +5. a 64-bit update of a 32-bit CRC state. + +The front ends deliberately retain several semantically redundant lowering forms +that arise from mux expansion, guarding, repeated expressions, and generic +Boolean lowering. Workload bytes and SHA-256 digests are deterministic and are +reported in `artifacts.json`. + +## Candidate interface + +Only this function is editable: + +```cpp +void optimize(certified_aig::Optimizer& optimizer); +``` + +The immutable class provides graph inspection plus two mutation calls: + +```cpp +bool try_rewrite( + uint32_t root, + const std::vector& leaves, + const std::vector& divisors, + const std::vector& local_ands, + uint32_t local_output); + +bool replace( + uint32_t root, + uint32_t replacement_global_literal, + const std::vector& leaves); +``` + +Useful read methods include `first_and_id()`, `node_count()`, `is_and(id)`, +`is_active(id)`, `resolve(literal)`, `fanins(id)`, `output_literal(index)`, +`primary_support(root)`, and `truth_table(root, leaves, &table)`. Their +implementations and precise failure conditions are visible in +`verification/rewrite_runtime.hpp`. + +`try_rewrite` may synthesize any acyclic local AIG. With `k` cut leaves and `d` +divisors, local literal references are: + +- reference 0: false; +- references `1..k`: the positive boundary leaves; +- references `k+1..k+d`: supplied global divisor literals; and +- subsequent references: local AND results in order. + +Each literal is encoded as `2 * reference + polarity`. A local AND may reference +only an earlier value. Divisors can lie outside the root cone, enabling real +DAG-aware reuse, but each divisor must be a function of the same cut leaves and +must not depend on the rewritten root. + +## Certificate and formal validity + +The candidate executable writes a line-oriented certificate. The immutable C++ +runtime checks proposals before recording them, but that check is not trusted for +the score. `verification/evaluator.py` independently parses the original AAG and +replays every certificate line. + +For a cut of `k <= 8` leaves, the checker: + +1. confirms that every path through the current root cone terminates at a listed + leaf or constant; +2. evaluates the old root on all `2^k` assignments; +3. independently evaluates every external divisor over the same assignments and + rejects root-dependent divisors; +4. evaluates the proposed local AIG on all assignments; +5. requires bit-for-bit equality; and +6. only then redirects the root and appends replacement nodes. + +Because every step is an exact equivalence and later steps operate on the graph +produced by earlier ones, the sequence is a compositional proof that all primary +outputs retain their original Boolean functions. The checker also detects cycles, +forward references, stale nodes, uncovered input paths, malformed certificates, +and resource-limit violations. + +## Resource limits + +The public limits are: + +- at most 8 cut leaves; +- at most 16 external divisors per rewrite; +- at most 64 new ANDs per rewrite; +- at most 20,000 accepted rewrites per workload; +- at most 300,000 total nodes; +- a 16 MB certificate; and +- 4 seconds of candidate execution per workload by default. + +The evaluator additionally limits process address space to 2 GiB and compiles +with `g++ -std=c++17 -O2`. Compilation time is not part of the candidate execution +budget, but it is included in reported evaluator wall time. + +## Objective + +After replay, the checker traverses only nodes reachable from primary outputs: + +- `A`: number of reachable AND nodes; and +- `D`: maximum AND level from any primary input or constant to an output. + +Let `A_b, D_b` be the frozen starter result and `A_c, D_c` the candidate result +for one workload. Its score is + +```text +(A_b / A_c)^0.75 * (D_b / D_c)^0.25 +``` + +`combined_score` is the geometric mean across all five workloads. The starter is +exactly 1.0. Invalid source edits, compilation failures, timeouts, altered inputs, +invalid certificates, or degenerate final graphs produce `valid=0.0` and score +0.0. + +The initial policy performs constant propagation, idempotence/complement +simplification, and exact structural hashing. It intentionally leaves substantial +headroom for cut resynthesis, absorption, mux reasoning, balancing, and divisor +reuse. + +## Reproducibility and direct evaluation + +No network access or nondeterministic input is used. The workload builder, config, +baseline, C++ runtime, and Python proof checker are all included and marked +read-only by the unified evaluator. + +```bash +python verification/evaluator.py scripts/init.cpp \ + --metrics-out metrics.json \ + --artifacts-out artifacts.json +``` + +`metrics.json` contains numeric leaderboard fields. `artifacts.json` contains the +per-workload input digests, baseline and candidate area/depth, rewrite counts, +truth-table rows checked, certificate digests, and process runtimes. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/result_log.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/result_log.txt new file mode 100644 index 00000000..d446e4b0 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/result_log.txt @@ -0,0 +1,53 @@ +CertifiedAIGResynthesis baseline validation +Date: 2026-07-13 + +Host + OS: Linux 5.15.0-153-generic x86_64 + CPU: 2 x AMD EPYC 7313 (32 physical / 64 logical cores total) + Python: 3.10.12 + Compiler: g++ 11.4.0 + GPU/container/external solver: not used + +Direct command (from task directory) + python verification/evaluator.py scripts/init.cpp \ + --metrics-out metrics.json --artifacts-out artifacts.json + +Direct metrics + valid: 1.0 + combined_score: 1.0 + runtime_s: 3.6762920655310154 + scenario_count: 5 + baseline_total_area: 6610 + candidate_total_area: 6610 + baseline_mean_depth: 108.6 + candidate_mean_depth: 108.6 + checked_truth_rows: 1546 + +Per-workload frozen starter result + ripple_adder_96: area=934, depth=222, rewrites=28 + barrel_shifter_64: area=1153, depth=18, rewrites=176 + priority_arbiter_128: area=359, depth=128, rewrites=44 + packet_classifier: area=926, depth=83, rewrites=181 + crc32_update_64: area=3238, depth=92, rewrites=221 + +Unified command (from repository root) + .venvs/frontier-eval-driver/bin/python -m frontier_eval \ + task=unified \ + task.benchmark=ElectronicDesignAutomation/CertifiedAIGResynthesis \ + algorithm=openevolve \ + algorithm.iterations=0 + +Unified result + exit code: 0 + valid: 1.0 + combined_score: 1.0 + evaluator runtime_s: 3.1896 + read-only/copy/process-isolation path: passed + +Development headroom check + A temporary candidate adding only same-arm mux elimination was independently + replayed by the same evaluator. It scored 1.1367188441269405, reduced total + live ANDs from 6610 to 5893, and reduced mean depth from 108.6 to 97.6. Its + minimum per-workload score was 1.0705928226806747. This candidate is not the + committed starter; the measurement confirms optimization headroom in every + frozen workload before more advanced cut synthesis or divisor reuse. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/solution.cpp b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/solution.cpp new file mode 100644 index 00000000..347a8c5c --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/baseline/solution.cpp @@ -0,0 +1,91 @@ +// Certified AIG resynthesis candidate policy. +// The evaluator permits edits only inside the marked region. + +#include "rewrite_runtime.hpp" + +namespace certified_aig { + +// EVOLVE-BLOCK-START +void optimize(Optimizer& optimizer) { + // Valid starter: constant propagation, idempotence, complement elimination, + // and exact structural hashing. More capable policies can enumerate cuts, + // synthesize smaller local AIGs, reuse divisors, and balance depth through + // Optimizer::try_rewrite(). + for (std::uint32_t pass = 0; pass < 8U; ++pass) { + std::unordered_map representative; + std::uint32_t changes = 0; + const std::uint32_t limit = optimizer.node_count(); + for (std::uint32_t root = optimizer.first_and_id(); root < limit; ++root) { + if (!optimizer.is_and(root) || !optimizer.is_active(root)) continue; + auto [lhs, rhs] = optimizer.fanins(root); + if (lhs > rhs) std::swap(lhs, rhs); + const auto leaves = boundary_nodes(lhs, rhs); + + std::optional replacement; + if (lhs == 0U || rhs == 0U) { + replacement = 0U; + } else if (lhs == 1U) { + replacement = rhs; + } else if (rhs == 1U) { + replacement = lhs; + } else if (lhs == rhs) { + replacement = lhs; + } else if ((lhs ^ rhs) == 1U) { + replacement = 0U; + } + if (replacement.has_value() && + optimizer.replace(root, *replacement, leaves)) { + ++changes; + continue; + } + + const std::uint64_t key = + (static_cast(lhs) << 32U) | rhs; + const auto found = representative.find(key); + if (found == representative.end()) { + representative.emplace(key, root << 1U); + } else { + const std::uint32_t prior = optimizer.resolve(found->second); + if (prior != (root << 1U) && optimizer.replace(root, prior, leaves)) { + ++changes; + } + } + } + if (changes == 0U) break; + } +} +// EVOLVE-BLOCK-END + +} // namespace certified_aig + +int main(int argc, char** argv) { + std::string input_path; + std::string certificate_path; + for (int index = 1; index < argc; ++index) { + const std::string argument = argv[index]; + if (argument == "--input" && index + 1 < argc) { + input_path = argv[++index]; + } else if (argument == "--certificate" && index + 1 < argc) { + certificate_path = argv[++index]; + } else { + std::cerr << "unknown or incomplete argument: " << argument << '\n'; + return 2; + } + } + if (input_path.empty() || certificate_path.empty()) { + std::cerr << "usage: candidate --input circuit.aag --certificate proof.cert\n"; + return 2; + } + try { + certified_aig::Optimizer optimizer(input_path, certificate_path); + certified_aig::optimize(optimizer); + const certified_aig::NetworkStats stats = optimizer.stats(); + std::cout << "accepted_rewrites=" << optimizer.accepted_rewrites() + << " live_ands=" << stats.live_ands + << " depth=" << stats.depth << '\n'; + return 0; + } catch (const std::exception& exc) { + std::cerr << "candidate failure: " << exc.what() << '\n'; + return 1; + } +} diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/agent_files.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/agent_files.txt new file mode 100644 index 00000000..a5a1ef43 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/agent_files.txt @@ -0,0 +1,8 @@ +README.md +Task.md +scripts/init.cpp +verification/rewrite_runtime.hpp +references/problem_config.json +references/README.md +verification/evaluator.py +frontier_eval/constraints.txt diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/artifact_files.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/artifact_files.txt new file mode 100644 index 00000000..d02f2a18 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/artifact_files.txt @@ -0,0 +1 @@ +# metrics.json and artifacts.json are collected by UnifiedTask directly. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/candidate_destination.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/candidate_destination.txt new file mode 100644 index 00000000..d26dd4fb --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/candidate_destination.txt @@ -0,0 +1 @@ +scripts/init.cpp diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/constraints.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/constraints.txt new file mode 100644 index 00000000..0073d73e --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/constraints.txt @@ -0,0 +1,13 @@ +CertifiedAIGResynthesis constraints: +1) Only modify code between the EVOLVE-BLOCK markers in `scripts/init.cpp`. +2) Preserve `optimize(certified_aig::Optimizer&)` and the immutable C++ shell. +3) Propose rewrites through `try_rewrite` or `replace`; the evaluator accepts only + certificates that its independent Python checker can replay exactly. +4) Each cut has at most 8 leaves, 16 divisors, and 64 new AND nodes. Respect all + public process, certificate, rewrite, and graph-size budgets in `Task.md`. +5) Optimize reachable AND area and depth across all circuit families. A locally + smaller tree can still lose through DAG fanout, reconvergence, or depth. +6) Do not modify documentation, baseline, references, verification, or + `frontier_eval` metadata. These paths are checked read-only. +7) Use only the fixed C++17 standard-library environment. No downloads, network, + external solvers, containers, GPUs, or vendor EDA tools are available. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/copy_files.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/copy_files.txt new file mode 100644 index 00000000..9c558e35 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/copy_files.txt @@ -0,0 +1 @@ +. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_command.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_command.txt new file mode 100644 index 00000000..c8c51ef9 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_command.txt @@ -0,0 +1 @@ +bash frontier_eval/run_eval.sh {python} {candidate} metrics.json artifacts.json diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_cwd.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_cwd.txt new file mode 100644 index 00000000..9c558e35 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/eval_cwd.txt @@ -0,0 +1 @@ +. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/initial_program.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/initial_program.txt new file mode 100644 index 00000000..d26dd4fb --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/initial_program.txt @@ -0,0 +1 @@ +scripts/init.cpp diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/readonly_files.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/readonly_files.txt new file mode 100644 index 00000000..3e459e21 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/readonly_files.txt @@ -0,0 +1,8 @@ +README.md +Task.md +baseline +references +verification +verification/evaluator.py +frontier_eval +frontier_eval/run_eval.sh diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/run_eval.sh b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/run_eval.sh new file mode 100644 index 00000000..f49aa26b --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/frontier_eval/run_eval.sh @@ -0,0 +1,16 @@ +#!/usr/bin/env bash +set -euo pipefail + +if [[ $# -ne 4 ]]; then + echo "usage: run_eval.sh PYTHON CANDIDATE METRICS_JSON ARTIFACTS_JSON" >&2 + exit 2 +fi + +python_path=$1 +candidate_path=$2 +metrics_path=$3 +artifacts_path=$4 + +exec "$python_path" verification/evaluator.py "$candidate_path" \ + --metrics-out "$metrics_path" \ + --artifacts-out "$artifacts_path" diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/README.md b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/README.md new file mode 100644 index 00000000..c3e76a23 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/README.md @@ -0,0 +1,17 @@ +# References and design rationale + +- The [AIGER format and tool distribution](https://fmv.jku.at/aiger/) defines the + literal and ASCII AIG representation used by the benchmark. +- The [EPFL combinational benchmark suite](https://www.epfl.ch/labs/lsi/page-102566-en-html/benchmarks/) + illustrates the arithmetic and control-oriented AIG workloads commonly used to + evaluate logic-synthesis flows. +- *E-morphic* ([arXiv:2504.11574](https://arxiv.org/abs/2504.11574)) motivates + equality saturation as an active approach to scalable circuit optimization. +- *DAG-aware AIG rewriting orchestration* ([arXiv:2310.07846](https://arxiv.org/abs/2310.07846)) + motivates evaluating rewrite scheduling on the shared graph rather than adding + isolated per-rule gains. + +The benchmark does not redistribute third-party circuits or software. Its five +circuits are deterministic, repository-owned Boolean front ends specified by +`problem_config.json` and implemented in the frozen evaluator. The cited suites +and papers provide representation, workload, and research context. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/problem_config.json b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/problem_config.json new file mode 100644 index 00000000..4d98ffd2 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/references/problem_config.json @@ -0,0 +1,71 @@ +{ + "benchmark_id": "certified_aig_resynthesis", + "version": 1, + "description": "Deterministic combinational AIG workloads with independently replayed local equivalence certificates.", + "objective": { + "area_weight": 0.75, + "depth_weight": 0.25 + }, + "limits": { + "candidate_timeout_s_per_workload": 4.0, + "compile_timeout_s": 30.0, + "max_candidate_bytes": 1000000, + "max_certificate_bytes": 16000000, + "max_cut_leaves": 8, + "max_divisors": 16, + "max_local_ands": 64, + "max_rewrites": 20000, + "max_total_nodes": 300000 + }, + "workloads": [ + { + "id": "ripple_adder_96", + "kind": "ripple_adder", + "width": 96, + "lowering_period": 7, + "expected_sha256": "d5c682f1e9d665177ef675298c20050cdca904f56e4ba75b8bf2ea116eb652c2", + "expected_live_ands": 962, + "expected_depth": 230 + }, + { + "id": "barrel_shifter_64", + "kind": "barrel_shifter", + "width": 64, + "lowering_period": 5, + "expected_sha256": "2534c2e949d7cfd9d3e1c87948c2375a014b9cb87ec03ca7177f9f875000e292", + "expected_live_ands": 1329, + "expected_depth": 19 + }, + { + "id": "priority_arbiter_128", + "kind": "priority_arbiter", + "width": 128, + "lowering_period": 4, + "expected_sha256": "c712ad116b4b427c399c689f2357a38d508dd3845ebfe18c3a50f2fa5596251e", + "expected_live_ands": 403, + "expected_depth": 129 + }, + { + "id": "packet_classifier_48x12", + "kind": "packet_classifier", + "header_bits": 32, + "rules": 48, + "bits_per_rule": 12, + "lowering_period": 3, + "expected_sha256": "a6edceef1c7b0620b8f4b7e477c048a470440e8ffa7c58d0aee0c936e6ea2733", + "expected_live_ands": 1107, + "expected_depth": 96 + }, + { + "id": "crc32_update_64", + "kind": "crc_update", + "state_bits": 32, + "data_bits": 64, + "polynomial": 79764919, + "lowering_period": 6, + "expected_sha256": "2fce8a90bc9e71715f35c567f89b7f695bd7b393da833b55890aabac078fa066", + "expected_live_ands": 3459, + "expected_depth": 106 + } + ] +} diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/scripts/init.cpp b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/scripts/init.cpp new file mode 100644 index 00000000..347a8c5c --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/scripts/init.cpp @@ -0,0 +1,91 @@ +// Certified AIG resynthesis candidate policy. +// The evaluator permits edits only inside the marked region. + +#include "rewrite_runtime.hpp" + +namespace certified_aig { + +// EVOLVE-BLOCK-START +void optimize(Optimizer& optimizer) { + // Valid starter: constant propagation, idempotence, complement elimination, + // and exact structural hashing. More capable policies can enumerate cuts, + // synthesize smaller local AIGs, reuse divisors, and balance depth through + // Optimizer::try_rewrite(). + for (std::uint32_t pass = 0; pass < 8U; ++pass) { + std::unordered_map representative; + std::uint32_t changes = 0; + const std::uint32_t limit = optimizer.node_count(); + for (std::uint32_t root = optimizer.first_and_id(); root < limit; ++root) { + if (!optimizer.is_and(root) || !optimizer.is_active(root)) continue; + auto [lhs, rhs] = optimizer.fanins(root); + if (lhs > rhs) std::swap(lhs, rhs); + const auto leaves = boundary_nodes(lhs, rhs); + + std::optional replacement; + if (lhs == 0U || rhs == 0U) { + replacement = 0U; + } else if (lhs == 1U) { + replacement = rhs; + } else if (rhs == 1U) { + replacement = lhs; + } else if (lhs == rhs) { + replacement = lhs; + } else if ((lhs ^ rhs) == 1U) { + replacement = 0U; + } + if (replacement.has_value() && + optimizer.replace(root, *replacement, leaves)) { + ++changes; + continue; + } + + const std::uint64_t key = + (static_cast(lhs) << 32U) | rhs; + const auto found = representative.find(key); + if (found == representative.end()) { + representative.emplace(key, root << 1U); + } else { + const std::uint32_t prior = optimizer.resolve(found->second); + if (prior != (root << 1U) && optimizer.replace(root, prior, leaves)) { + ++changes; + } + } + } + if (changes == 0U) break; + } +} +// EVOLVE-BLOCK-END + +} // namespace certified_aig + +int main(int argc, char** argv) { + std::string input_path; + std::string certificate_path; + for (int index = 1; index < argc; ++index) { + const std::string argument = argv[index]; + if (argument == "--input" && index + 1 < argc) { + input_path = argv[++index]; + } else if (argument == "--certificate" && index + 1 < argc) { + certificate_path = argv[++index]; + } else { + std::cerr << "unknown or incomplete argument: " << argument << '\n'; + return 2; + } + } + if (input_path.empty() || certificate_path.empty()) { + std::cerr << "usage: candidate --input circuit.aag --certificate proof.cert\n"; + return 2; + } + try { + certified_aig::Optimizer optimizer(input_path, certificate_path); + certified_aig::optimize(optimizer); + const certified_aig::NetworkStats stats = optimizer.stats(); + std::cout << "accepted_rewrites=" << optimizer.accepted_rewrites() + << " live_ands=" << stats.live_ands + << " depth=" << stats.depth << '\n'; + return 0; + } catch (const std::exception& exc) { + std::cerr << "candidate failure: " << exc.what() << '\n'; + return 1; + } +} diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/evaluator.py b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/evaluator.py new file mode 100644 index 00000000..8666eaea --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/evaluator.py @@ -0,0 +1,1062 @@ +"""Independent evaluator for proof-carrying AIG resynthesis candidates.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import math +import os +import resource +import shutil +import signal +import subprocess +import tempfile +import time +from dataclasses import dataclass +from pathlib import Path +from typing import Any + + +TASK_DIR = Path(__file__).resolve().parents[1] +CONFIG_PATH = TASK_DIR / "references" / "problem_config.json" +BASELINE_PATH = TASK_DIR / "baseline" / "solution.cpp" +START_MARKER = "// EVOLVE-BLOCK-START" +END_MARKER = "// EVOLVE-BLOCK-END" + + +class EvaluationError(RuntimeError): + """A deterministic candidate, certificate, or benchmark validation failure.""" + + +def _strict_json(path: Path) -> dict[str, Any]: + def reject_constant(value: str) -> None: + raise ValueError(f"non-finite JSON constant is not allowed: {value}") + + data = json.loads(path.read_text(encoding="utf-8"), parse_constant=reject_constant) + if not isinstance(data, dict): + raise ValueError("configuration root must be an object") + return data + + +def _positive_int(value: Any, label: str) -> int: + if isinstance(value, bool) or not isinstance(value, int) or value <= 0: + raise ValueError(f"{label} must be a positive integer") + return value + + +def _finite_float(value: Any, label: str) -> float: + if isinstance(value, bool) or not isinstance(value, (int, float)): + raise ValueError(f"{label} must be a finite number") + result = float(value) + if not math.isfinite(result): + raise ValueError(f"{label} must be finite") + return result + + +def _validated_config() -> dict[str, Any]: + config = _strict_json(CONFIG_PATH) + if config.get("benchmark_id") != "certified_aig_resynthesis": + raise ValueError("unexpected benchmark_id") + objective = config.get("objective") + limits = config.get("limits") + workloads = config.get("workloads") + if not isinstance(objective, dict) or not isinstance(limits, dict): + raise ValueError("objective and limits must be objects") + if not isinstance(workloads, list) or not workloads: + raise ValueError("workloads must be a non-empty list") + area_weight = _finite_float(objective.get("area_weight"), "area_weight") + depth_weight = _finite_float(objective.get("depth_weight"), "depth_weight") + if area_weight <= 0.0 or depth_weight <= 0.0: + raise ValueError("objective weights must be positive") + if not math.isclose(area_weight + depth_weight, 1.0, abs_tol=1e-12): + raise ValueError("objective weights must sum to one") + for key in ( + "max_candidate_bytes", + "max_certificate_bytes", + "max_cut_leaves", + "max_divisors", + "max_local_ands", + "max_rewrites", + "max_total_nodes", + ): + _positive_int(limits.get(key), key) + _finite_float(limits.get("candidate_timeout_s_per_workload"), "candidate timeout") + _finite_float(limits.get("compile_timeout_s"), "compile timeout") + ids: set[str] = set() + for index, workload in enumerate(workloads): + if not isinstance(workload, dict): + raise ValueError(f"workloads[{index}] must be an object") + workload_id = str(workload.get("id", "")).strip() + kind = str(workload.get("kind", "")).strip() + if not workload_id or workload_id in ids or not kind: + raise ValueError(f"invalid or duplicate workload at index {index}") + ids.add(workload_id) + return config + + +class AigBuilder: + """Small deterministic Boolean front end that emits raw ASCII AIGER.""" + + def __init__(self, input_count: int) -> None: + if input_count <= 0: + raise ValueError("an AIG workload needs at least one input") + self.input_count = input_count + self.inputs = [2 * node_id for node_id in range(1, input_count + 1)] + self.ands: list[tuple[int, int]] = [] + self.outputs: list[int] = [] + self._lowering_index = 0 + + @staticmethod + def inv(literal: int) -> int: + return literal ^ 1 + + def and_gate(self, lhs: int, rhs: int) -> int: + node_id = self.input_count + len(self.ands) + 1 + self.ands.append((lhs, rhs)) + return node_id * 2 + + def or_gate(self, lhs: int, rhs: int) -> int: + return self.inv(self.and_gate(self.inv(lhs), self.inv(rhs))) + + def xor_gate(self, lhs: int, rhs: int) -> int: + lhs_only = self.and_gate(lhs, self.inv(rhs)) + rhs_only = self.and_gate(self.inv(lhs), rhs) + return self.or_gate(lhs_only, rhs_only) + + def mux(self, select: int, when_true: int, when_false: int) -> int: + selected_true = self.and_gate(select, when_true) + selected_false = self.and_gate(self.inv(select), when_false) + return self.or_gate(selected_true, selected_false) + + def lower_equivalent(self, literal: int, guard: int, period: int) -> int: + """Model common front-end lowering patterns without changing semantics.""" + index = self._lowering_index + self._lowering_index += 1 + if period <= 0 or index % period != 0: + return literal + mode = (index // period) % 6 + if mode == 0: + return self.and_gate(literal, 1) # x & true + if mode == 1: + return self.or_gate(literal, 0) # x | false + if mode == 2: + return self.mux(guard, literal, literal) + if mode == 3: + return self.or_gate(literal, self.and_gate(literal, guard)) + if mode == 4: + return self.and_gate(literal, self.or_gate(literal, guard)) + true_arm = self.and_gate(literal, 1) + false_arm = self.or_gate(literal, 0) + return self.mux(guard, true_arm, false_arm) + + def to_aag(self) -> bytes: + if not self.outputs: + raise ValueError("AIG workload has no outputs") + maximum = self.input_count + len(self.ands) + lines = [ + f"aag {maximum} {self.input_count} 0 {len(self.outputs)} {len(self.ands)}" + ] + lines.extend(str(literal) for literal in self.inputs) + lines.extend(str(literal) for literal in self.outputs) + for index, (lhs, rhs) in enumerate(self.ands): + node_id = self.input_count + index + 1 + lines.append(f"{2 * node_id} {lhs} {rhs}") + lines.append("c") + lines.append("generated deterministically by CertifiedAIGResynthesis") + return ("\n".join(lines) + "\n").encode("ascii") + + +def _ripple_adder(spec: dict[str, Any]) -> bytes: + width = _positive_int(spec.get("width"), "ripple_adder.width") + period = _positive_int(spec.get("lowering_period"), "lowering_period") + builder = AigBuilder(2 * width + 1) + lhs = builder.inputs[:width] + rhs = builder.inputs[width : 2 * width] + carry = builder.inputs[-1] + sums: list[int] = [] + for bit in range(width): + guard = lhs[(bit + 11) % width] + propagate = builder.xor_gate(lhs[bit], rhs[bit]) + propagate = builder.lower_equivalent(propagate, guard, period) + result = builder.xor_gate(propagate, carry) + result = builder.lower_equivalent(result, rhs[(bit + 7) % width], period) + generate = builder.and_gate(lhs[bit], rhs[bit]) + carry_prop = builder.and_gate(propagate, carry) + carry = builder.or_gate(generate, carry_prop) + carry = builder.lower_equivalent(carry, guard, period) + sums.append(result) + builder.outputs = sums + [carry] + return builder.to_aag() + + +def _barrel_shifter(spec: dict[str, Any]) -> bytes: + width = _positive_int(spec.get("width"), "barrel_shifter.width") + if width & (width - 1): + raise ValueError("barrel_shifter.width must be a power of two") + stages = width.bit_length() - 1 + period = _positive_int(spec.get("lowering_period"), "lowering_period") + builder = AigBuilder(width + stages) + data = builder.inputs[:width] + shift = builder.inputs[width:] + current = data + for stage, select in enumerate(shift): + distance = 1 << stage + next_stage: list[int] = [] + for bit in range(width): + shifted = current[bit - distance] if bit >= distance else 0 + value = builder.mux(select, shifted, current[bit]) + guard = data[(bit + 3 * stage + 1) % width] + next_stage.append(builder.lower_equivalent(value, guard, period)) + current = next_stage + builder.outputs = current + return builder.to_aag() + + +def _priority_arbiter(spec: dict[str, Any]) -> bytes: + width = _positive_int(spec.get("width"), "priority_arbiter.width") + period = _positive_int(spec.get("lowering_period"), "lowering_period") + builder = AigBuilder(width) + requests = builder.inputs + seen = 0 + grants: list[int] = [] + for index, request in enumerate(requests): + grant = builder.and_gate(request, builder.inv(seen)) + grant = builder.lower_equivalent( + grant, requests[(index + 17) % width], period + ) + grants.append(grant) + seen = builder.or_gate(seen, request) + seen = builder.lower_equivalent(seen, requests[(index + 29) % width], period) + builder.outputs = grants + [seen] + return builder.to_aag() + + +def _packet_classifier(spec: dict[str, Any]) -> bytes: + header_bits = _positive_int(spec.get("header_bits"), "header_bits") + rule_count = _positive_int(spec.get("rules"), "rules") + bits_per_rule = _positive_int(spec.get("bits_per_rule"), "bits_per_rule") + period = _positive_int(spec.get("lowering_period"), "lowering_period") + if bits_per_rule > header_bits: + raise ValueError("bits_per_rule exceeds header_bits") + builder = AigBuilder(header_bits) + header = builder.inputs + matched = 0 + hits: list[int] = [] + for rule in range(rule_count): + selected: list[int] = [] + used: set[int] = set() + cursor = (rule * 7 + 3) % header_bits + while len(selected) < bits_per_rule: + if cursor not in used: + used.add(cursor) + literal = header[cursor] + if ((rule * 13 + cursor * 5) >> 1) & 1: + literal = builder.inv(literal) + selected.append(literal) + cursor = (cursor + 5) % header_bits + condition = selected[0] + for position, literal in enumerate(selected[1:], start=1): + condition = builder.and_gate(condition, literal) + condition = builder.lower_equivalent( + condition, header[(rule + position * 3) % header_bits], period + ) + hit = builder.and_gate(condition, builder.inv(matched)) + hit = builder.lower_equivalent(hit, header[(rule + 19) % header_bits], period) + hits.append(hit) + matched = builder.or_gate(matched, condition) + matched = builder.lower_equivalent( + matched, header[(rule + 23) % header_bits], period + ) + builder.outputs = hits + [matched] + return builder.to_aag() + + +def _crc_update(spec: dict[str, Any]) -> bytes: + state_bits = _positive_int(spec.get("state_bits"), "state_bits") + data_bits = _positive_int(spec.get("data_bits"), "data_bits") + polynomial = _positive_int(spec.get("polynomial"), "polynomial") + period = _positive_int(spec.get("lowering_period"), "lowering_period") + if polynomial >= (1 << state_bits): + raise ValueError("CRC polynomial does not fit state width") + builder = AigBuilder(state_bits + data_bits) + state = builder.inputs[:state_bits] + data = builder.inputs[state_bits:] + for data_index, data_literal in enumerate(data): + feedback = builder.xor_gate(state[-1], data_literal) + next_state = [feedback] + for bit in range(1, state_bits): + value = state[bit - 1] + if (polynomial >> bit) & 1: + value = builder.xor_gate(value, feedback) + guard = data[(data_index + bit * 7) % data_bits] + value = builder.lower_equivalent(value, guard, period) + next_state.append(value) + state = next_state + builder.outputs = state + return builder.to_aag() + + +WORKLOAD_GENERATORS = { + "ripple_adder": _ripple_adder, + "barrel_shifter": _barrel_shifter, + "priority_arbiter": _priority_arbiter, + "packet_classifier": _packet_classifier, + "crc_update": _crc_update, +} + + +def _generate_workload(spec: dict[str, Any]) -> bytes: + kind = str(spec.get("kind", "")) + generator = WORKLOAD_GENERATORS.get(kind) + if generator is None: + raise ValueError(f"unknown workload kind: {kind}") + return generator(spec) + + +@dataclass(frozen=True) +class AigStats: + live_ands: int + depth: int + + +@dataclass(frozen=True) +class ReplayResult: + stats: AigStats + rewrites: int + checked_rows: int + appended_ands: int + certificate_sha256: str + + +class ProofChecker: + """A checker intentionally independent from the candidate's C++ engine.""" + + KIND_UNUSED = 0 + KIND_INPUT = 1 + KIND_AND = 2 + + def __init__(self, aag: bytes, limits: dict[str, Any]) -> None: + self.limits = limits + self.nodes: list[tuple[int, int] | None] + self.kinds: list[int] + self.outputs: list[int] + self.redirect: list[int] + self.first_and_id: int + self.input_count: int + self._parse_aag(aag) + + @staticmethod + def _numbers(line: str, expected: int | None = None) -> list[int]: + fields = line.split() + if expected is not None and len(fields) != expected: + raise EvaluationError("malformed AAG field count") + if not fields or any(not field.isascii() or not field.isdecimal() for field in fields): + raise EvaluationError("AAG numeric fields must be unsigned decimal integers") + return [int(field) for field in fields] + + def _parse_aag(self, aag: bytes) -> None: + try: + text = aag.decode("ascii") + except UnicodeDecodeError as exc: + raise EvaluationError(f"AAG is not ASCII: {exc}") from exc + lines = text.splitlines() + if not lines: + raise EvaluationError("empty AAG") + header = lines[0].split() + if len(header) != 6 or header[0] != "aag": + raise EvaluationError("unsupported AAG header") + values = self._numbers(" ".join(header[1:]), expected=5) + maximum, inputs, latches, outputs, ands = values + if latches != 0 or inputs <= 0 or outputs <= 0 or maximum != inputs + ands: + raise EvaluationError("only dense combinational AAGs are supported") + if maximum > int(self.limits["max_total_nodes"]): + raise EvaluationError("input AAG exceeds node limit") + required = 1 + inputs + outputs + ands + if len(lines) < required: + raise EvaluationError("truncated AAG") + self.input_count = inputs + self.first_and_id = inputs + 1 + self.nodes = [None] * (maximum + 1) + self.kinds = [self.KIND_UNUSED] * (maximum + 1) + for index in range(inputs): + literal = self._numbers(lines[1 + index], expected=1)[0] + node_id = index + 1 + if literal != 2 * node_id: + raise EvaluationError("AAG inputs are not dense positive literals") + self.kinds[node_id] = self.KIND_INPUT + output_start = 1 + inputs + self.outputs = [] + for index in range(outputs): + literal = self._numbers(lines[output_start + index], expected=1)[0] + if literal > 2 * maximum + 1: + raise EvaluationError("AAG output references an unknown node") + self.outputs.append(literal) + and_start = output_start + outputs + for index in range(ands): + lhs, rhs0, rhs1 = self._numbers(lines[and_start + index], expected=3) + node_id = self.first_and_id + index + if lhs != 2 * node_id or rhs0 >= lhs or rhs1 >= lhs: + raise EvaluationError("AAG ANDs are not dense and topological") + self.nodes[node_id] = (rhs0, rhs1) + self.kinds[node_id] = self.KIND_AND + self.redirect = [2 * node_id for node_id in range(maximum + 1)] + + def resolve(self, literal: int) -> int: + node_id = literal >> 1 + inverted = literal & 1 + if node_id >= len(self.redirect): + raise EvaluationError("global literal references an unknown node") + for _ in range(len(self.redirect) + 1): + mapped = self.redirect[node_id] + if mapped == 2 * node_id: + return 2 * node_id + inverted + inverted ^= mapped & 1 + node_id = mapped >> 1 + if node_id >= len(self.redirect): + raise EvaluationError("rewrite redirect references an unknown node") + raise EvaluationError("cycle in rewrite redirects") + + def is_active(self, node_id: int) -> bool: + return 0 <= node_id < len(self.redirect) and self.redirect[node_id] == 2 * node_id + + @staticmethod + def _variable_pattern(index: int, assignments: int) -> int: + pattern = 0 + for assignment in range(assignments): + if (assignment >> index) & 1: + pattern |= 1 << assignment + return pattern + + def _evaluate_cut( + self, + literal: int, + leaves: list[int], + *, + forbidden_root: int | None, + require_all_leaves: bool, + ) -> int: + leaf_positions = {leaf: index for index, leaf in enumerate(leaves)} + if len(leaf_positions) != len(leaves): + raise EvaluationError("cut leaves are not unique") + assignments = 1 << len(leaves) + mask = (1 << assignments) - 1 + used: set[int] = set() + memo: dict[int, int] = {} + visiting: set[int] = set() + + def evaluate_literal(current: int) -> int: + current = self.resolve(current) + value = evaluate_node(current >> 1) + return mask ^ value if current & 1 else value + + def evaluate_node(node_id: int) -> int: + leaf_index = leaf_positions.get(node_id) + if leaf_index is not None: + used.add(node_id) + return self._variable_pattern(leaf_index, assignments) + if node_id == 0: + return 0 + if forbidden_root is not None and node_id == forbidden_root: + raise EvaluationError("a divisor depends on the rewritten root") + if node_id >= len(self.kinds): + raise EvaluationError("cut traversal left the AIG") + if self.kinds[node_id] == self.KIND_INPUT: + raise EvaluationError("cut does not cover a primary-input path") + if self.kinds[node_id] != self.KIND_AND or self.nodes[node_id] is None: + raise EvaluationError("cut contains an invalid node") + if node_id in memo: + return memo[node_id] + if node_id in visiting: + raise EvaluationError("cycle in cut cone") + visiting.add(node_id) + lhs, rhs = self.nodes[node_id] + value = evaluate_literal(lhs) & evaluate_literal(rhs) + visiting.remove(node_id) + memo[node_id] = value + return value + + result = evaluate_literal(literal) + if require_all_leaves and used != set(leaves): + raise EvaluationError("cut includes a leaf outside the root cone") + return result + + @staticmethod + def _local_value(literal: int, values: list[int], mask: int) -> int: + reference = literal >> 1 + if reference >= len(values): + raise EvaluationError("local literal is forward or out of range") + value = values[reference] + return mask ^ value if literal & 1 else value + + def apply_rewrite( + self, + root: int, + leaves: list[int], + divisors: list[int], + local_ands: list[tuple[int, int]], + local_output: int, + ) -> tuple[int, int]: + max_cut = int(self.limits["max_cut_leaves"]) + max_divisors = int(self.limits["max_divisors"]) + max_local_ands = int(self.limits["max_local_ands"]) + if ( + len(leaves) > max_cut + or len(divisors) > max_divisors + or len(local_ands) > max_local_ands + or root < self.first_and_id + or root >= len(self.nodes) + or self.kinds[root] != self.KIND_AND + or not self.is_active(root) + ): + raise EvaluationError("rewrite root or resource limits are invalid") + if len(self.nodes) + len(local_ands) > int(self.limits["max_total_nodes"]): + raise EvaluationError("certificate exceeds total node limit") + if any( + leaf <= 0 + or leaf == root + or leaf >= len(self.nodes) + or not self.is_active(leaf) + for leaf in leaves + ): + raise EvaluationError("invalid cut leaf") + if len(set(leaves)) != len(leaves): + raise EvaluationError("duplicate cut leaf") + + old_function = self._evaluate_cut( + 2 * root, + leaves, + forbidden_root=None, + require_all_leaves=True, + ) + assignments = 1 << len(leaves) + mask = (1 << assignments) - 1 + values = [0] + values.extend( + self._variable_pattern(index, assignments) for index in range(len(leaves)) + ) + normalized_divisors: list[int] = [] + for divisor in divisors: + if divisor < 0 or divisor >> 1 >= len(self.nodes): + raise EvaluationError("invalid divisor literal") + normalized = self.resolve(divisor) + if normalized >> 1 == root: + raise EvaluationError("divisor resolves to rewritten root") + value = self._evaluate_cut( + normalized, + leaves, + forbidden_root=root, + require_all_leaves=False, + ) + normalized_divisors.append(normalized) + values.append(value) + if normalized_divisors != divisors: + raise EvaluationError("certificate divisor is not normalized") + + for lhs, rhs in local_ands: + lhs_value = self._local_value(lhs, values, mask) + rhs_value = self._local_value(rhs, values, mask) + values.append(lhs_value & rhs_value) + replacement = self._local_value(local_output, values, mask) + if replacement != old_function: + raise EvaluationError("local replacement truth table is not equivalent") + + global_values = [0] + global_values.extend(2 * leaf for leaf in leaves) + global_values.extend(normalized_divisors) + + def translate(local_literal: int) -> int: + reference = local_literal >> 1 + if reference >= len(global_values): + raise EvaluationError("local-to-global translation failed") + return global_values[reference] ^ (local_literal & 1) + + for lhs, rhs in local_ands: + global_lhs = translate(lhs) + global_rhs = translate(rhs) + new_id = len(self.nodes) + self.nodes.append((global_lhs, global_rhs)) + self.kinds.append(self.KIND_AND) + self.redirect.append(2 * new_id) + global_values.append(2 * new_id) + self.redirect[root] = translate(local_output) + checked_rows = assignments * (1 + len(divisors)) + return checked_rows, len(local_ands) + + def stats(self) -> AigStats: + reachable: set[int] = set() + depths: dict[int, int] = {} + visiting: set[int] = set() + + def depth_literal(literal: int) -> int: + literal = self.resolve(literal) + node_id = literal >> 1 + if node_id == 0 or self.kinds[node_id] == self.KIND_INPUT: + return 0 + if self.kinds[node_id] != self.KIND_AND or self.nodes[node_id] is None: + raise EvaluationError("live graph contains an invalid node") + if node_id in depths: + return depths[node_id] + if node_id in visiting: + raise EvaluationError("live graph is cyclic") + visiting.add(node_id) + reachable.add(node_id) + lhs, rhs = self.nodes[node_id] + result = 1 + max(depth_literal(lhs), depth_literal(rhs)) + visiting.remove(node_id) + depths[node_id] = result + return result + + maximum_depth = max(depth_literal(output) for output in self.outputs) + return AigStats(live_ands=len(reachable), depth=maximum_depth) + + def replay(self, certificate: bytes) -> ReplayResult: + digest = hashlib.sha256(certificate).hexdigest() + try: + text = certificate.decode("ascii") + except UnicodeDecodeError as exc: + raise EvaluationError(f"certificate is not ASCII: {exc}") from exc + lines = text.splitlines() + if not lines or lines[0] != "CERT1": + raise EvaluationError("missing CERT1 header") + rewrites = 0 + checked_rows = 0 + appended_ands = 0 + max_rewrites = int(self.limits["max_rewrites"]) + for line_number, line in enumerate(lines[1:], start=2): + if not line: + raise EvaluationError(f"blank certificate line {line_number}") + fields = line.split() + if len(fields) < 6 or fields[0] != "R": + raise EvaluationError(f"malformed certificate line {line_number}") + if any(not field.isascii() or not field.isdecimal() for field in fields[1:]): + raise EvaluationError(f"non-decimal certificate token on line {line_number}") + values = [int(field) for field in fields[1:]] + root, cut_count, divisor_count, and_count = values[:4] + expected = 4 + cut_count + divisor_count + 2 * and_count + 1 + if len(values) != expected: + raise EvaluationError(f"wrong field count on certificate line {line_number}") + if rewrites >= max_rewrites: + raise EvaluationError("certificate exceeds rewrite limit") + cursor = 4 + leaves = values[cursor : cursor + cut_count] + cursor += cut_count + divisors = values[cursor : cursor + divisor_count] + cursor += divisor_count + local_ands = [ + (values[cursor + 2 * index], values[cursor + 2 * index + 1]) + for index in range(and_count) + ] + cursor += 2 * and_count + local_output = values[cursor] + rows, appended = self.apply_rewrite( + root, leaves, divisors, local_ands, local_output + ) + rewrites += 1 + checked_rows += rows + appended_ands += appended + return ReplayResult( + stats=self.stats(), + rewrites=rewrites, + checked_rows=checked_rows, + appended_ands=appended_ands, + certificate_sha256=digest, + ) + + +def _immutable_parts(source: str) -> tuple[str, str]: + if source.count(START_MARKER) != 1 or source.count(END_MARKER) != 1: + raise EvaluationError("candidate must contain exactly one marker pair") + start = source.index(START_MARKER) + start_end = source.index("\n", start) + 1 + end = source.index(END_MARKER, start_end) + if end <= start_end: + raise EvaluationError("EVOLVE markers are out of order") + return source[:start_end], source[end:] + + +def _validate_candidate_shell(candidate_path: Path, max_bytes: int) -> bytes: + if not candidate_path.is_file(): + raise EvaluationError(f"candidate not found: {candidate_path}") + if candidate_path.stat().st_size > max_bytes: + raise EvaluationError("candidate exceeds source-size limit") + candidate = candidate_path.read_bytes() + baseline = BASELINE_PATH.read_bytes() + try: + candidate_text = candidate.decode("utf-8") + baseline_text = baseline.decode("utf-8") + except UnicodeDecodeError as exc: + raise EvaluationError(f"candidate source is not UTF-8: {exc}") from exc + if _immutable_parts(candidate_text) != _immutable_parts(baseline_text): + raise EvaluationError("code outside the EVOLVE block differs from the frozen shell") + return candidate + + +def _tail(path: Path, limit: int = 8000) -> str: + if not path.is_file(): + return "" + data = path.read_bytes() + return data[-limit:].decode("utf-8", errors="replace") + + +def _compile( + compiler: str, + source: Path, + output: Path, + timeout_s: float, + log_path: Path, +) -> None: + command = [ + compiler, + "-std=c++17", + "-O2", + "-DNDEBUG", + "-pipe", + "-Wall", + "-Wextra", + "-pedantic", + "-I", + str(TASK_DIR / "verification"), + str(source), + "-o", + str(output), + ] + with log_path.open("wb") as log: + try: + process = subprocess.run( + command, + cwd=TASK_DIR, + stdout=log, + stderr=subprocess.STDOUT, + timeout=timeout_s, + check=False, + env={**os.environ, "LC_ALL": "C"}, + ) + except subprocess.TimeoutExpired as exc: + raise EvaluationError(f"compilation timed out after {timeout_s:.1f}s") from exc + if process.returncode != 0 or not output.is_file(): + raise EvaluationError( + f"compilation failed with code {process.returncode}: {_tail(log_path)}" + ) + + +def _resource_limits(cpu_s: float, file_bytes: int) -> None: + cpu_limit = max(2, int(math.ceil(cpu_s)) + 1) + resource.setrlimit(resource.RLIMIT_CPU, (cpu_limit, cpu_limit)) + resource.setrlimit(resource.RLIMIT_FSIZE, (file_bytes, file_bytes)) + memory = 2 * 1024 * 1024 * 1024 + resource.setrlimit(resource.RLIMIT_AS, (memory, memory)) + resource.setrlimit(resource.RLIMIT_NOFILE, (64, 64)) + + +@dataclass(frozen=True) +class ProgramRun: + certificate: bytes + stdout_tail: str + elapsed_s: float + + +def _run_program( + executable: Path, + aag: bytes, + run_dir: Path, + timeout_s: float, + max_certificate_bytes: int, +) -> ProgramRun: + run_dir.mkdir(parents=True, exist_ok=False) + input_path = run_dir / "input.aag" + certificate_path = run_dir / "rewrites.cert" + log_path = run_dir / "candidate.log" + input_path.write_bytes(aag) + started = time.perf_counter() + with log_path.open("wb") as log: + process = subprocess.Popen( + [ + str(executable), + "--input", + str(input_path), + "--certificate", + str(certificate_path), + ], + cwd=run_dir, + stdout=log, + stderr=subprocess.STDOUT, + start_new_session=True, + preexec_fn=lambda: _resource_limits(timeout_s, max_certificate_bytes), + env={"PATH": os.environ.get("PATH", ""), "LC_ALL": "C"}, + ) + try: + returncode = process.wait(timeout=timeout_s) + except subprocess.TimeoutExpired as exc: + try: + os.killpg(process.pid, signal.SIGKILL) + except ProcessLookupError: + pass + process.wait() + raise EvaluationError(f"candidate timed out after {timeout_s:.1f}s") from exc + elapsed = time.perf_counter() - started + if returncode != 0: + raise EvaluationError( + f"candidate exited with code {returncode}: {_tail(log_path)}" + ) + if input_path.read_bytes() != aag: + raise EvaluationError("candidate modified the frozen input AAG") + if not certificate_path.is_file(): + raise EvaluationError("candidate did not produce a certificate") + if certificate_path.stat().st_size > max_certificate_bytes: + raise EvaluationError("candidate certificate exceeds size limit") + return ProgramRun( + certificate=certificate_path.read_bytes(), + stdout_tail=_tail(log_path), + elapsed_s=elapsed, + ) + + +def _invalid_metrics(runtime_s: float, *, timeout: bool = False) -> dict[str, float]: + return { + "combined_score": 0.0, + "valid": 0.0, + "timeout": 1.0 if timeout else 0.0, + "runtime_s": float(runtime_s), + } + + +def evaluate( + candidate_path: Path, + *, + timeout_override_s: float | None = None, +) -> tuple[dict[str, float], dict[str, Any]]: + started = time.perf_counter() + artifacts: dict[str, Any] = { + "benchmark_id": "certified_aig_resynthesis", + "checker": "independent exhaustive truth-table replay", + } + try: + config = _validated_config() + limits = config["limits"] + source = _validate_candidate_shell( + candidate_path, int(limits["max_candidate_bytes"]) + ) + compiler = shutil.which("g++") + if compiler is None: + raise EvaluationError("g++ is required but was not found on PATH") + timeout_s = ( + float(timeout_override_s) + if timeout_override_s is not None + else _finite_float( + limits["candidate_timeout_s_per_workload"], "candidate timeout" + ) + ) + if timeout_s <= 0.0: + raise EvaluationError("candidate timeout must be positive") + compile_timeout = _finite_float(limits["compile_timeout_s"], "compile timeout") + workloads: list[tuple[str, bytes]] = [] + workload_manifest: list[dict[str, Any]] = [] + for spec in config["workloads"]: + workload_id = str(spec["id"]) + aag = _generate_workload(spec) + original_stats = ProofChecker(aag, limits).stats() + digest = hashlib.sha256(aag).hexdigest() + if digest != str(spec.get("expected_sha256", "")): + raise EvaluationError( + f"frozen workload digest mismatch for {workload_id}" + ) + if original_stats.live_ands != _positive_int( + spec.get("expected_live_ands"), f"{workload_id}.expected_live_ands" + ) or original_stats.depth != _positive_int( + spec.get("expected_depth"), f"{workload_id}.expected_depth" + ): + raise EvaluationError( + f"frozen workload topology mismatch for {workload_id}" + ) + workloads.append((workload_id, aag)) + workload_manifest.append( + { + "id": workload_id, + "sha256": digest, + "bytes": len(aag), + "input_live_ands": original_stats.live_ands, + "input_depth": original_stats.depth, + } + ) + artifacts["workload_manifest"] = workload_manifest + + with tempfile.TemporaryDirectory(prefix="certified_aig_eval_") as temporary: + temp = Path(temporary) + candidate_copy = temp / "candidate.cpp" + candidate_copy.write_bytes(source) + candidate_executable = temp / "candidate" + baseline_executable = temp / "baseline" + candidate_compile_log = temp / "candidate_compile.log" + baseline_compile_log = temp / "baseline_compile.log" + compile_started = time.perf_counter() + _compile( + compiler, + BASELINE_PATH, + baseline_executable, + compile_timeout, + baseline_compile_log, + ) + baseline_compile_s = time.perf_counter() - compile_started + compile_started = time.perf_counter() + _compile( + compiler, + candidate_copy, + candidate_executable, + compile_timeout, + candidate_compile_log, + ) + candidate_compile_s = time.perf_counter() - compile_started + + area_weight = float(config["objective"]["area_weight"]) + depth_weight = float(config["objective"]["depth_weight"]) + scenario_scores: list[float] = [] + baseline_total_area = 0 + candidate_total_area = 0 + baseline_depth_sum = 0 + candidate_depth_sum = 0 + total_checked_rows = 0 + workload_results: dict[str, Any] = {} + for index, (workload_id, aag) in enumerate(workloads): + baseline_run = _run_program( + baseline_executable, + aag, + temp / f"baseline_{index}", + timeout_s, + int(limits["max_certificate_bytes"]), + ) + candidate_run = _run_program( + candidate_executable, + aag, + temp / f"candidate_{index}", + timeout_s, + int(limits["max_certificate_bytes"]), + ) + baseline_result = ProofChecker(aag, limits).replay( + baseline_run.certificate + ) + candidate_result = ProofChecker(aag, limits).replay( + candidate_run.certificate + ) + baseline_stats = baseline_result.stats + candidate_stats = candidate_result.stats + if ( + baseline_stats.live_ands <= 0 + or baseline_stats.depth <= 0 + or candidate_stats.live_ands <= 0 + or candidate_stats.depth <= 0 + ): + raise EvaluationError("a workload produced a degenerate scored graph") + area_ratio = baseline_stats.live_ands / candidate_stats.live_ands + depth_ratio = baseline_stats.depth / candidate_stats.depth + scenario_score = (area_ratio**area_weight) * ( + depth_ratio**depth_weight + ) + if not math.isfinite(scenario_score) or scenario_score <= 0.0: + raise EvaluationError("non-finite workload score") + scenario_scores.append(scenario_score) + baseline_total_area += baseline_stats.live_ands + candidate_total_area += candidate_stats.live_ands + baseline_depth_sum += baseline_stats.depth + candidate_depth_sum += candidate_stats.depth + total_checked_rows += candidate_result.checked_rows + workload_results[workload_id] = { + "score": scenario_score, + "area_ratio": area_ratio, + "depth_ratio": depth_ratio, + "baseline": { + "live_ands": baseline_stats.live_ands, + "depth": baseline_stats.depth, + "accepted_rewrites": baseline_result.rewrites, + "checked_truth_rows": baseline_result.checked_rows, + "appended_ands": baseline_result.appended_ands, + "certificate_sha256": baseline_result.certificate_sha256, + "runtime_s": baseline_run.elapsed_s, + "stdout_tail": baseline_run.stdout_tail, + }, + "candidate": { + "live_ands": candidate_stats.live_ands, + "depth": candidate_stats.depth, + "accepted_rewrites": candidate_result.rewrites, + "checked_truth_rows": candidate_result.checked_rows, + "appended_ands": candidate_result.appended_ands, + "certificate_sha256": candidate_result.certificate_sha256, + "runtime_s": candidate_run.elapsed_s, + "stdout_tail": candidate_run.stdout_tail, + }, + } + + combined_score = math.exp( + sum(math.log(score) for score in scenario_scores) + / len(scenario_scores) + ) + runtime_s = time.perf_counter() - started + metrics = { + "combined_score": combined_score, + "valid": 1.0, + "timeout": 0.0, + "runtime_s": runtime_s, + "scenario_count": float(len(scenario_scores)), + "mean_score": sum(scenario_scores) / len(scenario_scores), + "min_score": min(scenario_scores), + "baseline_total_area": float(baseline_total_area), + "candidate_total_area": float(candidate_total_area), + "baseline_mean_depth": baseline_depth_sum / len(scenario_scores), + "candidate_mean_depth": candidate_depth_sum / len(scenario_scores), + "checked_truth_rows": float(total_checked_rows), + } + artifacts["compiler"] = compiler + artifacts["compile"] = { + "baseline_s": baseline_compile_s, + "candidate_s": candidate_compile_s, + } + artifacts["objective"] = config["objective"] + artifacts["limits"] = limits + artifacts["workloads"] = workload_results + return metrics, artifacts + except Exception as exc: + message = str(exc) + artifacts["error_message"] = message + timed_out = "timed out" in message.lower() + return _invalid_metrics(time.perf_counter() - started, timeout=timed_out), artifacts + + +def _write_json(path_text: str | None, payload: dict[str, Any]) -> None: + if not path_text: + return + path = Path(path_text).expanduser().resolve() + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text( + json.dumps(payload, indent=2, sort_keys=True, allow_nan=False) + "\n", + encoding="utf-8", + ) + + +def parse_args() -> argparse.Namespace: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("candidate", help="candidate C++ source") + parser.add_argument( + "--timeout-s", + type=float, + default=None, + help="optional per-workload execution timeout override", + ) + parser.add_argument("--metrics-out", default=None) + parser.add_argument("--artifacts-out", default=None) + return parser.parse_args() + + +def main() -> int: + args = parse_args() + timeout = None if args.timeout_s is None else max(0.1, float(args.timeout_s)) + metrics, artifacts = evaluate( + Path(args.candidate).expanduser().resolve(), timeout_override_s=timeout + ) + _write_json(args.metrics_out, metrics) + _write_json(args.artifacts_out, artifacts) + print(json.dumps(metrics, sort_keys=True, allow_nan=False)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/requirements.txt b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/requirements.txt new file mode 100644 index 00000000..2e457109 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/requirements.txt @@ -0,0 +1 @@ +# No third-party Python packages are required. diff --git a/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/rewrite_runtime.hpp b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/rewrite_runtime.hpp new file mode 100644 index 00000000..b4fd4921 --- /dev/null +++ b/benchmarks/ElectronicDesignAutomation/CertifiedAIGResynthesis/verification/rewrite_runtime.hpp @@ -0,0 +1,602 @@ +// Immutable runtime and public API for certified AIG resynthesis candidates. +// +// This header parses ASCII AIGER, maintains the current Boolean DAG, +// validates every proposed local replacement exactly, and emits a replayable +// certificate. Search algorithms must not modify this file. + +#pragma once + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace certified_aig { + +constexpr std::uint32_t kMaxCutLeaves = 8; +constexpr std::uint32_t kMaxDivisors = 16; +constexpr std::uint32_t kMaxLocalAnds = 64; +constexpr std::uint32_t kMaxRewrites = 20000; +constexpr std::uint32_t kMaxTotalNodes = 300000; + +struct LocalAnd { + std::uint32_t lhs; + std::uint32_t rhs; +}; + +struct TruthTable { + std::array words{}; + std::uint32_t variables = 0; + + bool operator==(const TruthTable& other) const { + return variables == other.variables && words == other.words; + } +}; + +struct NetworkStats { + std::uint32_t live_ands = 0; + std::uint32_t depth = 0; +}; + +class Optimizer { + public: + explicit Optimizer(const std::string& input_path, + const std::string& certificate_path) { + load_aag(input_path); + original_node_count_ = static_cast(nodes_.size()); + certificate_.open(certificate_path, std::ios::out | std::ios::trunc); + if (!certificate_) { + throw std::runtime_error("cannot open certificate output: " + + certificate_path); + } + certificate_ << "CERT1\n"; + if (!certificate_) { + throw std::runtime_error("cannot write certificate header"); + } + } + + std::uint32_t first_and_id() const { return first_and_id_; } + std::uint32_t original_node_count() const { return original_node_count_; } + std::uint32_t node_count() const { + return static_cast(nodes_.size()); + } + std::uint32_t input_count() const { return input_count_; } + std::uint32_t output_count() const { + return static_cast(outputs_.size()); + } + std::uint32_t output_literal(std::uint32_t index) const { + if (index >= outputs_.size()) { + throw std::out_of_range("output index is out of range"); + } + return resolve(outputs_[index]); + } + std::uint32_t accepted_rewrites() const { return accepted_rewrites_; } + + bool is_and(std::uint32_t id) const { + return id < nodes_.size() && nodes_[id].kind == Kind::kAnd; + } + + bool is_primary_input(std::uint32_t id) const { + return id < nodes_.size() && nodes_[id].kind == Kind::kInput; + } + + bool is_active(std::uint32_t id) const { + return id < redirect_.size() && redirect_[id] == (id << 1U); + } + + // Resolve a global AIG literal through all previously accepted rewrites. + // Literal encoding follows AIGER: 2*node_id is positive, xor 1 is inverted. + std::uint32_t resolve(std::uint32_t literal) const { + if ((literal >> 1U) >= redirect_.size()) { + throw std::out_of_range("global literal references an unknown node"); + } + std::uint32_t id = literal >> 1U; + std::uint32_t inverted = literal & 1U; + for (std::size_t steps = 0; steps <= redirect_.size(); ++steps) { + const std::uint32_t mapped = redirect_[id]; + if (mapped == (id << 1U)) { + return (id << 1U) | inverted; + } + inverted ^= mapped & 1U; + id = mapped >> 1U; + if (id >= redirect_.size()) { + throw std::runtime_error("corrupt rewrite redirect"); + } + } + throw std::runtime_error("cycle in rewrite redirects"); + } + + std::pair fanins( + std::uint32_t id) const { + if (!is_and(id) || !is_active(id)) { + throw std::invalid_argument("fanins() needs an active AND node"); + } + return {resolve(nodes_[id].lhs), resolve(nodes_[id].rhs)}; + } + + // Return the primary-input support when it fits within limit. An empty + // optional means that the limit was exceeded or the root was invalid. + std::optional> primary_support( + std::uint32_t root, std::uint32_t limit = kMaxCutLeaves) const { + if (root >= nodes_.size() || !is_active(root) || limit > kMaxCutLeaves) { + return std::nullopt; + } + std::set support; + std::unordered_set visiting; + std::unordered_set done; + std::function visit_literal; + visit_literal = [&](std::uint32_t literal) -> bool { + literal = resolve(literal); + const std::uint32_t id = literal >> 1U; + if (id == 0) return true; + if (is_primary_input(id)) { + support.insert(id); + return support.size() <= limit; + } + if (!is_and(id)) return false; + if (done.count(id)) return true; + if (!visiting.insert(id).second) return false; + const bool ok = visit_literal(nodes_[id].lhs) && + visit_literal(nodes_[id].rhs); + visiting.erase(id); + done.insert(id); + return ok; + }; + if (!visit_literal(root << 1U) || support.size() > limit) { + return std::nullopt; + } + return std::vector(support.begin(), support.end()); + } + + bool truth_table(std::uint32_t root, + const std::vector& leaves, + TruthTable* output) const { + if (output == nullptr || root >= nodes_.size() || !is_active(root)) { + return false; + } + std::string error; + return evaluate_cut(root << 1U, leaves, kNoForbiddenRoot, true, output, + &error); + } + + // Propose an arbitrary local AIG replacement. + // + // Local literal encoding is 2*reference xor polarity: + // reference 0 : constant false + // references 1..k : positive cut leaves + // references k+1..k+d : supplied global divisor literals + // later references : LocalAnd results, in order + // + // Divisors may come from outside the root cone, but they must themselves be + // functions of the same cut leaves and must not depend on root. This is the + // usual DAG-aware resynthesis setting: existing equivalent logic can be + // reused without adding gates. The method returns false for an invalid or + // non-equivalent proposal and changes nothing. + bool try_rewrite(std::uint32_t root, + const std::vector& leaves, + const std::vector& divisors, + const std::vector& local_ands, + std::uint32_t local_output) { + if (accepted_rewrites_ >= kMaxRewrites || root >= nodes_.size() || + !is_and(root) || !is_active(root) || + leaves.size() > kMaxCutLeaves || divisors.size() > kMaxDivisors || + local_ands.size() > kMaxLocalAnds || + nodes_.size() + local_ands.size() > kMaxTotalNodes) { + return false; + } + + std::unordered_set unique_leaves; + for (const std::uint32_t leaf : leaves) { + if (leaf == 0 || leaf == root || leaf >= nodes_.size() || + !is_active(leaf) || !unique_leaves.insert(leaf).second) { + return false; + } + } + + TruthTable old_function; + std::string error; + if (!evaluate_cut(root << 1U, leaves, kNoForbiddenRoot, true, + &old_function, &error)) { + return false; + } + + const std::uint32_t assignments = 1U << leaves.size(); + const std::uint32_t word_count = (assignments + 63U) / 64U; + const std::uint64_t final_mask = + (assignments % 64U == 0U) + ? std::numeric_limits::max() + : ((std::uint64_t{1} << (assignments % 64U)) - 1U); + + std::vector values; + values.reserve(1 + leaves.size() + divisors.size() + local_ands.size()); + TruthTable constant; + constant.variables = static_cast(leaves.size()); + values.push_back(constant); + + for (std::size_t index = 0; index < leaves.size(); ++index) { + TruthTable variable; + variable.variables = static_cast(leaves.size()); + for (std::uint32_t assignment = 0; assignment < assignments; + ++assignment) { + if ((assignment >> index) & 1U) { + variable.words[assignment / 64U] |= + std::uint64_t{1} << (assignment % 64U); + } + } + values.push_back(variable); + } + + std::vector normalized_divisors; + normalized_divisors.reserve(divisors.size()); + for (const std::uint32_t divisor : divisors) { + if ((divisor >> 1U) >= nodes_.size()) return false; + std::uint32_t normalized; + try { + normalized = resolve(divisor); + } catch (const std::exception&) { + return false; + } + if ((normalized >> 1U) == root) return false; + TruthTable divisor_function; + if (!evaluate_cut(normalized, leaves, root, false, &divisor_function, + &error)) { + return false; + } + normalized_divisors.push_back(normalized); + values.push_back(divisor_function); + } + + auto local_value = [&](std::uint32_t literal, + TruthTable* result) -> bool { + const std::uint32_t reference = literal >> 1U; + if (reference >= values.size()) return false; + *result = values[reference]; + if (literal & 1U) { + for (std::uint32_t word = 0; word < word_count; ++word) { + result->words[word] = ~result->words[word]; + } + result->words[word_count - 1U] &= final_mask; + } + return true; + }; + + for (const LocalAnd gate : local_ands) { + TruthTable lhs; + TruthTable rhs; + if (!local_value(gate.lhs, &lhs) || !local_value(gate.rhs, &rhs)) { + return false; + } + TruthTable result; + result.variables = static_cast(leaves.size()); + for (std::uint32_t word = 0; word < word_count; ++word) { + result.words[word] = lhs.words[word] & rhs.words[word]; + } + values.push_back(result); + } + + TruthTable replacement; + if (!local_value(local_output, &replacement) || + !(replacement == old_function)) { + return false; + } + + certificate_ << "R " << root << ' ' << leaves.size() << ' ' + << normalized_divisors.size() << ' ' << local_ands.size(); + for (const std::uint32_t leaf : leaves) certificate_ << ' ' << leaf; + for (const std::uint32_t divisor : normalized_divisors) { + certificate_ << ' ' << divisor; + } + for (const LocalAnd gate : local_ands) { + certificate_ << ' ' << gate.lhs << ' ' << gate.rhs; + } + certificate_ << ' ' << local_output << '\n'; + if (!certificate_) { + throw std::runtime_error("failed while writing rewrite certificate"); + } + + std::vector global_values; + global_values.reserve(values.size()); + global_values.push_back(0U); + for (const std::uint32_t leaf : leaves) { + global_values.push_back(leaf << 1U); + } + for (const std::uint32_t divisor : normalized_divisors) { + global_values.push_back(divisor); + } + auto translate_local = [&](std::uint32_t literal) -> std::uint32_t { + const std::uint32_t reference = literal >> 1U; + if (reference >= global_values.size()) { + throw std::runtime_error("internal local-literal translation failure"); + } + return global_values[reference] ^ (literal & 1U); + }; + for (const LocalAnd gate : local_ands) { + const std::uint32_t lhs = translate_local(gate.lhs); + const std::uint32_t rhs = translate_local(gate.rhs); + Node node; + node.kind = Kind::kAnd; + node.lhs = lhs; + node.rhs = rhs; + nodes_.push_back(node); + const std::uint32_t new_id = + static_cast(nodes_.size() - 1U); + redirect_.push_back(new_id << 1U); + global_values.push_back(new_id << 1U); + } + redirect_[root] = translate_local(local_output); + ++accepted_rewrites_; + return true; + } + + // Convenience wrapper for replacing root by an existing global literal. + // `leaves` must be a structural cut for root and for any external divisor. + bool replace(std::uint32_t root, std::uint32_t replacement, + const std::vector& leaves) { + try { + replacement = resolve(replacement); + } catch (const std::exception&) { + return false; + } + const std::uint32_t replacement_id = replacement >> 1U; + if (replacement_id == 0U) { + return try_rewrite(root, leaves, {}, {}, replacement & 1U); + } + for (std::size_t index = 0; index < leaves.size(); ++index) { + if (leaves[index] == replacement_id) { + const std::uint32_t local_literal = + (static_cast(index) + 1U) << 1U; + return try_rewrite(root, leaves, {}, {}, + local_literal ^ (replacement & 1U)); + } + } + const std::uint32_t divisor_reference = + static_cast(leaves.size()) + 1U; + return try_rewrite(root, leaves, {replacement}, {}, + divisor_reference << 1U); + } + + NetworkStats stats() const { + std::unordered_set reachable; + std::unordered_map depths; + std::unordered_set visiting; + std::function depth_literal; + depth_literal = [&](std::uint32_t literal) -> std::uint32_t { + literal = resolve(literal); + const std::uint32_t id = literal >> 1U; + if (id == 0U || is_primary_input(id)) return 0U; + const auto cached = depths.find(id); + if (cached != depths.end()) return cached->second; + if (!is_and(id) || !visiting.insert(id).second) { + throw std::runtime_error("invalid or cyclic live AIG"); + } + reachable.insert(id); + const std::uint32_t result = + 1U + std::max(depth_literal(nodes_[id].lhs), + depth_literal(nodes_[id].rhs)); + visiting.erase(id); + depths[id] = result; + return result; + }; + std::uint32_t max_depth = 0; + for (const std::uint32_t output : outputs_) { + max_depth = std::max(max_depth, depth_literal(output)); + } + return {static_cast(reachable.size()), max_depth}; + } + + private: + enum class Kind : std::uint8_t { kUnused, kInput, kAnd }; + struct Node { + Kind kind = Kind::kUnused; + std::uint32_t lhs = 0; + std::uint32_t rhs = 0; + }; + + static constexpr std::uint32_t kNoForbiddenRoot = + std::numeric_limits::max(); + + static std::vector parse_numbers(const std::string& line) { + std::istringstream stream(line); + std::vector values; + std::uint64_t value = 0; + while (stream >> value) values.push_back(value); + if (!stream.eof()) throw std::runtime_error("malformed numeric AAG line"); + return values; + } + + void load_aag(const std::string& path) { + std::ifstream input(path); + if (!input) throw std::runtime_error("cannot open AAG input: " + path); + std::string line; + if (!std::getline(input, line)) throw std::runtime_error("empty AAG input"); + std::istringstream header(line); + std::string magic; + std::uint64_t maximum = 0, inputs = 0, latches = 0, outputs = 0, ands = 0; + if (!(header >> magic >> maximum >> inputs >> latches >> outputs >> ands) || + magic != "aag" || latches != 0 || maximum > kMaxTotalNodes || + maximum != inputs + ands || inputs == 0 || outputs == 0) { + throw std::runtime_error("unsupported AAG header"); + } + input_count_ = static_cast(inputs); + first_and_id_ = input_count_ + 1U; + nodes_.assign(static_cast(maximum) + 1U, Node{}); + redirect_.resize(nodes_.size()); + for (std::uint32_t id = 0; id < redirect_.size(); ++id) { + redirect_[id] = id << 1U; + } + for (std::uint32_t index = 0; index < input_count_; ++index) { + if (!std::getline(input, line)) throw std::runtime_error("truncated inputs"); + const auto fields = parse_numbers(line); + const std::uint32_t expected_id = index + 1U; + if (fields.size() != 1U || fields[0] != (expected_id << 1U)) { + throw std::runtime_error("inputs must use consecutive positive literals"); + } + nodes_[expected_id].kind = Kind::kInput; + } + outputs_.reserve(static_cast(outputs)); + for (std::uint64_t index = 0; index < outputs; ++index) { + if (!std::getline(input, line)) throw std::runtime_error("truncated outputs"); + const auto fields = parse_numbers(line); + if (fields.size() != 1U || fields[0] > 2U * maximum + 1U) { + throw std::runtime_error("invalid output literal"); + } + outputs_.push_back(static_cast(fields[0])); + } + for (std::uint64_t index = 0; index < ands; ++index) { + if (!std::getline(input, line)) throw std::runtime_error("truncated ANDs"); + const auto fields = parse_numbers(line); + const std::uint32_t id = first_and_id_ + static_cast(index); + if (fields.size() != 3U || fields[0] != (id << 1U) || + fields[1] >= fields[0] || fields[2] >= fields[0]) { + throw std::runtime_error("AND nodes must be consecutive and topological"); + } + nodes_[id].kind = Kind::kAnd; + nodes_[id].lhs = static_cast(fields[1]); + nodes_[id].rhs = static_cast(fields[2]); + } + } + + static TruthTable inverted(TruthTable value) { + const std::uint32_t assignments = 1U << value.variables; + const std::uint32_t word_count = (assignments + 63U) / 64U; + for (std::uint32_t word = 0; word < word_count; ++word) { + value.words[word] = ~value.words[word]; + } + if (assignments % 64U != 0U) { + value.words[word_count - 1U] &= + (std::uint64_t{1} << (assignments % 64U)) - 1U; + } + return value; + } + + bool evaluate_cut(std::uint32_t literal, + const std::vector& leaves, + std::uint32_t forbidden_root, bool require_all_leaves, + TruthTable* output, std::string* error) const { + if (leaves.size() > kMaxCutLeaves) return false; + std::unordered_map leaf_indices; + for (std::size_t index = 0; index < leaves.size(); ++index) { + if (!leaf_indices.emplace(leaves[index], index).second) return false; + } + std::vector used(leaves.size(), false); + std::unordered_map memo; + std::unordered_set visiting; + bool failed = false; + const std::uint32_t assignments = 1U << leaves.size(); + + std::function evaluate_literal; + std::function evaluate_node; + evaluate_node = [&](std::uint32_t id) -> TruthTable { + TruthTable zero; + zero.variables = static_cast(leaves.size()); + if (failed) return zero; + const auto leaf = leaf_indices.find(id); + if (leaf != leaf_indices.end()) { + used[leaf->second] = true; + TruthTable variable = zero; + for (std::uint32_t assignment = 0; assignment < assignments; + ++assignment) { + if ((assignment >> leaf->second) & 1U) { + variable.words[assignment / 64U] |= + std::uint64_t{1} << (assignment % 64U); + } + } + return variable; + } + if (id == 0U) return zero; + if (id == forbidden_root) { + failed = true; + if (error) *error = "divisor depends on rewritten root"; + return zero; + } + if (is_primary_input(id)) { + failed = true; + if (error) *error = "cut does not cover a primary-input path"; + return zero; + } + const auto cached = memo.find(id); + if (cached != memo.end()) return cached->second; + if (!is_and(id) || !visiting.insert(id).second) { + failed = true; + if (error) *error = "invalid or cyclic cut cone"; + return zero; + } + TruthTable lhs = evaluate_literal(nodes_[id].lhs); + TruthTable rhs = evaluate_literal(nodes_[id].rhs); + visiting.erase(id); + TruthTable result = zero; + for (std::size_t word = 0; word < result.words.size(); ++word) { + result.words[word] = lhs.words[word] & rhs.words[word]; + } + memo[id] = result; + return result; + }; + evaluate_literal = [&](std::uint32_t input_literal) -> TruthTable { + TruthTable zero; + zero.variables = static_cast(leaves.size()); + if (failed) return zero; + std::uint32_t normalized = 0; + try { + normalized = resolve(input_literal); + } catch (const std::exception& exc) { + failed = true; + if (error) *error = exc.what(); + return zero; + } + TruthTable value = evaluate_node(normalized >> 1U); + return (normalized & 1U) ? inverted(value) : value; + }; + + *output = evaluate_literal(literal); + if (failed) return false; + if (require_all_leaves && + std::find(used.begin(), used.end(), false) != used.end()) { + if (error) *error = "cut contains a leaf outside the root cone"; + return false; + } + return true; + } + + std::vector nodes_; + std::vector redirect_; + std::vector outputs_; + std::uint32_t input_count_ = 0; + std::uint32_t first_and_id_ = 0; + std::uint32_t original_node_count_ = 0; + std::uint32_t accepted_rewrites_ = 0; + std::ofstream certificate_; +}; + +static std::vector boundary_nodes( + std::uint32_t lhs, std::uint32_t rhs) { + std::vector leaves; + const std::uint32_t lhs_id = lhs >> 1U; + const std::uint32_t rhs_id = rhs >> 1U; + if (lhs_id != 0U) leaves.push_back(lhs_id); + if (rhs_id != 0U && rhs_id != lhs_id) leaves.push_back(rhs_id); + return leaves; +} + +} // namespace certified_aig diff --git a/benchmarks/ElectronicDesignAutomation/README.md b/benchmarks/ElectronicDesignAutomation/README.md index 7bb075ff..b5798946 100644 --- a/benchmarks/ElectronicDesignAutomation/README.md +++ b/benchmarks/ElectronicDesignAutomation/README.md @@ -1,3 +1,15 @@ # Electronic Design Automation -> This task is not yet complete and is in progress. \ No newline at end of file +Electronic design automation turns behavioral and structural circuit descriptions +into implementations that satisfy correctness, area, timing, power, and physical +constraints. The tasks here expose optimization decisions together with +machine-checkable engineering objectives. + +## Tasks + +| Task | Description | Runtime | +|---|---|---| +| [CertifiedAIGResynthesis](CertifiedAIGResynthesis/) | Proof-carrying, DAG-aware Boolean resynthesis with exact small-cut equivalence checking and area/depth scoring | Python 3 + C++17; CPU only | + +`IntegrationPhysicalDesignOptimization` is retained as a historical placeholder +and is not an executable benchmark. diff --git a/benchmarks/ElectronicDesignAutomation/README_zh-CN.md b/benchmarks/ElectronicDesignAutomation/README_zh-CN.md index 7bed5a94..b058d99a 100644 --- a/benchmarks/ElectronicDesignAutomation/README_zh-CN.md +++ b/benchmarks/ElectronicDesignAutomation/README_zh-CN.md @@ -1,3 +1,13 @@ # 电子设计自动化 -> 这个任务尚且没有完善，正在进行中 \ No newline at end of file +电子设计自动化将行为级或结构级电路描述转化为满足功能正确性、面积、 +时序、功耗和物理约束的实现。本领域任务同时提供可优化的工程决策与可由 +机器独立验证的目标。 + +## 任务 + +| 任务 | 描述 | 运行环境 | +|---|---|---| +| [CertifiedAIGResynthesis](CertifiedAIGResynthesis/) | 带证明证书的 DAG 感知布尔重综合：精确验证小割集等价性，并按面积与深度评分 | Python 3 + C++17；仅 CPU | + +`IntegrationPhysicalDesignOptimization` 仅保留为历史占位，不是可执行基准。