Welcome to Pomelo, an open-source initiative dedicated to advancing the state-of-the-art in DRAM specification formalization and tooling. Pomelo is part of a research program at Normal Computing focused on enhancing and extending the DRAMml modeling language and its associated tools.
Pomelo aims to create robust datasets, benchmarks, and automated formalization frameworks to foster research and innovation in formal methods for hardware verification.
The Pomelo project is structured into three primary workstreams:
We leverage existing DRAMml models as high-quality "gold standard" datasets to drive advancements in formal specification techniques. Our goal is to provide the research community with openly accessible datasets and clearly defined benchmarks for evaluating automated specification formalization tools.
Key Objectives:
- Curate existing DRAM specifications into structured datasets.
- Develop a publicly available benchmark suite with evaluation metrics.
- Provide synthetic and augmented datasets to enhance training robustness.
Outputs:
- Benchmark datasets and documentation
- Baseline performance reports
- Published technical reports or papers
Pomelo is evolving the DRAMml language to broaden its applicability and expressiveness, potentially developing a generalized modeling language (tentatively "CHIPml") suitable for various hardware specifications beyond DRAM.
Key Objectives:
- Collaborative ideation and knowledge transfer
- Extend DRAMml with generalized abstractions and semantics
- Incorporate community research ideas
Outputs:
- Extended DRAMml ("CHIPml") specification
- Peer-reviewed research publications
- Whitepapers and community feedback documents
Pomelo actively develops a robust, open-source toolchain around DRAMml, focusing on simulation, verification, and test generation. Our toolkit integrates Normal Computing’s existing stimulus generators with community insights and possibly the DRAMSys simulator for a seamless verification workflow.
Key Objectives:
- Build and debug simulation and verification tooling
- Generalize tooling for DDR3, DDR4, DDR5, and future DRAM standards
- Develop sustainable, open-source infrastructure
Outputs:
- Open-source codebase available on GitHub
- Documentation, tutorials, and comprehensive examples
- Demonstrations and integration guides
Clone the repository:
git clone https://github.com/normal-computing/pomelo.git
cd pomelo
Check out our documentation to learn how to set up and use the tools.
We invite contributions from the broader community. Please see our contributing guide for details on how to participate, report bugs, request features, or improve documentation.
For further reading, please refer to our published benchmarks, technical reports, and research papers available within the repository under docs/
.
Pomelo is actively developed in collaboration with:
- Normal Computing
- Oxford University (formalization research collaboration)
- Others
Join our discussion forum or attend our bi-weekly community meetings.
Pomelo is built on a philosophy of openness, collaboration, and innovation in formal methods. We welcome your participation in shaping the future of executable hardware specifications!