ChiSA: Static Analysis for Lightweight Chisel Verification (Supplementary Material)

ChiSA: Static Analysis for Lightweight Chisel Verification (Supplementary Material) JIACAI CUI,QINLIN CHEN, and ZHONGSHENG ZHAN,Nanjing University, China TIAN TAN∗and YUE LI∗,Nanjing University, China This supplementary material presents additional details omitted from the main paper due to space constraints. It includes the specification of ChAIR (Section 1) and presents complete proofs for key theoretical results whose proof sketches in the main text require further elaboration (Section 2). CCS Concepts: •Theory of computation → Program analysis;•Hardware → Hardware description languages and compilation. Additional Key Words and Phrases: Static Analysis, Hardware, Chisel ACM Reference Format: Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li. 2025. ChiSA: Static Analysis for Lightweight Chisel Verification: (Supplementary Material). Zenodo, v1 (November 2025), 10 pages. https://doi.org/10.5281/ zenodo.17623491 1 Specification of ChAIR ChAIR ( Ch isel-specific I ntermediate R epresentation for A nalysis) is a linear intermediate representation (IR) based on three-address code (3AC), which simplifies the construction of static analyses [ 7 ]. Unlike Firrtl [ 1 ]—the official Chisel compiler IR—and its related CIRCT [ 3 ] dialects, all of which adopt a recursive IR structure based on either abstract syntax trees (ASTs) or MLIR [ 4 ] operations and are primarily designed for transformation and lowering tasks, ChAIR adopts a flat, analyzable structure better suited for static analysis. It also employs static single assignment (SSA) form, aligning with the intrinsic structure of hardware designs (as discussed in Section 2.2 of the main paper) and enabling efficient sparse analysis [9]. We begin by introducing the core classes in ChAIR that abstract key language constructs of Chisel (Section 1.1). To preserve anonymity, we omit organization-specific prefixes when referencing classes and packages (shown in purple) from the ChiSA project. We then present the 3AC grammar for expressions (Section 1.2) and statements (Section 1.3) in ChAIR. Additional details about APIs provided by ChAIR to facilitate static analysis development are available in the documentation accompanying the ChiSA project. ∗Corresponding author. Authors’ Contact Information: Jiacai Cui, [email protected]; Qinlin Chen, [email protected]du.cn; Zhongsheng Zhan, [email protected], State Key Laboratory for Novel Software Technology, Nanjing University, China; Tian Tan, [email protected]; Yue Li, [email protected]du.cn, State Key Laboratory for Novel Software Technology, Nanjing University, China. This work is licensed under a Creative Commons Attribution 4.0 International License. ©2025 Copyright held by the owner/author(s). ACM XXXX-XXXX/2025/11-ART https://doi.org/10.5281/zenodo.17623491 , Vol. Zenodo, No. v1, Article . Publication date: November 2025. 2 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li 1.1 Core Classes •Circuit (in package ir ) serves as the entry point of ChAIR, representing an entire circuit design. A circuit consists of multiple reusable modules, one of which is designated as the top module. The name of the circuit is defined by the name of this top module. •Module (in package ir ) represents a reusable hardware block that can be instantiated multiple times. Each module contains various pieces of information, including its name, member declarations (variables, submodule instances, memories), and native metadata (for inaccessible external definitions). •Type (in package ir.type ) represents the type system in ChAIR. It includes several subclasses for both data and control types: ◦UIntType and SIntType represent fixed-width unsigned and signed integers, respectively. ◦ClockType represents clock signals that synchronize the behavior of registers and memories. ◦AsyncResetType represents signals used to asynchronously reset register values, temporarily overriding clock-driven synchronization. •Var (in package ir.expr ) represents variables within a module that correspond to circuit locations holding values. It has several subclasses, each capturing different value-updating semantics: ◦Ports represent a module’s interface used to communicate with other modules. ◦Wire models a circuit component that reactively propagates values but does not retain state. ◦Reg models a state-holding component that remembers its value across clock cycles. Its updates are synchronized by an associated clock signal. Special registers may include asynchronous reset logic, allowing them to reset independently of clock synchronization. ◦Memory.Cell represents the abstract location in the memory that stores values. The semantics of value updates for a memory cell are determined by the memory to which it belongs. •Memory (in package ir ) provides an abstract representation of a hardware memory in ChAIR. A memory is characterized by the following components: (1) A data type that specifies the type of each memory element, and a positive integer denoting the total number of elements. (2) A variable number of named MemoryAccessor ’s (in package ir ), each associated with an AccessorKind (in package ir.memory ) such as reader , writer , or readwriter . The precise semantics of these accessors are detailed in ChiSA’s documentation. (3) A non-negative integer representing the read latency—i.e., the number of clock cycles between setting a read address and observing the corresponding data value at the read port. (4) A positive integer representing the write latency—i.e., the number of clock cycles between setting a write address and data, and the point at which the written value is committed to the memory. (5) A ReadUnderWrite (in package ir.memory ) flag, which can take values such as old , new , or undefined , specifying the memory’s behavior when a location is read and written concurrently. The precise semantics of each flag are documented in the ChiSA’s documentation. •Native (in package ir ) represents native metadata, such as intellectual property (IP) core parameters. It is used exclusively in external modules whose internal definitions are inaccessible. , Vol. Zenodo, No. v1, Article . Publication date: November 2025. ChiSA : Static Analysis for Lightweight Chisel Verification 3 •Attribute (in package ir.attribute ) conveys additional metadata from the Chisel frontend to ChAIR, such as source locations and annotations that encode designer intentions. It also provides an extensible interface for enriching the semantic information in ChAIR. •Exp (in package ir.expr ) represents expressions, and Stmt (in package ir.stmt ) represents statements. Both include a rich suite of subclasses that comprehensively cover Chisel language features. Due to the large number of variants, we do not enumerate all expressions and statements here. Instead, we provide their grammar in Section 1.2 (for Exp ) and Section 1.3 (for Stmt ). Full semantic and implementation details can be found in the well-documented source code of ChiSA. All the aforementioned classes are thoughtfully designed with rich, well-documented, and userfriendly APIs to streamline the development of Chisel static analyses using ChiSA. These resources are available in the open-source ChiSA repository. 1.2 Grammar of Expressions In the grammar presented below, identifier denotes identifiers, integer denotes integer literals, and string denotes text strings. For readability, all non-terminal symbols are typeset in italics, and all terminal symbols are rendered in red. Exp →Var |Value |Access |MuxExp |UnaryExp |BinaryExp •Var →Identifier •Value →UInt<Integer>(Integer)|SInt<Integer>(Integer) •Access →PortAccess |MemAccess ◦PortAccess →ModuleInstance.Port ∗ModuleInstance →Identifier ∗Port →Identifier ◦MemAccess →Memory.MemoryAccessor.Field ∗Memory →Identifier ∗MemoryAccessor →Identifier ∗Field →clk |en |addr |data |mask |rdata |wmode |wdata |wmask •MuxExp →mux(Var,Var,Var) •UnaryExp →CastExp |NegExp |NotExp |ReductionExp |ResizeExp |BitsExp ◦CastExp →CastOp(Var) ∗CastOp →asUInt |asSInt |asClock |asAsyncReset |cvt ◦NegExp →neg(Var) ◦NotExp →not(Var) ◦ReductionExp →ReductionOp(Var) ∗ReductionOp →andr |orr |xorr ◦ResizeExp →ResizeOp(Var,Integer) ∗ResizeOp →pad |shl |shr |head |tail ◦BitsExp →bits(Var,Integer,Integer) •BinaryExp →ArithmeticExp |ComparisonExp |DynamicShiftExp |BitwiseExp , Vol. Zenodo, No. v1, Article . Publication date: November 2025. 4 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li ◦ArithmeticExp →ArithmeticOp(Var,Var) ∗ArithmeticOp →add |sub |mul |div |rem ◦ComparisonExp →ComparisonOp(Var,Var) ∗ComparisonOp →lt |leq |gt |geq |eq |neq ◦DynamicShiftExp →DynamicShiftOp(Var,Var) ∗DynamicShiftOp →dshl |dshr ◦BitwiseExp →BitwiseOp(Var,Var) ∗BitwiseOp →and |or |xor |cat 1.3 Grammar of Statements Stmt →ConnectStmt |MonitorStmt •ConnectStmt →Const |LoadPort |StorePort |LoadMem |StoreMem |Mux |Unary |Binary ◦Const →Var := Value ◦Copy →Var := Var ◦LoadPort →Var := PortAccess ◦StorePort →PortAccess := Var ◦LoadMem →Var := MemAccess ◦StoreMem →MemAccess := Var ◦Mux →Var := MuxExp ◦Unary →Var := UnaryExp ◦Binary →Var := BinaryExp •MonitorStmt →Printf |Stop |VerificationStmt ◦Printf →printf(Var,Var,String,Var∗ ,) ◦Stop →stop(Var,Var,Integer) ◦VerificationStmt →VerificationPrimitive(Var,Var,Var,String) ∗VerificationPrimitive →assert |assume |cover 2 Detailed Proofs of Properties in Main Paper Due to space constraints and to aid readability, the main paper includes only proof sketches for key results. This section provides the full versions of those proofs, along with additional formal discussions and elaborations where appropriate. 2.1 Proofs of Properties in Section 2 We begin by recalling the first two theorems from Section 2 of the main paper. Since their proof sketches are already sufficiently detailed to constitute complete proofs, we do not repeat them here for brevity. Theorem 2.1 (Original Theorem 2.1 In Our Paper). A circuit could oscillate even if only a finite sequence of external stimuli is applied: ∃𝐶∈Circuit.∃𝑐∈Config𝐶.∃an infinite reduction sequence from 𝑐. , Vol. Zenodo, No. v1, Article . Publication date: November 2025. ChiSA : Static Analysis for Lightweight Chisel Verification 5 Theorem 2.2 (Original Theorem 2.2 In Our Paper). A circuit without a combinational loop cannot oscillate: If 𝐶contains no combinational loop, then infinite reduction sequence from any 𝑐∈Config𝐶. In this subsection, we prove Theorem 2.3 from our main paper, which establishes that the final environment produced by any reduction sequence from the same initial configuration is deterministic. In fact, we prove a stronger proposition concerning stability (Lemma 2.7), from which Theorem 2.3 follows as a corollary. To facilitate this, we introduce a new definition along with several prerequisite lemmas. Definition 2.3. For a configuration ⟨𝑆, 𝐸, 𝐼⟩ of a circuit 𝐶 without combinational loops, if 𝐸(𝑥)= ⟦𝑒⟧𝐸holds for any 𝑥=𝑒∈𝐶=−𝐼, we call the configuration legal. The initial configuration 𝑐0=⟨𝑆, 𝐸rand,𝐶=⟩is legal since 𝐶=−𝐶==∅. Lemma 2.4. If ⟨𝑆, 𝐸, 𝐼⟩ is a legal configuration of a circuit 𝐶 without combinational loops and 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩,⟨𝑆′, 𝐸′, 𝐼′⟩is also legal. Proof. Do case analysis on 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩: (1) Case S-Poke : In this case, 𝐼=∅, 𝐼′=A𝐶(𝐸, 𝐸′) . For any 𝑥=𝑒∈𝐶=−𝐼′ , any 𝑣∈Use(𝑥=𝑒) satisfies 𝐸(𝑣)=𝐸′(𝑣)since 𝑥=𝑒will be in A𝐶(𝐸, 𝐸′)=𝐼′otherwise. Therefore, ⟦𝑒⟧𝐸′=⟦𝑒⟧𝐸=𝐸(𝑥). Since 𝑥 is not poked in this step (because 𝑥 is not an input), 𝐸(𝑥)=𝐸′(𝑥) . It follows that ⟨𝑆′, 𝐸′, 𝐼′⟩is legal. (2) Case S-Tick: Similar. (3) Case C-Eval : Suppose the item 𝜄 used in this step is 𝑥=𝑒 . Since 𝐶 has no combinational loop, 𝑥∉Use(𝑥=𝑒)holds and thus 𝐸′(𝑥)=⟦𝑒⟧𝐸′. If 𝐸(𝑥)=𝐸′(𝑥) , it deduces that 𝐼′=𝐼− {𝑥=𝑒} and 𝐸=𝐸′ . Therefore, any 𝑥′=𝑒′∈𝐶=−𝐼′= (𝐶=−𝐼) ∪ {𝑥=𝑒} is either identical to 𝑥=𝑒 or in 𝐶=−𝐼 . The former case is trivial. For the latter case, ⟦𝑒′⟧𝐸′=⟦𝑒′⟧𝐸=𝐸(𝑥′)=𝐸′(𝑥′). If 𝐸(𝑥)≠𝐸′(𝑥) , 𝐶=−𝐼′=𝐶=− (𝐼− {𝑥=𝑒}) − A𝐶(𝐸, 𝐸′) , where A𝐶(𝐸, 𝐸′)=Succ(𝑥=𝑒) . In this case, any 𝑥′=𝑒′∈𝐶=−𝐼′ which is not identical to 𝑥=𝑒 is in 𝐶=−𝐼 and not in Succ(𝑥=𝑒) , whence 𝑥∉Use(𝑥′=𝑒′). Since 𝐸and 𝐸′only differ in 𝑥,⟦𝑒′⟧𝐸′=⟦𝑒′⟧𝐸=𝐸(𝑥′)=𝐸′(𝑥′). □ Corollary 2.5. Given a legal configuration ⟨𝑆, 𝐸, 𝐼⟩ a circuit 𝐶 without combinational loops, ⟨𝑆′, 𝐸′, 𝐼′⟩is legal if 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩. Proof. Trivial induction. □ Lemma 2.6 (Local Confluence). For a legal configuration ⟨𝑆, 𝐸, 𝐼⟩ of a circuit 𝐶 without combinational loops, if 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆1, 𝐸1, 𝐼1⟩ ∧ 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆2, 𝐸2, 𝐼2⟩ , there exists ⟨𝑆′, 𝐸′, 𝐼′⟩ such that ⟨𝑆1, 𝐸1, 𝐼1⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩∧⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩. Proof. Do a case analysis on 𝐼: (1) If 𝐼=∅ , only S-Poke or S-Tick can be used to make progress. The choice is determined by the first element of 𝑆, so 𝑆1=𝑆2∧𝐸1=𝐸2∧𝐼1=𝐼2. Let ⟨𝑆′, 𝐸′, 𝐼′⟩be ⟨𝑆1, 𝐸1, 𝐼1⟩. (2) If 𝐼≠∅, only C-Eval can be used to make progress. Assume that: 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆, 𝐸[𝑥1↦→ 𝑣1], 𝐼′ 1∪𝐴1⟩=⟨𝑆1, 𝐸1, 𝐼1⟩, 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆, 𝐸[𝑥2↦→ 𝑣2], 𝐼′ 2∪𝐴2⟩=⟨𝑆2, 𝐸2, 𝐼2⟩, where: , Vol. Zenodo, No. v1, Article . Publication date: November 2025. 6 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li •𝑣1=⟦𝑒1⟧𝐸,𝐴1=A𝐶(𝐸, 𝐸[𝑥1↦→ 𝑣1]) ,𝐼′ 1=𝐼− {𝑥1=𝑒1}; •𝑣2=⟦𝑒2⟧𝐸,𝐴2=A𝐶(𝐸, 𝐸[𝑥2↦→ 𝑣2]) ,𝐼′ 2=𝐼− {𝑥2=𝑒2}. The case when 𝑥1=𝑒1 is identical with 𝑥2=𝑒2 is trivial, so we assume that the two items are not identical. Since 𝐶 has no combinational loop, it is impossible that 𝑥1∈Use(𝑥2=𝑒2) ∧ 𝑥2∈ Use(𝑥1=𝑒1). Therefore, we could do a case analysis on their use-relation: (a) If 𝑥1∉Use(𝑥2=𝑒2) ∧ 𝑥2∉Use(𝑥1=𝑒1), let: 𝐸′=𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣2], 𝐼′=(𝐼− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴1∪𝐴2. It follows immediately that ⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩and ⟨𝑆2, 𝐸2, 𝐼2⟩⇝⟨𝑆, 𝐸′, 𝐼′⟩. (b) If 𝑥1∈Use(𝑥2=𝑒2) ∧ 𝑥2∉Use(𝑥1=𝑒1) , let 𝑣′ 2=⟦𝑒2⟧𝐸[𝑥1↦→𝑣1], 𝐴′ 2=A𝐶(𝐸[𝑥1↦→ 𝑣1], 𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣′ 2]) and: 𝐸′=𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣′ 2], 𝐼′=(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′ 2. It immediately deduces that ⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆, 𝐸′, 𝐼′⟩ . As for another configuration ⟨𝑆2, 𝐸2, 𝐼2⟩ , we have ⟨𝑆2, 𝐸2, 𝐼2⟩⇝⟨𝑆2, 𝐸2[𝑥1↦→ 𝑣1],(𝐼2− {𝑥1=𝑒1}) ∪ A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1])⟩ . A further case analysis is needed: (i) Case 𝑣1=𝐸2(𝑥1) : it follows that 𝐸(𝑥1)=𝐸2(𝑥1)=𝑣1 , whence A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1]) = 𝐴1=∅ . Therefore, we have 𝐸=𝐸1 and 𝑣′ 2=𝑣2 , whence 𝐴2=𝐴′ 2 . It deduces that 𝐸2[𝑥1↦→ 𝑣1]=𝐸2=𝐸[𝑥2↦→ 𝑣2]=𝐸[𝑥2↦→ 𝑣′ 2]=𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣′ 2]=𝐸′ and (𝐼2− {𝑥1=𝑒1}) ∪ A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1]) =𝐼2− {𝑥1=𝑒1}=(𝐼− {𝑥1=𝑒1, 𝑥2= 𝑒2}) ∪ 𝐴′ 2=𝐼′. So ⟨𝑆2, 𝐸2, 𝐼2⟩⇝⟨𝑆, 𝐸′, 𝐼′⟩. (ii) Case 𝑣1≠𝐸2(𝑥1) : in this case 𝐴′ 1=A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1]) =Succ(𝑥1=𝑒1) ∩ 𝐶==𝐴1 is not empty. Notice that ⟨𝑆2, 𝐸2, 𝐼2⟩ ⇝⟨𝑆2, 𝐸2[𝑥1↦→ 𝑣1],(𝐼2− {𝑥1=𝑒1}) ∪ 𝐴′ 1⟩ ⇝⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′′ 2⟩, where 𝐴′′ 2=A𝐶(𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣2], 𝐸′). It is worth noting that 𝐴′ 2 is either empty or identical to Succ(𝑥2=𝑒2) ∩ 𝐶= , so is 𝐴′′ 2 . If 𝐴′ 2=𝐴′′ 2, everything is done. However, what if 𝐴′ 2≠𝐴′′ 2 ? In this case, 𝐴′ 2⊊𝐴′′ 2∨𝐴′ 2⊋𝐴′′ 2 holds. For now, we assume that 𝐴′ 2⊊𝐴′′ 2 . Since ⟨𝑆, 𝐸′, 𝐼′⟩ is legal, any 𝑥′=𝑒′ in 𝐴′′ 2−𝐴′ 2 satisfies 𝐸′(𝑥′)=⟦𝑒′⟧𝐸′ . Eliminating such items deduces that ⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2= 𝑒2}) ∪ 𝐴′′ 2⟩⇝∗⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′ 2⟩=⟨𝑆, 𝐸′, 𝐼′⟩. As for the case when 𝐴′ 2⊋𝐴′′ 2 , let ⟨𝑆′′, 𝐸′′, 𝐼′′⟩ be ⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2= 𝑒2}) ∪ 𝐴′′ 2⟩ . Similarly, we can prove that ⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2= 𝑒2}) ∪ 𝐴′ 2⟩⇝∗⟨𝑆′′, 𝐸′′, 𝐼′′⟩, while ⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′′, 𝐸′′, 𝐼′′⟩is proved as above. (c) If 𝑥1∉Use(𝑥2=𝑒2) ∧ 𝑥2∈Use(𝑥1=𝑒1), mimic the above proof. □ Lemma 2.7 (Confluence). For a legal configuration ⟨𝑆, 𝐸, 𝐼⟩ of a circuit 𝐶 without combinational loops, if 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆1, 𝐸1, 𝐼1⟩ ∧ 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆2, 𝐸2, 𝐼2⟩ , there exists ⟨𝑆′, 𝐸′, 𝐼′⟩ such that ⟨𝑆1, 𝐸1, 𝐼1⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩∧⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩. Proof. Theorem 2.2 indicates 𝜆𝐹 satisfies strong normalization, and Lemma 2.6 provides local confluence for legal configurations. The conclusion is deduced from Newman’s lemma [6]. □ , Vol. Zenodo, No. v1, Article . Publication date: November 2025. ChiSA : Static Analysis for Lightweight Chisel Verification 7 We can thus prove original Theorem 2.3 in our paper as follows: Theorem 2.8 (Original Theorem 2.3 In Our Paper). The steady-state reached by a circuit without combinational loops is uniquely determined: 𝐶has no combinational loop∧𝐶⊢ ⟨𝑆, 𝐸,𝐶=⟩⇝∗⟨𝜖, 𝐸1,∅⟩∧𝐶⊢ ⟨𝑆, 𝐸,𝐶=⟩⇝∗⟨𝜖, 𝐸2,∅⟩ ⇒ 𝐸1=𝐸2. Proof. Since ⟨𝑆, 𝐸,𝐶=⟩ is legal, it follows from Lemma 2.7 that there is a configuration ⟨𝑆′, 𝐸′, 𝐼′⟩ such that 𝐶⊢ ⟨𝜖, 𝐸1,∅⟩ ⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩ ∧ 𝐶⊢ ⟨𝜖, 𝐸2,∅⟩ ⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩ . However, ⟨𝜖, 𝐸1,∅⟩ and ⟨𝜖, 𝐸2,∅⟩ are irreducible, whence 𝐸1=𝐸′=𝐸2.□ 2.2 Proofs of Properties in Section 3 In this subsection, we provide complete proofs for Theorems 3.4 and 3.6 from the main paper. The proof sketches for the other theorems and lemmas in this section are already sufficiently detailed to serve as complete proofs and are therefore not repeated here. Definition 2.9. For a non-empty Store′⊆Store where ⟨Store′,⊑⟩ is a complete lattice, we call Store′a limited set of stores. As follows, we use Store′to denote any limited set of stores. For convenience, we introduce a generalization of synchronous flow functions: Definition 2.10 (Fusion). We define Aff(𝑓) as {𝑣∈Var | ∃𝜎∈Store′.𝜎(𝑣)≠𝑓(𝜎)(𝑣)} for any function 𝑓 : Store′→Store′ . For any two monotone functions 𝑓 ,𝑔 : Store′→Store′ where Aff(𝑓) ∩ Aff(𝑔)=∅, we write: (𝑓∗𝑔)(𝑥)(𝑣)=        𝑓(𝑥)(𝑣),if 𝑣∈Aff(𝑓), 𝑔(𝑥)(𝑣),if 𝑣∈Aff(𝑔), 𝑣, otherwise. We refer to 𝑓∗𝑔 as the fusion of 𝑓 and 𝑔 . The function 𝑓∗𝑔 is also monotone and satisfies Aff(𝑓∗𝑔) ⊆ Aff(𝑓) ∪ Aff(𝑔). For a finite sequence of monotone functions 𝑓1, . . . , 𝑓𝑠 : Store′→Store′ where ∀𝑖, 𝑗.𝑖 ≠𝑗=⇒ Aff(𝑓𝑖) ∩ Aff(𝑓𝑗)=∅ , we call the sequence a disjoint sequence of flow functions and write 𝑓∗ : = 𝑓1∗ · · · ∗ 𝑓𝑠for 𝑓1∗ (𝑓2∗ · · · (𝑓𝑠−1∗𝑓𝑠)). Lemma 2.11. For any disjoint sequence of flow functions 𝑓1, . . . , 𝑓𝑠 : Store′→Store′ , 𝜎∈Store′ is a common fixed point of 𝑓1, . . . , 𝑓𝑠iff it is a fixed point of 𝑓∗=𝑓1∗ · · · ∗ 𝑓𝑠. Proof. Assume 𝜎 is a common fixed point of 𝑓1, . . . , 𝑓𝑠 . For any 𝑥∈Var , there exists at most one index 𝑗 such that 𝑥∈Aff(𝑓𝑗) . If there is no such index, 𝑓∗(𝜎)(𝑥)=𝜎(𝑥) . Otherwise, 𝑓∗(𝜎)(𝑥)= 𝑓𝑗(𝜎)(𝑥)=𝜎(𝑥). Therefore, 𝑓∗(𝜎)(𝑥)=𝜎(𝑥)holds for any 𝑥∈Var, namely that 𝑓∗(𝜎)=𝜎. Conversely, suppose 𝜎 is a fixed point of 𝑓∗ . Notice that 𝑓𝑗(𝜎)(𝑥) is either 𝜎(𝑥) or 𝑓∗(𝜎)(𝑥)=𝜎(𝑥) for any index 𝑗and 𝑥∈Var, whence 𝑓𝑗(𝜎)=𝜎holds for any 𝑗.□ Lemma 2.12. If Store′ is a complete lattice with finite height, for any disjoint sequence of flow functions 𝑓1, . . . , 𝑓𝑠:Store′→Store′, the functions: 𝑓∗=𝑓1∗ · · · ∗ 𝑓𝑠, 𝑓◦=𝑓1◦ · · · ◦ 𝑓𝑠, have the same least fixed point. , Vol. Zenodo, No. v1, Article . Publication date: November 2025. 8 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li Proof. Suppose the least fixed points of 𝑓∗and 𝑓◦are 𝜎∗and 𝜎◦respectively. On the one hand, for any 𝜎∈Store′ , if 𝑓∗(𝜎) ⊑ 𝜎 , we have 𝑓𝑖(𝜎) ⊑ 𝜎 for any index 𝑖 . This implies that 𝑓1(𝑓2(· · · (𝑓𝑛−1(𝑓𝑛(𝜎))))) ⊑ 𝑓1(𝑓2(· · · (𝑓𝑛−1(𝜎)))) ⊑ . . . ⊑𝑓1(𝜎) ⊑ 𝜎, whence: {𝜎∈Store′| (𝑓∗)(𝜎) ⊑ 𝜎} ⊆ {𝜎∈Store′| (𝑓◦)(𝜎) ⊑ 𝜎}. By Tarski’s fixed-point theorem [8], 𝜎∗⊒𝜎◦. On the other hand, Kleene’s fixed-point theorem [ 2 , 5 ] indicates that, for any monotone function ℎ : 𝐿→𝐿 , there exists 𝑛∈N such that ℎ𝑛+1(⊥) =ℎ𝑛(⊥) is the least fixed point of ℎ . Suppose (𝑓∗)𝑚(⊥) and (𝑓◦)𝑛(⊥) are least fixed points of 𝑓∗and 𝑓◦respectively. Let: 𝑝𝑛=(𝑓◦)𝑛(⊥), 𝑞𝑛=(𝑓∗)𝑛(⊥). As the proof of Kleene’s fixed-point theorem [ 5 ] demonstrates, 𝑝𝑖⊑𝑝𝑖+1 holds for any index 𝑖 . Similarly, 𝑞𝑖⊑𝑞𝑖+1also holds for any index 𝑖. We shall prove that 𝑝𝑖⊒𝑞𝑖for any index 𝑖∈Nby induction: (1) Base Case: From 𝑝0=𝑞0=⊥, it follows that 𝑝0⊒𝑞0. (2) Induction Step: Assume 𝑝𝑖⊒𝑞𝑖. We shall prove 𝑝𝑖+1⊒𝑞𝑖+1. Since 𝑞𝑖⊑𝑞𝑖+1 , every 𝑥∈Var satisfies that 𝑞𝑖(𝑥) ⊑ 𝑞𝑖+1(𝑥)=(𝑓∗)(𝑞𝑖)(𝑥) . From the definition of 𝑓∗, it follows immediately that 𝑞𝑖⊑𝑓𝑗(𝑞𝑖)for any index 𝑗=1, . . . ,𝑠. Notice that: 𝑝𝑖+1=𝑓◦(𝑝𝑖)⊒𝑓◦(𝑞𝑖). For any 𝑥∈Var , there is at most one index 𝑗 such that 𝑥∈Aff(𝑓𝑗) . If such index does not exist, 𝑓◦(𝑞𝑖)(𝑥)=𝑞𝑖(𝑥)=𝑓∗(𝑞𝑖)(𝑥) . Otherwise, suppose such 𝑗 exists. From the assumption, it follows that: 𝑓◦(𝑞𝑖)(𝑥)=(𝑓1◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥)=(𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥). By ∀𝑗.𝑓𝑗(𝑞𝑖) ⊒ 𝑞𝑖, we have: (𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)⊒(𝑓𝑗◦ · · · ◦ 𝑓𝑠−1)(𝑞𝑖) ⊒ . . . ⊒𝑓𝑗(𝑞𝑖), whence (𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥)⊒𝑓𝑗(𝑞𝑖)(𝑥)=𝑓∗(𝑞𝑖)(𝑥). Therefore, 𝑓◦(𝑞𝑖)(𝑥) ⊒ 𝑓∗(𝑞𝑖)(𝑥) holds for any 𝑥∈Var , namely that 𝑝𝑖+1⊒𝑓◦(𝑞𝑖) ⊒ 𝑓∗(𝑞𝑖)=𝑞𝑖+1. Let 𝑢=max(𝑚,𝑛) , it follows that 𝜎◦=(𝑓◦)𝑛(⊥) =(𝑓◦)𝑢(⊥) ⊒ (𝑓∗)𝑢(⊥) =(𝑓∗)𝑚(⊥) =𝜎∗ . Therefore, the least fixed points of 𝑓◦and 𝑓∗are equivalent. □ We will prove Theorem 3.4 in our paper as follows: Theorem 2.13 (Original Theorem 3.4 In Our Paper). Algorithm 1 converges to the least synchronized fixed point LSFP𝐶,𝛿 𝑓if 𝑓is monotonic and ⟨𝐿, ⊑⟩ is a complete lattice with finite height. Proof. Since Var is finite, it follows that Store is also a complete lattice with finite height. Let Store𝛿 denote {𝜎∈Store|∀𝑣∈Input𝐶.𝜎 (𝑣)=𝛿(𝑣)} , which is a limited set of stores with finite height. Sort 𝐶= into 𝜄1, . . . , 𝜄𝑠 by a reverse topological order of 𝐺𝐶[𝐶=] . By Kleene’s fixed-point theorem [ 2 , 5], Algorithm 1 computes the least fixed point of the function: 𝑓⟦𝐶⇐⟧ ◦ 𝑓⟦𝜄1⟧ ◦ · · · ◦ 𝑓⟦𝜄𝑠⟧. , Vol. Zenodo, No. v1, Article . Publication date: November 2025. ChiSA : Static Analysis for Lightweight Chisel Verification 9 While any element in LSFP𝐶,𝛿 𝑓 is a common least fixed point of 𝑓⟦𝐶⇐⟧, 𝑓 ⟦𝜄1⟧, . . . , 𝑓 ⟦𝜄𝑠⟧ , which is indeed the least fixed point of 𝑓⟦𝐶⇐⟧∗ 𝑓⟦𝜄1⟧∗· · ·∗⟦𝜄𝑠⟧ by Lemma 2.11. By Lemma 2.12, Algorithm 1 computes this least fixed point. □ We can thus prove Theorem 3.6 in our paper as follows: Theorem 2.14 (Original Theorem 3.6 In Our Paper). If ⟨𝐿, ⊑⟩ is a complete lattice, 𝑓1⊑𝑓2 , 𝜎1∈LSFP𝐶,𝛿 𝑓1, and 𝜎2∈LSFP𝐶,𝛿 𝑓2, then 𝜎1⊑𝜎2. Proof. Since 𝐿 is complete, Store is also a complete lattice. Let Store𝛿 denote {𝜎∈Store|∀𝑣∈ Input𝐶.𝜎(𝑣)=𝛿(𝑣)}, which is a limited set of stores. By the assumption, 𝑓∗ 1⊑𝑓∗ 2 . From Lemma 2.11, it follows that 𝜎1 is the least fixed point of 𝑓∗ 1 and 𝜎2is that of 𝑓∗ 2. By definition, 𝑓∗ 1 is equal to 𝑓1⟦𝐶⟧ . Similarly, 𝑓∗ 2=𝑓2⟦𝐶⟧ . From 𝑓1⊑𝑓2 , it follows that 𝑓1⟦𝐶⟧ ⊑ 𝑓2⟦𝐶⟧. Consider any 𝜎∈Store𝛿which satisfies 𝑓∗ 2(𝜎) ⊑ 𝜎, we have: 𝑓∗ 1(𝜎)⊑𝑓1⟦𝐶⟧(𝜎)⊑𝑓2⟦𝐶⟧(𝜎)=𝑓∗ 2(𝜎) ⊑ 𝜎. Therefore, {𝜎∈Store𝛿|𝑓∗ 1(𝜎) ⊑ 𝜎} ⊇ {𝜎∈Store𝛿|𝑓∗ 2(𝜎) ⊑ 𝜎}holds. By Tarski’s fixed-point theorem [8], 𝜎1=⊓{𝜎∈Store𝛿|𝑓∗ 1(𝜎) ⊑ 𝜎} ⊑ ⊓{𝜎∈Store𝛿|𝑓∗ 2(𝜎) ⊑ 𝜎}=𝜎2. □ 3 Discussion: Chaotic Values In our main paper (Definition 2.1), we chose Value =Z (i.e., the set of mathematical integers) purely for ease of understanding and presentation. A more rigorous and complete treatment of values is as follows: Value :=Z∪Z′where Z′:={𝑖′|𝑖∈Z} Here, each 𝑖′ represents a random value drawn from 𝐸rand : Var →Z′ in the initial configuration 𝑐0=⟨𝑆0, 𝐸rand,𝐶=⟩ , modeling the non-deterministic behavior of real-world digital circuits at powerup. We refer to such values as chaotic values to reflect their physical meaning. The definition of evaluation (original Definition 2.9 in our paper) requires only a slight refinement, as defined case by case below, which preserves the overall structure and spirit of the original semantics: ⟦𝑛⟧𝐸:=𝑛⟦𝑦⟧𝐸:=𝐸(𝑦) ⟦𝑦op 𝑧⟧𝐸:=(ℭ(ℨ(𝐸(𝑦)) op ℨ(𝐸(𝑧))) if 𝐸(𝑦) ∈ Z′∨𝐸(𝑧) ∈ Z′, 𝐸(𝑦)op 𝐸(𝑧)otherwise . ⟦mux(𝑤, 𝑦, 𝑧)⟧𝐸:=(ℭ(𝐸(𝑦)) if 𝐸(𝑤)≠0′∧𝐸(𝑤) ∈ Z′,ℭ(𝐸(𝑧)) if 𝐸(𝑤)=0′, 𝐸(𝑦)if 𝐸(𝑤)≠0∧𝐸(𝑤)∉Z′, 𝐸(𝑧)if 𝐸(𝑤)=0. where: ℨ(𝑥):=(𝑥, if 𝑥∈Z, 𝑖, if 𝑥=𝑖′∈Z′.ℭ(𝑥):=(𝑥′,if 𝑥∈Z, 𝑥, if 𝑥∈Z′. , Vol. Zenodo, No. v1, Article . Publication date: November 2025.