Fungible Memories for Automated Technology Mapping and Retargeting
summary
Memo implements a write-once, map-anywhere memory abstraction that automatically retargets memories across simulation, FPGA and ASIC backends, and lifts gate-level nets back to high-level memories. A Lean formalization proves its rewrite rules preserve read/write semantics, and the tool reduces a Pearl register-file from 130 lines to 3. Memory decompilation uses structure-aware scope rewriting, inverse transformations, and equality saturation in SQLite to recover memories Yosys misses and handles 700k gates in ~1 min, 1.5M in ~2 min, 12M in ~6 min.
AI-written summary · about
chapters (17)
- 0:00Introduction
- 0:43Current memory mapping problems
- 3:10Technology-specific mapping challenges
- 5:19Fungible memories abstraction
- 7:04Formalizing in Lean
- 7:45Memory compiler with fungible
- 9:07Need for memory decompilation
- 9:48How decompilation works
- 11:14Optimizations for decompilation
- 12:58Equality saturation in SQLite
- 14:02Memo tool workflow
- 15:05Memory decompiler evaluation
- 16:31Case study results
- 17:35Takeaways and future work
- 18:17Open-source tools and conclusion
- 18:39Q&A part one
- 19:41Q&A part two
related talks
18mHarvesting Idle Memory for Application-managed Soft State with Midas
01h 04mWe Live in Interesting Times
43mMemento Memori
14mFreedom from memory interference
15mModal Abstractions for Virtualizing Memory Addresses
17mA Difference World: High-performance, NVM-invariant, Software-only Intermittent...
01h 03mPrinciples of Persistent Programming
16mMemory-Efficient Fixpoint Computation