Zhongsheng Zhan

dblp:425/5321 · DBLP profile ↗
← Back
1ranked-venue papers
0as first author
1since 2021 · last 2026
0009-0004-7151-9608ORCID · reported

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 1 · 1 since 2021

Expertise — from the expertise taxonomy: the topics of the expert's papers under the CCF categories. A weight counts papers with recency: 1 for a paper about the topic, 0.3 when the topic is its context, halved every five years.

Computer architecture, parallel and distributed computing, and storage systems
1 paper
Electronic design automation · 87% Distributed systems · 13%
Software engineering, system software, and programming languages
1 paper
Programming languages and type systems · 100%

Topics — the 5 heaviest of 5, each with the papers that count most for it

TopicWeightPapersLastEvidence papers
Programming languages and type systems › language semantics
core calculus
1.012026
ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026
Programming languages and type systems
language design
1.012026
ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026
Electronic design automation
hardware verification and test
1.012026
ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026
Electronic design automation › hardware verification and test
static analysis
1.012026
ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026
Distributed systems
bug detection
0.312026
ChiSA: Static Analysis for Lightweight Chisel Verification · Proc. ACM Program. Lang. 2026

Methods — techniques the papers use, named apart from their topics

fixed-point analysis · 2.0logical relations · 1.0logical relation · 1.0
YearPublicationVenuePosition
2026 ChiSA: Static Analysis for Lightweight Chisel Verification
abstract
The growing demand for productivity in hardware development opens up new opportunities for applying programming language (PL) techniques to hardware description languages (HDLs). Chisel, a leading agile HDL, embraces this shift by leveraging modern PL features to enhance hardware design productivity. However, verification for Chisel remains a major productivity bottleneck, requiring substantial time and manual effort. To address this issue, we advocate the use of static analysis —a technique proven well-suited to agile development workflows in software—for lightweight Chisel verification. This work establishes a theoretical foundation for Chisel static analysis. At its core is λ C , a formal core calculus of ChAIR (a Chisel-specific intermediate representation for analysis). λ C is the first formalism that captures the essence of Chisel while being deliberately minimal to ease rigorous reasoning about static analysis built on λ C . We prove key properties of λ C that reflect real hardware characteristics, which in turn offer a form of retrospective validation for its design. On the basis of λ C , we define and formalize the hardware value flow analysis (HVFA) problem, which underpins our static analyses for critical Chisel verification tasks, including bug detection and security analysis. We then propose a synchronized fixed-point solution to the HVFA problem, featuring hardware-specific treatment of the synchronous behavior of clock-driven hardware registers—the essential feature of Chisel programs. We further prove key theorems establishing the guarantees and limitations of our solution. As a proof of concept, we develop ChiSA (30K+ LoC)—the first Chisel static analyzer that can analyze intricate hardware value flows to enable lightweight analyses for critical Chisel verification tasks such as bug detection and security analysis. To facilitate thorough evaluation of both ChiSA and future work, we provide ChiSABench (11M+ LoC), a comprehensive benchmark for Chisel static analysis. Our evaluation on ChiSABench demonstrates that ChiSA offers an effective and significantly more lightweight approach for critical Chisel verification tasks, especially on large and complex real-world designs. For example, ChiSA identified 69 violable developer-inserted assertions in large-scale Chisel designs (9.7M+ LoC) in under 200 seconds—eight of which were recognized by developers and scheduled for future fixes—and detected all 60 information-leak vulnerabilities in the well-known TrustHub benchmark (1.1M+ LoC) in just one second—outperforming state-of-the-art Chisel approaches like ChiselTest’s bounded model checking and ChiselFlow’s secure type system. These results underscore the high promise of static analysis for lightweight Chisel verification. To encourage continued research and innovation, we will fully open-source ChiSA (30K+ LoC) and ChiSABench (11M+ LoC).
Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan 0001, Yue Li 0006
Proc. ACM Program. Lang.3