tree traverse

.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

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 _ =>

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)
+  }
 }

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.*

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))

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
+
 }

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) }
 }

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

src/main/scala/dependentChisel/monadic/monadicAST.scala → 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],

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 = {

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 {

src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala

@@ -1,35 +1,36 @@
 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 domainMapT[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
+    * 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],
+      val transferF: ((Int, stmtT, Int), domainMapT[domain]) => domainMapT[domain],
+      val botMap: domainMapT[domain],
       baseLattice: semiLattice[domain]
   ) extends semiLattice[domainMapT[domain]] {
     // type domainMap = Map[String, domain] // var name to domain
 
-    /** 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)
+    // lift domain to domainMap[domain] lattice
+    val liftedLattice = baseLattice.liftWithMap(botMap)
     override val bottom: domainMapT[domain] = liftedLattice.bottom
     override val lub = liftedLattice.lub
     override val smallerThan = liftedLattice.smallerThan
@@ -40,8 +41,19 @@ object MonotoneFramework {
       worklistAlgo.wlAlgoMonotone(this, progGraph)
   }
 
-  extension [domain](lattice: semiLattice[domain]) {
-    def liftWithMap(initMap: domainMapT[domain]) =
+  /** lift any t to string->t semiLattice
+    *
+    * that is, for t:SemiLattice, the function space String->t is also a SemiLattice
+    */
+  extension [domain](base: semiLattice[domain]) {
+
+    /** lift the t:lattice to string->t lattice (function space)
+      *
+      * @param botMap
+      *   the bottom element mapping, since we need to know var names
+      * @return
+      */
+    def liftWithMap(botMap: domainMapT[domain]): semiLattice[domainMapT[domain]] =
       new semiLattice[domainMapT[domain]] {
         override val smallerThan: (domainMapT[domain], domainMapT[domain]) => Boolean = {
           (m1, m2) =>
@@ -50,24 +62,25 @@ object MonotoneFramework {
               val i1o = k1._2
               val i2o = m2(k1._1)
 
-              lattice.smallerThan(i1o, i2o)
+              base.smallerThan(i1o, i2o)
             }
         }
-        override val lub
-            : (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
+        /*  for lub, take union of keys, for each key do lub on values
+         */
+        override val lub: (domainMapT[domain], domainMapT[domain]) => domainMapT[domain] = {
           (m1, m2) =>
             val newmap =
               (m1.keys ++ m2.keys).toSet map { k =>
                 val i1o = m1(k)
                 val i2o = m2(k)
-                val rr = lattice.lub(i1o, i2o)
+                val rr = base.lub(i1o, i2o)
                 (k, rr)
               }
             Map(newmap.toSeq*)
         }
 
         override val bottom: domainMapT[domain] =
-          initMap.map(s => (s._1, lattice.bottom))
+          botMap.map(s => (s._1, base.bottom))
       }
   }
 }