"Architecting for Jagged Intelligence"

Prof. Johnny Qiang XU (The Chinese University of Hong Kong (CUHK))

Abstract

The semiconductor industry has mastered deterministic reliability, yet modern AI introduces a sharply contrasting paradigm: ""Jagged Intelligence."" Powered by Large Language Models, autonomous AI agents exhibit advanced but fundamentally probabilistic capabilities—excelling at complex reasoning while frequently failing at basic logic. This unpredictability creates a severe reliability bottleneck for mission-critical applications.
To move beyond fragile prompt engineering, we must adopt a ""Governance-First"" paradigm. The presentation introduces a neuro-symbolic kernel designed to enforce strict reliability policies. By decoupling the probabilistic reasoning engine from a deterministic, logic-based governor, this architecture establishes a verifiable firewall that transforms unpredictable AI outputs into reliable, structured actions, laying the foundation for trustworthy agentic computing.

“Efficient Hardware for AI and AI for Hardware”

Prof. Grace ZHANG (TU Darmstadt)

Abstract

The last decade has witnessed significant breakthroughs of deep neural networks (DNNs) in many fields. These breakthroughs have been achieved at extremely high computation and memory cost. Accordingly, the increasing complexity of DNNs has led to a quest for efficient hardware platforms. In this talk, several techniques such as power-aware weight selection, logic design of neural networks, and conversion of neural networks into control logic flow will be presented. Furthermore, LLMs assisted electronic design automation will also be discussed.  In the end, on-going research topics and future research plan will be summarized. 

"A Tale of Two Worlds: Formal Verification Meets AI Acceleration"

Prof. Hongce ZHANG (HKUST-GZ)

Abstract

AI accelerators are rapidly becoming a dominant workload in modern computing systems, yet their verification poses unique challenges. Unlike control-centric designs, these accelerators often come with customized datapaths, sometimes generated through high-level synthesis. They exhibit complex arithmetic behaviors that often strain traditional bit-level formal methods. Facing the challenge, this talk will present a word-level perspective on hardware formal verification, tailored to the verification of accelerators. We introduce a suite of techniques, including word-level symbolic simulation, word-level SMT sweeping and modular C-to-RTL equivalence checking, enabling more scalable and effective reasoning about datapath-intensive systems.

Conversely, advances in AI are also reshaping the landscape of formal verification. This talk will briefly highlight our recent progress in AI-accelerated equivalence checking and model checking, as well as the emerging role of large language models in assisting verification setup, such as assertion generation and model abstraction. Together, these developments point toward a promising synergy between formal methods and AI.