Skip to content

CODA-Team/TACO

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

2 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

TACO — Theory-guided Action-space Compression(-Guided) Orchestration

Logic optimization engine: context-guided AIG orchestration plus a native-MIG, NDP-audited orchestration loop, with theorem-certified predicate gates (provably lossless skips) on top.

Modes: certified (-C, theorem mechanisms only) and fast mode (the default; older artifacts call it "full mode" — same thing, result directory names kept as-is).

Build

You need Berkeley ABC and the mockturtle headers at these exact pins:

  • ABC revision bcfdf592289a408cd67ec19260f8a60a37b085b6
  • mockturtle revision fb8f879829f269692f211bb6026bc34a6ca508b6, checked out as a sibling directory of the ABC root named mockturtle-fb8f879829f269692f211bb6026bc34a6ca508b6

Then install the overlay and build:

python3 implementation/cgo_overlay/apply_cgo_overlay.py --check  <ABC_ROOT>
python3 implementation/cgo_overlay/apply_cgo_overlay.py --apply  <ABC_ROOT>
python3 implementation/cgo_overlay/apply_cgo_overlay.py --verify <ABC_ROOT>
cd <ABC_ROOT> && make -j8 ABC_USE_CUDD=1 ABC_USE_PTHREADS=1

Run

# Orchestration track (AIG in, AIG out; -M 0 single, 1 iterative, 2 resyn, 3 resyn3)
abc -q "read_aiger <case>.aig; strash; cgo -M 2; write_aiger out.aig"

# HeLO track (native-MIG orchestration; NDP-audited)
abc -q "read_aiger <case>.aig; strash; cgo -M 2; cgo_mig -o out.mig20"

# Certified mode: add -C to cgo and/or cgo_mig.  Gate bitmask: -G <bits>
# (1=P1, 2=P2, 4=P3, 8=P4, 16=T9.1 on cgo; 32=P5', 64=P6, 128=P12 on cgo_mig).

# Gated-skip exhibit: stock orchestrate with two certified pre-filters —
# output bit-identical to baseline orchestrate, ~5% faster
abc -q "read_aiger <case>.aig; strash; orchestrate -g 3; write_aiger out.aig"

Layout

  • implementation/cgo_overlay/ — the optimizer: src/opt/cgo/ (native-MIG orchestration, cgo_mig) + patches/ (cgo command + build glue) + apply_cgo_overlay.py (check/apply/verify).
  • benchmarks/ — input AIGs and manifests: real_visible.jsonl (55 dev cases, dev_aigs/), orchestration_paper_inputs.jsonl (11 paper inputs, paper_aigs/, sha256-pinned), helo_development.jsonl (6 HeLO cases: paper_aigs/, epfl/, mockturtle/), and the trusted reference values orchestration_paper.jsonl / helo_paper.jsonl.
  • results/ — everything we produced:
    • orchestration/, orchestration_certified/ — 66 cases × 4 modes, output AIGs (aigs/), runtime.json, cgo_pass_stats.json;
    • helo/, helo_certified/, helo_max/, helo_max_certified/ — 6 cases, output migs/*.mig20, runtime.json, cgo_mig_stats.json;
    • gates/bit_identity.json (gated-skip vs stock orchestrate, all 66 circuits bit-identical, per-gate split), per_gate_matrix.json (each gate alone vs all-on);
    • cec/report.json — final CEC sweep: 552/552 equivalent, 0 failures;
    • comparison_orchestration.json, comparison_helo.json — the side-by-side comparison tables.

Headline numbers (from results/)

  • HeLO track, NDP vs the paper's published values, 6/6 wins on every certified track; best track geomean 0.8996 (max-effort certified), per-case best: fpu 0.823, mem_ctrl 0.873, aes_core 0.880.
  • Orchestration track vs the paper's columns: geomean 0.87–1.013 (resyn3 0.870; only LGP_resyn/LGP_resyn3 marginally ahead at 1.006/1.013).
  • Gated-skip: 66/66 bit-identical outputs, −5.3% runtime on stock orchestrate.

About

TACO(Theory-guided Action-space Compression for Orchestration) for logic optimization

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages