Nayab Hossain
CEO,
Chipster
About the Speaker
Nayab Hossain is a Computer Engineering student at San José State University working on Chipster, an autonomous formal verification system for ASIC and SoC RTL designs. His work focuses on AI – assisted assertion generation, formal proof, non-vacuity analysis, and verification automation. He is also in Plug and Play’s accelerator program and has earned 10+ awards through engineering
competitions and hackathons.
Formal Verification via Data Generation & Bi-directional Data Synthesis
Overview
Formal verification is difficult to scale with AI because high-quality assertion and proof data remains scarce. This talk presents an approach to generating stronger verification data through automated formal feedback and bi-directional data synthesis. Using RTL, naturallanguage specifications, SystemVerilog Assertions, proof results, counterexamples, non-vacuity checks, and coverage signals, the workflow creates iterative training and evaluation data for LLM assisted verification. The presentation will discuss the architecture, data-generation process, experimental results, and the challenges involved in building more reliable autonomous formal-verification
systems.
Key Points
- Why the scarcity of high-quality formal verification data limits LLM performance in hardware verification.
- How automated data generation and bi-directional data synthesis can create richer RTL, specification, assertion, and proof datasets.
- How formal proof, counterexamples, non-vacuity checks, and coverage feedback can be used to improve the reliability of AI – generated assertions.
