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/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..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..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/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..66edf43 100644 --- a/src/main/scala/dependentChisel/staticAnalysis/MonotoneFramework.scala +++ b/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)) } } } 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/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..7e9fede 100644 --- a/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala +++ b/src/main/scala/dependentChisel/staticAnalysis/semiLattice.scala @@ -1,19 +1,20 @@ package dependentChisel.staticAnalysis -/** a complete lattice is a partially ordered set in which all subsets have both - * a supremum (join) and an infimum (meet). +/** a complete lattice is a partially ordered set in which all subsets have both a supremum (join) + * and an infimum (meet). * * A complete lattice always hasa least and greatest element * - * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered - * set such that all finite subsets Y of L have a least upper bound. + * A pointed semi-lattice (or upper semilattice) (L, <=) is a partially ordered set such that all + * finite subsets Y of L have a least upper bound. * - * The set Q of all rational numbers, with the usual linear order, is an - * infinite distributive lattice which is not complete. + * The set Q of all rational numbers, with the usual linear order, is an infinite distributive + * lattice which is not complete. * @tparam domain * satisify acc */ trait semiLattice[domain] { + type mDomain = domain val smallerThan: (domain, domain) => Boolean // partial ordering val lub: (domain, domain) => domain // least upper bound val bottom: domain 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..5fe9019 --- /dev/null +++ b/src/main/scala/dependentChisel/staticAnalysis/unInitAnalysis.scala @@ -0,0 +1,70 @@ +package dependentChisel.staticAnalysis + +import dependentChisel.codegen.sequentialCommands.AtomicCmds +import dependentChisel.staticAnalysis.MonotoneFramework.domainMapT + +import dependentChisel.staticAnalysis.MonotoneFramework.MonoFrameworkT +import dependentChisel.codegen.sequentialCommands.NewInstance +import dependentChisel.codegen.sequentialCommands.WeakStmt +import dependentChisel.codegen.sequentialCommands.VarDecls +import dependentChisel.typesAndSyntax.typesAndOps.VarLit +import dependentChisel.typesAndSyntax.typesAndOps.BinOp +import dependentChisel.typesAndSyntax.typesAndOps.MulOp +import dependentChisel.typesAndSyntax.typesAndOps.AddOp +import dependentChisel.typesAndSyntax.typesAndOps.UniOp +import dependentChisel.typesAndSyntax.typesAndOps.VarDynamic +import dependentChisel.typesAndSyntax.typesAndOps.VarTyped +import dependentChisel.typesAndSyntax.typesAndOps.Lit +import dependentChisel.typesAndSyntax.typesAndOps.LitDym + +/** check if vars have an value + */ +object unInitAnalysis { + type mDomain = checkUnInitLattice.mDomain // which is Boolean + type mStmt = AtomicCmds // statements + + val transferF: ((Int, mStmt, Int), domainMapT[mDomain]) => domainMapT[mDomain] = { + case ((q0, cmd, q1), varmap) => + cmd match { + case WeakStmt(lhs, op, rhs, prefix) => + rhs match + case VarLit(name) => + case BinOp(a, b, nm) => + case MulOp(a, b, nm) => + case AddOp(a, b, nm) => + case UniOp(a, nm) => + case VarDynamic(width, tp, name) => + case VarTyped(name, tp) => + case Lit(i) => + case LitDym(i, width) => + + // any assignment makes var initialized + if op == ":=" then varmap.updated(lhs.getname, true) else varmap + case _ => varmap + } + } + + object checkUnInitLattice extends semiLattice[Boolean] { + + override val smallerThan = { + case (_, true) => true + case (false, false) => true + case _ => false + } + + override val lub = { + _ || _ + } + + override val bottom = false + + } + + def mMonoFramework( + mBotMap: domainMapT[mDomain] + ) = new MonoFrameworkT[mDomain, mStmt]( + transferF, + mBotMap, + checkUnInitLattice + ) {} +} diff --git a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala index 7a418aa..f4449e0 100644 --- a/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala +++ b/src/main/scala/dependentChisel/staticAnalysis/worklistAlgo.scala @@ -26,6 +26,15 @@ object worklistAlgo { override def isEmpty: Boolean = as.isEmpty } + /** worklist algorithm for monotone framework + * @param mf + * monotone framework + * @param progGraph + * program graph as list of (src point,stmt,tgt point) + * + * @return + * mapping from program point to domainMap at that point + */ def wlAlgoMonotone[domainT, stmtT]( mf: MonoFrameworkT[domainT, stmtT], progGraph: List[(Int, stmtT, Int)] @@ -36,11 +45,13 @@ object worklistAlgo { mf.transferF, mf.smallerThan, mf.lub, - mf.initMap, + mf.botMap, mf.bottom ) } + /** worklist algorithm implementation for program graph + */ private def wlAlgoProgGraphP[domainT, stmtT]( progGraph: List[(Int, stmtT, Int)], transferF: ((Int, stmtT, Int), domainT) => domainT, @@ -54,10 +65,9 @@ object worklistAlgo { val mutList: Worklist[Int] = new WlStack() pp(progGraph) -// get program points from edges,ignore stmt in (Int, Stmt, Int) + // get program points val progPoints = progGraph.flatMap(x => List(x._1, x._3)).distinct -// initialise work list mutList.insertAll(progPoints) val resMapMut: mutable.Map[Int, domainT] = mutable.Map() @@ -67,8 +77,8 @@ object worklistAlgo { resMapMut(q) = if (q == 0) initD else bottomD } -// pp(resMapMut.toMap, "init resMap : ") - // second loop,keep applying transferF to program graph until the node value is stable + // keep applying transferF to program graph until the node value is stable + // according to the ascending order property, this will terminate var steps = 0 while (!mutList.isEmpty) { steps += 1 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..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,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 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..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 @@ -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/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/unInitAnalysisSuite.scala b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala new file mode 100644 index 0000000..59159fb --- /dev/null +++ b/src/test/scala/dependentChisel/unInitAnalysisSuite.scala @@ -0,0 +1,45 @@ +package dependentChisel + +import dependentChisel.typesAndSyntax.typesAndOps.Lit +import dependentChisel.typesAndSyntax.typesAndOps.VarLit +import dependentChisel.codegen.sequentialCommands.* +import dependentChisel.staticAnalysis.unInitAnalysis + +import com.doofin.stdScalaCross.* + +class unInitAnalysisSuite extends munit.FunSuite { + test("unInitAnalysis test") { + + // each var is uninitialized at the beginning + val initMap: Map[String, Boolean] = + Map( + "xyz".toCharArray + .map(x => x.toString() -> false) + .toList* + ) + + /* a program graph +0 -> x:=.. ->1 -> 3 -> 5 +0 -> 2 -> 4 + */ + val pg = + List( + (0, WeakStmt(VarLit("x"), ":=", Lit[1](1)), 1), + (1, Skip, 3), // x is initialized from 0->1->3 + (0, Skip, 2), // x is not initialized from 0->2 + (2, Skip, 4), // x is not initialized from 0->2->4 + (3, Skip, 5) // x is initialized from 0->1->3->5 + ) + val monoF = unInitAnalysis.mMonoFramework(initMap) + + val res = monoF.runWithProgGraph(pg) + val expectedInit = Set(1, 3, 5) + val resultInit = res.filter { case (k, v) => + v("x") // filter where x is true + }.keySet + + pp(res) + assertEquals(resultInit, expectedInit, "so x is only initialized at point 1,3,5") + + } +}