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 1/8] 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 2/8] 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 3/8] 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 4/8] 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 5/8] 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 6/8] 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 7/8] 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 8/8] 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 =>