ChiSA: Static Analysis for Lightweight Chisel Verification

Jiacai Cui

doi:10.1145/3776660

ChiSA: Static Analysis for Lightweight Chisel Verification

2026-01-01

0

PRE

AI

DOI：10.1145/3776660

摘要

En 中文

对硬件开发中日益增长的生产力需求为将编程语言（PL）技术应用于硬件描述语言（HDLs）带来了新的机遇。作为领先的敏捷型HDL，Chisel通过利用现代PL特性来提升硬件设计生产力。然而，Chisel的验证仍然是主要的生产力瓶颈，需要大量时间和人工努力。为解决此问题，我们主张采用静态分析技术——一种被证明非常适合软件敏捷开发工作流的手段——用于轻量级Chisel验证。本工作为Chisel静态分析奠定了理论基础。其核心是A，一种形式化的ChAIR（Chisel分析专用中间表示）核心演算。A是首个既捕捉了Chisel本质又刻意保持最小化以简化基于A的严格静态分析推理的形式化方法。我们证明了A的关键属性，这些属性反映了真实硬件特性，从而为其设计提供了某种形式的回顾性验证。基于A，我们定义并形式化了硬件值流分析（HVFA）问题，该问题支撑着我们针对关键Chisel验证任务（包括错误检测和安全分析）的静态分析。随后，我们提出了一种同步固定点解法来求解HVFA问题，该解法专门处理时钟驱动硬件寄存器的同步行为——这是Chisel程序的关键特性。我们进一步证明了关键定理，以确立我们解法的保证和局限性。为验证概念，我们开发了ChiSA（3万+行代码）——首个能够分析复杂硬件值流以支持轻量级关键Chisel验证任务的静态分析器，例如错误检测和安全分析。为促进对ChiSA及未来工作的全面评估，我们提供了ChiSABench（1100万+行代码），一个全面的Chisel静态分析基准。在ChiSABench上的评估表明，ChiSA为关键Chisel验证任务提供了一种有效且显著更轻量的方法，特别是在大型和复杂真实设计上。例如，ChiSA在200秒内识别出大规模Chisel设计（970万+行代码）中69个可违反的开发者插入断言（其中8个已被开发者识别并计划未来修复），并在1秒内检测出知名TrustHub基准（110万+行代码）中的所有60个信息泄露漏洞——优于当前最先进的Chisel方法，如ChiselTest的有限模型检查和ChiselFlow的安全类型系统。这些结果突显了静态分析在轻量级Chisel验证中的巨大潜力。为鼓励持续研究和创新，我们将完全开源ChiSA（3万+行代码）和ChiSABench（1100万+行代码）。

Keyword:

Static Analysis

Hardware

Chisel

ChiSA: Static Analysis for Lightweight Chisel Verification

摘要

期刊

机构

引用论文