ChiSA: S a ic Analysis o Ligh weigh Chisel Ve i ica ion
(Supplemen a y Ma e ial)
JIACAI CUI,QINLIN CHEN, and ZHONGSHENG ZHAN,Nanjing Uni e si y, China
TIAN TAN∗and YUE LI∗,Nanjing Uni e si y, China
This supplemen a y ma e ial p esen s addi ional de ails omi ed om he main pape due o space cons ain s.
I includes he speci ica ion o ChAIR (Sec ion 1) and p esen s comple e p oo s o key heo e ical esul s
whose p oo ske ches in he main ex equi e u he elabo a ion (Sec ion 2).
CCS Concep s: •Theo y o compu a ion
→
P og am analysis;•Ha dwa e
→
Ha dwa e desc ip ion
languages and compila ion.
Addi ional Key Wo ds and Ph ases: S a ic Analysis, Ha dwa e, Chisel
ACM Re e ence Fo ma :
Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li. 2025. ChiSA: S a ic Analysis o Ligh weigh
Chisel Ve i ica ion: (Supplemen a y Ma e ial). Zenodo, 1 (No embe 2025), 10 pages. h ps://doi.o g/10.5281/
zenodo.17623491
1 Speci ica ion o ChAIR
ChAIR (
Ch
isel-speci ic
I
n e media e
R
ep esen a ion o
A
nalysis) is a linea in e media e ep-
esen a ion (IR) based on h ee-add ess code (3AC), which simpli ies he cons uc ion o s a ic
analyses [
7
]. Unlike Fi l [
1
]— he o icial Chisel compile IR—and i s ela ed CIRCT [
3
] dialec s, all
o which adop a ecu si e IR s uc u e based on ei he abs ac syn ax ees (ASTs) o MLIR [
4
]
ope a ions and a e p ima ily designed o ans o ma ion and lowe ing asks, ChAIR adop s a la ,
analyzable s uc u e be e sui ed o s a ic analysis. I also employs s a ic single assignmen (SSA)
o m, aligning wi h he in insic s uc u e o ha dwa e designs (as discussed in Sec ion 2.2 o he
main pape ) and enabling e icien spa se analysis [9].
We begin by in oducing he co e classes in ChAIR ha abs ac key language cons uc s o Chisel
(Sec ion 1.1). To p ese e anonymi y, we omi o ganiza ion-speci ic p e ixes when e e encing
classes and packages (shown in pu ple) om he ChiSA p ojec . We hen p esen he 3AC g amma
o exp essions (Sec ion 1.2) and s a emen s (Sec ion 1.3) in ChAIR. Addi ional de ails abou APIs
p o ided by ChAIR o acili a e s a ic analysis de elopmen a e a ailable in he documen a ion
accompanying he ChiSA p ojec .
∗Co esponding au ho .
Au ho s’ Con ac In o ma ion: Jiacai Cui, [email p o ec ed]; Qinlin Chen, [email p o ec ed]du.cn; Zhong-
sheng Zhan, [email p o ec ed], S a e Key Labo a o y o No el So wa e Technology, Nanjing Uni e si y,
China; Tian Tan, [email p o ec ed]; Yue Li, [email p o ec ed]du.cn, S a e Key Labo a o y o No el So wa e Technology,
Nanjing Uni e si y, China.
This wo k is licensed unde a C ea i e Commons A ibu ion 4.0 In e na ional License.
©2025 Copy igh held by he owne /au ho (s).
ACM XXXX-XXXX/2025/11-ART
h ps://doi.o g/10.5281/zenodo.17623491
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
2 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li
1.1 Co e Classes
•Ci cui
(in package
i
) se es as he en y poin o ChAIR, ep esen ing an en i e ci cui design.
A ci cui consis s o mul iple eusable modules, one o which is designa ed as he op module.
The name o he ci cui is de ined by he name o his op module.
•Module
(in package
i
) ep esen s a eusable ha dwa e block ha can be ins an ia ed mul iple
imes. Each module con ains a ious pieces o in o ma ion, including i s name, membe decla a-
ions ( a iables, submodule ins ances, memo ies), and na i e me ada a ( o inaccessible ex e nal
de ini ions).
•Type
(in package
i . ype
) ep esen s he ype sys em in ChAIR. I includes se e al subclasses
o bo h da a and con ol ypes:
◦UIn Type and SIn Type ep esen ixed-wid h unsigned and signed in ege s, espec i ely.
◦ClockType ep esen s clock signals ha synch onize he beha io o egis e s and memo ies.
◦AsyncRese Type
ep esen s signals used o asynch onously ese egis e alues, empo a ily
o e iding clock-d i en synch oniza ion.
•Va
(in package
i .exp
) ep esen s a iables wi hin a module ha co espond o ci cui loca ions
holding alues. I has se e al subclasses, each cap u ing di e en alue-upda ing seman ics:
◦Po s ep esen a module’s in e ace used o communica e wi h o he modules.
◦Wi e models a ci cui componen ha eac i ely p opaga es alues bu does no e ain s a e.
◦Reg
models a s a e-holding componen ha emembe s i s alue ac oss clock cycles. I s upda es
a e synch onized by an associa ed clock signal. Special egis e s may include asynch onous
ese logic, allowing hem o ese independen ly o clock synch oniza ion.
◦Memo y.Cell
ep esen s he abs ac loca ion in he memo y ha s o es alues. The seman ics
o alue upda es o a memo y cell a e de e mined by he memo y o which i belongs.
•Memo y
(in package
i
) p o ides an abs ac ep esen a ion o a ha dwa e memo y in ChAIR. A
memo y is cha ac e ized by he ollowing componen s:
(1)
A da a ype ha speci ies he ype o each memo y elemen , and a posi i e in ege deno ing
he o al numbe o elemen s.
(2)
A a iable numbe o named
Memo yAccesso
’s (in package
i
), each associa ed wi h an
Accesso Kind
(in package
i .memo y
) such as
eade
,
w i e
, o
eadw i e
. The p ecise
seman ics o hese accesso s a e de ailed in ChiSA’s documen a ion.
(3)
A non-nega i e in ege ep esen ing he ead la ency—i.e., he numbe o clock cycles be ween
se ing a ead add ess and obse ing he co esponding da a alue a he ead po .
(4)
A posi i e in ege ep esen ing he w i e la ency—i.e., he numbe o clock cycles be ween
se ing a w i e add ess and da a, and he poin a which he w i en alue is commi ed o he
memo y.
(5)
A
ReadUnde W i e
(in package
i .memo y
) lag, which can ake alues such as
old
,
new
, o
unde ined
, speci ying he memo y’s beha io when a loca ion is ead and w i en concu en ly.
The p ecise seman ics o each lag a e documen ed in he ChiSA’s documen a ion.
•Na i e
(in package
i
) ep esen s na i e me ada a, such as in ellec ual p ope y (IP) co e pa am-
e e s. I is used exclusi ely in ex e nal modules whose in e nal de ini ions a e inaccessible.
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
ChiSA : S a ic Analysis o Ligh weigh Chisel Ve i ica ion 3
•A ibu e
(in package
i .a ibu e
) con eys addi ional me ada a om he Chisel on end o
ChAIR, such as sou ce loca ions and anno a ions ha encode designe in en ions. I also p o ides
an ex ensible in e ace o en iching he seman ic in o ma ion in ChAIR.
•Exp
(in package
i .exp
) ep esen s exp essions, and
S m
(in package
i .s m
) ep esen s
s a emen s. Bo h include a ich sui e o subclasses ha comp ehensi ely co e Chisel language
ea u es. Due o he la ge numbe o a ian s, we do no enume a e all exp essions and s a emen s
he e. Ins ead, we p o ide hei g amma in Sec ion 1.2 ( o
Exp
) and Sec ion 1.3 ( o
S m
). Full
seman ic and implemen a ion de ails can be ound in he well-documen ed sou ce code o ChiSA.
All he a o emen ioned classes a e hough ully designed wi h ich, well-documen ed, and use -
iendly APIs o s eamline he de elopmen o Chisel s a ic analyses using ChiSA. These esou ces
a e a ailable in he open-sou ce ChiSA eposi o y.
1.2 G amma o Exp essions
In he g amma p esen ed below,
iden i ie
deno es iden i ie s,
in ege
deno es in ege li e als, and
s ing
deno es ex s ings. Fo eadabili y, all non- e minal symbols a e ypese in i alics, and all
e minal symbols a e ende ed in ed.
Exp →Va |Value |Access |MuxExp |Una yExp |Bina yExp
•Va →Iden i ie
•Value →UIn <In ege >(In ege )|SIn <In ege >(In ege )
•Access →Po Access |MemAccess
◦Po Access →ModuleIns ance.Po
∗ModuleIns ance →Iden i ie
∗Po →Iden i ie
◦MemAccess →Memo y.Memo yAccesso .Field
∗Memo y →Iden i ie
∗Memo yAccesso →Iden i ie
∗Field →clk |en |add |da a |mask | da a |wmode |wda a |wmask
•MuxExp →mux(Va ,Va ,Va )
•Una yExp →Cas Exp |NegExp |No Exp |Reduc ionExp |ResizeExp |Bi sExp
◦Cas Exp →Cas Op(Va )
∗Cas Op →asUIn |asSIn |asClock |asAsyncRese |c
◦NegExp →neg(Va )
◦No Exp →no (Va )
◦Reduc ionExp →Reduc ionOp(Va )
∗Reduc ionOp →and |o |xo
◦ResizeExp →ResizeOp(Va ,In ege )
∗ResizeOp →pad |shl |sh |head | ail
◦Bi sExp →bi s(Va ,In ege ,In ege )
•Bina yExp →A i hme icExp |Compa isonExp |DynamicShi Exp |Bi wiseExp
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
4 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li
◦A i hme icExp →A i hme icOp(Va ,Va )
∗A i hme icOp →add |sub |mul |di | em
◦Compa isonExp →Compa isonOp(Va ,Va )
∗Compa isonOp →l |leq |g |geq |eq |neq
◦DynamicShi Exp →DynamicShi Op(Va ,Va )
∗DynamicShi Op →dshl |dsh
◦Bi wiseExp →Bi wiseOp(Va ,Va )
∗Bi wiseOp →and |o |xo |ca
1.3 G amma o S a emen s
S m →Connec S m |Moni o S m
•Connec S m →Cons |LoadPo |S o ePo |LoadMem |S o eMem |Mux |Una y |Bina y
◦Cons →Va := Value
◦Copy →Va := Va
◦LoadPo →Va := Po Access
◦S o ePo →Po Access := Va
◦LoadMem →Va := MemAccess
◦S o eMem →MemAccess := Va
◦Mux →Va := MuxExp
◦Una y →Va := Una yExp
◦Bina y →Va := Bina yExp
•Moni o S m →P in |S op |Ve i ica ionS m
◦P in →p in (Va ,Va ,S ing,Va ∗
,)
◦S op →s op(Va ,Va ,In ege )
◦Ve i ica ionS m →Ve i ica ionP imi i e(Va ,Va ,Va ,S ing)
∗Ve i ica ionP imi i e →asse |assume |co e
2 De ailed P oo s o P ope ies in Main Pape
Due o space cons ain s and o aid eadabili y, he main pape includes only p oo ske ches o
key esul s. This sec ion p o ides he ull e sions o hose p oo s, along wi h addi ional o mal
discussions and elabo a ions whe e app op ia e.
2.1 P oo s o P ope ies in Sec ion 2
We begin by ecalling he i s wo heo ems om Sec ion 2 o he main pape . Since hei p oo
ske ches a e al eady su icien ly de ailed o cons i u e comple e p oo s, we do no epea hem he e
o b e i y.
Theo em 2.1 (O iginal Theo em 2.1 In Ou Pape ). A ci cui could oscilla e e en i only a ini e
sequence o ex e nal s imuli is applied:
∃𝐶∈Ci cui .∃𝑐∈Con ig𝐶.∃an in ini e educ ion sequence om 𝑐.
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
ChiSA : S a ic Analysis o Ligh weigh Chisel Ve i ica ion 5
Theo em 2.2 (O iginal Theo em 2.2 In Ou Pape ). A ci cui wi hou a combina ional loop
canno oscilla e:
I 𝐶con ains no combina ional loop, hen in ini e educ ion sequence om any 𝑐∈Con ig𝐶.
In his subsec ion, we p o e Theo em 2.3 om ou main pape , which es ablishes ha he
inal en i onmen p oduced by any educ ion sequence om he same ini ial con igu a ion is
de e minis ic. In ac , we p o e a s onge p oposi ion conce ning s abili y (Lemma 2.7), om which
Theo em 2.3 ollows as a co olla y. To acili a e his, we in oduce a new de ini ion along wi h
se e al p e equisi e lemmas.
De ini ion 2.3. Fo a con igu a ion
⟨𝑆, 𝐸, 𝐼⟩
o a ci cui
𝐶
wi hou combina ional loops, i
𝐸(𝑥)=
⟦𝑒⟧𝐸holds o any 𝑥=𝑒∈𝐶=−𝐼, we call he con igu a ion legal.
The ini ial con igu a ion 𝑐0=⟨𝑆, 𝐸 and,𝐶=⟩is legal since 𝐶=−𝐶==∅.
Lemma 2.4. I
⟨𝑆, 𝐸, 𝐼⟩
is a legal con igu a ion o a ci cui
𝐶
wi hou combina ional loops and
𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩,⟨𝑆′, 𝐸′, 𝐼′⟩is also legal.
P oo . Do case analysis on 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩:
(1)
Case
S-Poke
: In his case,
𝐼=∅, 𝐼′=A𝐶(𝐸, 𝐸′)
. Fo any
𝑥=𝑒∈𝐶=−𝐼′
, any
𝑣∈Use(𝑥=𝑒)
sa is ies 𝐸(𝑣)=𝐸′(𝑣)since 𝑥=𝑒will be in A𝐶(𝐸, 𝐸′)=𝐼′o he wise. The e o e,
⟦𝑒⟧𝐸′=⟦𝑒⟧𝐸=𝐸(𝑥).
Since
𝑥
is no poked in his s ep (because
𝑥
is no an inpu ),
𝐸(𝑥)=𝐸′(𝑥)
. I ollows ha
⟨𝑆′, 𝐸′, 𝐼′⟩is legal.
(2) Case S-Tick: Simila .
(3)
Case
C-E al
: Suppose he i em
𝜄
used in his s ep is
𝑥=𝑒
. Since
𝐶
has no combina ional loop,
𝑥∉Use(𝑥=𝑒)holds and hus 𝐸′(𝑥)=⟦𝑒⟧𝐸′.
I
𝐸(𝑥)=𝐸′(𝑥)
, i deduces ha
𝐼′=𝐼− {𝑥=𝑒}
and
𝐸=𝐸′
. The e o e, any
𝑥′=𝑒′∈𝐶=−𝐼′=
(𝐶=−𝐼) ∪ {𝑥=𝑒}
is ei he iden ical o
𝑥=𝑒
o in
𝐶=−𝐼
. The o me case is i ial. Fo he
la e case, ⟦𝑒′⟧𝐸′=⟦𝑒′⟧𝐸=𝐸(𝑥′)=𝐸′(𝑥′).
I
𝐸(𝑥)≠𝐸′(𝑥)
,
𝐶=−𝐼′=𝐶=− (𝐼− {𝑥=𝑒}) − A𝐶(𝐸, 𝐸′)
, whe e
A𝐶(𝐸, 𝐸′)=Succ(𝑥=𝑒)
. In
his case, any
𝑥′=𝑒′∈𝐶=−𝐼′
which is no iden ical o
𝑥=𝑒
is in
𝐶=−𝐼
and no in
Succ(𝑥=𝑒)
,
whence 𝑥∉Use(𝑥′=𝑒′). Since 𝐸and 𝐸′only di e in 𝑥,⟦𝑒′⟧𝐸′=⟦𝑒′⟧𝐸=𝐸(𝑥′)=𝐸′(𝑥′).
□
Co olla y 2.5. Gi en a legal con igu a ion
⟨𝑆, 𝐸, 𝐼⟩
a ci cui
𝐶
wi hou combina ional loops,
⟨𝑆′, 𝐸′, 𝐼′⟩is legal i 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩.
P oo . T i ial induc ion. □
Lemma 2.6 (Local Con luence). Fo a legal con igu a ion
⟨𝑆, 𝐸, 𝐼⟩
o a ci cui
𝐶
wi hou combi-
na ional loops, i
𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆1, 𝐸1, 𝐼1⟩ ∧ 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆2, 𝐸2, 𝐼2⟩
, he e exis s
⟨𝑆′, 𝐸′, 𝐼′⟩
such
ha ⟨𝑆1, 𝐸1, 𝐼1⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩∧⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩.
P oo . Do a case analysis on 𝐼:
(1)
I
𝐼=∅
, only
S-Poke
o
S-Tick
can be used o make p og ess. The choice is de e mined by he
i s elemen o 𝑆, so 𝑆1=𝑆2∧𝐸1=𝐸2∧𝐼1=𝐼2. Le ⟨𝑆′, 𝐸′, 𝐼′⟩be ⟨𝑆1, 𝐸1, 𝐼1⟩.
(2) I 𝐼≠∅, only C-E al can be used o make p og ess. Assume ha :
𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆, 𝐸[𝑥1↦→ 𝑣1], 𝐼′
1∪𝐴1⟩=⟨𝑆1, 𝐸1, 𝐼1⟩,
𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝⟨𝑆, 𝐸[𝑥2↦→ 𝑣2], 𝐼′
2∪𝐴2⟩=⟨𝑆2, 𝐸2, 𝐼2⟩,
whe e:
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 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 iden ical wi h
𝑥2=𝑒2
is i ial, so we assume ha he wo i ems a e
no iden ical. Since
𝐶
has no combina ional loop, i is impossible ha
𝑥1∈Use(𝑥2=𝑒2) ∧ 𝑥2∈
Use(𝑥1=𝑒1). The e o e, we could do a case analysis on hei use- ela ion:
(a) I 𝑥1∉Use(𝑥2=𝑒2) ∧ 𝑥2∉Use(𝑥1=𝑒1), le :
𝐸′=𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣2],
𝐼′=(𝐼− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴1∪𝐴2.
I ollows immedia ely ha ⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆′, 𝐸′, 𝐼′⟩and ⟨𝑆2, 𝐸2, 𝐼2⟩⇝⟨𝑆, 𝐸′, 𝐼′⟩.
(b)
I
𝑥1∈Use(𝑥2=𝑒2) ∧ 𝑥2∉Use(𝑥1=𝑒1)
, le
𝑣′
2=⟦𝑒2⟧𝐸[𝑥1↦→𝑣1], 𝐴′
2=A𝐶(𝐸[𝑥1↦→
𝑣1], 𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣′
2]) and:
𝐸′=𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣′
2],
𝐼′=(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′
2.
I immedia ely deduces ha
⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆, 𝐸′, 𝐼′⟩
. As o ano he con igu a ion
⟨𝑆2, 𝐸2, 𝐼2⟩
,
we ha e
⟨𝑆2, 𝐸2, 𝐼2⟩⇝⟨𝑆2, 𝐸2[𝑥1↦→ 𝑣1],(𝐼2− {𝑥1=𝑒1}) ∪ A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1])⟩
. A u he
case analysis is needed:
(i)
Case
𝑣1=𝐸2(𝑥1)
: i ollows ha
𝐸(𝑥1)=𝐸2(𝑥1)=𝑣1
, whence
A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1]) =
𝐴1=∅
. The e o e, we ha e
𝐸=𝐸1
and
𝑣′
2=𝑣2
, whence
𝐴2=𝐴′
2
. I deduces ha
𝐸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 his case
𝐴′
1=A𝐶(𝐸2, 𝐸2[𝑥1↦→ 𝑣1]) =Succ(𝑥1=𝑒1) ∩ 𝐶==𝐴1
is no emp y. No ice ha
⟨𝑆2, 𝐸2, 𝐼2⟩
⇝⟨𝑆2, 𝐸2[𝑥1↦→ 𝑣1],(𝐼2− {𝑥1=𝑒1}) ∪ 𝐴′
1⟩
⇝⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′′
2⟩,
whe e 𝐴′′
2=A𝐶(𝐸[𝑥1↦→ 𝑣1][𝑥2↦→ 𝑣2], 𝐸′).
I is wo h no ing ha
𝐴′
2
is ei he emp y o iden ical o
Succ(𝑥2=𝑒2) ∩ 𝐶=
, so is
𝐴′′
2
.
I 𝐴′
2=𝐴′′
2, e e y hing is done.
Howe e , wha i
𝐴′
2≠𝐴′′
2
? In his case,
𝐴′
2⊊𝐴′′
2∨𝐴′
2⊋𝐴′′
2
holds. Fo now,
we assume ha
𝐴′
2⊊𝐴′′
2
. Since
⟨𝑆, 𝐸′, 𝐼′⟩
is legal, any
𝑥′=𝑒′
in
𝐴′′
2−𝐴′
2
sa is ies
𝐸′(𝑥′)=⟦𝑒′⟧𝐸′
. Elimina ing such i ems deduces ha
⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=
𝑒2}) ∪ 𝐴′′
2⟩⇝∗⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=𝑒2}) ∪ 𝐴′
2⟩=⟨𝑆, 𝐸′, 𝐼′⟩.
As o he case when
𝐴′
2⊋𝐴′′
2
, le
⟨𝑆′′, 𝐸′′, 𝐼′′⟩
be
⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=
𝑒2}) ∪ 𝐴′′
2⟩
. Simila ly, we can p o e ha
⟨𝑆1, 𝐸1, 𝐼1⟩⇝⟨𝑆, 𝐸′,(𝐼∪𝐴1− {𝑥1=𝑒1, 𝑥2=
𝑒2}) ∪ 𝐴′
2⟩⇝∗⟨𝑆′′, 𝐸′′, 𝐼′′⟩, while ⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′′, 𝐸′′, 𝐼′′⟩is p o ed as abo e.
(c) I 𝑥1∉Use(𝑥2=𝑒2) ∧ 𝑥2∈Use(𝑥1=𝑒1), mimic he abo e p oo .
□
Lemma 2.7 (Con luence). Fo a legal con igu a ion
⟨𝑆, 𝐸, 𝐼⟩
o a ci cui
𝐶
wi hou combina ional
loops, i
𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆1, 𝐸1, 𝐼1⟩ ∧ 𝐶⊢ ⟨𝑆, 𝐸, 𝐼⟩⇝∗⟨𝑆2, 𝐸2, 𝐼2⟩
, he e exis s
⟨𝑆′, 𝐸′, 𝐼′⟩
such ha
⟨𝑆1, 𝐸1, 𝐼1⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩∧⟨𝑆2, 𝐸2, 𝐼2⟩⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩.
P oo .
Theo em 2.2 indica es
𝜆𝐹
sa is ies s ong no maliza ion, and Lemma 2.6 p o ides local
con luence o legal con igu a ions. The conclusion is deduced om Newman’s lemma [6]. □
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
ChiSA : S a ic Analysis o Ligh weigh Chisel Ve i ica ion 7
We can hus p o e o iginal Theo em 2.3 in ou pape as ollows:
Theo em 2.8 (O iginal Theo em 2.3 In Ou Pape ). The s eady-s a e eached by a ci cui wi hou
combina ional loops is uniquely de e mined:
𝐶has no combina ional loop∧𝐶⊢ ⟨𝑆, 𝐸,𝐶=⟩⇝∗⟨𝜖, 𝐸1,∅⟩∧𝐶⊢ ⟨𝑆, 𝐸,𝐶=⟩⇝∗⟨𝜖, 𝐸2,∅⟩ ⇒ 𝐸1=𝐸2.
P oo .
Since
⟨𝑆, 𝐸,𝐶=⟩
is legal, i ollows om Lemma 2.7 ha he e is a con igu a ion
⟨𝑆′, 𝐸′, 𝐼′⟩
such ha
𝐶⊢ ⟨𝜖, 𝐸1,∅⟩ ⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩ ∧ 𝐶⊢ ⟨𝜖, 𝐸2,∅⟩ ⇝∗⟨𝑆′, 𝐸′, 𝐼′⟩
. Howe e ,
⟨𝜖, 𝐸1,∅⟩
and
⟨𝜖, 𝐸2,∅⟩ a e i educible, whence 𝐸1=𝐸′=𝐸2.□
2.2 P oo s o P ope ies in Sec ion 3
In his subsec ion, we p o ide comple e p oo s o Theo ems 3.4 and 3.6 om he main pape . The
p oo ske ches o he o he heo ems and lemmas in his sec ion a e al eady su icien ly de ailed
o se e as comple e p oo s and a e he e o e no epea ed he e.
De ini ion 2.9. Fo a non-emp y
S o e′⊆S o e
whe e
⟨S o e′,⊑⟩
is a comple e la ice, we call
S o e′a limi ed se o s o es.
As ollows, we use S o e′ o deno e any limi ed se o s o es.
Fo con enience, we in oduce a gene aliza ion o synch onous low unc ions:
De ini ion 2.10 (Fusion). We de ine
A (𝑓)
as
{𝑣∈Va | ∃𝜎∈S o e′.𝜎(𝑣)≠𝑓(𝜎)(𝑣)}
o any
unc ion
𝑓
:
S o e′→S o e′
. Fo any wo mono one unc ions
𝑓 ,𝑔
:
S o e′→S o e′
whe e
A (𝑓) ∩ A (𝑔)=∅, we w i e:
(𝑓∗𝑔)(𝑥)(𝑣)=
𝑓(𝑥)(𝑣),i 𝑣∈A (𝑓),
𝑔(𝑥)(𝑣),i 𝑣∈A (𝑔),
𝑣, o he wise.
We e e o
𝑓∗𝑔
as he usion o
𝑓
and
𝑔
. The unc ion
𝑓∗𝑔
is also mono one and sa is ies
A (𝑓∗𝑔) ⊆ A (𝑓) ∪ A (𝑔).
Fo a ini e sequence o mono one unc ions
𝑓1, . . . , 𝑓𝑠
:
S o e′→S o e′
whe e
∀𝑖, 𝑗.𝑖 ≠𝑗=⇒
A (𝑓𝑖) ∩ A (𝑓𝑗)=∅
, we call he sequence a disjoin sequence o low unc ions and w i e
𝑓∗
:
=
𝑓1∗ · · · ∗ 𝑓𝑠 o 𝑓1∗ (𝑓2∗ · · · (𝑓𝑠−1∗𝑓𝑠)).
Lemma 2.11. Fo any disjoin sequence o low unc ions
𝑓1, . . . , 𝑓𝑠
:
S o e′→S o e′
,
𝜎∈S o e′
is
a common ixed poin o 𝑓1, . . . , 𝑓𝑠i i is a ixed poin o 𝑓∗=𝑓1∗ · · · ∗ 𝑓𝑠.
P oo .
Assume
𝜎
is a common ixed poin o
𝑓1, . . . , 𝑓𝑠
. Fo any
𝑥∈Va
, he e exis s a mos one
index
𝑗
such ha
𝑥∈A (𝑓𝑗)
. I he e is no such index,
𝑓∗(𝜎)(𝑥)=𝜎(𝑥)
. O he wise,
𝑓∗(𝜎)(𝑥)=
𝑓𝑗(𝜎)(𝑥)=𝜎(𝑥). The e o e, 𝑓∗(𝜎)(𝑥)=𝜎(𝑥)holds o any 𝑥∈Va , namely ha 𝑓∗(𝜎)=𝜎.
Con e sely, suppose
𝜎
is a ixed poin o
𝑓∗
. No ice ha
𝑓𝑗(𝜎)(𝑥)
is ei he
𝜎(𝑥)
o
𝑓∗(𝜎)(𝑥)=𝜎(𝑥)
o any index 𝑗and 𝑥∈Va , whence 𝑓𝑗(𝜎)=𝜎holds o any 𝑗.□
Lemma 2.12. I
S o e′
is a comple e la ice wi h ini e heigh , o any disjoin sequence o low
unc ions 𝑓1, . . . , 𝑓𝑠:S o e′→S o e′, he unc ions:
𝑓∗=𝑓1∗ · · · ∗ 𝑓𝑠,
𝑓◦=𝑓1◦ · · · ◦ 𝑓𝑠,
ha e he same leas ixed poin .
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
8 Jiacai Cui, Qinlin Chen, Zhongsheng Zhan, Tian Tan, and Yue Li
P oo . Suppose he leas ixed poin s o 𝑓∗and 𝑓◦a e 𝜎∗and 𝜎◦ espec i ely.
On he one hand, o any
𝜎∈S o e′
, i
𝑓∗(𝜎) ⊑ 𝜎
, we ha e
𝑓𝑖(𝜎) ⊑ 𝜎
o any index
𝑖
. This
implies ha 𝑓1(𝑓2(· · · (𝑓𝑛−1(𝑓𝑛(𝜎))))) ⊑ 𝑓1(𝑓2(· · · (𝑓𝑛−1(𝜎)))) ⊑ . . . ⊑𝑓1(𝜎) ⊑ 𝜎, whence:
{𝜎∈S o e′| (𝑓∗)(𝜎) ⊑ 𝜎} ⊆ {𝜎∈S o e′| (𝑓◦)(𝜎) ⊑ 𝜎}.
By Ta ski’s ixed-poin heo em [8], 𝜎∗⊒𝜎◦.
On he o he hand, Kleene’s ixed-poin heo em [
2
,
5
] indica es ha , o any mono one unc ion
ℎ
:
𝐿→𝐿
, he e exis s
𝑛∈N
such ha
ℎ𝑛+1(⊥) =ℎ𝑛(⊥)
is he leas ixed poin o
ℎ
. Suppose
(𝑓∗)𝑚(⊥) and (𝑓◦)𝑛(⊥) a e leas ixed poin s o 𝑓∗and 𝑓◦ espec i ely.
Le :
𝑝𝑛=(𝑓◦)𝑛(⊥),
𝑞𝑛=(𝑓∗)𝑛(⊥).
As he p oo o Kleene’s ixed-poin heo em [
5
] demons a es,
𝑝𝑖⊑𝑝𝑖+1
holds o any index
𝑖
.
Simila ly, 𝑞𝑖⊑𝑞𝑖+1also holds o any index 𝑖.
We shall p o e ha 𝑝𝑖⊒𝑞𝑖 o any index 𝑖∈Nby induc ion:
(1) Base Case: F om 𝑝0=𝑞0=⊥, i ollows ha 𝑝0⊒𝑞0.
(2) Induc ion S ep: Assume 𝑝𝑖⊒𝑞𝑖. We shall p o e 𝑝𝑖+1⊒𝑞𝑖+1.
Since
𝑞𝑖⊑𝑞𝑖+1
, e e y
𝑥∈Va
sa is ies ha
𝑞𝑖(𝑥) ⊑ 𝑞𝑖+1(𝑥)=(𝑓∗)(𝑞𝑖)(𝑥)
. F om he
de ini ion o 𝑓∗, i ollows immedia ely ha 𝑞𝑖⊑𝑓𝑗(𝑞𝑖) o any index 𝑗=1, . . . ,𝑠.
No ice ha :
𝑝𝑖+1=𝑓◦(𝑝𝑖)⊒𝑓◦(𝑞𝑖).
Fo any
𝑥∈Va
, he e is a mos one index
𝑗
such ha
𝑥∈A (𝑓𝑗)
. I such index does no
exis ,
𝑓◦(𝑞𝑖)(𝑥)=𝑞𝑖(𝑥)=𝑓∗(𝑞𝑖)(𝑥)
. O he wise, suppose such
𝑗
exis s. F om he assump ion,
i ollows ha :
𝑓◦(𝑞𝑖)(𝑥)=(𝑓1◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥)=(𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥).
By ∀𝑗.𝑓𝑗(𝑞𝑖) ⊒ 𝑞𝑖, we ha e:
(𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)⊒(𝑓𝑗◦ · · · ◦ 𝑓𝑠−1)(𝑞𝑖) ⊒ . . . ⊒𝑓𝑗(𝑞𝑖),
whence (𝑓𝑗◦ · · · ◦ 𝑓𝑠)(𝑞𝑖)(𝑥)⊒𝑓𝑗(𝑞𝑖)(𝑥)=𝑓∗(𝑞𝑖)(𝑥).
The e o e,
𝑓◦(𝑞𝑖)(𝑥) ⊒ 𝑓∗(𝑞𝑖)(𝑥)
holds o any
𝑥∈Va
, namely ha
𝑝𝑖+1⊒𝑓◦(𝑞𝑖) ⊒
𝑓∗(𝑞𝑖)=𝑞𝑖+1.
Le
𝑢=max(𝑚,𝑛)
, i ollows ha
𝜎◦=(𝑓◦)𝑛(⊥) =(𝑓◦)𝑢(⊥) ⊒ (𝑓∗)𝑢(⊥) =(𝑓∗)𝑚(⊥) =𝜎∗
.
The e o e, he leas ixed poin s o 𝑓◦and 𝑓∗a e equi alen . □
We will p o e Theo em 3.4 in ou pape as ollows:
Theo em 2.13 (O iginal Theo em 3.4 In Ou Pape ). Algo i hm 1 con e ges o he leas syn-
ch onized ixed poin LSFP𝐶,𝛿
𝑓i 𝑓is mono onic and ⟨𝐿, ⊑⟩ is a comple e la ice wi h ini e heigh .
P oo .
Since
Va
is ini e, i ollows ha
S o e
is also a comple e la ice wi h ini e heigh . Le
S o e𝛿
deno e
{𝜎∈S o e|∀𝑣∈Inpu 𝐶.𝜎 (𝑣)=𝛿(𝑣)}
, which is a limi ed se o s o es wi h ini e
heigh .
So
𝐶=
in o
𝜄1, . . . , 𝜄𝑠
by a e e se opological o de o
𝐺𝐶[𝐶=]
. By Kleene’s ixed-poin heo em [
2
,
5], Algo i hm 1 compu es he leas ixed poin o he unc ion:
𝑓⟦𝐶⇐⟧ ◦ 𝑓⟦𝜄1⟧ ◦ · · · ◦ 𝑓⟦𝜄𝑠⟧.
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
ChiSA : S a ic Analysis o Ligh weigh Chisel Ve i ica ion 9
While any elemen in
LSFP𝐶,𝛿
𝑓
is a common leas ixed poin o
𝑓⟦𝐶⇐⟧, 𝑓 ⟦𝜄1⟧, . . . , 𝑓 ⟦𝜄𝑠⟧
, which is
indeed he leas ixed poin o
𝑓⟦𝐶⇐⟧∗ 𝑓⟦𝜄1⟧∗· · ·∗⟦𝜄𝑠⟧
by Lemma 2.11. By Lemma 2.12, Algo i hm
1 compu es his leas ixed poin . □
We can hus p o e Theo em 3.6 in ou pape as ollows:
Theo em 2.14 (O iginal Theo em 3.6 In Ou Pape ). I
⟨𝐿, ⊑⟩
is a comple e la ice,
𝑓1⊑𝑓2
,
𝜎1∈LSFP𝐶,𝛿
𝑓1, and 𝜎2∈LSFP𝐶,𝛿
𝑓2, hen 𝜎1⊑𝜎2.
P oo .
Since
𝐿
is comple e,
S o e
is also a comple e la ice. Le
S o e𝛿
deno e
{𝜎∈S o e|∀𝑣∈
Inpu 𝐶.𝜎(𝑣)=𝛿(𝑣)}, which is a limi ed se o s o es.
By he assump ion,
𝑓∗
1⊑𝑓∗
2
. F om Lemma 2.11, i ollows ha
𝜎1
is he leas ixed poin o
𝑓∗
1
and 𝜎2is ha o 𝑓∗
2.
By de ini ion,
𝑓∗
1
is equal o
𝑓1⟦𝐶⟧
. Simila ly,
𝑓∗
2=𝑓2⟦𝐶⟧
. F om
𝑓1⊑𝑓2
, i ollows ha
𝑓1⟦𝐶⟧ ⊑
𝑓2⟦𝐶⟧. Conside any 𝜎∈S o e𝛿which sa is ies 𝑓∗
2(𝜎) ⊑ 𝜎, we ha e:
𝑓∗
1(𝜎)⊑𝑓1⟦𝐶⟧(𝜎)⊑𝑓2⟦𝐶⟧(𝜎)=𝑓∗
2(𝜎) ⊑ 𝜎.
The e o e, {𝜎∈S o e𝛿|𝑓∗
1(𝜎) ⊑ 𝜎} ⊇ {𝜎∈S o e𝛿|𝑓∗
2(𝜎) ⊑ 𝜎}holds.
By Ta ski’s ixed-poin heo em [8],
𝜎1=⊓{𝜎∈S o e𝛿|𝑓∗
1(𝜎) ⊑ 𝜎} ⊑ ⊓{𝜎∈S o e𝛿|𝑓∗
2(𝜎) ⊑ 𝜎}=𝜎2.
□
3 Discussion: Chao ic Values
In ou main pape (De ini ion 2.1), we chose
Value =Z
(i.e., he se o ma hema ical in ege s) pu ely
o ease o unde s anding and p esen a ion. A mo e igo ous and comple e ea men o alues is
as ollows:
Value :=Z∪Z′whe e Z′:={𝑖′|𝑖∈Z}
He e, each
𝑖′
ep esen s a andom alue d awn om
𝐸 and
:
Va →Z′
in he ini ial con igu a ion
𝑐0=⟨𝑆0, 𝐸 and,𝐶=⟩
, modeling he non-de e minis ic beha io o eal-wo ld digi al ci cui s a powe -
up. We e e o such alues as chao ic alues o e lec hei physical meaning.
The de ini ion o e alua ion (o iginal De ini ion 2.9 in ou pape ) equi es only a sligh e inemen ,
as de ined case by case below, which p ese es he o e all s uc u e and spi i o he o iginal
seman ics:
⟦𝑛⟧𝐸:=𝑛⟦𝑦⟧𝐸:=𝐸(𝑦)
⟦𝑦op 𝑧⟧𝐸:=(ℭ(ℨ(𝐸(𝑦)) op ℨ(𝐸(𝑧))) i 𝐸(𝑦) ∈ Z′∨𝐸(𝑧) ∈ Z′,
𝐸(𝑦)op 𝐸(𝑧)o he wise .
⟦mux(𝑤, 𝑦, 𝑧)⟧𝐸:=(ℭ(𝐸(𝑦)) i 𝐸(𝑤)≠0′∧𝐸(𝑤) ∈ Z′,ℭ(𝐸(𝑧)) i 𝐸(𝑤)=0′,
𝐸(𝑦)i 𝐸(𝑤)≠0∧𝐸(𝑤)∉Z′, 𝐸(𝑧)i 𝐸(𝑤)=0.
whe e:
ℨ(𝑥):=(𝑥, i 𝑥∈Z,
𝑖, i 𝑥=𝑖′∈Z′.ℭ(𝑥):=(𝑥′,i 𝑥∈Z,
𝑥, i 𝑥∈Z′.
, Vol. Zenodo, No. 1, A icle . Publica ion da e: No embe 2025.
