From 9838bb9669eb7b710b779dad672591dbf8062576 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 10:48:38 +0800
Subject: [PATCH 01/23] refactor: Rename VarDymTyped to VarDynamic and update
 related usages

---
 .../dependentChisel/algo/treeTraverse.scala   | 41 ++++++++++++++++---
 .../dependentChisel/codegen/compiler.scala    |  6 +--
 .../codegen/sequentialCommands.scala          |  2 +-
 .../dependentChisel/staticAnalysis/readme.md  |  2 +
 .../typesAndSyntax/statements.scala           |  2 +-
 .../typesAndSyntax/typesAndOps.scala          |  4 +-
 .../typesAndSyntax/varDecls.scala             |  6 +--
 7 files changed, 47 insertions(+), 16 deletions(-)
 create mode 100644 src/main/scala/dependentChisel/staticAnalysis/readme.md

diff --git a/src/main/scala/dependentChisel/algo/treeTraverse.scala b/src/main/scala/dependentChisel/algo/treeTraverse.scala
index b2b959e..329d5a7 100644
--- a/src/main/scala/dependentChisel/algo/treeTraverse.scala
+++ b/src/main/scala/dependentChisel/algo/treeTraverse.scala
@@ -16,7 +16,20 @@ object treeTraverse {
     node.children.foreach(preOrder(visit, _))
   }
 
-  /** filter tree nodes based on predicate
+  /** filter tree nodes based on predicate. There are multiple ways to interpret this:
+    *
+    * 1 We remove only the leaves that do not satisfy the predicate, and for branch nodes, we keep
+    * them if either they satisfy the predicate or if they have any descendant that satisfies the
+    * predicate (so we keep the structure to reach the satisfying leaves).
+    *
+    * 2 We remove every node that does not satisfy the predicate, and if a branch node is removed,
+    * then we must somehow promote its children? But then the tree structure might change.
+    *
+    * 3 We do a transformation such that we keep the tree structure, but we remove any leaf that
+    * doesn't satisfy the predicate, and for branch nodes, we keep them only if they satisfy the
+    * predicate OR if they have at least one child that is kept. This is similar to a prune.
+    *
+    * 4 the assert is only top level and about inputs/outputs for assume-guarantee style
     *
     * TODO: test this function
     * @param predicate
@@ -26,21 +39,37 @@ object treeTraverse {
     */
   def filter[t](
       predicate: t => Boolean,
-      node: Tree.TreeNode[t]
+      tree: Tree.TreeNode[t]
   ): Tree.TreeNode[t] = {
-    val flag @ (yes, hasChild) = (predicate(node.value), node.children.nonEmpty)
+    val flag @ (yes, hasChild) = (predicate(tree.value), tree.children.nonEmpty)
 
     // if children is empty, it's leaf node, just return itself if satisfies predicate
     if hasChild then {
       // recursively filter its children
-      val filteredChildren = node.children
+      val filteredChildren = tree.children
         .map(child => filter(predicate, child))
         .filter(child => predicate(child.value) || child.children.nonEmpty)
-      Tree.TreeNode(node.value, filteredChildren)
+      Tree.TreeNode(tree.value, filteredChildren)
     } else {
       // leaf node, just return itself if satisfies predicate
-      if yes then node else Tree.TreeNode(node.value, ArrayBuffer())
+      if yes then tree else Tree.TreeNode(tree.value, ArrayBuffer())
     }
 
   }
+
+  /** only filter the top level children of the tree.Useful for assume-guarantee style formal
+    * verification
+    *
+    * @param predicate
+    * @param tree
+    * @return
+    */
+  def filterTop[t](
+      predicate: t => Boolean,
+      tree: Tree.TreeNode[t]
+  ): Tree.TreeNode[t] = {
+    val filteredChildren = tree.children
+      .filter(child => predicate(child.value))
+    tree.copy(children = filteredChildren)
+  }
 }
diff --git a/src/main/scala/dependentChisel/codegen/compiler.scala b/src/main/scala/dependentChisel/codegen/compiler.scala
index 5e81533..c7e6ae1 100644
--- a/src/main/scala/dependentChisel/codegen/compiler.scala
+++ b/src/main/scala/dependentChisel/codegen/compiler.scala
@@ -258,7 +258,7 @@ object compiler {
   }
 
   def varDecl2firrtlStr(indent: String = "", stmt: VarDecls) = {
-    val VarDymTyped(width: Int, tp: VarType, name: String) = stmt.v
+    val VarDynamic(width: Int, tp: VarType, name: String) = stmt.v
     tp match {
       case VarType.Reg => // reg without init
         /* reg mReg : UInt<16>, clock with :
@@ -355,7 +355,7 @@ object compiler {
         io.y:=a+b becomes y0=a+b;io.y<=y0
         new : don't do above
        */
-      case x: (VarTyped[?] | VarDymTyped) =>
+      case x: (VarTyped[?] | VarDynamic) =>
         val genStmt = expr2stmtBind(stmt.rhs)
         List(genStmt, stmt.copy(op = "<=", rhs = genStmt.lhs))
       // List(stmt.copy(op = "<="))
@@ -382,7 +382,7 @@ object compiler {
   def varNameTransform(thisInstName: String, v: Var[?]): Var[?] = {
     v match {
       case x @ VarLit(name) => x
-      case x @ VarDymTyped(width, tp, name) =>
+      case x @ VarDynamic(width, tp, name) =>
         tp match {
           case VarType.Input | VarType.Output =>
             x.copy(name = ioNameTransform(thisInstName, name))
diff --git a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
index 7db02bd..85525aa 100644
--- a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
+++ b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
@@ -49,7 +49,7 @@ object sequentialCommands {
   ) extends AtomicCmds
 
   /** for Wire, Reg, and IO */
-  case class VarDecls(v: VarDymTyped) extends AtomicCmds
+  case class VarDecls(v: VarDynamic) extends AtomicCmds
   case object Skip extends AtomicCmds
   /* TODO:also allow dym check which rm type sig of var[t] ,etc. cases
    * of (lhs,rhs) are (dym,stat),(dym,dym)....
diff --git a/src/main/scala/dependentChisel/staticAnalysis/readme.md b/src/main/scala/dependentChisel/staticAnalysis/readme.md
new file mode 100644
index 0000000..b4245e9
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/readme.md
@@ -0,0 +1,2 @@
+# static analysis
+This directory contains static analysis experiments for Chisel code, based on the classical program analysis techniques from Flemming Nielson's book "Principles of Program Analysis".
\ No newline at end of file
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
index 1b9f7ca..8f3f0fb 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
@@ -38,7 +38,7 @@ object statements {
   }
 
   /** untyped API for assign */
-  extension (v: VarDymTyped) {
+  extension (v: VarDynamic) {
     inline def :=(using md: ModuleData)(oth: Expr[?]) = {
       val name = v.getname
       md.typeMap.addOne(v, v.width)
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
index 750135a..7699448 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
@@ -67,7 +67,7 @@ represent a vector of bits */
   // new ExprC[1, VarDeclTp.Reg.type] {} + new ExprC[1, VarDeclTp.Wire.type] {} //ok ,will fail
 
   /** untyped API for Wire, Reg, and IO */
-  case class VarDymTyped(width: Int, tp: VarType, name: String)
+  case class VarDynamic(width: Int, tp: VarType, name: String)
       extends Var[Nothing](name) {
 
     /** dym check for type cast */
@@ -93,7 +93,7 @@ represent a vector of bits */
   case class VarTyped[w <: Int](name: String, tp: VarType) extends Var[w](name) {
 
     /** a dirty hack */
-    def toDym(width: Int) = VarDymTyped(width, tp, name)
+    def toDym(width: Int) = VarDynamic(width, tp, name)
   }
 
   // case class Input[w <: Int](name: String) extends Var[w](name)
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala b/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
index 9254919..e30288b 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
@@ -65,7 +65,7 @@ object varDecls {
   )(width: Int, tp: VarType.Input.type | VarType.Output.type, givenName: String = "") = {
 
     val genName = naming.genNameForVar(givenName, tp)
-    val r = VarDymTyped(
+    val r = VarDynamic(
       width,
       tp,
       mli.instanceName + "." + genName
@@ -97,7 +97,7 @@ object varDecls {
     def newRegDym(width: Int, givenName: String = "") = {
       // need to push this cmd for varDecl
       val genName = naming.genNameForVar(givenName, VarType.Reg)
-      val r = VarDymTyped(width, VarType.Reg, genName)
+      val r = VarDynamic(width, VarType.Reg, genName)
       moduleData.typeMap.addOne(r, width)
       moduleData.commands.append(VarDecls(r))
       r
@@ -107,7 +107,7 @@ object varDecls {
       // need to push this cmd for varDecl
       val width = init.width
       val genName = naming.genNameForVar(givenName, VarType.Reg)
-      val r = VarDymTyped(width, VarType.RegInit(init), genName)
+      val r = VarDynamic(width, VarType.RegInit(init), genName)
       moduleData.typeMap.addOne(r, width)
       moduleData.commands.append(VarDecls(r))
       r

From 573bd04c64ed4bea90aa297bb4a29f381b188123 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 10:54:59 +0800
Subject: [PATCH 02/23] feat: Add BoolProp for formal verification in
 sequentialCommands and update adder example

---
 .../codegen/sequentialCommands.scala                |  3 +++
 src/test/scala/dependentChisel/examples/adder.scala | 13 ++++++++++++-
 2 files changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
index 85525aa..59ac387 100644
--- a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
+++ b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
@@ -56,4 +56,7 @@ object sequentialCommands {
    1.new super type for Var[w]
    */
 
+  /** formal verification commands */
+  case class BoolProp(name: String, prop: Bool) extends AtomicCmds
+
 }
diff --git a/src/test/scala/dependentChisel/examples/adder.scala b/src/test/scala/dependentChisel/examples/adder.scala
index e394892..819a24f 100644
--- a/src/test/scala/dependentChisel/examples/adder.scala
+++ b/src/test/scala/dependentChisel/examples/adder.scala
@@ -13,8 +13,8 @@ import dependentChisel.typesAndSyntax.chiselModules.*
 import dependentChisel.typesAndSyntax.varDecls.newIO
 import dependentChisel.codegen.compiler.*
 
-
 import dependentChisel.typesAndSyntax.varDecls.newIODym
+import dependentChisel.codegen.sequentialCommands.BoolProp
 
 object adder extends mainRunnable {
 
@@ -109,4 +109,15 @@ object adder extends mainRunnable {
     m1.b := b
     y := m1.y
   }
+
+  /** adder with formal verification properties
+    */
+  class Adder1prop(using GlobalInfo) extends UserModule {
+    val a = newIO[2](VarType.Input)
+    val b = newIO[2](VarType.Input)
+    val y = newIO[2](VarType.Output)
+
+    y := a + b
+    BoolProp("assert", y === a + b)
+  }
 }

From 39fe02c8516038cbb42d415eb9d10a6e81a865ee Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 11:12:40 +0800
Subject: [PATCH 03/23] feat: Implement AST transformation methods in
 chiselModules and add tests for tree AST transformation

---
 .../dependentChisel/algo/stackList2tree.scala |  2 +-
 .../typesAndSyntax/chiselModules.scala        | 16 +++++++++-
 .../scala/dependentChisel/astTransform.scala  | 31 +++++++++++++++++++
 3 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 src/test/scala/dependentChisel/astTransform.scala

diff --git a/src/main/scala/dependentChisel/algo/stackList2tree.scala b/src/main/scala/dependentChisel/algo/stackList2tree.scala
index 3d16f0a..2bc5915 100644
--- a/src/main/scala/dependentChisel/algo/stackList2tree.scala
+++ b/src/main/scala/dependentChisel/algo/stackList2tree.scala
@@ -11,7 +11,7 @@ import dependentChisel.codegen.sequentialCommands.*
 /** algorithm to convert sequential commands to AST in tree structure
   */
 object stackList2tree {
-  type AST = TreeNode[NewInstance | WeakStmt | Ctrl | VarDecls]
+  type AST = TreeNode[Ctrl | Cmds]
 
   /** convert sequential commands to AST.
     *
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
index 4b7741b..44c5e69 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
@@ -21,6 +21,9 @@ import dependentChisel.global
 import scala.util.Try
 import scala.util.Failure
 import scala.util.Success
+import dependentChisel.algo.stackList2tree
+import dependentChisel.algo.Tree.TreeNode
+import dependentChisel.algo.stackList2tree.AST
 
 /** IR for current implementation
   *
@@ -50,7 +53,18 @@ object chiselModules {
       io: ArrayBuffer[IOdef] = ArrayBuffer(),
       commands: ArrayBuffer[Cmds] = ArrayBuffer(), // list of statements
       typeMap: mutable.Map[Expr[?] | Var[?], Int] = mutable.Map() // list of seq cmds
-  )
+  ) {
+    def commandAsTree(): AST = {
+      stackList2tree.list2tree(commands.toList)
+    }
+
+    def transformTree(
+        f: AST => AST
+    ): AST = {
+      val tree = commandAsTree()
+      f(tree)
+    }
+  }
 
   /* function style UserModule ,for example: when {} else {} */
   trait UserModule(using parent: GlobalInfo) extends UserModuleOps, UserModuleDecls {
diff --git a/src/test/scala/dependentChisel/astTransform.scala b/src/test/scala/dependentChisel/astTransform.scala
new file mode 100644
index 0000000..5b67f82
--- /dev/null
+++ b/src/test/scala/dependentChisel/astTransform.scala
@@ -0,0 +1,31 @@
+package dependentChisel
+import org.scalatest.funsuite.AnyFunSuite
+
+import dependentChisel.examples.adder.*
+import dependentChisel.examples.ifTest.*
+
+import dependentChisel.examples.dynamicAdder
+import dependentChisel.testUtils.checkWidthAndFirrtl
+import dependentChisel.examples.BubbleFifo.*
+import dependentChisel.examples.BubbleFifo
+
+import io.github.iltotore.iron.*
+import io.github.iltotore.iron.constraint.numeric.*
+import dependentChisel.examples.adder
+import dependentChisel.typesAndSyntax.chiselModules.makeModule
+import dependentChisel.algo.treeTraverse
+import dependentChisel.algo.treeTraverse.filter
+
+/* more tests for parameterized mod*/
+class astTransform extends AnyFunSuite {
+  test("tree AST transform works") {
+    val m = makeModule({ implicit p =>
+      new adder.Adder1prop
+    })
+
+    m.moduleData.transformTree { ast =>
+      treeTraverse.filterTop({ t => true }, ast)
+    }
+  }
+
+}

From 0a0a9488b877df977b5b3310d093e0fa4be9cfae Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 11:20:31 +0800
Subject: [PATCH 04/23] chore: Update CI workflow to rename job and improve
 Java setup steps

---
 .github/workflows/ci.yml | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index c0bf39d..c6de04d 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -8,7 +8,7 @@ env:
 
 jobs:
   run:
-    name: Compile
+    name: unit test
     strategy:
       matrix:
         java-version: [17]
@@ -19,16 +19,14 @@ jobs:
         with:
           fetch-depth: 0
 
-      - name: Setup Java
+      - name: Setup Java and SBT
         uses: actions/setup-java@v4
         with:
           distribution: temurin
           java-version: ${{ matrix.java-version }}
           cache: sbt
 
-          # cache sbt dependencies
       - uses: coursier/cache-action@v6
-
       - uses: sbt/setup-sbt@v1
 
       - name: unit test

From ec99a32759d27ff9b5a49e1ed80a777b653c700d Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 13:05:47 +0800
Subject: [PATCH 05/23] feat: Enhance AST transformation by adding BoolProp
 handling and refactor command appending

---
 .../dependentChisel/algo/stackList2tree.scala |  3 +-
 .../codegen/sequentialCommands.scala          |  8 +--
 .../typesAndSyntax/statements.scala           | 21 +++++++-
 .../scala/dependentChisel/astTransform.scala  | 31 ------------
 .../dependentChisel/astTransformSuite.scala   | 50 +++++++++++++++++++
 .../dependentChisel/examples/adder.scala      |  2 +-
 6 files changed, 77 insertions(+), 38 deletions(-)
 delete mode 100644 src/test/scala/dependentChisel/astTransform.scala
 create mode 100644 src/test/scala/dependentChisel/astTransformSuite.scala

diff --git a/src/main/scala/dependentChisel/algo/stackList2tree.scala b/src/main/scala/dependentChisel/algo/stackList2tree.scala
index 2bc5915..16f4dce 100644
--- a/src/main/scala/dependentChisel/algo/stackList2tree.scala
+++ b/src/main/scala/dependentChisel/algo/stackList2tree.scala
@@ -11,6 +11,7 @@ import dependentChisel.codegen.sequentialCommands.*
 /** algorithm to convert sequential commands to AST in tree structure
   */
 object stackList2tree {
+  // node can be control structure like if, or simple commands like assign
   type AST = TreeNode[Ctrl | Cmds]
 
   /** convert sequential commands to AST.
@@ -37,7 +38,7 @@ object stackList2tree {
           // end of block, pop out one parent
           parents.pop()
         // for other stmt,just append
-        case stmt: (WeakStmt | NewInstance | VarDecls) =>
+        case stmt: (WeakStmt | NewInstance | VarDecls | BoolProp) =>
           val newNd: AST = TreeNode(stmt)
           parents.top.children += newNd
         case _ =>
diff --git a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
index 59ac387..e60e795 100644
--- a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
+++ b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
@@ -18,13 +18,16 @@ object sequentialCommands {
     case If(cond: Bool)
     // case IfElse[w <: Int](b: Bool[w])
     case Else[w <: Int]()
-    case Top()
+    case Top() // represents top level
   }
 
   /** all sorts of sequential commands
     */
   sealed trait Cmds
 
+  /** atomic commands like decl,assign,etc */
+  sealed trait AtomicCmds extends Cmds
+
   /** represent start/end of control block
     *
     * @param ctrl
@@ -34,9 +37,8 @@ object sequentialCommands {
   case class End[CT <: Ctrl](ctrl: CT, uid: Uid) extends Cmds
 
   /** atomic commands like decl,assign,etc */
-  sealed trait AtomicCmds extends Cmds
 
-  /** for new mod */
+  /** new inst for a module */
   case class NewInstance(instNm: String, modNm: String) extends AtomicCmds
 
   /** firrtl statements: weakly typed which doesn't require width of lhs = wid of rhs.
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
index 8f3f0fb..f7e4cbb 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
@@ -18,6 +18,23 @@ import dependentChisel.misc.depTypes
 /** assignments */
 object statements {
 
+  def appendCmdToModule(using md: ModuleData)(stmt: Cmds): Unit = {
+    md.commands += stmt
+  }
+
+  extension (stmt: Cmds) {
+
+    /** this adds the statement to current module's command list
+      *
+      * if not using this, the statement will not be in the module IR
+      *
+      * @param md
+      */
+    def here(using md: ModuleData): Unit = {
+      appendCmdToModule(stmt)
+    }
+  }
+
   /** typed API for assign */
   extension [w <: Int, V <: Var[w]](v: V) {
 
@@ -32,7 +49,7 @@ object statements {
       // dbg(v)
       // dbg(oth)
       // mli.typeMap.addOne(v, constValueOpt[w].get)
-      md.commands += WeakStmt(v, ":=", oth)
+      appendCmdToModule(WeakStmt(v, ":=", oth))
     }
 
   }
@@ -43,7 +60,7 @@ object statements {
       val name = v.getname
       md.typeMap.addOne(v, v.width)
 
-      md.commands += WeakStmt(v, ":=", oth)
+      appendCmdToModule(WeakStmt(v, ":=", oth))
     }
   }
 }
diff --git a/src/test/scala/dependentChisel/astTransform.scala b/src/test/scala/dependentChisel/astTransform.scala
deleted file mode 100644
index 5b67f82..0000000
--- a/src/test/scala/dependentChisel/astTransform.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-package dependentChisel
-import org.scalatest.funsuite.AnyFunSuite
-
-import dependentChisel.examples.adder.*
-import dependentChisel.examples.ifTest.*
-
-import dependentChisel.examples.dynamicAdder
-import dependentChisel.testUtils.checkWidthAndFirrtl
-import dependentChisel.examples.BubbleFifo.*
-import dependentChisel.examples.BubbleFifo
-
-import io.github.iltotore.iron.*
-import io.github.iltotore.iron.constraint.numeric.*
-import dependentChisel.examples.adder
-import dependentChisel.typesAndSyntax.chiselModules.makeModule
-import dependentChisel.algo.treeTraverse
-import dependentChisel.algo.treeTraverse.filter
-
-/* more tests for parameterized mod*/
-class astTransform extends AnyFunSuite {
-  test("tree AST transform works") {
-    val m = makeModule({ implicit p =>
-      new adder.Adder1prop
-    })
-
-    m.moduleData.transformTree { ast =>
-      treeTraverse.filterTop({ t => true }, ast)
-    }
-  }
-
-}
diff --git a/src/test/scala/dependentChisel/astTransformSuite.scala b/src/test/scala/dependentChisel/astTransformSuite.scala
new file mode 100644
index 0000000..fbf64b8
--- /dev/null
+++ b/src/test/scala/dependentChisel/astTransformSuite.scala
@@ -0,0 +1,50 @@
+package dependentChisel
+import org.scalatest.funsuite.AnyFunSuite
+
+import dependentChisel.examples.adder.*
+import dependentChisel.examples.ifTest.*
+
+import dependentChisel.examples.dynamicAdder
+import dependentChisel.testUtils.checkWidthAndFirrtl
+import dependentChisel.examples.BubbleFifo.*
+import dependentChisel.examples.BubbleFifo
+
+import io.github.iltotore.iron.*
+import io.github.iltotore.iron.constraint.numeric.*
+import dependentChisel.examples.adder
+import dependentChisel.typesAndSyntax.chiselModules.makeModule
+import dependentChisel.algo.treeTraverse
+import dependentChisel.algo.treeTraverse.filter
+import dependentChisel.codegen.sequentialCommands.Cmds
+import dependentChisel.algo.Tree.TreeNode
+import dependentChisel.codegen.sequentialCommands.Ctrl
+import dependentChisel.codegen.sequentialCommands.Start
+import dependentChisel.codegen.sequentialCommands.End
+import dependentChisel.codegen.sequentialCommands.NewInstance
+import dependentChisel.codegen.sequentialCommands.WeakStmt
+import dependentChisel.codegen.sequentialCommands.VarDecls
+import dependentChisel.codegen.sequentialCommands.Skip
+import dependentChisel.codegen.sequentialCommands.BoolProp
+
+/* more tests for parameterized mod*/
+class astTransformSuite extends AnyFunSuite {
+  test("tree AST transform works") {
+    val m = makeModule({ implicit p =>
+      new adder.Adder1prop
+    })
+
+    pprint.pprintln(m.moduleData.commandAsTree())
+    val newAst =
+      m.moduleData.transformTree { (ast: TreeNode[Ctrl | Cmds]) =>
+        val predicate: Ctrl | Cmds => Boolean = {
+          case BoolProp(name, prop) => true
+          case _                    => false
+        }
+
+        treeTraverse.filterTop(predicate, ast)
+      }
+
+    pprint.pprintln(newAst)
+  }
+
+}
diff --git a/src/test/scala/dependentChisel/examples/adder.scala b/src/test/scala/dependentChisel/examples/adder.scala
index 819a24f..a99d510 100644
--- a/src/test/scala/dependentChisel/examples/adder.scala
+++ b/src/test/scala/dependentChisel/examples/adder.scala
@@ -118,6 +118,6 @@ object adder extends mainRunnable {
     val y = newIO[2](VarType.Output)
 
     y := a + b
-    BoolProp("assert", y === a + b)
+    BoolProp("assert", y === a + b).here
   }
 }

From cd015bb8a93b7204778f78ad0b01fc2e589ba929 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 13:12:30 +0800
Subject: [PATCH 06/23] feat: Add global settings and custom pprint method;
 update tests to use new pprint

---
 src/main/scala/dependentChisel/global.scala           | 11 ++++++++++-
 .../scala/dependentChisel/astTransformSuite.scala     |  6 ++++--
 2 files changed, 14 insertions(+), 3 deletions(-)

diff --git a/src/main/scala/dependentChisel/global.scala b/src/main/scala/dependentChisel/global.scala
index 7900af4..855522e 100644
--- a/src/main/scala/dependentChisel/global.scala
+++ b/src/main/scala/dependentChisel/global.scala
@@ -1,6 +1,9 @@
 package dependentChisel
 
-/* global vars */
+/** global and package-wide settings
+  *
+  * same as package object in scala 2
+  */
 object global {
   val enableWidthCheck = true
   // val enableWidthCheck = false
@@ -12,4 +15,10 @@ object global {
     counter += 1
     counter
   }
+
+  /** my pprint, not show field names
+    *
+    * @param x
+    */
+  def mPPrint[T](x: T) = { pprint.pprintln(x, showFieldNames = false) }
 }
diff --git a/src/test/scala/dependentChisel/astTransformSuite.scala b/src/test/scala/dependentChisel/astTransformSuite.scala
index fbf64b8..1a27f67 100644
--- a/src/test/scala/dependentChisel/astTransformSuite.scala
+++ b/src/test/scala/dependentChisel/astTransformSuite.scala
@@ -25,6 +25,7 @@ import dependentChisel.codegen.sequentialCommands.WeakStmt
 import dependentChisel.codegen.sequentialCommands.VarDecls
 import dependentChisel.codegen.sequentialCommands.Skip
 import dependentChisel.codegen.sequentialCommands.BoolProp
+import dependentChisel.global.mPPrint
 
 /* more tests for parameterized mod*/
 class astTransformSuite extends AnyFunSuite {
@@ -33,7 +34,7 @@ class astTransformSuite extends AnyFunSuite {
       new adder.Adder1prop
     })
 
-    pprint.pprintln(m.moduleData.commandAsTree())
+    mPPrint(m.moduleData.commandAsTree())
     val newAst =
       m.moduleData.transformTree { (ast: TreeNode[Ctrl | Cmds]) =>
         val predicate: Ctrl | Cmds => Boolean = {
@@ -44,7 +45,8 @@ class astTransformSuite extends AnyFunSuite {
         treeTraverse.filterTop(predicate, ast)
       }
 
-    pprint.pprintln(newAst)
+    mPPrint(newAst)
+    assert(newAst.children.length == 1, "filtered AST should have only 1 assertion")
   }
 
 }

From a615610545c50dd126fdb17b015a93e77e333080 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 20 Nov 2025 13:15:36 +0800
Subject: [PATCH 07/23] feat: Refactor imports to replace varDecls with
 circuitDecls and remove unused exprOperators

---
 src/main/scala/dependentChisel/api.scala                    | 2 +-
 .../dependentChisel/typesAndSyntax/chiselModules.scala      | 2 +-
 .../typesAndSyntax/{varDecls.scala => circuitDecls.scala}   | 6 +++---
 .../typesAndSyntax/{exprOperators.scala => exprOp.scala}    | 2 +-
 .../scala/dependentChisel/typesAndSyntax/typesAndOps.scala  | 2 +-
 src/test/scala/dependentChisel/examples/BubbleFifo.scala    | 2 +-
 src/test/scala/dependentChisel/examples/BubbleFifoErr.scala | 4 ++--
 src/test/scala/dependentChisel/examples/adder.scala         | 4 ++--
 src/test/scala/dependentChisel/examples/dynamicAdder.scala  | 2 +-
 src/test/scala/dependentChisel/examples/gcd.scala           | 2 +-
 10 files changed, 14 insertions(+), 14 deletions(-)
 rename src/main/scala/dependentChisel/typesAndSyntax/{varDecls.scala => circuitDecls.scala} (97%)
 rename src/main/scala/dependentChisel/typesAndSyntax/{exprOperators.scala => exprOp.scala} (98%)

diff --git a/src/main/scala/dependentChisel/api.scala b/src/main/scala/dependentChisel/api.scala
index d877b51..0aeb111 100644
--- a/src/main/scala/dependentChisel/api.scala
+++ b/src/main/scala/dependentChisel/api.scala
@@ -2,7 +2,7 @@ package dependentChisel
 
 object api {
   export dependentChisel.typesAndSyntax.chiselModules.*
-  export dependentChisel.typesAndSyntax.varDecls.*
+  export dependentChisel.typesAndSyntax.circuitDecls.*
   export dependentChisel.typesAndSyntax.typesAndOps.*
   export dependentChisel.typesAndSyntax.statements.*
   export dependentChisel.codegen.compiler.*
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
index 44c5e69..e094443 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
@@ -16,7 +16,7 @@ import dependentChisel.global.getUid
 import dependentChisel.syntax.naming
 
 import dependentChisel.typesAndSyntax.control
-import dependentChisel.typesAndSyntax.varDecls.UserModuleDecls
+import dependentChisel.typesAndSyntax.circuitDecls.UserModuleDecls
 import dependentChisel.global
 import scala.util.Try
 import scala.util.Failure
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala b/src/main/scala/dependentChisel/typesAndSyntax/circuitDecls.scala
similarity index 97%
rename from src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
rename to src/main/scala/dependentChisel/typesAndSyntax/circuitDecls.scala
index e30288b..f2c210b 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/circuitDecls.scala
@@ -18,10 +18,10 @@ import dependentChisel.codegen.compiler
 /* decls for variables like Wire, Reg, and IO
  type info is converted to value by constValueOpt
  */
-object varDecls {
+object circuitDecls {
 
-  /** use width in type param first,then try with width: Option[Int] in param. if both are
-    * not provided then auto infer the width
+  /** use width in type param first,then try with width: Option[Int] in param. if both are not
+    * provided then auto infer the width
     */
   inline def newLit[w <: Int](v: Int, width: Option[Int] = None) = {
     /* example : 199 is UInt<8>("hc7")
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/exprOperators.scala b/src/main/scala/dependentChisel/typesAndSyntax/exprOp.scala
similarity index 98%
rename from src/main/scala/dependentChisel/typesAndSyntax/exprOperators.scala
rename to src/main/scala/dependentChisel/typesAndSyntax/exprOp.scala
index 7ce683d..7630d55 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/exprOperators.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/exprOp.scala
@@ -6,7 +6,7 @@ import dependentChisel.typesAndSyntax.typesAndOps.UniOp
 import scala.compiletime.ops.int.*
 import scala.compiletime.*
 
-trait exprOperators {
+trait exprOp {
   // int ops
   extension [w <: Int](x: Expr[w]) {
     def +(oth: Expr[w]): BinOp[w] = BinOp(x, oth, "+")
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
index 7699448..af422fa 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
@@ -13,7 +13,7 @@ import dependentChisel.misc.macros
 /*
 https://github.com/MaximeKjaer/tf-dotty/blob/master/modules/compiletime/src/main/scala/io/kjaer/compiletime/Shape.scala
  */
-object typesAndOps extends exprOperators {
+object typesAndOps extends exprOp {
 
   /* Chisel provides three data types to describe connections, combinational logic, and
 registers: Bits, UInt, and SInt. UInt and SInt extend Bits, and all three types
diff --git a/src/test/scala/dependentChisel/examples/BubbleFifo.scala b/src/test/scala/dependentChisel/examples/BubbleFifo.scala
index cba9e11..07565d5 100644
--- a/src/test/scala/dependentChisel/examples/BubbleFifo.scala
+++ b/src/test/scala/dependentChisel/examples/BubbleFifo.scala
@@ -1,7 +1,7 @@
 package dependentChisel.examples
 
 import dependentChisel.typesAndSyntax.chiselModules.*
-import dependentChisel.typesAndSyntax.varDecls.*
+import dependentChisel.typesAndSyntax.circuitDecls.*
 import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.typesAndSyntax.statements.*
 import dependentChisel.codegen.compiler.*
diff --git a/src/test/scala/dependentChisel/examples/BubbleFifoErr.scala b/src/test/scala/dependentChisel/examples/BubbleFifoErr.scala
index 9783395..3009c49 100644
--- a/src/test/scala/dependentChisel/examples/BubbleFifoErr.scala
+++ b/src/test/scala/dependentChisel/examples/BubbleFifoErr.scala
@@ -1,10 +1,10 @@
 package dependentChisel.examples
 
 import dependentChisel.typesAndSyntax.chiselModules.*
-import dependentChisel.typesAndSyntax.varDecls.*
+import dependentChisel.typesAndSyntax.circuitDecls.*
 import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.typesAndSyntax.statements.*
-import dependentChisel.typesAndSyntax.varDecls.*
+import dependentChisel.typesAndSyntax.circuitDecls.*
 import dependentChisel.codegen.compiler.*
 import dependentChisel.firrtlUtils
 
diff --git a/src/test/scala/dependentChisel/examples/adder.scala b/src/test/scala/dependentChisel/examples/adder.scala
index a99d510..77727bb 100644
--- a/src/test/scala/dependentChisel/examples/adder.scala
+++ b/src/test/scala/dependentChisel/examples/adder.scala
@@ -10,10 +10,10 @@ import dependentChisel.*
 import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.typesAndSyntax.statements.*
 import dependentChisel.typesAndSyntax.chiselModules.*
-import dependentChisel.typesAndSyntax.varDecls.newIO
+import dependentChisel.typesAndSyntax.circuitDecls.newIO
 import dependentChisel.codegen.compiler.*
 
-import dependentChisel.typesAndSyntax.varDecls.newIODym
+import dependentChisel.typesAndSyntax.circuitDecls.newIODym
 import dependentChisel.codegen.sequentialCommands.BoolProp
 
 object adder extends mainRunnable {
diff --git a/src/test/scala/dependentChisel/examples/dynamicAdder.scala b/src/test/scala/dependentChisel/examples/dynamicAdder.scala
index 20c749f..a6e9cf0 100644
--- a/src/test/scala/dependentChisel/examples/dynamicAdder.scala
+++ b/src/test/scala/dependentChisel/examples/dynamicAdder.scala
@@ -8,7 +8,7 @@ import com.doofin.stdScala.mainRunnable
 import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.typesAndSyntax.statements.*
 import dependentChisel.typesAndSyntax.chiselModules.*
-import dependentChisel.typesAndSyntax.varDecls.*
+import dependentChisel.typesAndSyntax.circuitDecls.*
 import dependentChisel.codegen.compiler.*
 import dependentChisel.examples.adder
 
diff --git a/src/test/scala/dependentChisel/examples/gcd.scala b/src/test/scala/dependentChisel/examples/gcd.scala
index 8571657..7e7d917 100644
--- a/src/test/scala/dependentChisel/examples/gcd.scala
+++ b/src/test/scala/dependentChisel/examples/gcd.scala
@@ -12,7 +12,7 @@ import dependentChisel.typesAndSyntax.control.*
 import dependentChisel.typesAndSyntax.chiselModules.*
 
 import dependentChisel.typesAndSyntax.control
-import dependentChisel.typesAndSyntax.varDecls.*
+import dependentChisel.typesAndSyntax.circuitDecls.*
 import dependentChisel.codegen.compiler.*
 
 object gcd extends mainRunnable {

From a0e1575a3e1de843715eb579f49b391908c006f4 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 13 Dec 2025 11:27:47 +0800
Subject: [PATCH 08/23] feat: Refactor imports to use monadicSyntax and enhance
 code organization

---
 .../monadic/monadicCompilers.scala            |  2 +-
 .../{monadicAST.scala => monadicSyntax.scala} |  9 ++++-----
 .../dependentChisel/monadic/monadicTest.scala |  4 +++-
 .../dependentChisel/monadic/simpleAST.scala   |  2 +-
 .../staticAnalysis/MonotoneFramework.scala    | 19 +++++++++++--------
 5 files changed, 20 insertions(+), 16 deletions(-)
 rename src/main/scala/dependentChisel/monadic/{monadicAST.scala => monadicSyntax.scala} (95%)

diff --git a/src/main/scala/dependentChisel/monadic/monadicCompilers.scala b/src/main/scala/dependentChisel/monadic/monadicCompilers.scala
index 69df472..2ded338 100644
--- a/src/main/scala/dependentChisel/monadic/monadicCompilers.scala
+++ b/src/main/scala/dependentChisel/monadic/monadicCompilers.scala
@@ -4,7 +4,7 @@ package dependentChisel.monadic
 import cats.{Id, ~>}
 import cats.data.State
 
-import monadicAST.*
+import monadicSyntax.*
 import simpleAST.*
 import scala.collection.mutable
 import scala.collection.mutable.ArrayBuffer
diff --git a/src/main/scala/dependentChisel/monadic/monadicAST.scala b/src/main/scala/dependentChisel/monadic/monadicSyntax.scala
similarity index 95%
rename from src/main/scala/dependentChisel/monadic/monadicAST.scala
rename to src/main/scala/dependentChisel/monadic/monadicSyntax.scala
index ebc4d25..3c2cb76 100644
--- a/src/main/scala/dependentChisel/monadic/monadicAST.scala
+++ b/src/main/scala/dependentChisel/monadic/monadicSyntax.scala
@@ -1,4 +1,3 @@
-// package precondition.syntax
 package dependentChisel.monadic
 
 import scala.compiletime.*
@@ -11,7 +10,7 @@ import cats.free.Free
 import dependentChisel.syntax.naming.*
 import dependentChisel.syntax.naming
 
-object monadicAST {
+object monadicSyntax {
 
   sealed trait DslStoreA[A]
 
@@ -30,7 +29,8 @@ object monadicAST {
 
   case class NewVar(name: String = "") extends DslStoreA[Var] // DslStoreA[Var]
   // case class NewWire[t](name: String = "") extends DslStoreA[Var] // DslStoreA[Var]
-  case class NewWire[n <: Int]() extends DslStoreA[NewWire[n]] { // support both dynamic and static check
+  case class NewWire[n <: Int]()
+      extends DslStoreA[NewWire[n]] { // support both dynamic and static check
     inline def getVal = constValueOpt[n]
   }
 
@@ -69,8 +69,7 @@ object monadicAST {
   ): NewWire[n + m] = {
     NewWire[n + m]()
   }
-  case class IfElse(cond: BoolExpr, s1: DslStore[Unit], s2: DslStore[Unit])
-      extends DslStoreA[Unit]
+  case class IfElse(cond: BoolExpr, s1: DslStore[Unit], s2: DslStore[Unit]) extends DslStoreA[Unit]
   case class If(cond: BoolExpr, s1: DslStore[Unit]) extends DslStoreA[Unit]
   case class While(
       cond: DslStore[Boolean],
diff --git a/src/main/scala/dependentChisel/monadic/monadicTest.scala b/src/main/scala/dependentChisel/monadic/monadicTest.scala
index cf4f0be..6480028 100644
--- a/src/main/scala/dependentChisel/monadic/monadicTest.scala
+++ b/src/main/scala/dependentChisel/monadic/monadicTest.scala
@@ -5,11 +5,13 @@ package dependentChisel.monadic
 import cats.data.*
 import cats.implicits.*
 import cats.free.Free.*
+
 import com.doofin.stdScalaJvm.*
 import com.doofin.stdScala.mainRunnable
 
 import monadicCompilers.*
-import monadicAST.*
+import monadicSyntax.*
+
 object monadicTest extends mainRunnable {
 
   override def main(args: Array[String] = Array()): Unit = {
diff --git a/src/main/scala/dependentChisel/monadic/simpleAST.scala b/src/main/scala/dependentChisel/monadic/simpleAST.scala
index 4bf62be..8c60e07 100644
--- a/src/main/scala/dependentChisel/monadic/simpleAST.scala
+++ b/src/main/scala/dependentChisel/monadic/simpleAST.scala
@@ -1,6 +1,6 @@
 package dependentChisel.monadic
 
-import dependentChisel.monadic.monadicAST.BoolExpr
+import dependentChisel.monadic.monadicSyntax.BoolExpr
 
 object simpleAST {
   enum Stmt {
diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index f0c2709..d8a8ff1 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -1,21 +1,25 @@
 package dependentChisel.staticAnalysis
 
-/** lift domain to domainMap where both are lattices. domain ->> var->domain ->> prog
-  * point ->var->domain
+/** lift domain to domainMap where both are lattices. domain ->> var->domain ->> prog point
+  * ->var->domain
   */
 object MonotoneFramework {
   type VarName = String
   type domainMapT = [domain] =>> Map[VarName, domain]
 
-  /** usage : give initMap: domainMapT[domain] and baseLattice, then override
-    * transferF(transfer function) .
+  /** enrich the lattice to support monotone framework
     *
-    * Recommend : create two file named xxAnalysis impl this trait, and xxLattice impl
-    * just lattice
+    * tips : create two file named xxAnalysis to implement this trait, and xxLattice to implement
+    * the lattice separately.
     * @tparam domain
     *   domain lattice which satisify acc
     * @tparam stmtT
     *   type of statement
+    *
+    * @param initMap
+    *   initial mapping from var to domain value
+    * @param baseLattice
+    *   lattice for domain
     */
   trait MonoFrameworkT[domain, stmtT](
       val initMap: domainMapT[domain],
@@ -53,8 +57,7 @@ object MonotoneFramework {
               lattice.smallerThan(i1o, i2o)
             }
         }
-        override val lub
-            : (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
+        override val lub: (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
           (m1, m2) =>
             val newmap =
               (m1.keys ++ m2.keys).toSet map { k =>

From 4d922ecb41dfc62aa7393b41d8705f78314a2e8f Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 15 Jan 2026 18:32:15 +0800
Subject: [PATCH 09/23] feat: Enhance MonotoneFramework and related components
 with transfer function and initial mapping

---
 .../staticAnalysis/MonotoneFramework.scala    | 26 ++++++++++-------
 .../staticAnalysis/checkUnInitAnalysis.scala  | 29 ++++++++++---------
 .../staticAnalysis/checkUnInitLattice.scala   | 10 +++----
 .../staticAnalysis/test.worksheet.sc          |  2 +-
 .../staticAnalysis/worklistAlgo.scala         | 18 +++++++++---
 5 files changed, 51 insertions(+), 34 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index d8a8ff1..6fdd9f8 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -5,9 +5,10 @@ package dependentChisel.staticAnalysis
   */
 object MonotoneFramework {
   type VarName = String
+  // type level lambda from domain to Map[VarName, domain]
   type domainMapT = [domain] =>> Map[VarName, domain]
 
-  /** enrich the lattice to support monotone framework
+  /** enrich the lattice with transfer function and initial mapping
     *
     * tips : create two file named xxAnalysis to implement this trait, and xxLattice to implement
     * the lattice separately.
@@ -22,16 +23,13 @@ object MonotoneFramework {
     *   lattice for domain
     */
   trait MonoFrameworkT[domain, stmtT](
+      val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain],
+      val init: domain,
       val initMap: domainMapT[domain],
       baseLattice: semiLattice[domain]
   ) extends semiLattice[domainMapT[domain]] {
     // type domainMap = Map[String, domain] // var name to domain
 
-    /** src point,stmt,tgt point,prevMap=>newMap */
-    // val baseLattice: semiLattice[domain]
-    val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain]
-    val init: domain
-
     /** lift from semiLattice[domain] to semiLattice[domainMapT[domain]] */
     val liftedLattice = baseLattice.liftWithMap(initMap)
     override val bottom: domainMapT[domain] = liftedLattice.bottom
@@ -44,8 +42,12 @@ object MonotoneFramework {
       worklistAlgo.wlAlgoMonotone(this, progGraph)
   }
 
-  extension [domain](lattice: semiLattice[domain]) {
-    def liftWithMap(initMap: domainMapT[domain]) =
+  /** lift semiLattice[t] to semiLattice[Map[String,t]]
+    *
+    * that is, for t:SemiLattice, the function space String->t is also a SemiLattice
+    */
+  extension [domain](base: semiLattice[domain]) {
+    def liftWithMap(initMap: domainMapT[domain]): semiLattice[domainMapT[domain]] =
       new semiLattice[domainMapT[domain]] {
         override val smallerThan: (domainMapT[domain], domainMapT[domain]) => Boolean = {
           (m1, m2) =>
@@ -54,23 +56,25 @@ object MonotoneFramework {
               val i1o = k1._2
               val i2o = m2(k1._1)
 
-              lattice.smallerThan(i1o, i2o)
+              base.smallerThan(i1o, i2o)
             }
         }
+        /*  for lub, take union of keys, for each key do lub on values
+         */
         override val lub: (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
           (m1, m2) =>
             val newmap =
               (m1.keys ++ m2.keys).toSet map { k =>
                 val i1o = m1(k)
                 val i2o = m2(k)
-                val rr = lattice.lub(i1o, i2o)
+                val rr = base.lub(i1o, i2o)
                 (k, rr)
               }
             Map(newmap.toSeq*)
         }
 
         override val bottom: domainMapT[domain] =
-          initMap.map(s => (s._1, lattice.bottom))
+          initMap.map(s => (s._1, base.bottom))
       }
   }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
index fba74cd..457a1fa 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
@@ -15,26 +15,29 @@ object checkUnInitAnalysis {
   type mDomain = checkUnInitLattice.domain
   type mStmt = AtomicCmds // assign,var decls etc
 
+  val transferF: ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = {
+    case ((q0, cmd, q1), varmap) =>
+      cmd match {
+        case WeakStmt(lhs, op, rhs, prefix) =>
+          if op == ":=" then varmap.updated(lhs.getname, true) else varmap
+        // case NewInstStmt(instNm, modNm)    =>
+        // case VarDecls(v)                   =>
+        case _ => varmap
+      }
+  }
+
+  val init: mDomain = false
+
   case class MonoFramework(
       mInitMap: domainMapT[mDomain]
   ) extends MonoFrameworkT[mDomain, mStmt](
+        transferF,
+        init,
         mInitMap,
         checkUnInitLattice.lattice
       ) {
 
     // override val baseLattice: semiLattice[mDomain] = uninitializedLattice.lattice //bug! will cause null
-    override val transferF
-        : ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = {
-      case ((q0, cmd, q1), varmap) =>
-        cmd match {
-          case WeakStmt(lhs, op, rhs, prefix) =>
-            if op == ":=" then varmap.updated(lhs.getname, true) else varmap
-          // case NewInstStmt(instNm, modNm)    =>
-          // case VarDecls(v)                   =>
-          case _ => varmap
-        }
-    }
-
-    override val init: mDomain = false
+
   }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala
index fba757d..63900e3 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala
@@ -1,23 +1,23 @@
 package dependentChisel.staticAnalysis
 
-/** reaching definitions as a mapping Program point-> Var -> bool. only need to define
-  * last part bool saying whether var have an value
+/** reaching definitions as a mapping Program point-> Var -> bool. only need to define last part
+  * bool saying whether var have an value
   */
 object checkUnInitLattice {
   type domain = Boolean // PowerSet( Q? * Q )
   object lattice extends semiLattice[domain] {
 
-    override val smallerThan: (domain, domain) => Boolean = {
+    override val smallerThan = {
       case (_, true)      => true
       case (false, false) => true
       case _              => false
     }
 
-    override val lub: (domain, domain) => domain = {
+    override val lub = {
       _ || _
     }
 
-    override val bottom: domain = false
+    override val bottom = false
 
   }
 
diff --git a/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc b/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
index b2d4911..3791d1c 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
+++ b/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
@@ -19,7 +19,7 @@ val initMap: Map[String, Boolean] =
       .toList*
   )
 
-/*
+/* a program graph
 0 -> x:=.. ->1 -> 3 -> 5
 0 ->   2   -> 4
  */
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index 7a418aa..08c7a28 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -26,6 +26,15 @@ object worklistAlgo {
     override def isEmpty: Boolean = as.isEmpty
   }
 
+  /** worklist algorithm for monotone framework
+    * @param mf
+    *   monotone framework
+    * @param progGraph
+    *   program graph as list of (src point,stmt,tgt point)
+    *
+    * @return
+    *   mapping from program point to domainMap at that point
+    */
   def wlAlgoMonotone[domainT, stmtT](
       mf: MonoFrameworkT[domainT, stmtT],
       progGraph: List[(Int, stmtT, Int)]
@@ -41,6 +50,8 @@ object worklistAlgo {
     )
   }
 
+  /** worklist algorithm implementation for program graph
+    */
   private def wlAlgoProgGraphP[domainT, stmtT](
       progGraph: List[(Int, stmtT, Int)],
       transferF: ((Int, stmtT, Int), domainT) => domainT,
@@ -54,10 +65,9 @@ object worklistAlgo {
     val mutList: Worklist[Int] = new WlStack()
 
     pp(progGraph)
-//    get program points from edges,ignore stmt in (Int, Stmt, Int)
+    //    get program points
     val progPoints = progGraph.flatMap(x => List(x._1, x._3)).distinct
 
-//    initialise work list
     mutList.insertAll(progPoints)
 
     val resMapMut: mutable.Map[Int, domainT] = mutable.Map()
@@ -67,8 +77,8 @@ object worklistAlgo {
       resMapMut(q) = if (q == 0) initD else bottomD
     }
 
-//    pp(resMapMut.toMap, "init resMap : ")
-    // second loop,keep applying transferF to program graph until the node value is stable
+    // keep applying transferF to program graph until the node value is stable
+    // according to the ascending order property, this will terminate
     var steps = 0
     while (!mutList.isEmpty) {
       steps += 1

From 533bdf1d30569b559dd8d6d90fa59c2c2af8e319 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Thu, 15 Jan 2026 22:53:55 +0800
Subject: [PATCH 10/23] feat: Refactor domainMapT type definition and update
 checkUnInitAnalysis for clarity

---
 .../staticAnalysis/MonotoneFramework.scala     | 18 ++++++++++++------
 .../staticAnalysis/checkUnInitAnalysis.scala   | 11 ++++++-----
 2 files changed, 18 insertions(+), 11 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 6fdd9f8..5286c1d 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -6,7 +6,7 @@ package dependentChisel.staticAnalysis
 object MonotoneFramework {
   type VarName = String
   // type level lambda from domain to Map[VarName, domain]
-  type domainMapT = [domain] =>> Map[VarName, domain]
+  type domainMapT[domain] = Map[VarName, domain]
 
   /** enrich the lattice with transfer function and initial mapping
     *
@@ -24,13 +24,12 @@ object MonotoneFramework {
     */
   trait MonoFrameworkT[domain, stmtT](
       val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain],
-      val init: domain,
       val initMap: domainMapT[domain],
       baseLattice: semiLattice[domain]
   ) extends semiLattice[domainMapT[domain]] {
     // type domainMap = Map[String, domain] // var name to domain
 
-    /** lift from semiLattice[domain] to semiLattice[domainMapT[domain]] */
+    // lift domain to domainMap[domain] lattice
     val liftedLattice = baseLattice.liftWithMap(initMap)
     override val bottom: domainMapT[domain] = liftedLattice.bottom
     override val lub = liftedLattice.lub
@@ -42,12 +41,19 @@ object MonotoneFramework {
       worklistAlgo.wlAlgoMonotone(this, progGraph)
   }
 
-  /** lift semiLattice[t] to semiLattice[Map[String,t]]
+  /** lift any t to string->t semiLattice
     *
     * that is, for t:SemiLattice, the function space String->t is also a SemiLattice
     */
   extension [domain](base: semiLattice[domain]) {
-    def liftWithMap(initMap: domainMapT[domain]): semiLattice[domainMapT[domain]] =
+
+    /** lift the t:lattice to string->t lattice (function space)
+      *
+      * @param botMap
+      *   the bottom element mapping, since we need to know var names
+      * @return
+      */
+    def liftWithMap(botMap: domainMapT[domain]): semiLattice[domainMapT[domain]] =
       new semiLattice[domainMapT[domain]] {
         override val smallerThan: (domainMapT[domain], domainMapT[domain]) => Boolean = {
           (m1, m2) =>
@@ -74,7 +80,7 @@ object MonotoneFramework {
         }
 
         override val bottom: domainMapT[domain] =
-          initMap.map(s => (s._1, base.bottom))
+          botMap.map(s => (s._1, base.bottom))
       }
   }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
index 457a1fa..ae10295 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
@@ -12,13 +12,17 @@ import dependentChisel.codegen.sequentialCommands.VarDecls
 /** check if vars have an value
   */
 object checkUnInitAnalysis {
-  type mDomain = checkUnInitLattice.domain
-  type mStmt = AtomicCmds // assign,var decls etc
+  type mDomain = checkUnInitLattice.domain // which is Boolean
+  type mStmt = AtomicCmds // statements
 
+  // val init: mDomain = false
+
+  // for each stmt, how it mutate the map var->domain
   val transferF: ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = {
     case ((q0, cmd, q1), varmap) =>
       cmd match {
         case WeakStmt(lhs, op, rhs, prefix) =>
+          // any assignment makes var initialized
           if op == ":=" then varmap.updated(lhs.getname, true) else varmap
         // case NewInstStmt(instNm, modNm)    =>
         // case VarDecls(v)                   =>
@@ -26,13 +30,10 @@ object checkUnInitAnalysis {
       }
   }
 
-  val init: mDomain = false
-
   case class MonoFramework(
       mInitMap: domainMapT[mDomain]
   ) extends MonoFrameworkT[mDomain, mStmt](
         transferF,
-        init,
         mInitMap,
         checkUnInitLattice.lattice
       ) {

From 430f6ea1e5ce472364f48fca2a29d983528f975f Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Mon, 19 Jan 2026 18:25:07 +0800
Subject: [PATCH 11/23] feat: Rename initMap to botMap in MonoFramework and
 update related references

---
 .../dependentChisel/staticAnalysis/MonotoneFramework.scala    | 4 ++--
 .../dependentChisel/staticAnalysis/checkUnInitAnalysis.scala  | 4 ++--
 .../scala/dependentChisel/staticAnalysis/worklistAlgo.scala   | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 5286c1d..66edf43 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -24,13 +24,13 @@ object MonotoneFramework {
     */
   trait MonoFrameworkT[domain, stmtT](
       val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain],
-      val initMap: domainMapT[domain],
+      val botMap: domainMapT[domain],
       baseLattice: semiLattice[domain]
   ) extends semiLattice[domainMapT[domain]] {
     // type domainMap = Map[String, domain] // var name to domain
 
     // lift domain to domainMap[domain] lattice
-    val liftedLattice = baseLattice.liftWithMap(initMap)
+    val liftedLattice = baseLattice.liftWithMap(botMap)
     override val bottom: domainMapT[domain] = liftedLattice.bottom
     override val lub = liftedLattice.lub
     override val smallerThan = liftedLattice.smallerThan
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
index ae10295..8bf2aa6 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
@@ -31,10 +31,10 @@ object checkUnInitAnalysis {
   }
 
   case class MonoFramework(
-      mInitMap: domainMapT[mDomain]
+      mBotMap: domainMapT[mDomain]
   ) extends MonoFrameworkT[mDomain, mStmt](
         transferF,
-        mInitMap,
+        mBotMap,
         checkUnInitLattice.lattice
       ) {
 
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index 08c7a28..f4449e0 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -45,7 +45,7 @@ object worklistAlgo {
       mf.transferF,
       mf.smallerThan,
       mf.lub,
-      mf.initMap,
+      mf.botMap,
       mf.bottom
     )
   }

From c1fea95aac53fe982d2575da8bab9dac85888788 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Mon, 19 Jan 2026 18:31:15 +0800
Subject: [PATCH 12/23] feat: Refactor checkUnInitAnalysis and remove
 checkUnInitLattice, integrating its functionality directly

---
 .../staticAnalysis/checkUnInitAnalysis.scala  | 21 +++++++++++++---
 .../staticAnalysis/checkUnInitLattice.scala   | 24 -------------------
 .../staticAnalysis/semiLattice.scala          | 13 +++++-----
 3 files changed, 25 insertions(+), 33 deletions(-)
 delete mode 100644 src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala

diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
index 8bf2aa6..4b306a2 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
@@ -2,7 +2,6 @@ package dependentChisel.staticAnalysis
 
 import dependentChisel.codegen.sequentialCommands.AtomicCmds
 import dependentChisel.staticAnalysis.MonotoneFramework.domainMapT
-import dependentChisel.staticAnalysis.checkUnInitLattice
 
 import dependentChisel.staticAnalysis.MonotoneFramework.MonoFrameworkT
 import dependentChisel.codegen.sequentialCommands.NewInstance
@@ -12,7 +11,7 @@ import dependentChisel.codegen.sequentialCommands.VarDecls
 /** check if vars have an value
   */
 object checkUnInitAnalysis {
-  type mDomain = checkUnInitLattice.domain // which is Boolean
+  type mDomain = checkUnInitLattice.mDomain // which is Boolean
   type mStmt = AtomicCmds // statements
 
   // val init: mDomain = false
@@ -35,10 +34,26 @@ object checkUnInitAnalysis {
   ) extends MonoFrameworkT[mDomain, mStmt](
         transferF,
         mBotMap,
-        checkUnInitLattice.lattice
+        checkUnInitLattice
       ) {
 
     // override val baseLattice: semiLattice[mDomain] = uninitializedLattice.lattice //bug! will cause null
 
   }
+
+  object checkUnInitLattice extends semiLattice[Boolean] {
+
+    override val smallerThan = {
+      case (_, true)      => true
+      case (false, false) => true
+      case _              => false
+    }
+
+    override val lub = {
+      _ || _
+    }
+
+    override val bottom = false
+
+  }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala
deleted file mode 100644
index 63900e3..0000000
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitLattice.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-package dependentChisel.staticAnalysis
-
-/** reaching definitions as a mapping Program point-> Var -> bool. only need to define last part
-  * bool saying whether var have an value
-  */
-object checkUnInitLattice {
-  type domain = Boolean // PowerSet( Q? * Q )
-  object lattice extends semiLattice[domain] {
-
-    override val smallerThan = {
-      case (_, true)      => true
-      case (false, false) => true
-      case _              => false
-    }
-
-    override val lub = {
-      _ || _
-    }
-
-    override val bottom = false
-
-  }
-
-}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
index 11cea47..7e9fede 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
@@ -1,19 +1,20 @@
 package dependentChisel.staticAnalysis
 
-/** a complete lattice is a partially ordered set in which all subsets have both
-  * a supremum (join) and an infimum (meet).
+/** a complete lattice is a partially ordered set in which all subsets have both a supremum (join)
+  * and an infimum (meet).
   *
   * A complete lattice always hasa least and greatest element
   *
-  * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered
-  * set such that all finite subsets Y of L have a least upper bound.
+  * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered set such that all
+  * finite subsets Y of L have a least upper bound.
   *
-  * The set Q of all rational numbers, with the usual linear order, is an
-  * infinite distributive lattice which is not complete.
+  * The set Q of all rational numbers, with the usual linear order, is an infinite distributive
+  * lattice which is not complete.
   * @tparam domain
   *   satisify acc
   */
 trait semiLattice[domain] {
+  type mDomain = domain
   val smallerThan: (domain, domain) => Boolean // partial ordering
   val lub: (domain, domain) => domain // least upper bound
   val bottom: domain

From 92442faa62f110f1228671253985a839e227068f Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Tue, 20 Jan 2026 16:56:22 +0800
Subject: [PATCH 13/23] feat: Implement unInitAnalysis and associated test
 suite for variable initialization tracking

---
 .../staticAnalysis/test.worksheet.sc          | 36 --------------
 ...nitAnalysis.scala => unInitAnalysis.scala} | 47 ++++++++++++-------
 .../dependentChisel/unInitAnalysisSuite.scala | 45 ++++++++++++++++++
 3 files changed, 74 insertions(+), 54 deletions(-)
 delete mode 100644 src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
 rename src/main/scala/dependentChisel/staticAnalysis/{checkUnInitAnalysis.scala => unInitAnalysis.scala} (54%)
 create mode 100644 src/test/scala/dependentChisel/unInitAnalysisSuite.scala

diff --git a/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc b/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
deleted file mode 100644
index 3791d1c..0000000
--- a/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
+++ /dev/null
@@ -1,36 +0,0 @@
-import dependentChisel.typesAndSyntax.typesAndOps.Lit
-import dependentChisel.typesAndSyntax.typesAndOps.VarLit
-import dependentChisel.codegen.sequentialCommands.*
-import dependentChisel.staticAnalysis.checkUnInitAnalysis
-
-import com.doofin.stdScalaCross.*
-
-val varlist = "xyz"
-/* use  Some(bool) : none for all vars, some false for declared ,some true for declared and have values
-make sure no some true after some false
-
-can always make it pass for some test cases , but not formal guarantee ?
- */
-// initialize a default value for each var
-val initMap: Map[String, Boolean] =
-  Map(
-    varlist.toCharArray
-      .map(x => x.toString() -> false)
-      .toList*
-  )
-
-/* a program graph
-0 -> x:=.. ->1 -> 3 -> 5
-0 ->   2   -> 4
- */
-val pg =
-  List(
-    (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
-    (1, Skip, 3),
-    (0, Skip, 2),
-    (2, Skip, 4),
-    (3, Skip, 5)
-  )
-val mf = checkUnInitAnalysis.MonoFramework(initMap)
-
-pp(mf.runWithProgGraph(pg))
diff --git a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
similarity index 54%
rename from src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
rename to src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index 4b306a2..5fe9019 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -7,40 +7,43 @@ import dependentChisel.staticAnalysis.MonotoneFramework.MonoFrameworkT
 import dependentChisel.codegen.sequentialCommands.NewInstance
 import dependentChisel.codegen.sequentialCommands.WeakStmt
 import dependentChisel.codegen.sequentialCommands.VarDecls
+import dependentChisel.typesAndSyntax.typesAndOps.VarLit
+import dependentChisel.typesAndSyntax.typesAndOps.BinOp
+import dependentChisel.typesAndSyntax.typesAndOps.MulOp
+import dependentChisel.typesAndSyntax.typesAndOps.AddOp
+import dependentChisel.typesAndSyntax.typesAndOps.UniOp
+import dependentChisel.typesAndSyntax.typesAndOps.VarDynamic
+import dependentChisel.typesAndSyntax.typesAndOps.VarTyped
+import dependentChisel.typesAndSyntax.typesAndOps.Lit
+import dependentChisel.typesAndSyntax.typesAndOps.LitDym
 
 /** check if vars have an value
   */
-object checkUnInitAnalysis {
+object unInitAnalysis {
   type mDomain = checkUnInitLattice.mDomain // which is Boolean
   type mStmt = AtomicCmds // statements
 
-  // val init: mDomain = false
-
-  // for each stmt, how it mutate the map var->domain
   val transferF: ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = {
     case ((q0, cmd, q1), varmap) =>
       cmd match {
         case WeakStmt(lhs, op, rhs, prefix) =>
+          rhs match
+            case VarLit(name) => 
+            case BinOp(a, b, nm) =>
+            case MulOp(a, b, nm) =>
+            case AddOp(a, b, nm) =>
+            case UniOp(a, nm) =>
+            case VarDynamic(width, tp, name) =>
+            case VarTyped(name, tp) =>
+            case Lit(i) =>
+            case LitDym(i, width) =>
+          
           // any assignment makes var initialized
           if op == ":=" then varmap.updated(lhs.getname, true) else varmap
-        // case NewInstStmt(instNm, modNm)    =>
-        // case VarDecls(v)                   =>
         case _ => varmap
       }
   }
 
-  case class MonoFramework(
-      mBotMap: domainMapT[mDomain]
-  ) extends MonoFrameworkT[mDomain, mStmt](
-        transferF,
-        mBotMap,
-        checkUnInitLattice
-      ) {
-
-    // override val baseLattice: semiLattice[mDomain] = uninitializedLattice.lattice //bug! will cause null
-
-  }
-
   object checkUnInitLattice extends semiLattice[Boolean] {
 
     override val smallerThan = {
@@ -56,4 +59,12 @@ object checkUnInitAnalysis {
     override val bottom = false
 
   }
+
+  def mMonoFramework(
+      mBotMap: domainMapT[mDomain]
+  ) = new MonoFrameworkT[mDomain, mStmt](
+    transferF,
+    mBotMap,
+    checkUnInitLattice
+  ) {}
 }
diff --git a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
new file mode 100644
index 0000000..59159fb
--- /dev/null
+++ b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
@@ -0,0 +1,45 @@
+package dependentChisel
+
+import dependentChisel.typesAndSyntax.typesAndOps.Lit
+import dependentChisel.typesAndSyntax.typesAndOps.VarLit
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.staticAnalysis.unInitAnalysis
+
+import com.doofin.stdScalaCross.*
+
+class unInitAnalysisSuite extends munit.FunSuite {
+  test("unInitAnalysis test") {
+
+    // each var is uninitialized at the beginning
+    val initMap: Map[String, Boolean] =
+      Map(
+        "xyz".toCharArray
+          .map(x => x.toString() -> false)
+          .toList*
+      )
+
+    /* a program graph
+0 -> x:=.. ->1 -> 3 -> 5
+0 ->   2   -> 4
+     */
+    val pg =
+      List(
+        (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
+        (1, Skip, 3), // x is initialized from 0->1->3
+        (0, Skip, 2), // x is not initialized from 0->2
+        (2, Skip, 4), // x is not initialized from 0->2->4
+        (3, Skip, 5) // x is initialized from 0->1->3->5
+      )
+    val monoF = unInitAnalysis.mMonoFramework(initMap)
+
+    val res = monoF.runWithProgGraph(pg)
+    val expectedInit = Set(1, 3, 5)
+    val resultInit = res.filter { case (k, v) =>
+      v("x") // filter where x is true
+    }.keySet
+
+    pp(res)
+    assertEquals(resultInit, expectedInit, "so x is only initialized at point 1,3,5")
+
+  }
+}

From 20ac2386b72bba59b2bd20c0788015513e26fa50 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 31 Jan 2026 11:53:55 +0800
Subject: [PATCH 14/23] feat: Refactor domainMapT to VarMap for consistency
 across MonotoneFramework and related components

---
 .../staticAnalysis/MonotoneFramework.scala    | 61 +++++++++----------
 .../staticAnalysis/semiLattice.scala          | 14 ++---
 .../staticAnalysis/unInitAnalysis.scala       |  8 +--
 .../staticAnalysis/worklistAlgo.scala         |  4 +-
 4 files changed, 41 insertions(+), 46 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 66edf43..e88fa3c 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -6,7 +6,7 @@ package dependentChisel.staticAnalysis
 object MonotoneFramework {
   type VarName = String
   // type level lambda from domain to Map[VarName, domain]
-  type domainMapT[domain] = Map[VarName, domain]
+  type VarMap[domain] = Map[VarName, domain]
 
   /** enrich the lattice with transfer function and initial mapping
     *
@@ -22,22 +22,19 @@ object MonotoneFramework {
     * @param baseLattice
     *   lattice for domain
     */
-  trait MonoFrameworkT[domain, stmtT](
-      val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain],
-      val botMap: domainMapT[domain],
-      baseLattice: semiLattice[domain]
-  ) extends semiLattice[domainMapT[domain]] {
-    // type domainMap = Map[String, domain] // var name to domain
-
-    // lift domain to domainMap[domain] lattice
+  trait MonoFrameworkT[T, stmtT](
+      val transferF: ((Int, stmtT, Int), VarMap[T]) => VarMap[T],
+      val botMap: VarMap[T],
+      baseLattice: semiLattice[T]
+  ) extends semiLattice[VarMap[T]] {
     val liftedLattice = baseLattice.liftWithMap(botMap)
-    override val bottom: domainMapT[domain] = liftedLattice.bottom
+    override val bottom: VarMap[T] = liftedLattice.bottom
     override val lub = liftedLattice.lub
-    override val smallerThan = liftedLattice.smallerThan
+    override val leq = liftedLattice.leq
 
     def runWithProgGraph(
         progGraph: List[(Int, stmtT, Int)]
-    ): Map[Int, domainMapT[domain]] =
+    ): Map[Int, VarMap[T]] =
       worklistAlgo.wlAlgoMonotone(this, progGraph)
   }
 
@@ -53,33 +50,31 @@ object MonotoneFramework {
       *   the bottom element mapping, since we need to know var names
       * @return
       */
-    def liftWithMap(botMap: domainMapT[domain]): semiLattice[domainMapT[domain]] =
-      new semiLattice[domainMapT[domain]] {
-        override val smallerThan: (domainMapT[domain], domainMapT[domain]) => Boolean = {
-          (m1, m2) =>
-            m1 forall { k1 =>
-              // im1 is subset of im2
-              val i1o = k1._2
-              val i2o = m2(k1._1)
+    def liftWithMap(botMap: VarMap[domain]): semiLattice[VarMap[domain]] =
+      new semiLattice[VarMap[domain]] {
+        override val leq: (VarMap[domain], VarMap[domain]) => Boolean = { (m1, m2) =>
+          m1 forall { k1 =>
+            // im1 is subset of im2
+            val i1o = k1._2
+            val i2o = m2(k1._1)
 
-              base.smallerThan(i1o, i2o)
-            }
+            base.leq(i1o, i2o)
+          }
         }
         /*  for lub, take union of keys, for each key do lub on values
          */
-        override val lub: (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
-          (m1, m2) =>
-            val newmap =
-              (m1.keys ++ m2.keys).toSet map { k =>
-                val i1o = m1(k)
-                val i2o = m2(k)
-                val rr = base.lub(i1o, i2o)
-                (k, rr)
-              }
-            Map(newmap.toSeq*)
+        override val lub: (VarMap[domain], VarMap[domain]) => VarMap[domain] = { (m1, m2) =>
+          val newmap =
+            (m1.keys ++ m2.keys).toSet map { k =>
+              val i1o = m1(k)
+              val i2o = m2(k)
+              val rr = base.lub(i1o, i2o)
+              (k, rr)
+            }
+          Map(newmap.toSeq*)
         }
 
-        override val bottom: domainMapT[domain] =
+        override val bottom: VarMap[domain] =
           botMap.map(s => (s._1, base.bottom))
       }
   }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
index 7e9fede..7eb1bf4 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
@@ -10,12 +10,12 @@ package dependentChisel.staticAnalysis
   *
   * The set Q of all rational numbers, with the usual linear order, is an infinite distributive
   * lattice which is not complete.
-  * @tparam domain
-  *   satisify acc
+  * @tparam t
+  *   acc(ascending chain condition)
   */
-trait semiLattice[domain] {
-  type mDomain = domain
-  val smallerThan: (domain, domain) => Boolean // partial ordering
-  val lub: (domain, domain) => domain // least upper bound
-  val bottom: domain
+trait semiLattice[t] {
+  type mDomain = t
+  val leq: (t, t) => Boolean // partial ordering
+  val lub: (t, t) => t // least upper bound
+  val bottom: t
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index 5fe9019..6d76cba 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -1,7 +1,7 @@
 package dependentChisel.staticAnalysis
 
 import dependentChisel.codegen.sequentialCommands.AtomicCmds
-import dependentChisel.staticAnalysis.MonotoneFramework.domainMapT
+import dependentChisel.staticAnalysis.MonotoneFramework.VarMap
 
 import dependentChisel.staticAnalysis.MonotoneFramework.MonoFrameworkT
 import dependentChisel.codegen.sequentialCommands.NewInstance
@@ -23,7 +23,7 @@ object unInitAnalysis {
   type mDomain = checkUnInitLattice.mDomain // which is Boolean
   type mStmt = AtomicCmds // statements
 
-  val transferF: ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = {
+  val transferF: ((Int, mStmt, Int), VarMap[mDomain]) => VarMap[mDomain] = {
     case ((q0, cmd, q1), varmap) =>
       cmd match {
         case WeakStmt(lhs, op, rhs, prefix) =>
@@ -46,7 +46,7 @@ object unInitAnalysis {
 
   object checkUnInitLattice extends semiLattice[Boolean] {
 
-    override val smallerThan = {
+    override val leq = {
       case (_, true)      => true
       case (false, false) => true
       case _              => false
@@ -61,7 +61,7 @@ object unInitAnalysis {
   }
 
   def mMonoFramework(
-      mBotMap: domainMapT[mDomain]
+      mBotMap: VarMap[mDomain]
   ) = new MonoFrameworkT[mDomain, mStmt](
     transferF,
     mBotMap,
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index f4449e0..ea75e97 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -40,10 +40,10 @@ object worklistAlgo {
       progGraph: List[(Int, stmtT, Int)]
   ) = {
 
-    wlAlgoProgGraphP[domainMapT[domainT], stmtT](
+    wlAlgoProgGraphP[VarMap[domainT], stmtT](
       progGraph,
       mf.transferF,
-      mf.smallerThan,
+      mf.leq,
       mf.lub,
       mf.botMap,
       mf.bottom

From 47315ef01f407f74402c9425746017f5fd392c05 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 31 Jan 2026 12:05:58 +0800
Subject: [PATCH 15/23] feat: Refactor MonoFrameworkT to use baseLattice
 directly and update related usages

---
 .scalafmt.conf                                |  2 +-
 .../staticAnalysis/MonotoneFramework.scala    | 22 +++++++-----
 .../staticAnalysis/unInitAnalysis.scala       | 34 +++++++++++--------
 .../staticAnalysis/worklistAlgo.scala         |  4 +--
 4 files changed, 35 insertions(+), 27 deletions(-)

diff --git a/.scalafmt.conf b/.scalafmt.conf
index c129416..ee12572 100644
--- a/.scalafmt.conf
+++ b/.scalafmt.conf
@@ -1,5 +1,5 @@
 version = "3.10.1"
 runner.dialect = scala3
 maxColumn = 100 # For my wide 30" display.
-runner.dialectOverride.allowSignificantIndentation = false
+# runner.dialectOverride.allowSignificantIndentation = false
 runner.dialectOverride.allowQuietSyntax = true
diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index e88fa3c..2786763 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -22,19 +22,23 @@ object MonotoneFramework {
     * @param baseLattice
     *   lattice for domain
     */
-  trait MonoFrameworkT[T, stmtT](
-      val transferF: ((Int, stmtT, Int), VarMap[T]) => VarMap[T],
-      val botMap: VarMap[T],
+  case class MonoFrameworkT[T, stmtT](
+      val transferF: ((Int, stmtT, Int), T) => T,
+      // val botMap: VarMap[T],
       baseLattice: semiLattice[T]
-  ) extends semiLattice[VarMap[T]] {
-    val liftedLattice = baseLattice.liftWithMap(botMap)
-    override val bottom: VarMap[T] = liftedLattice.bottom
-    override val lub = liftedLattice.lub
-    override val leq = liftedLattice.leq
+  ) extends semiLattice[T] {
+    // val liftedLattice = baseLattice.liftWithMap(botMap)
+    // override val bottom: VarMap[T] = liftedLattice.bottom
+    // override val lub = liftedLattice.lub
+    // override val leq = liftedLattice.leq
+
+    override val bottom: T = baseLattice.bottom
+    override val lub = baseLattice.lub
+    override val leq = baseLattice.leq
 
     def runWithProgGraph(
         progGraph: List[(Int, stmtT, Int)]
-    ): Map[Int, VarMap[T]] =
+    ) =
       worklistAlgo.wlAlgoMonotone(this, progGraph)
   }
 
diff --git a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index 6d76cba..a837158 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -3,7 +3,7 @@ package dependentChisel.staticAnalysis
 import dependentChisel.codegen.sequentialCommands.AtomicCmds
 import dependentChisel.staticAnalysis.MonotoneFramework.VarMap
 
-import dependentChisel.staticAnalysis.MonotoneFramework.MonoFrameworkT
+import dependentChisel.staticAnalysis.MonotoneFramework.*
 import dependentChisel.codegen.sequentialCommands.NewInstance
 import dependentChisel.codegen.sequentialCommands.WeakStmt
 import dependentChisel.codegen.sequentialCommands.VarDecls
@@ -28,16 +28,16 @@ object unInitAnalysis {
       cmd match {
         case WeakStmt(lhs, op, rhs, prefix) =>
           rhs match
-            case VarLit(name) => 
-            case BinOp(a, b, nm) =>
-            case MulOp(a, b, nm) =>
-            case AddOp(a, b, nm) =>
-            case UniOp(a, nm) =>
+            case VarLit(name)                =>
+            case BinOp(a, b, nm)             =>
+            case MulOp(a, b, nm)             =>
+            case AddOp(a, b, nm)             =>
+            case UniOp(a, nm)                =>
             case VarDynamic(width, tp, name) =>
-            case VarTyped(name, tp) =>
-            case Lit(i) =>
-            case LitDym(i, width) =>
-          
+            case VarTyped(name, tp)          =>
+            case Lit(i)                      =>
+            case LitDym(i, width)            =>
+
           // any assignment makes var initialized
           if op == ":=" then varmap.updated(lhs.getname, true) else varmap
         case _ => varmap
@@ -62,9 +62,13 @@ object unInitAnalysis {
 
   def mMonoFramework(
       mBotMap: VarMap[mDomain]
-  ) = new MonoFrameworkT[mDomain, mStmt](
-    transferF,
-    mBotMap,
-    checkUnInitLattice
-  ) {}
+  ) = {
+    val lifted =
+      checkUnInitLattice.liftWithMap(mBotMap)
+
+    MonoFrameworkT(
+      transferF = transferF,
+      baseLattice = lifted
+    )
+  }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index ea75e97..9b24743 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -40,12 +40,12 @@ object worklistAlgo {
       progGraph: List[(Int, stmtT, Int)]
   ) = {
 
-    wlAlgoProgGraphP[VarMap[domainT], stmtT](
+    wlAlgoProgGraphP[domainT, stmtT](
       progGraph,
       mf.transferF,
       mf.leq,
       mf.lub,
-      mf.botMap,
+      mf.bottom,
       mf.bottom
     )
   }

From 9dd87a2f49b8b98b7dc2b431b7fd228b5fa0bcc1 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 31 Jan 2026 12:18:44 +0800
Subject: [PATCH 16/23] refactor: Remove unused type alias and streamline
 unInitAnalysis imports

---
 .../staticAnalysis/semiLattice.scala          |  1 -
 .../staticAnalysis/unInitAnalysis.scala       | 69 ++++++++-----------
 2 files changed, 30 insertions(+), 40 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
index 7eb1bf4..9f0de52 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
@@ -14,7 +14,6 @@ package dependentChisel.staticAnalysis
   *   acc(ascending chain condition)
   */
 trait semiLattice[t] {
-  type mDomain = t
   val leq: (t, t) => Boolean // partial ordering
   val lub: (t, t) => t // least upper bound
   val bottom: t
diff --git a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index a837158..93c5f6b 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -1,50 +1,40 @@
 package dependentChisel.staticAnalysis
 
-import dependentChisel.codegen.sequentialCommands.AtomicCmds
-import dependentChisel.staticAnalysis.MonotoneFramework.VarMap
-
 import dependentChisel.staticAnalysis.MonotoneFramework.*
-import dependentChisel.codegen.sequentialCommands.NewInstance
-import dependentChisel.codegen.sequentialCommands.WeakStmt
-import dependentChisel.codegen.sequentialCommands.VarDecls
-import dependentChisel.typesAndSyntax.typesAndOps.VarLit
-import dependentChisel.typesAndSyntax.typesAndOps.BinOp
-import dependentChisel.typesAndSyntax.typesAndOps.MulOp
-import dependentChisel.typesAndSyntax.typesAndOps.AddOp
-import dependentChisel.typesAndSyntax.typesAndOps.UniOp
-import dependentChisel.typesAndSyntax.typesAndOps.VarDynamic
-import dependentChisel.typesAndSyntax.typesAndOps.VarTyped
-import dependentChisel.typesAndSyntax.typesAndOps.Lit
-import dependentChisel.typesAndSyntax.typesAndOps.LitDym
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
 
 /** check if vars have an value
   */
 object unInitAnalysis {
-  type mDomain = checkUnInitLattice.mDomain // which is Boolean
-  type mStmt = AtomicCmds // statements
+  type Domain = VarMap[Boolean]
+  type Stmt = AtomicCmds // statements
 
-  val transferF: ((Int, mStmt, Int), VarMap[mDomain]) => VarMap[mDomain] = {
-    case ((q0, cmd, q1), varmap) =>
-      cmd match {
-        case WeakStmt(lhs, op, rhs, prefix) =>
-          rhs match
-            case VarLit(name)                =>
-            case BinOp(a, b, nm)             =>
-            case MulOp(a, b, nm)             =>
-            case AddOp(a, b, nm)             =>
-            case UniOp(a, nm)                =>
-            case VarDynamic(width, tp, name) =>
-            case VarTyped(name, tp)          =>
-            case Lit(i)                      =>
-            case LitDym(i, width)            =>
+  val transferF: ((Int, Stmt, Int), Domain) => Domain = { case ((q0, cmd, q1), varmap) =>
+    cmd match {
+      case WeakStmt(lhs, op, rhs, prefix) =>
+        rhs match
+          case VarLit(name)                =>
+          case BinOp(a, b, nm)             =>
+          case MulOp(a, b, nm)             =>
+          case AddOp(a, b, nm)             =>
+          case UniOp(a, nm)                =>
+          case VarDynamic(width, tp, name) =>
+          case VarTyped(name, tp)          =>
+          case Lit(i)                      =>
+          case LitDym(i, width)            =>
 
-          // any assignment makes var initialized
-          if op == ":=" then varmap.updated(lhs.getname, true) else varmap
-        case _ => varmap
-      }
+        // any assignment makes var initialized
+        if op == ":=" then varmap.updated(lhs.getname, true) else varmap
+      case _ => varmap
+    }
   }
 
-  object checkUnInitLattice extends semiLattice[Boolean] {
+  /** lattice for uninitialized analysis is Var->Boolean where false means uninitialized
+    *
+    * we first define a simple boolean lattice and later lift it to Var->Boolean lattice
+    */
+  object unInitAnalysis extends semiLattice[Boolean] {
 
     override val leq = {
       case (_, true)      => true
@@ -61,10 +51,11 @@ object unInitAnalysis {
   }
 
   def mMonoFramework(
-      mBotMap: VarMap[mDomain]
+      mBotMap: Domain
   ) = {
-    val lifted =
-      checkUnInitLattice.liftWithMap(mBotMap)
+    // lift the boolean lattice to Var->Boolean lattice
+    val lifted: semiLattice[VarMap[Boolean]] =
+      unInitAnalysis.liftWithMap(mBotMap)
 
     MonoFrameworkT(
       transferF = transferF,

From 724613fdabf5d34d0310a0af99afece791e1f001 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 31 Jan 2026 23:32:18 +0800
Subject: [PATCH 17/23] feat: Update Scala version and enhance static analysis
 with live variable analysis

---
 build.sbt                                     |  9 ++-
 .../dependentChisel/codegen/compiler.scala    | 10 +--
 .../dependentChisel/codegen/typeCheck.scala   |  2 +-
 .../staticAnalysis/MonotoneFramework.scala    | 49 ++++++++----
 .../staticAnalysis/liveVarAnalysis.scala      | 73 ++++++++++++++++++
 .../staticAnalysis/semiLattice.scala          | 19 +++--
 .../staticAnalysis/unInitAnalysis.scala       | 21 ++---
 .../staticAnalysis/worklistAlgo.scala         | 36 ++-------
 .../typesAndSyntax/statements.scala           |  4 +-
 .../typesAndSyntax/typesAndOps.scala          | 31 ++++----
 .../liveVarAnalysisSuite.scala                | 77 +++++++++++++++++++
 .../dependentChisel/unInitAnalysisSuite.scala | 19 +++--
 12 files changed, 255 insertions(+), 95 deletions(-)
 create mode 100644 src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
 create mode 100644 src/test/scala/dependentChisel/liveVarAnalysisSuite.scala

diff --git a/build.sbt b/build.sbt
index 34dea9d..9ec7441 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,7 @@ resolvers ++= Seq(
   "jitpack" at "https://jitpack.io",
   "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
 )
-val mScala3Version = "3.3.3" // "3.3.1-RC1-bin-SNAPSHOT" 3.3.0-RC3
+val mScala3Version = "3.3.7" // "3.3.1-RC1-bin-SNAPSHOT" 3.3.0-RC3
 
 /* To print the code as it is transformed through the compiler, use the compiler flag -Xprint:all
 trace the code that generated the error by adding the -Ydebug-error compiler flag,
@@ -19,13 +19,16 @@ lazy val root = project
     scalaVersion := mScala3Version,
     scalacOptions ++= mScalacOptions,
     libraryDependencies ++= Seq(
+      // typelevel
+      "org.typelevel" %% "cats-core" % catsV,
+      "org.typelevel" %% "cats-free" % catsV,
+      "dev.optics" %% "monocle-core" % "3.3.0",
+      // debugging and printing
       "com.lihaoyi" %% "pprint" % "0.8.1", // print,debug
       "org.scalameta" %% "munit" % "0.7.29" % Test,
       // https://mvnrepository.com/artifact/org.scalatest/scalatest
       "org.scalatest" %% "scalatest" % "3.2.14" % Test,
       "io.bullet" %% "macrolizer" % "0.6.2" % "compile-internal", // print,debug
-      "org.typelevel" %% "cats-core" % catsV,
-      "org.typelevel" %% "cats-free" % catsV,
       "com.github.doofin.stdScala" %% "stdscala" % "b10536c37c", // new : 184b5cbc7d  %%% for cr
       "io.github.iltotore" %% "iron" % "2.1.0",
       ("edu.berkeley.cs" %% "chisel3" % "3.5.5")
diff --git a/src/main/scala/dependentChisel/codegen/compiler.scala b/src/main/scala/dependentChisel/codegen/compiler.scala
index c7e6ae1..ee2633f 100644
--- a/src/main/scala/dependentChisel/codegen/compiler.scala
+++ b/src/main/scala/dependentChisel/codegen/compiler.scala
@@ -166,7 +166,7 @@ object compiler {
         })
       case stmt: WeakStmt    => indent + stmt2firrtlStr(stmt)
       case stmt: NewInstance => newInstStmt2firrtlStr(indent, stmt) + "\n"
-      case stmt: VarDecls =>
+      case stmt: VarDecls    =>
         indent + varDecl2firrtlStr(indent, stmt)
     }
 
@@ -201,7 +201,7 @@ object compiler {
         s"$opName(${expr2firrtlStr(a)})"
       case x: Var[?] =>
         // dbg(x)
-        x.getname
+        x.getName
       case Lit(w) =>
         // h0 means HexLit of 0
         s"""UInt<${w}>("$w")"""
@@ -315,7 +315,7 @@ object compiler {
             WeakStmt(
               stmt.lhs,
               ":=",
-              bop.copy(a = VarLit(genStmt.lhs.getname)),
+              bop.copy(a = VarLit(genStmt.lhs.getName)),
               prefix = "node "
             )
           ) ++ resList
@@ -381,7 +381,7 @@ object compiler {
     */
   def varNameTransform(thisInstName: String, v: Var[?]): Var[?] = {
     v match {
-      case x @ VarLit(name) => x
+      case x @ VarLit(name)                => x
       case x @ VarDynamic(width, tp, name) =>
         tp match {
           case VarType.Input | VarType.Output =>
@@ -411,7 +411,7 @@ object compiler {
   /** recursively apply expr to expr Transform like varNameTransform */
   def exprTransform(thisInstName: String, e: Expr[?]): Expr[?] = {
     e match {
-      case v: Var[?] => varNameTransform(thisInstName, v)
+      case v: Var[?]   => varNameTransform(thisInstName, v)
       case x: BinOp[w] =>
         BinOp(
           exprTransform(thisInstName, x.a).asInstanceOf[Expr[Nothing]],
diff --git a/src/main/scala/dependentChisel/codegen/typeCheck.scala b/src/main/scala/dependentChisel/codegen/typeCheck.scala
index e709cc5..0552aa2 100644
--- a/src/main/scala/dependentChisel/codegen/typeCheck.scala
+++ b/src/main/scala/dependentChisel/codegen/typeCheck.scala
@@ -53,7 +53,7 @@ object typeCheck {
             val isWidthOk = isWidthEqu // | lhsGeqRhs
             val msg =
               "[error]".toRed() +
-                s" width mismatch in statement:\n${showPair(lhs.getname, i)}\n " +
+                s" width mismatch in statement:\n${showPair(lhs.getName, i)}\n " +
                 s"$op \n" +
                 s"${showPair(rhs.toString(), j)} "
 
diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 2786763..e4aa9f1 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -23,7 +23,7 @@ object MonotoneFramework {
     *   lattice for domain
     */
   case class MonoFrameworkT[T, stmtT](
-      val transferF: ((Int, stmtT, Int), T) => T,
+      val transferFn: ((Int, stmtT, Int), T) => T,
       // val botMap: VarMap[T],
       baseLattice: semiLattice[T]
   ) extends semiLattice[T] {
@@ -36,27 +36,48 @@ object MonotoneFramework {
     override val lub = baseLattice.lub
     override val leq = baseLattice.leq
 
+    /** run the monotone framework on a program graph
+      *
+      * @param progGraph
+      * @param isForward
+      *   true for forward analysis,false for backward analysis
+      * @return
+      */
     def runWithProgGraph(
-        progGraph: List[(Int, stmtT, Int)]
-    ) =
-      worklistAlgo.wlAlgoMonotone(this, progGraph)
+        progGraph: List[(Int, stmtT, Int)],
+        isForward: Boolean = true
+    ) = {
+      val mf = this
+
+      worklistAlgo.wlAlgoProgGraphP(
+        progGraph,
+        mf.transferFn,
+        mf.leq,
+        mf.lub,
+        mf.bottom,
+        mf.bottom,
+        isForward = isForward
+      )
+    }
   }
 
-  /** lift any t to string->t semiLattice
+  /** lift semiLattice[t] to semiLattice[VarMap[t]]
     *
-    * that is, for t:SemiLattice, the function space String->t is also a SemiLattice
+    * useful for some static analysis like interval analysis, sign analysis
     */
-  extension [domain](base: semiLattice[domain]) {
+  extension [t](base: semiLattice[t]) {
 
-    /** lift the t:lattice to string->t lattice (function space)
+    /** lift semiLattice[t] to semiLattice[VarMap[t]]
+      *
+      * where VarMap[t] represents VarName->t
       *
       * @param botMap
-      *   the bottom element mapping, since we need to know var names
+      *   all variable names as bottom element
       * @return
       */
-    def liftWithMap(botMap: VarMap[domain]): semiLattice[VarMap[domain]] =
-      new semiLattice[VarMap[domain]] {
-        override val leq: (VarMap[domain], VarMap[domain]) => Boolean = { (m1, m2) =>
+    def liftToVarMap(botMap: VarMap[t]): semiLattice[VarMap[t]] =
+      new semiLattice[VarMap[t]] {
+        override val leq: (VarMap[t], VarMap[t]) => Boolean = { (m1, m2) =>
           m1 forall { k1 =>
             // im1 is subset of im2
             val i1o = k1._2
@@ -67,7 +88,7 @@ object MonotoneFramework {
         }
         /*  for lub, take union of keys, for each key do lub on values
          */
-        override val lub: (VarMap[domain], VarMap[domain]) => VarMap[domain] = { (m1, m2) =>
+        override val lub: (VarMap[t], VarMap[t]) => VarMap[t] = { (m1, m2) =>
           val newmap =
             (m1.keys ++ m2.keys).toSet map { k =>
               val i1o = m1(k)
@@ -78,7 +99,7 @@ object MonotoneFramework {
           Map(newmap.toSeq*)
         }
 
-        override val bottom: VarMap[domain] =
+        override val bottom: VarMap[t] =
           botMap.map(s => (s._1, base.bottom))
       }
   }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
new file mode 100644
index 0000000..65c5819
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
@@ -0,0 +1,73 @@
+package dependentChisel.staticAnalysis
+
+import monocle.*
+
+import dependentChisel.staticAnalysis.MonotoneFramework.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
+
+/** live variable analysis is a backward analysis
+  *
+  * we want to know which variables are live (will be used afterwards) at each program point.
+  *
+  * For example, var x is live at program point p, if there is a path downstream from p that uses x
+  * and x is not re-defined(we consider re-definition as kill)
+  */
+object liveVarAnalysis {
+  type Domain = Set[VarName]
+  type Stmt = AtomicCmds // statements
+
+  /** free var in a expr, which is just all var names
+    */
+  def fv(e: Expr[_]): Set[VarName] = {
+    e match
+      case VarLit(name)    => Set(name)
+      case BinOp(a, b, nm) => fv(a) ++ fv(b)
+      case UniOp(a, nm)    => fv(a)
+      case _               => Set.empty[VarName]
+  }
+
+  def genSetLV(s: Stmt): Set[VarName] = s match
+    case WeakStmt(lhs, op, rhs, prefix) => fv(rhs)
+    case _                              => Set.empty[VarName]
+
+  def killSetLV(s: Stmt): Set[VarName] = s match {
+    case WeakStmt(lhs, op, rhs, prefix) => Set(lhs.getName)
+    case _                              => Set.empty[VarName]
+  }
+
+  /** transfer function for living variable analysis
+    *
+    * Stmt, Lattice => Lattice
+    */
+  def transferLV(ppoint: (Int, Stmt, Int), l: Domain): Domain = {
+    val stmt = ppoint._2
+    val ks = killSetLV(stmt).toSet
+    val gs = genSetLV(stmt).toSet
+    val res = (l -- ks) union gs
+    println(s"tran for $ppoint : in = $l , kill = $ks , gen = $gs , out = $res")
+    res
+  }
+
+  /** lattice for live variable analysis is Set[Var],if a var is in the set, it is live
+    */
+  object liveVarLattice extends semiLattice[Domain] {
+
+    override val leq = (a: Set[VarName], b: Set[VarName]) => a.subsetOf(b)
+
+    override val lub = (a: Set[VarName], b: Set[VarName]) => a.union(b)
+
+    override val bottom = Set.empty[VarName]
+
+  }
+
+  def monoFramework(
+      mBotMap: Domain
+  ) = {
+
+    MonoFrameworkT(
+      transferFn = transferLV,
+      baseLattice = liveVarLattice
+    )
+  }
+}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
index 9f0de52..780b71f 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
@@ -3,18 +3,27 @@ package dependentChisel.staticAnalysis
 /** a complete lattice is a partially ordered set in which all subsets have both a supremum (join)
   * and an infimum (meet).
   *
-  * A complete lattice always hasa least and greatest element
+  * A complete lattice always has a least and greatest element
   *
   * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered set such that all
   * finite subsets Y of L have a least upper bound.
   *
-  * The set Q of all rational numbers, with the usual linear order, is an infinite distributive
-  * lattice which is not complete.
+  * The rational number Q with the usual linear order, is an distributive lattice which is not
+  * complete, while the real number R is complete.
+  *
   * @tparam t
-  *   acc(ascending chain condition)
   */
 trait semiLattice[t] {
-  val leq: (t, t) => Boolean // partial ordering
+
+  /** partial ordering, less than or equal to
+    */
+  val leq: (t, t) => Boolean
+
+  /** least upper bound
+    */
   val lub: (t, t) => t // least upper bound
+
+  /** least element, bottom
+    */
   val bottom: t
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index 93c5f6b..f75f82f 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -13,19 +13,8 @@ object unInitAnalysis {
   val transferF: ((Int, Stmt, Int), Domain) => Domain = { case ((q0, cmd, q1), varmap) =>
     cmd match {
       case WeakStmt(lhs, op, rhs, prefix) =>
-        rhs match
-          case VarLit(name)                =>
-          case BinOp(a, b, nm)             =>
-          case MulOp(a, b, nm)             =>
-          case AddOp(a, b, nm)             =>
-          case UniOp(a, nm)                =>
-          case VarDynamic(width, tp, name) =>
-          case VarTyped(name, tp)          =>
-          case Lit(i)                      =>
-          case LitDym(i, width)            =>
-
         // any assignment makes var initialized
-        if op == ":=" then varmap.updated(lhs.getname, true) else varmap
+        if op == ":=" then varmap.updated(lhs.getName, true) else varmap
       case _ => varmap
     }
   }
@@ -34,7 +23,7 @@ object unInitAnalysis {
     *
     * we first define a simple boolean lattice and later lift it to Var->Boolean lattice
     */
-  object unInitAnalysis extends semiLattice[Boolean] {
+  object unInitLattice extends semiLattice[Boolean] {
 
     override val leq = {
       case (_, true)      => true
@@ -50,15 +39,15 @@ object unInitAnalysis {
 
   }
 
-  def mMonoFramework(
+  def monoFramework(
       mBotMap: Domain
   ) = {
     // lift the boolean lattice to Var->Boolean lattice
     val lifted: semiLattice[VarMap[Boolean]] =
-      unInitAnalysis.liftWithMap(mBotMap)
+      unInitLattice.liftToVarMap(mBotMap)
 
     MonoFrameworkT(
-      transferF = transferF,
+      transferFn = transferF,
       baseLattice = lifted
     )
   }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index 9b24743..e371f58 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -26,45 +26,25 @@ object worklistAlgo {
     override def isEmpty: Boolean = as.isEmpty
   }
 
-  /** worklist algorithm for monotone framework
-    * @param mf
-    *   monotone framework
-    * @param progGraph
-    *   program graph as list of (src point,stmt,tgt point)
-    *
-    * @return
-    *   mapping from program point to domainMap at that point
-    */
-  def wlAlgoMonotone[domainT, stmtT](
-      mf: MonoFrameworkT[domainT, stmtT],
-      progGraph: List[(Int, stmtT, Int)]
-  ) = {
-
-    wlAlgoProgGraphP[domainT, stmtT](
-      progGraph,
-      mf.transferF,
-      mf.leq,
-      mf.lub,
-      mf.bottom,
-      mf.bottom
-    )
-  }
-
   /** worklist algorithm implementation for program graph
     */
-  private def wlAlgoProgGraphP[domainT, stmtT](
-      progGraph: List[(Int, stmtT, Int)],
+  def wlAlgoProgGraphP[domainT, stmtT](
+      progGraph_ : List[(Int, stmtT, Int)],
       transferF: ((Int, stmtT, Int), domainT) => domainT,
       smallerThan: (domainT, domainT) => Boolean,
       lubOp: (domainT, domainT) => domainT,
       initD: domainT,
       bottomD: domainT,
-      isReverse: Boolean = false
+      isForward: Boolean = true
   ): Map[Int, domainT] = {
 
     val mutList: Worklist[Int] = new WlStack()
 
-    pp(progGraph)
+    val progGraph =
+      if isForward then progGraph_
+      else progGraph_.map { case (a, st, c) => (c, st, a) }
+
+    // pp(progGraph)
     //    get program points
     val progPoints = progGraph.flatMap(x => List(x._1, x._3)).distinct
 
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
index f7e4cbb..8f9ba3d 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
@@ -39,7 +39,7 @@ object statements {
   extension [w <: Int, V <: Var[w]](v: V) {
 
     inline def :=(using md: ModuleData)(oth: Expr[w]) = {
-      val name = v.getname
+      val name = v.getName
 
       /* v match {
         case VarLit(name) =>
@@ -57,7 +57,7 @@ object statements {
   /** untyped API for assign */
   extension (v: VarDynamic) {
     inline def :=(using md: ModuleData)(oth: Expr[?]) = {
-      val name = v.getname
+      val name = v.getName
       md.typeMap.addOne(v, v.width)
 
       appendCmdToModule(WeakStmt(v, ":=", oth))
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
index af422fa..0b32d90 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
@@ -19,28 +19,32 @@ object typesAndOps extends exprOp {
 registers: Bits, UInt, and SInt. UInt and SInt extend Bits, and all three types
 represent a vector of bits */
 
+  sealed trait Expr[w <: Int] {
+    def asUnTyped = this.asInstanceOf[Expr[Nothing]]
+    inline def asTypedUnsafe[w <: Int] = {
+      this.asInstanceOf[Expr[w]]
+    }
+  }
+
   /* mutable vars which can be mutated in lhs, incl input,output */
   sealed trait Var[w <: Int](name: String) extends Expr[w] {
-    def getname = name
+    def getName = name
     // def getIsIO = isIO
   }
 
+  /** declare a variable like: WeakStmt(VarLit(newValue), ":=", a)
+    *
+    * @param name
+    */
   case class VarLit[w <: Int](name: String) extends Var[w](name)
 
-  sealed trait Expr[w <: Int] {
-    def asUnTyped = this.asInstanceOf[Expr[Nothing]]
-    inline def asTypedUnsafe[w <: Int] = {
-      this.asInstanceOf[Expr[w]]
-    }
-  }
+  // binary op like add,sub,and,or
   case class BinOp[w <: Int](a: Expr[w], b: Expr[w], nm: String) extends Expr[w]
 
   // to prevent overflow like AFix in spinalHDL
-  case class MulOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul")
-      extends Expr[2 * w]
+  case class MulOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul") extends Expr[2 * w]
 
-  case class AddOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul")
-      extends Expr[w + 1]
+  case class AddOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul") extends Expr[w + 1]
 
   /** uniary op like negate */
   case class UniOp[w <: Int](a: Expr[w], nm: String) extends Expr[w]
@@ -67,8 +71,7 @@ represent a vector of bits */
   // new ExprC[1, VarDeclTp.Reg.type] {} + new ExprC[1, VarDeclTp.Wire.type] {} //ok ,will fail
 
   /** untyped API for Wire, Reg, and IO */
-  case class VarDynamic(width: Int, tp: VarType, name: String)
-      extends Var[Nothing](name) {
+  case class VarDynamic(width: Int, tp: VarType, name: String) extends Var[Nothing](name) {
 
     /** dym check for type cast */
     inline def asTyped[w <: Int] = {
@@ -103,7 +106,7 @@ represent a vector of bits */
   // for future use
 
 // case class Lit[w <: Int](i: w, name: String) extends Expr[w] {}
-  type sml[w <: Int] <: w ^ 2
+  // type sml[w <: Int] <: w ^ 2
   case class Lit[w <: Int](i: w) extends Expr[w] {}
   case class LitDym(i: Int, width: Int) extends Expr[Nothing]
   /*
diff --git a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
new file mode 100644
index 0000000..605f516
--- /dev/null
+++ b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
@@ -0,0 +1,77 @@
+package dependentChisel
+
+import com.doofin.stdScalaCross.*
+
+import dependentChisel.typesAndSyntax.typesAndOps.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.staticAnalysis.liveVarAnalysis
+
+class liveVarAnalysisSuite extends munit.FunSuite {
+  test("test free variable function".ignore) {
+    val expr = VarLit("x") + VarLit("y") + Lit[8](8)
+    val expr2 = UniOp(expr + VarLit("z"), "neg")
+
+    val fvResult = liveVarAnalysis.fv(expr2)
+    val expectedFv = Set("x", "y", "z")
+    assertEquals(fvResult, expectedFv, "free var should be x,y,z")
+  }
+
+  test("live variable transfer function test") {
+
+    val stmt1 = (0, WeakStmt(VarLit("r"), ":=", VarLit("r") - VarLit("y")), 1)
+
+    val t1 = liveVarAnalysis.transferLV(stmt1, Set())
+    assertEquals(t1, Set("r", "y"), "after r:=r - y , r and y should be live ")
+
+    val stmt2 = (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1)
+
+    // x should be dead after assignment
+    val t2 = liveVarAnalysis.transferLV(stmt2, Set("x", "y"))
+    assertEquals(t2, Set("y"), "after x:=1, x should be dead ")
+
+    // pp(res)
+
+  }
+
+  test("live variable analysis full test with worklist algo") {
+
+    // each var is uninitialized at the beginning
+    val initMap =
+      Set.empty[String]
+
+    val pg =
+      List(
+        (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
+        (1, Skip, 3),
+        (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2),
+        (2, Skip, 4),
+        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + Lit[1](1)), 5)
+      )
+
+    /*
+    ASCII visualization:
+
+             0
+             / \
+          (x:=1)   (y:=1)
+           |       \
+           v        v
+           1        2
+           |        |
+           v        v
+           3        4
+           |
+          (z:=x+1)
+           |
+           v
+           5
+     */
+    val monoF = liveVarAnalysis.monoFramework(initMap)
+
+    // live variable analysis is a backward analysis
+    val res = monoF.runWithProgGraph(pg, isForward = false)
+
+    pp(res)
+
+  }
+}
diff --git a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
index 59159fb..8696094 100644
--- a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
@@ -1,7 +1,6 @@
 package dependentChisel
 
-import dependentChisel.typesAndSyntax.typesAndOps.Lit
-import dependentChisel.typesAndSyntax.typesAndOps.VarLit
+import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.codegen.sequentialCommands.*
 import dependentChisel.staticAnalysis.unInitAnalysis
 
@@ -26,20 +25,26 @@ class unInitAnalysisSuite extends munit.FunSuite {
       List(
         (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
         (1, Skip, 3), // x is initialized from 0->1->3
-        (0, Skip, 2), // x is not initialized from 0->2
-        (2, Skip, 4), // x is not initialized from 0->2->4
+        (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2), // x is not init from 0->2, y yes
+        (2, Skip, 4), // x not, y yes
         (3, Skip, 5) // x is initialized from 0->1->3->5
       )
-    val monoF = unInitAnalysis.mMonoFramework(initMap)
+    val monoF = unInitAnalysis.monoFramework(initMap)
 
     val res = monoF.runWithProgGraph(pg)
     val expectedInit = Set(1, 3, 5)
-    val resultInit = res.filter { case (k, v) =>
+    val resultInitX = res.filter { case (k, v) =>
       v("x") // filter where x is true
     }.keySet
 
     pp(res)
-    assertEquals(resultInit, expectedInit, "so x is only initialized at point 1,3,5")
+    assertEquals(resultInitX, expectedInit, "so x is only initialized at point 1,3,5")
+
+    val expectedInitY = Set(2, 4)
+    val resultInitY = res.filter { case (k, v) =>
+      v("y") // filter where y is true
+    }.keySet
+    assertEquals(resultInitY, expectedInitY, "so y is only initialized at point 2,4")
 
   }
 }

From b4bc6667e48937398f93188fa0d2e8b072239f61 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Sat, 31 Jan 2026 23:42:25 +0800
Subject: [PATCH 18/23] feat: Enhance worklist algorithm and live variable
 analysis with entry/exit point support

---
 .../staticAnalysis/MonotoneFramework.scala    |  4 ++-
 .../staticAnalysis/worklistAlgo.scala         | 28 +++++++++++++++++--
 .../liveVarAnalysisSuite.scala                | 26 ++++++++++-------
 3 files changed, 45 insertions(+), 13 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index e4aa9f1..6675db2 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -45,7 +45,8 @@ object MonotoneFramework {
       */
     def runWithProgGraph(
         progGraph: List[(Int, stmtT, Int)],
-        isForward: Boolean = true
+        isForward: Boolean = true,
+        entryExitPoint: (Int, Int) = (0, 0)
     ) = {
       val mf = this
 
@@ -56,6 +57,7 @@ object MonotoneFramework {
         mf.lub,
         mf.bottom,
         mf.bottom,
+        entryExitPoint = entryExitPoint,
         isForward = isForward
       )
     }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index e371f58..21ba729 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -4,6 +4,7 @@ import com.doofin.stdScalaJvm.*
 import scala.collection.{immutable, mutable}
 
 import MonotoneFramework.*
+import chisel3.util.is
 
 object worklistAlgo {
   trait Worklist[t] {
@@ -26,7 +27,22 @@ object worklistAlgo {
     override def isEmpty: Boolean = as.isEmpty
   }
 
-  /** worklist algorithm implementation for program graph
+  /** worklist algorithm on program graph
+    *
+    * @param progGraph_
+    * @param transferF
+    * @param smallerThan
+    * @param lubOp
+    * @param initD
+    *   for program point 0 if it's forward analysis, or exiting point if backward analysis
+    * @param bottomD
+    *   for other program points
+    * @param entryExitPoint
+    *   the (entry, exit) program points. forward analysis only use entry point, backward analysis
+    *   only use exit
+    * @param isForward
+    *   true for forward analysis,false for backward analysis
+    * @return
     */
   def wlAlgoProgGraphP[domainT, stmtT](
       progGraph_ : List[(Int, stmtT, Int)],
@@ -35,6 +51,7 @@ object worklistAlgo {
       lubOp: (domainT, domainT) => domainT,
       initD: domainT,
       bottomD: domainT,
+      entryExitPoint: (Int, Int),
       isForward: Boolean = true
   ): Map[Int, domainT] = {
 
@@ -54,7 +71,14 @@ object worklistAlgo {
 
 //    initialize at each program points,set to init for point 0 (first loop)
     progPoints foreach { q =>
-      resMapMut(q) = if (q == 0) initD else bottomD
+      val (entryPoint, exitPoint) = entryExitPoint
+      if isForward then //
+        resMapMut(q) = if (q == entryPoint) then initD else bottomD
+      else
+        resMapMut(q) = if (q == exitPoint) then initD else bottomD
+
+        //
+        // resMapMut(q) = if (q == 0) then initD else bottomD
     }
 
     // keep applying transferF to program graph until the node value is stable
diff --git a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
index 605f516..6d19545 100644
--- a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
@@ -33,11 +33,7 @@ class liveVarAnalysisSuite extends munit.FunSuite {
 
   }
 
-  test("live variable analysis full test with worklist algo") {
-
-    // each var is uninitialized at the beginning
-    val initMap =
-      Set.empty[String]
+  test("live variable analysis full test") {
 
     val pg =
       List(
@@ -45,14 +41,20 @@ class liveVarAnalysisSuite extends munit.FunSuite {
         (1, Skip, 3),
         (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2),
         (2, Skip, 4),
-        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + Lit[1](1)), 5)
+        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + Lit[1](1)), 5),
+        (4, Skip, 5)
       )
 
+    // each var is uninitialized at the beginning
+    val initMap =
+      Set.empty[String]
+
+    val entryExitPoint = (0, 5)
     /*
     ASCII visualization:
 
-             0
-             / \
+                0
+             /    \
           (x:=1)   (y:=1)
            |       \
            v        v
@@ -63,13 +65,17 @@ class liveVarAnalysisSuite extends munit.FunSuite {
            |
           (z:=x+1)
            |
-           v
+           v   /
            5
      */
     val monoF = liveVarAnalysis.monoFramework(initMap)
 
     // live variable analysis is a backward analysis
-    val res = monoF.runWithProgGraph(pg, isForward = false)
+    val res = monoF.runWithProgGraph(
+      pg, //
+      isForward = false,
+      entryExitPoint
+    )
 
     pp(res)
 

From 6eac0c1cdc3b4c2cab363f450b8ecf136801ef11 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Mon, 2 Feb 2026 20:15:04 +0800
Subject: [PATCH 19/23] feat: Introduce reaching definition analysis and
 related test suite

---
 .../staticAnalysis/MonotoneFramework.scala    |  2 +-
 .../staticAnalysis/reachingDefAnalysis.scala  | 54 +++++++++++++++++++
 .../staticAnalysis/reachingDefLattice.scala   | 10 ----
 .../staticAnalysis/worklistAlgo.scala         | 13 ++---
 .../reachingDefAnalysisSuite.scala            | 38 +++++++++++++
 .../dependentChisel/unInitAnalysisSuite.scala |  7 +--
 6 files changed, 102 insertions(+), 22 deletions(-)
 create mode 100644 src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
 delete mode 100644 src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala
 create mode 100644 src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 6675db2..cf4d992 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -46,7 +46,7 @@ object MonotoneFramework {
     def runWithProgGraph(
         progGraph: List[(Int, stmtT, Int)],
         isForward: Boolean = true,
-        entryExitPoint: (Int, Int) = (0, 0)
+        entryExitPoint: (Int, Int)
     ) = {
       val mf = this
 
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
new file mode 100644
index 0000000..1878f76
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
@@ -0,0 +1,54 @@
+package dependentChisel.staticAnalysis
+
+import dependentChisel.staticAnalysis.MonotoneFramework.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
+
+/** reaching definitions as a mapping Var -> PowerSet( Q? * Q ) */
+object reachingDefAnalysis {
+  type Domain = Set[(VarName, Int, Int)] // PowerSet( Q? * Q )
+  type Stmt = AtomicCmds // statements
+
+  def transferFn(ppoint: (Int, Stmt, Int), l: Domain): Domain = {
+    val stmt = ppoint._2
+    val gs = genSet(ppoint)
+    val res = stmt match {
+      case WeakStmt(lhs, ":=", rhs, prefix) =>
+        // res = l- kill + gen
+        val killed = l.filter(_._1 != lhs.getName)
+        killed ++ gs
+      case _ => l
+    }
+
+    println(s"tran for $ppoint : in = $l ,  gen = $gs , out = $res")
+    res
+  }
+
+  def genSet(ppoint: (Int, Stmt, Int)): Domain = {
+    val (p, stmt, q) = ppoint
+    stmt match {
+      case WeakStmt(lhs, op, rhs, prefix) =>
+        Set((lhs.getName, p, q))
+      case _ => Set.empty
+    }
+  }
+
+  object RDLattice extends semiLattice[Domain] {
+
+    override val leq = (a: Domain, b: Domain) => a.subsetOf(b)
+
+    override val lub = (a: Domain, b: Domain) => a.union(b)
+
+    override val bottom: Domain = Set.empty
+  }
+
+  def monoFramework(
+      mBotMap: Domain
+  ) = {
+
+    MonoFrameworkT(
+      transferFn = transferFn,
+      baseLattice = RDLattice
+    )
+  }
+}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala
deleted file mode 100644
index 5bc9b42..0000000
--- a/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-package dependentChisel.staticAnalysis
-
-/** reaching definitions as a mapping Var -> PowerSet( Q? * Q ) */
-object reachingDefLattice {
-  type domain = Set[(Int, Int)] // PowerSet( Q? * Q )
-// domainMap is  Var -> PowerSet( Q? * Q ) uninitializedLattice
-
-  /* For this define Bot to be the mapping that maps each variable to the empty set */
-
-}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index 21ba729..c1a8fd4 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -57,10 +57,14 @@ object worklistAlgo {
 
     val mutList: Worklist[Int] = new WlStack()
 
+    //  for backward analysis just reverse the edges and swap entry exit (or init final)
     val progGraph =
       if isForward then progGraph_
       else progGraph_.map { case (a, st, c) => (c, st, a) }
 
+    val (entryPoint, exitPoint) =
+      if isForward then entryExitPoint else (entryExitPoint._2, entryExitPoint._1)
+
     // pp(progGraph)
     //    get program points
     val progPoints = progGraph.flatMap(x => List(x._1, x._3)).distinct
@@ -71,14 +75,7 @@ object worklistAlgo {
 
 //    initialize at each program points,set to init for point 0 (first loop)
     progPoints foreach { q =>
-      val (entryPoint, exitPoint) = entryExitPoint
-      if isForward then //
-        resMapMut(q) = if (q == entryPoint) then initD else bottomD
-      else
-        resMapMut(q) = if (q == exitPoint) then initD else bottomD
-
-        //
-        // resMapMut(q) = if (q == 0) then initD else bottomD
+      resMapMut(q) = if (q == 0) then initD else bottomD
     }
 
     // keep applying transferF to program graph until the node value is stable
diff --git a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
new file mode 100644
index 0000000..9eefe0f
--- /dev/null
+++ b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
@@ -0,0 +1,38 @@
+package dependentChisel
+
+import com.doofin.stdScalaCross.*
+
+import dependentChisel.typesAndSyntax.typesAndOps.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.staticAnalysis.reachingDefAnalysis
+
+class reachingDefAnalysisSuite extends munit.FunSuite {
+
+  // program graph in PA appetizer,p17
+  val pg1 =
+    List(
+      (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 1),
+      (1, Skip, 2),
+      (2, WeakStmt(VarLit("y"), ":=", VarLit("x") + VarLit("y")), 3),
+      (3, WeakStmt(VarLit("x"), ":=", VarLit("x") - Lit[1](1)), 1),
+      (1, Skip, 4)
+    )
+  test("reaching definition transfer function test") {
+    val initMap: reachingDefAnalysis.Domain = Set.empty
+    val t1 = reachingDefAnalysis.transferFn(pg1(0), initMap)
+
+    val mono = reachingDefAnalysis.monoFramework(initMap)
+    val res = mono.runWithProgGraph(pg1, isForward = true, entryExitPoint = (0, 4))
+
+    pp(res)
+
+    val expected = Map(
+      0 -> Set(),
+      1 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),
+      2 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),
+      3 -> Set(("y", 2, 3), ("x", 3, 1)),
+      4 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1))
+    )
+    assertEquals(res, expected)
+  }
+}
diff --git a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
index 8696094..2d34e7f 100644
--- a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
@@ -16,7 +16,7 @@ class unInitAnalysisSuite extends munit.FunSuite {
           .map(x => x.toString() -> false)
           .toList*
       )
-
+    val initFinal = (0, 5)
     /* a program graph
 0 -> x:=.. ->1 -> 3 -> 5
 0 ->   2   -> 4
@@ -27,11 +27,12 @@ class unInitAnalysisSuite extends munit.FunSuite {
         (1, Skip, 3), // x is initialized from 0->1->3
         (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2), // x is not init from 0->2, y yes
         (2, Skip, 4), // x not, y yes
-        (3, Skip, 5) // x is initialized from 0->1->3->5
+        (3, Skip, 5), // x is initialized from 0->1->3->5
+        (4, Skip, 5)
       )
     val monoF = unInitAnalysis.monoFramework(initMap)
 
-    val res = monoF.runWithProgGraph(pg)
+    val res = monoF.runWithProgGraph(pg, entryExitPoint = initFinal)
     val expectedInit = Set(1, 3, 5)
     val resultInitX = res.filter { case (k, v) =>
       v("x") // filter where x is true

From 0e915c3be2b7ea753fd7c4474b2be99069a743ba Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Mon, 2 Feb 2026 22:28:18 +0800
Subject: [PATCH 20/23] refactor: Simplify worklist algorithm and update
 monoFramework signatures

---
 .../staticAnalysis/MonotoneFramework.scala    |  8 +++----
 .../staticAnalysis/liveVarAnalysis.scala      |  4 +---
 .../staticAnalysis/reachingDefAnalysis.scala  |  2 +-
 .../staticAnalysis/worklistAlgo.scala         | 24 +++++++++----------
 .../liveVarAnalysisSuite.scala                |  2 +-
 .../reachingDefAnalysisSuite.scala            |  8 +++----
 6 files changed, 20 insertions(+), 28 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index cf4d992..3bf901b 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -50,13 +50,11 @@ object MonotoneFramework {
     ) = {
       val mf = this
 
-      worklistAlgo.wlAlgoProgGraphP(
+      worklistAlgo.onProgGraph(
         progGraph,
         mf.transferFn,
-        mf.leq,
-        mf.lub,
-        mf.bottom,
-        mf.bottom,
+        lattice = baseLattice,
+        initD = mf.bottom,
         entryExitPoint = entryExitPoint,
         isForward = isForward
       )
diff --git a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
index 65c5819..2a0c107 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
@@ -61,9 +61,7 @@ object liveVarAnalysis {
 
   }
 
-  def monoFramework(
-      mBotMap: Domain
-  ) = {
+  def monoFramework() = {
 
     MonoFrameworkT(
       transferFn = transferLV,
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
index 1878f76..ab7001b 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
@@ -6,6 +6,7 @@ import dependentChisel.typesAndSyntax.typesAndOps.*
 
 /** reaching definitions as a mapping Var -> PowerSet( Q? * Q ) */
 object reachingDefAnalysis {
+  // (x, p, q) means variable x is modified by the edge p->q. (x,?,qi) means x is not modified before initial point qi. Here we don't use ? for simplicity
   type Domain = Set[(VarName, Int, Int)] // PowerSet( Q? * Q )
   type Stmt = AtomicCmds // statements
 
@@ -43,7 +44,6 @@ object reachingDefAnalysis {
   }
 
   def monoFramework(
-      mBotMap: Domain
   ) = {
 
     MonoFrameworkT(
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index c1a8fd4..2730925 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -44,16 +44,14 @@ object worklistAlgo {
     *   true for forward analysis,false for backward analysis
     * @return
     */
-  def wlAlgoProgGraphP[domainT, stmtT](
+  def onProgGraph[T, stmtT](
       progGraph_ : List[(Int, stmtT, Int)],
-      transferF: ((Int, stmtT, Int), domainT) => domainT,
-      smallerThan: (domainT, domainT) => Boolean,
-      lubOp: (domainT, domainT) => domainT,
-      initD: domainT,
-      bottomD: domainT,
+      transferFn: ((Int, stmtT, Int), T) => T,
+      lattice: semiLattice[T],
+      initD: T,
       entryExitPoint: (Int, Int),
       isForward: Boolean = true
-  ): Map[Int, domainT] = {
+  ): Map[Int, T] = {
 
     val mutList: Worklist[Int] = new WlStack()
 
@@ -71,11 +69,11 @@ object worklistAlgo {
 
     mutList.insertAll(progPoints)
 
-    val resMapMut: mutable.Map[Int, domainT] = mutable.Map()
+    val resMapMut: mutable.Map[Int, T] = mutable.Map()
 
 //    initialize at each program points,set to init for point 0 (first loop)
     progPoints foreach { q =>
-      resMapMut(q) = if (q == 0) then initD else bottomD
+      resMapMut(q) = if (q == 0) then initD else lattice.bottom
     }
 
     // keep applying transferF to program graph until the node value is stable
@@ -93,11 +91,11 @@ object worklistAlgo {
       progGraphTups foreach { case tup @ (pre, stmtT, post) =>
         val preMap = resMapMut(pre)
         val postMap = resMapMut(post) // AA(q dot)
-        val preMapTransfered = transferF(tup, preMap)
+        val preMapTransfered = transferFn(tup, preMap)
 
 //          update if preMapAnalysised >=  postMap (not <=)
 //        println("doUpdate:", subOrderOp, preMapTransfered, postMap) // subOrderOp can be null
-        val doUpdate = !smallerThan(preMapTransfered, postMap)
+        val doUpdate = !lattice.leq(preMapTransfered, postMap)
 
 //        println(s"doUpdate if presetF ${pre} notSubOrder postset ${post}:: at ${post}", doUpdate)
 //          pp(preMapTransfered, s"preSetF f(${pre}):")
@@ -105,7 +103,7 @@ object worklistAlgo {
 
         if (doUpdate) {
 
-          val lubR = lubOp(postMap, preMapTransfered)
+          val lubR = lattice.lub(postMap, preMapTransfered)
 //            pp(lubR, "lub : ")
           resMapMut(post) = lubR
 //            wlMut += post
@@ -115,7 +113,7 @@ object worklistAlgo {
         }
       }
     }
-    println(s"iter step : ${steps}")
+    println(s"worklist algo finished in $steps steps")
     resMapMut.toMap
   }
 }
diff --git a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
index 6d19545..49cd8d1 100644
--- a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
@@ -68,7 +68,7 @@ class liveVarAnalysisSuite extends munit.FunSuite {
            v   /
            5
      */
-    val monoF = liveVarAnalysis.monoFramework(initMap)
+    val monoF = liveVarAnalysis.monoFramework()
 
     // live variable analysis is a backward analysis
     val res = monoF.runWithProgGraph(
diff --git a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
index 9eefe0f..818769d 100644
--- a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
@@ -8,7 +8,7 @@ import dependentChisel.staticAnalysis.reachingDefAnalysis
 
 class reachingDefAnalysisSuite extends munit.FunSuite {
 
-  // program graph in PA appetizer,p17
+  // program graph in PA appetizer,p17 and example 2.2 at p18
   val pg1 =
     List(
       (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 1),
@@ -17,15 +17,13 @@ class reachingDefAnalysisSuite extends munit.FunSuite {
       (3, WeakStmt(VarLit("x"), ":=", VarLit("x") - Lit[1](1)), 1),
       (1, Skip, 4)
     )
-  test("reaching definition transfer function test") {
+  test("reaching definition full test") {
     val initMap: reachingDefAnalysis.Domain = Set.empty
     val t1 = reachingDefAnalysis.transferFn(pg1(0), initMap)
 
-    val mono = reachingDefAnalysis.monoFramework(initMap)
+    val mono = reachingDefAnalysis.monoFramework()
     val res = mono.runWithProgGraph(pg1, isForward = true, entryExitPoint = (0, 4))
 
-    pp(res)
-
     val expected = Map(
       0 -> Set(),
       1 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),

From 17df06218c79fd91f6560971c3267570d9004415 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Mon, 2 Feb 2026 22:57:48 +0800
Subject: [PATCH 21/23] liveVarAnalysisSuite ok, Update MonoFrameworkT

---
 .../staticAnalysis/MonotoneFramework.scala    | 34 ++++++---------
 .../staticAnalysis/liveVarAnalysis.scala      |  6 +--
 .../staticAnalysis/reachingDefAnalysis.scala  |  2 +-
 .../staticAnalysis/unInitAnalysis.scala       |  2 +-
 .../liveVarAnalysisSuite.scala                | 42 +++++++++++--------
 .../reachingDefAnalysisSuite.scala            |  1 +
 6 files changed, 42 insertions(+), 45 deletions(-)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
index 3bf901b..3c90473 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -12,29 +12,20 @@ object MonotoneFramework {
     *
     * tips : create two file named xxAnalysis to implement this trait, and xxLattice to implement
     * the lattice separately.
-    * @tparam domain
-    *   domain lattice which satisify acc
+    * @tparam T
+    *   lattice type
     * @tparam stmtT
-    *   type of statement
-    *
-    * @param initMap
-    *   initial mapping from var to domain value
-    * @param baseLattice
-    *   lattice for domain
+    *   statement type
+    * @param transferFn
+    *   transfer function
+    * @param lattice
+    *   lattice over T for the analysis
     */
   case class MonoFrameworkT[T, stmtT](
       val transferFn: ((Int, stmtT, Int), T) => T,
       // val botMap: VarMap[T],
-      baseLattice: semiLattice[T]
-  ) extends semiLattice[T] {
-    // val liftedLattice = baseLattice.liftWithMap(botMap)
-    // override val bottom: VarMap[T] = liftedLattice.bottom
-    // override val lub = liftedLattice.lub
-    // override val leq = liftedLattice.leq
-
-    override val bottom: T = baseLattice.bottom
-    override val lub = baseLattice.lub
-    override val leq = baseLattice.leq
+      lattice: semiLattice[T]
+  ) {
 
     /** run the monotone framework on a program graph
       *
@@ -48,13 +39,12 @@ object MonotoneFramework {
         isForward: Boolean = true,
         entryExitPoint: (Int, Int)
     ) = {
-      val mf = this
 
       worklistAlgo.onProgGraph(
         progGraph,
-        mf.transferFn,
-        lattice = baseLattice,
-        initD = mf.bottom,
+        transferFn,
+        lattice = lattice,
+        initD = lattice.bottom,
         entryExitPoint = entryExitPoint,
         isForward = isForward
       )
diff --git a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
index 2a0c107..37b83c9 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
@@ -42,8 +42,8 @@ object liveVarAnalysis {
     */
   def transferLV(ppoint: (Int, Stmt, Int), l: Domain): Domain = {
     val stmt = ppoint._2
-    val ks = killSetLV(stmt).toSet
-    val gs = genSetLV(stmt).toSet
+    val ks = killSetLV(stmt)
+    val gs = genSetLV(stmt)
     val res = (l -- ks) union gs
     println(s"tran for $ppoint : in = $l , kill = $ks , gen = $gs , out = $res")
     res
@@ -65,7 +65,7 @@ object liveVarAnalysis {
 
     MonoFrameworkT(
       transferFn = transferLV,
-      baseLattice = liveVarLattice
+      lattice = liveVarLattice
     )
   }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
index ab7001b..57b92b4 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
@@ -48,7 +48,7 @@ object reachingDefAnalysis {
 
     MonoFrameworkT(
       transferFn = transferFn,
-      baseLattice = RDLattice
+      lattice = RDLattice
     )
   }
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
index f75f82f..39cefe9 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -48,7 +48,7 @@ object unInitAnalysis {
 
     MonoFrameworkT(
       transferFn = transferF,
-      baseLattice = lifted
+      lattice = lifted
     )
   }
 }
diff --git a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
index 49cd8d1..52a7478 100644
--- a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
@@ -7,7 +7,7 @@ import dependentChisel.codegen.sequentialCommands.*
 import dependentChisel.staticAnalysis.liveVarAnalysis
 
 class liveVarAnalysisSuite extends munit.FunSuite {
-  test("test free variable function".ignore) {
+  test("test free variable function") {
     val expr = VarLit("x") + VarLit("y") + Lit[8](8)
     val expr2 = UniOp(expr + VarLit("z"), "neg")
 
@@ -18,8 +18,9 @@ class liveVarAnalysisSuite extends munit.FunSuite {
 
   test("live variable transfer function test") {
 
+    // r:= r - y
     val stmt1 = (0, WeakStmt(VarLit("r"), ":=", VarLit("r") - VarLit("y")), 1)
-
+    // {}-{r}+{r,y} = {r,y} for l-kill + gen
     val t1 = liveVarAnalysis.transferLV(stmt1, Set())
     assertEquals(t1, Set("r", "y"), "after r:=r - y , r and y should be live ")
 
@@ -40,15 +41,11 @@ class liveVarAnalysisSuite extends munit.FunSuite {
         (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
         (1, Skip, 3),
         (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2),
-        (2, Skip, 4),
-        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + Lit[1](1)), 5),
+        (2, WeakStmt(VarLit("y"), ":=", VarLit("y") + Lit[1](1)), 4),
+        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + VarLit("y") + Lit[1](1)), 5),
         (4, Skip, 5)
       )
 
-    // each var is uninitialized at the beginning
-    val initMap =
-      Set.empty[String]
-
     val entryExitPoint = (0, 5)
     /*
     ASCII visualization:
@@ -56,16 +53,17 @@ class liveVarAnalysisSuite extends munit.FunSuite {
                 0
              /    \
           (x:=1)   (y:=1)
-           |       \
-           v        v
-           1        2
-           |        |
-           v        v
-           3        4
+           |         \
+           v          v
+           1          2
+           |          | (y:=y+1)
+           v          v
+           3          4
            |
-          (z:=x+1)
-           |
-           v   /
+      (z:=x+y+1)   /
+           |      /
+           v     /
+          
            5
      */
     val monoF = liveVarAnalysis.monoFramework()
@@ -77,7 +75,15 @@ class liveVarAnalysisSuite extends munit.FunSuite {
       entryExitPoint
     )
 
-    pp(res)
+    val expected = Map(
+      0 -> Set("y"),
+      5 -> Set(),
+      1 -> Set("x", "y"),
+      2 -> Set("y"),
+      3 -> Set("x", "y"),
+      4 -> Set()
+    )
+    assertEquals(res, expected)
 
   }
 }
diff --git a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
index 818769d..acd2c17 100644
--- a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
@@ -24,6 +24,7 @@ class reachingDefAnalysisSuite extends munit.FunSuite {
     val mono = reachingDefAnalysis.monoFramework()
     val res = mono.runWithProgGraph(pg1, isForward = true, entryExitPoint = (0, 4))
 
+    // from 2.12 p21, the result of Example 2.2
     val expected = Map(
       0 -> Set(),
       1 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),

From 3d7652adadaf7e4b86eca628a8e4e8ae31b8d4ad Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Tue, 3 Feb 2026 19:52:48 +0800
Subject: [PATCH 22/23] feat: Add live variable and reaching definition
 analysis test suites

---
 .../dependentChisel/staticAnalysis/reachingDefAnalysis.scala  | 4 +---
 .../{ => staticAnalysis}/liveVarAnalysisSuite.scala           | 2 +-
 .../{ => staticAnalysis}/reachingDefAnalysisSuite.scala       | 2 +-
 .../{ => staticAnalysis}/unInitAnalysisSuite.scala            | 2 +-
 4 files changed, 4 insertions(+), 6 deletions(-)
 rename src/test/scala/dependentChisel/{ => staticAnalysis}/liveVarAnalysisSuite.scala (98%)
 rename src/test/scala/dependentChisel/{ => staticAnalysis}/reachingDefAnalysisSuite.scala (96%)
 rename src/test/scala/dependentChisel/{ => staticAnalysis}/unInitAnalysisSuite.scala (97%)

diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
index 57b92b4..344d222 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
@@ -44,11 +44,9 @@ object reachingDefAnalysis {
   }
 
   def monoFramework(
-  ) = {
-
+  ) =
     MonoFrameworkT(
       transferFn = transferFn,
       lattice = RDLattice
     )
-  }
 }
diff --git a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala
similarity index 98%
rename from src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
rename to src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala
index 52a7478..6959839 100644
--- a/src/test/scala/dependentChisel/liveVarAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala
@@ -1,4 +1,4 @@
-package dependentChisel
+package dependentChisel.staticAnalysis
 
 import com.doofin.stdScalaCross.*
 
diff --git a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala
similarity index 96%
rename from src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
rename to src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala
index acd2c17..d473bc5 100644
--- a/src/test/scala/dependentChisel/reachingDefAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala
@@ -1,4 +1,4 @@
-package dependentChisel
+package dependentChisel.staticAnalysis
 
 import com.doofin.stdScalaCross.*
 
diff --git a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
similarity index 97%
rename from src/test/scala/dependentChisel/unInitAnalysisSuite.scala
rename to src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
index 2d34e7f..e4292e8 100644
--- a/src/test/scala/dependentChisel/unInitAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
@@ -1,4 +1,4 @@
-package dependentChisel
+package dependentChisel.staticAnalysis
 
 import dependentChisel.typesAndSyntax.typesAndOps.*
 import dependentChisel.codegen.sequentialCommands.*

From b282cb9ed587fbd45979f38635f76c1d32233d71 Mon Sep 17 00:00:00 2001
From: doofin <8177dph@gmail.com>
Date: Tue, 3 Feb 2026 20:01:35 +0800
Subject: [PATCH 23/23] fix: Update assertions in unInitAnalysisSuite for
 expected initialization points

---
 .../staticAnalysis/unInitAnalysisSuite.scala                | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
index e4292e8..8755256 100644
--- a/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
+++ b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
@@ -39,13 +39,13 @@ class unInitAnalysisSuite extends munit.FunSuite {
     }.keySet
 
     pp(res)
-    assertEquals(resultInitX, expectedInit, "so x is only initialized at point 1,3,5")
+    assertEquals(resultInitX, expectedInit)
 
-    val expectedInitY = Set(2, 4)
+    val expectedInitY = Set(2, 4, 5)
     val resultInitY = res.filter { case (k, v) =>
       v("y") // filter where y is true
     }.keySet
-    assertEquals(resultInitY, expectedInitY, "so y is only initialized at point 2,4")
+    assertEquals(resultInitY, expectedInitY)
 
   }
 }