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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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/13] 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")
+
+  }
+}