Synthesizing Correct Hardware Without Hallucination

Speaker: Dr Satnam Singh - Harmonic. Visiting academic at the Department of Computer Science and Technology, University of Cambridge
Series: Wednesday Seminars – Department of Computer Science and Technology

Hardware can be formally verified by writing theorems about its desired correct behaviour and then proving these theorems correct against a formal mathematical representation of the circuit. Until now this has been a challenging task requiring rare deep expertise both in using interactive theorem provers and in hardware design and verification. AI theorem provers now automate the process of finding a proof for a theorem. This presentation illustrates how an AI theorem prover based on the Lean 4 interface proof assistant can help prove formal properties of digital hardware. This significantly reduces the effort and cost of formally verifying circuit properties that might be beyond the capacity of existing tools, while also providing an effective alternative to other verification techniques due to better scaling properties.

Once we can formally verify a circuit's correctness against formal properties, we can use this capability as guardrails to help AI algorithms synthesize hardware using LLMs, keeping the synthesis process in check by formally verifying each iteration with the AI theorem prover. The end result is a circuit that is correct by construction, without any hallucination.

Bio :

Satnam Singh is a software engineer working at the intersection of programming languages, hardware design and formal methods. Satnam works at Harmonic to apply Lean-based formal verification to computer hardware. Previously he was a computer scientist and hardware engineer working for the AI chip company Groq in California that deploys LLMs (large language models) at scale with very low latency. There he worked on the design of hardware for the power management of machine learning inference chips, the formal verification of machine learning hardware, and the front-end components of a compiler for machine learning models. Satnam has also worked at Google (twice), Facebook and Microsoft. He started his career as an academic at the University of Glasgow.

Link to join virtually:

This talk is being recorded. Any questions asked will also be included in the recording. The recording will be made available on the Department’s webpage