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
diff --git a/.scalafmt.conf b/.scalafmt.conf
index c129416..ee12572 100644
--- a/.scalafmt.conf
+++ b/.scalafmt.conf
@@ -1,5 +1,5 @@
 version = "3.10.1"
 runner.dialect = scala3
 maxColumn = 100 # For my wide 30" display.
-runner.dialectOverride.allowSignificantIndentation = false
+# runner.dialectOverride.allowSignificantIndentation = false
 runner.dialectOverride.allowQuietSyntax = true
diff --git a/build.sbt b/build.sbt
index 34dea9d..9ec7441 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,7 @@ resolvers ++= Seq(
   "jitpack" at "https://jitpack.io",
   "Sonatype OSS Snapshots" at "https://oss.sonatype.org/content/repositories/snapshots"
 )
-val mScala3Version = "3.3.3" // "3.3.1-RC1-bin-SNAPSHOT" 3.3.0-RC3
+val mScala3Version = "3.3.7" // "3.3.1-RC1-bin-SNAPSHOT" 3.3.0-RC3
 
 /* To print the code as it is transformed through the compiler, use the compiler flag -Xprint:all
 trace the code that generated the error by adding the -Ydebug-error compiler flag,
@@ -19,13 +19,16 @@ lazy val root = project
     scalaVersion := mScala3Version,
     scalacOptions ++= mScalacOptions,
     libraryDependencies ++= Seq(
+      // typelevel
+      "org.typelevel" %% "cats-core" % catsV,
+      "org.typelevel" %% "cats-free" % catsV,
+      "dev.optics" %% "monocle-core" % "3.3.0",
+      // debugging and printing
       "com.lihaoyi" %% "pprint" % "0.8.1", // print,debug
       "org.scalameta" %% "munit" % "0.7.29" % Test,
       // https://mvnrepository.com/artifact/org.scalatest/scalatest
       "org.scalatest" %% "scalatest" % "3.2.14" % Test,
       "io.bullet" %% "macrolizer" % "0.6.2" % "compile-internal", // print,debug
-      "org.typelevel" %% "cats-core" % catsV,
-      "org.typelevel" %% "cats-free" % catsV,
       "com.github.doofin.stdScala" %% "stdscala" % "b10536c37c", // new : 184b5cbc7d  %%% for cr
       "io.github.iltotore" %% "iron" % "2.1.0",
       ("edu.berkeley.cs" %% "chisel3" % "3.5.5")
diff --git a/src/main/scala/dependentChisel/algo/stackList2tree.scala b/src/main/scala/dependentChisel/algo/stackList2tree.scala
index 3d16f0a..16f4dce 100644
--- a/src/main/scala/dependentChisel/algo/stackList2tree.scala
+++ b/src/main/scala/dependentChisel/algo/stackList2tree.scala
@@ -11,7 +11,8 @@ import dependentChisel.codegen.sequentialCommands.*
 /** algorithm to convert sequential commands to AST in tree structure
   */
 object stackList2tree {
-  type AST = TreeNode[NewInstance | WeakStmt | Ctrl | VarDecls]
+  // 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/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/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/codegen/compiler.scala b/src/main/scala/dependentChisel/codegen/compiler.scala
index 5e81533..ee2633f 100644
--- a/src/main/scala/dependentChisel/codegen/compiler.scala
+++ b/src/main/scala/dependentChisel/codegen/compiler.scala
@@ -166,7 +166,7 @@ object compiler {
         })
       case stmt: WeakStmt    => indent + stmt2firrtlStr(stmt)
       case stmt: NewInstance => newInstStmt2firrtlStr(indent, stmt) + "\n"
-      case stmt: VarDecls =>
+      case stmt: VarDecls    =>
         indent + varDecl2firrtlStr(indent, stmt)
     }
 
@@ -201,7 +201,7 @@ object compiler {
         s"$opName(${expr2firrtlStr(a)})"
       case x: Var[?] =>
         // dbg(x)
-        x.getname
+        x.getName
       case Lit(w) =>
         // h0 means HexLit of 0
         s"""UInt<${w}>("$w")"""
@@ -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 :
@@ -315,7 +315,7 @@ object compiler {
             WeakStmt(
               stmt.lhs,
               ":=",
-              bop.copy(a = VarLit(genStmt.lhs.getname)),
+              bop.copy(a = VarLit(genStmt.lhs.getName)),
               prefix = "node "
             )
           ) ++ resList
@@ -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 = "<="))
@@ -381,8 +381,8 @@ object compiler {
     */
   def varNameTransform(thisInstName: String, v: Var[?]): Var[?] = {
     v match {
-      case x @ VarLit(name) => x
-      case x @ VarDymTyped(width, tp, name) =>
+      case x @ VarLit(name)                => x
+      case x @ VarDynamic(width, tp, name) =>
         tp match {
           case VarType.Input | VarType.Output =>
             x.copy(name = ioNameTransform(thisInstName, name))
@@ -411,7 +411,7 @@ object compiler {
   /** recursively apply expr to expr Transform like varNameTransform */
   def exprTransform(thisInstName: String, e: Expr[?]): Expr[?] = {
     e match {
-      case v: Var[?] => varNameTransform(thisInstName, v)
+      case v: Var[?]   => varNameTransform(thisInstName, v)
       case x: BinOp[w] =>
         BinOp(
           exprTransform(thisInstName, x.a).asInstanceOf[Expr[Nothing]],
diff --git a/src/main/scala/dependentChisel/codegen/sequentialCommands.scala b/src/main/scala/dependentChisel/codegen/sequentialCommands.scala
index 7db02bd..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.
@@ -49,11 +51,14 @@ 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)....
    1.new super type for Var[w]
    */
 
+  /** formal verification commands */
+  case class BoolProp(name: String, prop: Bool) extends AtomicCmds
+
 }
diff --git a/src/main/scala/dependentChisel/codegen/typeCheck.scala b/src/main/scala/dependentChisel/codegen/typeCheck.scala
index e709cc5..0552aa2 100644
--- a/src/main/scala/dependentChisel/codegen/typeCheck.scala
+++ b/src/main/scala/dependentChisel/codegen/typeCheck.scala
@@ -53,7 +53,7 @@ object typeCheck {
             val isWidthOk = isWidthEqu // | lhsGeqRhs
             val msg =
               "[error]".toRed() +
-                s" width mismatch in statement:\n${showPair(lhs.getname, i)}\n " +
+                s" width mismatch in statement:\n${showPair(lhs.getName, i)}\n " +
                 s"$op \n" +
                 s"${showPair(rhs.toString(), j)} "
 
diff --git a/src/main/scala/dependentChisel/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/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..3c90473 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala
@@ -1,73 +1,96 @@
 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]
+  // type level lambda from domain to Map[VarName, domain]
+  type VarMap[domain] = Map[VarName, domain]
 
-  /** usage : give initMap: domainMapT[domain] and baseLattice, then override
-    * transferF(transfer function) .
+  /** enrich the lattice with transfer function and initial mapping
     *
-    * Recommend : create two file named xxAnalysis impl this trait, and xxLattice impl
-    * just lattice
-    * @tparam domain
-    *   domain lattice which satisify acc
+    * tips : create two file named xxAnalysis to implement this trait, and xxLattice to implement
+    * the lattice separately.
+    * @tparam T
+    *   lattice type
     * @tparam stmtT
-    *   type of statement
+    *   statement type
+    * @param transferFn
+    *   transfer function
+    * @param lattice
+    *   lattice over T for the analysis
     */
-  trait MonoFrameworkT[domain, stmtT](
-      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
-    override val lub = liftedLattice.lub
-    override val smallerThan = liftedLattice.smallerThan
+  case class MonoFrameworkT[T, stmtT](
+      val transferFn: ((Int, stmtT, Int), T) => T,
+      // val botMap: VarMap[T],
+      lattice: semiLattice[T]
+  ) {
 
+    /** run the monotone framework on a program graph
+      *
+      * @param progGraph
+      * @param isForward
+      *   true for forward analysis,false for backward analysis
+      * @return
+      */
     def runWithProgGraph(
-        progGraph: List[(Int, stmtT, Int)]
-    ): Map[Int, domainMapT[domain]] =
-      worklistAlgo.wlAlgoMonotone(this, progGraph)
+        progGraph: List[(Int, stmtT, Int)],
+        isForward: Boolean = true,
+        entryExitPoint: (Int, Int)
+    ) = {
+
+      worklistAlgo.onProgGraph(
+        progGraph,
+        transferFn,
+        lattice = lattice,
+        initD = lattice.bottom,
+        entryExitPoint = entryExitPoint,
+        isForward = isForward
+      )
+    }
   }
 
-  extension [domain](lattice: semiLattice[domain]) {
-    def liftWithMap(initMap: domainMapT[domain]) =
-      new semiLattice[domainMapT[domain]] {
-        override val smallerThan: (domainMapT[domain], domainMapT[domain]) => Boolean = {
-          (m1, m2) =>
-            m1 forall { k1 =>
-              // im1 is subset of im2
-              val i1o = k1._2
-              val i2o = m2(k1._1)
+  /** lift semiLattice[t] to semiLattice[VarMap[t]]
+    *
+    * useful for some static analysis like interval analysis, sign analysis
+    */
+  extension [t](base: semiLattice[t]) {
+
+    /** lift semiLattice[t] to semiLattice[VarMap[t]]
+      *
+      * where VarMap[t] represents VarName->t
+      *
+      * @param botMap
+      *   all variable names as bottom element
+      * @return
+      */
+    def liftToVarMap(botMap: VarMap[t]): semiLattice[VarMap[t]] =
+      new semiLattice[VarMap[t]] {
+        override val leq: (VarMap[t], VarMap[t]) => Boolean = { (m1, m2) =>
+          m1 forall { k1 =>
+            // im1 is subset of im2
+            val i1o = k1._2
+            val i2o = m2(k1._1)
 
-              lattice.smallerThan(i1o, i2o)
-            }
+            base.leq(i1o, i2o)
+          }
         }
-        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)
-                (k, rr)
-              }
-            Map(newmap.toSeq*)
+        /*  for lub, take union of keys, for each key do lub on values
+         */
+        override val lub: (VarMap[t], VarMap[t]) => VarMap[t] = { (m1, m2) =>
+          val newmap =
+            (m1.keys ++ m2.keys).toSet map { k =>
+              val i1o = m1(k)
+              val i2o = m2(k)
+              val rr = base.lub(i1o, i2o)
+              (k, rr)
+            }
+          Map(newmap.toSeq*)
         }
 
-        override val bottom: domainMapT[domain] =
-          initMap.map(s => (s._1, lattice.bottom))
+        override val bottom: VarMap[t] =
+          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
deleted file mode 100644
index fba74cd..0000000
--- a/src/main/scala/dependentChisel/staticAnalysis/checkUnInitAnalysis.scala
+++ /dev/null
@@ -1,40 +0,0 @@
-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
-import dependentChisel.codegen.sequentialCommands.WeakStmt
-import dependentChisel.codegen.sequentialCommands.VarDecls
-
-/** check if vars have an value
-  */
-object checkUnInitAnalysis {
-  type mDomain = checkUnInitLattice.domain
-  type mStmt = AtomicCmds // assign,var decls etc
-
-  case class MonoFramework(
-      mInitMap: domainMapT[mDomain]
-  ) extends MonoFrameworkT[mDomain, mStmt](
-        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
deleted file mode 100644
index fba757d..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: (domain, domain) => Boolean = {
-      case (_, true)      => true
-      case (false, false) => true
-      case _              => false
-    }
-
-    override val lub: (domain, domain) => domain = {
-      _ || _
-    }
-
-    override val bottom: domain = false
-
-  }
-
-}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
new file mode 100644
index 0000000..37b83c9
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/liveVarAnalysis.scala
@@ -0,0 +1,71 @@
+package dependentChisel.staticAnalysis
+
+import monocle.*
+
+import dependentChisel.staticAnalysis.MonotoneFramework.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
+
+/** live variable analysis is a backward analysis
+  *
+  * we want to know which variables are live (will be used afterwards) at each program point.
+  *
+  * For example, var x is live at program point p, if there is a path downstream from p that uses x
+  * and x is not re-defined(we consider re-definition as kill)
+  */
+object liveVarAnalysis {
+  type Domain = Set[VarName]
+  type Stmt = AtomicCmds // statements
+
+  /** free var in a expr, which is just all var names
+    */
+  def fv(e: Expr[_]): Set[VarName] = {
+    e match
+      case VarLit(name)    => Set(name)
+      case BinOp(a, b, nm) => fv(a) ++ fv(b)
+      case UniOp(a, nm)    => fv(a)
+      case _               => Set.empty[VarName]
+  }
+
+  def genSetLV(s: Stmt): Set[VarName] = s match
+    case WeakStmt(lhs, op, rhs, prefix) => fv(rhs)
+    case _                              => Set.empty[VarName]
+
+  def killSetLV(s: Stmt): Set[VarName] = s match {
+    case WeakStmt(lhs, op, rhs, prefix) => Set(lhs.getName)
+    case _                              => Set.empty[VarName]
+  }
+
+  /** transfer function for living variable analysis
+    *
+    * Stmt, Lattice => Lattice
+    */
+  def transferLV(ppoint: (Int, Stmt, Int), l: Domain): Domain = {
+    val stmt = ppoint._2
+    val ks = killSetLV(stmt)
+    val gs = genSetLV(stmt)
+    val res = (l -- ks) union gs
+    println(s"tran for $ppoint : in = $l , kill = $ks , gen = $gs , out = $res")
+    res
+  }
+
+  /** lattice for live variable analysis is Set[Var],if a var is in the set, it is live
+    */
+  object liveVarLattice extends semiLattice[Domain] {
+
+    override val leq = (a: Set[VarName], b: Set[VarName]) => a.subsetOf(b)
+
+    override val lub = (a: Set[VarName], b: Set[VarName]) => a.union(b)
+
+    override val bottom = Set.empty[VarName]
+
+  }
+
+  def monoFramework() = {
+
+    MonoFrameworkT(
+      transferFn = transferLV,
+      lattice = liveVarLattice
+    )
+  }
+}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
new file mode 100644
index 0000000..344d222
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/reachingDefAnalysis.scala
@@ -0,0 +1,52 @@
+package dependentChisel.staticAnalysis
+
+import dependentChisel.staticAnalysis.MonotoneFramework.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
+
+/** reaching definitions as a mapping Var -> PowerSet( Q? * Q ) */
+object reachingDefAnalysis {
+  // (x, p, q) means variable x is modified by the edge p->q. (x,?,qi) means x is not modified before initial point qi. Here we don't use ? for simplicity
+  type Domain = Set[(VarName, Int, Int)] // PowerSet( Q? * Q )
+  type Stmt = AtomicCmds // statements
+
+  def transferFn(ppoint: (Int, Stmt, Int), l: Domain): Domain = {
+    val stmt = ppoint._2
+    val gs = genSet(ppoint)
+    val res = stmt match {
+      case WeakStmt(lhs, ":=", rhs, prefix) =>
+        // res = l- kill + gen
+        val killed = l.filter(_._1 != lhs.getName)
+        killed ++ gs
+      case _ => l
+    }
+
+    println(s"tran for $ppoint : in = $l ,  gen = $gs , out = $res")
+    res
+  }
+
+  def genSet(ppoint: (Int, Stmt, Int)): Domain = {
+    val (p, stmt, q) = ppoint
+    stmt match {
+      case WeakStmt(lhs, op, rhs, prefix) =>
+        Set((lhs.getName, p, q))
+      case _ => Set.empty
+    }
+  }
+
+  object RDLattice extends semiLattice[Domain] {
+
+    override val leq = (a: Domain, b: Domain) => a.subsetOf(b)
+
+    override val lub = (a: Domain, b: Domain) => a.union(b)
+
+    override val bottom: Domain = Set.empty
+  }
+
+  def monoFramework(
+  ) =
+    MonoFrameworkT(
+      transferFn = transferFn,
+      lattice = RDLattice
+    )
+}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala
deleted file mode 100644
index 5bc9b42..0000000
--- a/src/main/scala/dependentChisel/staticAnalysis/reachingDefLattice.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-package dependentChisel.staticAnalysis
-
-/** reaching definitions as a mapping Var -> PowerSet( Q? * Q ) */
-object reachingDefLattice {
-  type domain = Set[(Int, Int)] // PowerSet( Q? * Q )
-// domainMap is  Var -> PowerSet( Q? * Q ) uninitializedLattice
-
-  /* For this define Bot to be the mapping that maps each variable to the empty set */
-
-}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/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/staticAnalysis/semiLattice.scala b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
index 11cea47..780b71f 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala
@@ -1,20 +1,29 @@
 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 complete lattice always has a least and greatest element
   *
-  * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered
-  * set such that all finite subsets Y of L have a least upper bound.
+  * 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.
-  * @tparam domain
-  *   satisify acc
+  * The rational number Q with the usual linear order, is an distributive lattice which is not
+  * complete, while the real number R is complete.
+  *
+  * @tparam t
   */
-trait semiLattice[domain] {
-  val smallerThan: (domain, domain) => Boolean // partial ordering
-  val lub: (domain, domain) => domain // least upper bound
-  val bottom: domain
+trait semiLattice[t] {
+
+  /** partial ordering, less than or equal to
+    */
+  val leq: (t, t) => Boolean
+
+  /** least upper bound
+    */
+  val lub: (t, t) => t // least upper bound
+
+  /** least element, bottom
+    */
+  val bottom: t
 }
diff --git a/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc b/src/main/scala/dependentChisel/staticAnalysis/test.worksheet.sc
deleted file mode 100644
index b2d4911..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*
-  )
-
-/*
-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/unInitAnalysis.scala b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
new file mode 100644
index 0000000..39cefe9
--- /dev/null
+++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala
@@ -0,0 +1,54 @@
+package dependentChisel.staticAnalysis
+
+import dependentChisel.staticAnalysis.MonotoneFramework.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.typesAndSyntax.typesAndOps.*
+
+/** check if vars have an value
+  */
+object unInitAnalysis {
+  type Domain = VarMap[Boolean]
+  type Stmt = AtomicCmds // statements
+
+  val transferF: ((Int, Stmt, Int), Domain) => Domain = { 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 _ => varmap
+    }
+  }
+
+  /** lattice for uninitialized analysis is Var->Boolean where false means uninitialized
+    *
+    * we first define a simple boolean lattice and later lift it to Var->Boolean lattice
+    */
+  object unInitLattice extends semiLattice[Boolean] {
+
+    override val leq = {
+      case (_, true)      => true
+      case (false, false) => true
+      case _              => false
+    }
+
+    override val lub = {
+      _ || _
+    }
+
+    override val bottom = false
+
+  }
+
+  def monoFramework(
+      mBotMap: Domain
+  ) = {
+    // lift the boolean lattice to Var->Boolean lattice
+    val lifted: semiLattice[VarMap[Boolean]] =
+      unInitLattice.liftToVarMap(mBotMap)
+
+    MonoFrameworkT(
+      transferFn = transferF,
+      lattice = lifted
+    )
+  }
+}
diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
index 7a418aa..2730925 100644
--- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
+++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala
@@ -4,6 +4,7 @@ import com.doofin.stdScalaJvm.*
 import scala.collection.{immutable, mutable}
 
 import MonotoneFramework.*
+import chisel3.util.is
 
 object worklistAlgo {
   trait Worklist[t] {
@@ -26,49 +27,57 @@ object worklistAlgo {
     override def isEmpty: Boolean = as.isEmpty
   }
 
-  def wlAlgoMonotone[domainT, stmtT](
-      mf: MonoFrameworkT[domainT, stmtT],
-      progGraph: List[(Int, stmtT, Int)]
-  ) = {
-
-    wlAlgoProgGraphP[domainMapT[domainT], stmtT](
-      progGraph,
-      mf.transferF,
-      mf.smallerThan,
-      mf.lub,
-      mf.initMap,
-      mf.bottom
-    )
-  }
-
-  private def wlAlgoProgGraphP[domainT, stmtT](
-      progGraph: List[(Int, stmtT, Int)],
-      transferF: ((Int, stmtT, Int), domainT) => domainT,
-      smallerThan: (domainT, domainT) => Boolean,
-      lubOp: (domainT, domainT) => domainT,
-      initD: domainT,
-      bottomD: domainT,
-      isReverse: Boolean = false
-  ): Map[Int, domainT] = {
+  /** worklist algorithm on program graph
+    *
+    * @param progGraph_
+    * @param transferF
+    * @param smallerThan
+    * @param lubOp
+    * @param initD
+    *   for program point 0 if it's forward analysis, or exiting point if backward analysis
+    * @param bottomD
+    *   for other program points
+    * @param entryExitPoint
+    *   the (entry, exit) program points. forward analysis only use entry point, backward analysis
+    *   only use exit
+    * @param isForward
+    *   true for forward analysis,false for backward analysis
+    * @return
+    */
+  def onProgGraph[T, stmtT](
+      progGraph_ : List[(Int, stmtT, Int)],
+      transferFn: ((Int, stmtT, Int), T) => T,
+      lattice: semiLattice[T],
+      initD: T,
+      entryExitPoint: (Int, Int),
+      isForward: Boolean = true
+  ): Map[Int, T] = {
 
     val mutList: Worklist[Int] = new WlStack()
 
-    pp(progGraph)
-//    get program points from edges,ignore stmt in (Int, Stmt, Int)
+    //  for backward analysis just reverse the edges and swap entry exit (or init final)
+    val progGraph =
+      if isForward then progGraph_
+      else progGraph_.map { case (a, st, c) => (c, st, a) }
+
+    val (entryPoint, exitPoint) =
+      if isForward then entryExitPoint else (entryExitPoint._2, entryExitPoint._1)
+
+    // pp(progGraph)
+    //    get program points
     val progPoints = progGraph.flatMap(x => List(x._1, x._3)).distinct
 
-//    initialise work list
     mutList.insertAll(progPoints)
 
-    val resMapMut: mutable.Map[Int, domainT] = mutable.Map()
+    val resMapMut: mutable.Map[Int, T] = mutable.Map()
 
 //    initialize at each program points,set to init for point 0 (first loop)
     progPoints foreach { q =>
-      resMapMut(q) = if (q == 0) initD else bottomD
+      resMapMut(q) = if (q == 0) then initD else lattice.bottom
     }
 
-//    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
@@ -82,11 +91,11 @@ object worklistAlgo {
       progGraphTups foreach { case tup @ (pre, stmtT, post) =>
         val preMap = resMapMut(pre)
         val postMap = resMapMut(post) // AA(q dot)
-        val preMapTransfered = transferF(tup, preMap)
+        val preMapTransfered = transferFn(tup, preMap)
 
 //          update if preMapAnalysised >=  postMap (not <=)
 //        println("doUpdate:", subOrderOp, preMapTransfered, postMap) // subOrderOp can be null
-        val doUpdate = !smallerThan(preMapTransfered, postMap)
+        val doUpdate = !lattice.leq(preMapTransfered, postMap)
 
 //        println(s"doUpdate if presetF ${pre} notSubOrder postset ${post}:: at ${post}", doUpdate)
 //          pp(preMapTransfered, s"preSetF f(${pre}):")
@@ -94,7 +103,7 @@ object worklistAlgo {
 
         if (doUpdate) {
 
-          val lubR = lubOp(postMap, preMapTransfered)
+          val lubR = lattice.lub(postMap, preMapTransfered)
 //            pp(lubR, "lub : ")
           resMapMut(post) = lubR
 //            wlMut += post
@@ -104,7 +113,7 @@ object worklistAlgo {
         }
       }
     }
-    println(s"iter step : ${steps}")
+    println(s"worklist algo finished in $steps steps")
     resMapMut.toMap
   }
 }
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
index 4b7741b..e094443 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/chiselModules.scala
@@ -16,11 +16,14 @@ 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
 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/main/scala/dependentChisel/typesAndSyntax/varDecls.scala b/src/main/scala/dependentChisel/typesAndSyntax/circuitDecls.scala
similarity index 94%
rename from src/main/scala/dependentChisel/typesAndSyntax/varDecls.scala
rename to src/main/scala/dependentChisel/typesAndSyntax/circuitDecls.scala
index 9254919..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")
@@ -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
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/statements.scala b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
index 1b9f7ca..8f9ba3d 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/statements.scala
@@ -18,11 +18,28 @@ 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) {
 
     inline def :=(using md: ModuleData)(oth: Expr[w]) = {
-      val name = v.getname
+      val name = v.getName
 
       /* v match {
         case VarLit(name) =>
@@ -32,18 +49,18 @@ object statements {
       // dbg(v)
       // dbg(oth)
       // mli.typeMap.addOne(v, constValueOpt[w].get)
-      md.commands += WeakStmt(v, ":=", oth)
+      appendCmdToModule(WeakStmt(v, ":=", oth))
     }
 
   }
 
   /** untyped API for assign */
-  extension (v: VarDymTyped) {
+  extension (v: VarDynamic) {
     inline def :=(using md: ModuleData)(oth: Expr[?]) = {
-      val name = v.getname
+      val name = v.getName
       md.typeMap.addOne(v, v.width)
 
-      md.commands += WeakStmt(v, ":=", oth)
+      appendCmdToModule(WeakStmt(v, ":=", oth))
     }
   }
 }
diff --git a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
index 750135a..0b32d90 100644
--- a/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
+++ b/src/main/scala/dependentChisel/typesAndSyntax/typesAndOps.scala
@@ -13,34 +13,38 @@ 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
 represent a vector of bits */
 
+  sealed trait Expr[w <: Int] {
+    def asUnTyped = this.asInstanceOf[Expr[Nothing]]
+    inline def asTypedUnsafe[w <: Int] = {
+      this.asInstanceOf[Expr[w]]
+    }
+  }
+
   /* mutable vars which can be mutated in lhs, incl input,output */
   sealed trait Var[w <: Int](name: String) extends Expr[w] {
-    def getname = name
+    def getName = name
     // def getIsIO = isIO
   }
 
+  /** declare a variable like: WeakStmt(VarLit(newValue), ":=", a)
+    *
+    * @param name
+    */
   case class VarLit[w <: Int](name: String) extends Var[w](name)
 
-  sealed trait Expr[w <: Int] {
-    def asUnTyped = this.asInstanceOf[Expr[Nothing]]
-    inline def asTypedUnsafe[w <: Int] = {
-      this.asInstanceOf[Expr[w]]
-    }
-  }
+  // binary op like add,sub,and,or
   case class BinOp[w <: Int](a: Expr[w], b: Expr[w], nm: String) extends Expr[w]
 
   // to prevent overflow like AFix in spinalHDL
-  case class MulOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul")
-      extends Expr[2 * w]
+  case class MulOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul") extends Expr[2 * w]
 
-  case class AddOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul")
-      extends Expr[w + 1]
+  case class AddOp[w <: Int](a: Expr[w], b: Expr[w], nm: String = "mul") extends Expr[w + 1]
 
   /** uniary op like negate */
   case class UniOp[w <: Int](a: Expr[w], nm: String) extends Expr[w]
@@ -67,8 +71,7 @@ represent a vector of bits */
   // new ExprC[1, VarDeclTp.Reg.type] {} + new ExprC[1, VarDeclTp.Wire.type] {} //ok ,will fail
 
   /** untyped API for Wire, Reg, and IO */
-  case class VarDymTyped(width: Int, tp: VarType, name: String)
-      extends Var[Nothing](name) {
+  case class VarDynamic(width: Int, tp: VarType, name: String) extends Var[Nothing](name) {
 
     /** dym check for type cast */
     inline def asTyped[w <: Int] = {
@@ -93,7 +96,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)
@@ -103,7 +106,7 @@ represent a vector of bits */
   // for future use
 
 // case class Lit[w <: Int](i: w, name: String) extends Expr[w] {}
-  type sml[w <: Int] <: w ^ 2
+  // type sml[w <: Int] <: w ^ 2
   case class Lit[w <: Int](i: w) extends Expr[w] {}
   case class LitDym(i: Int, width: Int) extends Expr[Nothing]
   /*
diff --git a/src/test/scala/dependentChisel/astTransformSuite.scala b/src/test/scala/dependentChisel/astTransformSuite.scala
new file mode 100644
index 0000000..1a27f67
--- /dev/null
+++ b/src/test/scala/dependentChisel/astTransformSuite.scala
@@ -0,0 +1,52 @@
+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
+import dependentChisel.global.mPPrint
+
+/* more tests for parameterized mod*/
+class astTransformSuite extends AnyFunSuite {
+  test("tree AST transform works") {
+    val m = makeModule({ implicit p =>
+      new adder.Adder1prop
+    })
+
+    mPPrint(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)
+      }
+
+    mPPrint(newAst)
+    assert(newAst.children.length == 1, "filtered AST should have only 1 assertion")
+  }
+
+}
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 e394892..77727bb 100644
--- a/src/test/scala/dependentChisel/examples/adder.scala
+++ b/src/test/scala/dependentChisel/examples/adder.scala
@@ -10,11 +10,11 @@ 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 {
 
@@ -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).here
+  }
 }
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 {
diff --git a/src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala
new file mode 100644
index 0000000..6959839
--- /dev/null
+++ b/src/test/scala/dependentChisel/staticAnalysis/liveVarAnalysisSuite.scala
@@ -0,0 +1,89 @@
+package dependentChisel.staticAnalysis
+
+import com.doofin.stdScalaCross.*
+
+import dependentChisel.typesAndSyntax.typesAndOps.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.staticAnalysis.liveVarAnalysis
+
+class liveVarAnalysisSuite extends munit.FunSuite {
+  test("test free variable function") {
+    val expr = VarLit("x") + VarLit("y") + Lit[8](8)
+    val expr2 = UniOp(expr + VarLit("z"), "neg")
+
+    val fvResult = liveVarAnalysis.fv(expr2)
+    val expectedFv = Set("x", "y", "z")
+    assertEquals(fvResult, expectedFv, "free var should be x,y,z")
+  }
+
+  test("live variable transfer function test") {
+
+    // r:= r - y
+    val stmt1 = (0, WeakStmt(VarLit("r"), ":=", VarLit("r") - VarLit("y")), 1)
+    // {}-{r}+{r,y} = {r,y} for l-kill + gen
+    val t1 = liveVarAnalysis.transferLV(stmt1, Set())
+    assertEquals(t1, Set("r", "y"), "after r:=r - y , r and y should be live ")
+
+    val stmt2 = (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1)
+
+    // x should be dead after assignment
+    val t2 = liveVarAnalysis.transferLV(stmt2, Set("x", "y"))
+    assertEquals(t2, Set("y"), "after x:=1, x should be dead ")
+
+    // pp(res)
+
+  }
+
+  test("live variable analysis full test") {
+
+    val pg =
+      List(
+        (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1),
+        (1, Skip, 3),
+        (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2),
+        (2, WeakStmt(VarLit("y"), ":=", VarLit("y") + Lit[1](1)), 4),
+        (3, WeakStmt(VarLit("z"), ":=", VarLit("x") + VarLit("y") + Lit[1](1)), 5),
+        (4, Skip, 5)
+      )
+
+    val entryExitPoint = (0, 5)
+    /*
+    ASCII visualization:
+
+                0
+             /    \
+          (x:=1)   (y:=1)
+           |         \
+           v          v
+           1          2
+           |          | (y:=y+1)
+           v          v
+           3          4
+           |
+      (z:=x+y+1)   /
+           |      /
+           v     /
+          
+           5
+     */
+    val monoF = liveVarAnalysis.monoFramework()
+
+    // live variable analysis is a backward analysis
+    val res = monoF.runWithProgGraph(
+      pg, //
+      isForward = false,
+      entryExitPoint
+    )
+
+    val expected = Map(
+      0 -> Set("y"),
+      5 -> Set(),
+      1 -> Set("x", "y"),
+      2 -> Set("y"),
+      3 -> Set("x", "y"),
+      4 -> Set()
+    )
+    assertEquals(res, expected)
+
+  }
+}
diff --git a/src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala
new file mode 100644
index 0000000..d473bc5
--- /dev/null
+++ b/src/test/scala/dependentChisel/staticAnalysis/reachingDefAnalysisSuite.scala
@@ -0,0 +1,37 @@
+package dependentChisel.staticAnalysis
+
+import com.doofin.stdScalaCross.*
+
+import dependentChisel.typesAndSyntax.typesAndOps.*
+import dependentChisel.codegen.sequentialCommands.*
+import dependentChisel.staticAnalysis.reachingDefAnalysis
+
+class reachingDefAnalysisSuite extends munit.FunSuite {
+
+  // program graph in PA appetizer,p17 and example 2.2 at p18
+  val pg1 =
+    List(
+      (0, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 1),
+      (1, Skip, 2),
+      (2, WeakStmt(VarLit("y"), ":=", VarLit("x") + VarLit("y")), 3),
+      (3, WeakStmt(VarLit("x"), ":=", VarLit("x") - Lit[1](1)), 1),
+      (1, Skip, 4)
+    )
+  test("reaching definition full test") {
+    val initMap: reachingDefAnalysis.Domain = Set.empty
+    val t1 = reachingDefAnalysis.transferFn(pg1(0), initMap)
+
+    val mono = reachingDefAnalysis.monoFramework()
+    val res = mono.runWithProgGraph(pg1, isForward = true, entryExitPoint = (0, 4))
+
+    // from 2.12 p21, the result of Example 2.2
+    val expected = Map(
+      0 -> Set(),
+      1 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),
+      2 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1)),
+      3 -> Set(("y", 2, 3), ("x", 3, 1)),
+      4 -> Set(("y", 0, 1), ("y", 2, 3), ("x", 3, 1))
+    )
+    assertEquals(res, expected)
+  }
+}
diff --git a/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
new file mode 100644
index 0000000..8755256
--- /dev/null
+++ b/src/test/scala/dependentChisel/staticAnalysis/unInitAnalysisSuite.scala
@@ -0,0 +1,51 @@
+package dependentChisel.staticAnalysis
+
+import dependentChisel.typesAndSyntax.typesAndOps.*
+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*
+      )
+    val initFinal = (0, 5)
+    /* 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, WeakStmt(VarLit("y"), ":=", Lit[1](1)), 2), // x is not init from 0->2, y yes
+        (2, Skip, 4), // x not, y yes
+        (3, Skip, 5), // x is initialized from 0->1->3->5
+        (4, Skip, 5)
+      )
+    val monoF = unInitAnalysis.monoFramework(initMap)
+
+    val res = monoF.runWithProgGraph(pg, entryExitPoint = initFinal)
+    val expectedInit = Set(1, 3, 5)
+    val resultInitX = res.filter { case (k, v) =>
+      v("x") // filter where x is true
+    }.keySet
+
+    pp(res)
+    assertEquals(resultInitX, expectedInit)
+
+    val expectedInitY = Set(2, 4, 5)
+    val resultInitY = res.filter { case (k, v) =>
+      v("y") // filter where y is true
+    }.keySet
+    assertEquals(resultInitY, expectedInitY)
+
+  }
+}