Yosys + egglog: supercharge your passes with equality saturation
summary
Prototype Yosys plugin converts RTL into an egraph via egraph ingestion and expansion, runs many rewrites simultaneously (examples shown: commutativity and a retiming rewrite) and writes optimized RTL back with a single-command Yosys pass. Rewrites come from a user script but the tool handles ingestion; extraction chooses a result and can incorporate extraction-time metrics. Current limits: conversion cost and RAM for large designs are real but active work (including a 10× ingestion speedup) is reducing them.
AI-written summary · about
chapters (7)
- 0:00Yosys and egglog intro
- 1:43What is equality saturation
- 3:30How equality saturation works
- 3:50Egglog transformation demo
- 8:48Yosys + egglog integration
- 9:30Yosys pass demo
- 10:35Q&A
related talks
19mLoop Rerolling for Hardware Decompilation
23mLoop Saturation for Scalable High-Level Synthesis
30megg: Fast and Extensible Equality Saturation
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
17mBetter Together: Unifying Datalog and Equality Saturation
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification
22mOatlog: A performant ahead-of-time compiled e-graph engine
19meqsat: An Equality Saturation Dialect for Non-destructive Rewriting