From 9d2bd201f8a1995ccda80a56daf42aeed76482c2 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 12:50:53 -0700 Subject: [PATCH 01/11] Updated scala version --- build.sbt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.sbt b/build.sbt index e04501c..4e60345 100644 --- a/build.sbt +++ b/build.sbt @@ -2,7 +2,7 @@ organization := "edu.berkeley.cs" name := "chiselucl" version := "0.2-SNAPSHOT" -scalaVersion := "2.12.7" +scalaVersion := "2.12.11" addCompilerPlugin("org.scalamacros" % "paradise" % "2.1.1" cross CrossVersion.full) //crossScalaVersions := Nil From 5277d24ad8fc45156e464c351d57f1866cb581be Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 13:24:07 -0700 Subject: [PATCH 02/11] Reorganized project structure --- .gitignore | 7 ++++++- .../chisel/AdderExample.scala | 3 +++ examples/firrtl/.RocketCore.fir.swp | Bin 0 -> 16384 bytes .../examples => examples}/firrtl/Adder.fir | 0 .../firrtl/AsyncResetTester.fir | 0 .../firrtl/ChirrtlMems.fir | 0 .../firrtl/CustomTransform.fir | 0 .../firrtl/DecoupledGCD.fir | 0 .../firrtl/EmptyChirrtlMem.fir | 0 .../firrtl/ExpandWhens.fir | 0 .../examples => examples}/firrtl/FPU.fir | 0 .../examples => examples}/firrtl/GCDTester.fir | 0 .../firrtl/HasDeadCode.fir | 0 .../examples => examples}/firrtl/HasLoops.fir | 0 .../firrtl/HwachaSequencer.fir | 0 .../examples => examples}/firrtl/ICache.fir | 0 .../examples => examples}/firrtl/ICache.lo.fir | 0 .../firrtl/LargeParamTester.fir | 0 .../examples => examples}/firrtl/Legalize.fir | 0 .../examples => examples}/firrtl/MemTester.fir | 0 .../firrtl/MultiExtModuleTester.fir | 0 .../firrtl/NestedSubAccessTester.fir | 0 .../examples => examples}/firrtl/NodeType.fir | 0 .../firrtl/ParameterizedExtModuleTester.fir | 0 .../examples => examples}/firrtl/PipeTester.fir | 0 .../examples => examples}/firrtl/Printf.fir | 0 .../firrtl/RenamedExtModuleTester.fir | 0 .../firrtl/RightShiftTester.fir | 0 .../examples => examples}/firrtl/Rob.fir | 0 .../examples => examples}/firrtl/RocketCore.fir | 0 .../firrtl/RocketCore.lo.fir | 0 .../firrtl/SimpleExtModuleTester.fir | 0 .../examples => examples}/firrtl/Trivial.fir | 0 .../firrtl/ZeroPortMem.fir | 0 .../firrtl/ZeroWidthMem.fir | 0 .../{backend => transforms}/RemoveTail.scala | 2 ++ .../SimplyRegUpdate.scala | 2 ++ .../{backend => transforms}/UclidEmitter.scala | 4 ++-- src/main/scala/chiselucl/uclid/package.scala | 3 ++- 39 files changed, 17 insertions(+), 4 deletions(-) rename {src/main/scala/chiselucl/examples => examples}/chisel/AdderExample.scala (85%) create mode 100644 examples/firrtl/.RocketCore.fir.swp rename {src/main/scala/chiselucl/examples => examples}/firrtl/Adder.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/AsyncResetTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ChirrtlMems.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/CustomTransform.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/DecoupledGCD.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/EmptyChirrtlMem.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ExpandWhens.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/FPU.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/GCDTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/HasDeadCode.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/HasLoops.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/HwachaSequencer.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ICache.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ICache.lo.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/LargeParamTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/Legalize.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/MemTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/MultiExtModuleTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/NestedSubAccessTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/NodeType.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ParameterizedExtModuleTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/PipeTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/Printf.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/RenamedExtModuleTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/RightShiftTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/Rob.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/RocketCore.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/RocketCore.lo.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/SimpleExtModuleTester.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/Trivial.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ZeroPortMem.fir (100%) rename {src/main/scala/chiselucl/examples => examples}/firrtl/ZeroWidthMem.fir (100%) rename src/main/scala/chiselucl/{backend => transforms}/RemoveTail.scala (94%) rename src/main/scala/chiselucl/{backend => transforms}/SimplyRegUpdate.scala (96%) rename src/main/scala/chiselucl/{backend => transforms}/UclidEmitter.scala (99%) diff --git a/.gitignore b/.gitignore index 18173d7..acefae4 100644 --- a/.gitignore +++ b/.gitignore @@ -49,6 +49,10 @@ channel_info .project +# Metals Stuff +.bloop +.metals + # sbt specific .cache .history @@ -59,13 +63,14 @@ lib_managed/ src_managed/ project/boot/ project/plugins/project/ +project/metals.sbt .idea/ gen/ project/project/ /bin/ # include FIRRTL examples -!src/main/scala/chiselucl/examples/firrtl/* +!examples/firrtl/* *~ diff --git a/src/main/scala/chiselucl/examples/chisel/AdderExample.scala b/examples/chisel/AdderExample.scala similarity index 85% rename from src/main/scala/chiselucl/examples/chisel/AdderExample.scala rename to examples/chisel/AdderExample.scala index 76e301f..4545d81 100644 --- a/src/main/scala/chiselucl/examples/chisel/AdderExample.scala +++ b/examples/chisel/AdderExample.scala @@ -11,9 +11,12 @@ class Adder extends Module { val sum = Output(UInt(4.W)) }) + val revert = io.sum - io.b + io.sum := io.a + io.b Assume(io.a > 1.U, "a_bigger_than_one") Assert(io.sum > io.b, "output_bigger") + Assert(revert =/= 0.U, "nonsense") } object AdderModel extends App { diff --git a/examples/firrtl/.RocketCore.fir.swp b/examples/firrtl/.RocketCore.fir.swp new file mode 100644 index 0000000000000000000000000000000000000000..1e31b0fb94c2409d3b0a006006f52bdaa47e77ce GIT binary patch literal 16384 zcmeI(TWl0n90u?aL`6h}q9B;KtuGL}-JRWTcUvni)M%=KVAD1sie%hf%VxJbbuU1C zfEQ!pizW(Qzzd*&sDPlLRYXzoE{a?fyl@q?6};dDyr0?q{lnVN0+1ZpYo5&@sY;1-vZ`C_BGkDR3hJCXA@QG$jOJORVSbmFoqhz zfLXlMFRdu|lnrmundk&`0y+VmfKEUspcBvu=mc~E|Dy!*9qq{ECO-i;aeOoy zO8eu~{yOqs$>)&&LiN{>{|vtp{qHCL30@5^N3i&qaSUDyZz2B?9){mV{sYzDO#VI9 zKSBN-Jc{~(fu%PxzN6HCmi!3$3i5Bs_mX#$kHkWi{=482jBhgeH{^Gae+{og`;Fv> z;ZgW;@o?*2c8k4OD_ z@=xG$ecndC6E5p-75NUhoc}}Q+u`!_ZOmZz__o1iev`;QruMg!Z-vYF){}n(m-!tf z|B$@mZ1?!Kz-4{5l79e~`Q1(aKKUl{_o)6c@^|5~ekzB!$M+7r9_Kej{x)3J|8nxT z$oG-I377RV<{Wqbo8fYOOeKE#WWuOweVet`T5xU9d6 z%G~2y4wvhmz0(Q&rwLeb!3t$ z`tx@6+5lVZxZZREIsu)4PCzH16VM6h1atyA0iA$OKqsIRI7JC~)RxS26!ISDSLXAc zI!{YuCSPxkH+m$de!)Jaq`}#%i%DzKXt16edigtSG^9ZXXy*ot4X~EtJfZUeixqcpQ4HDvN{2sfKEUspcBvu=mc~E zIsu)4PCzHnuLPXCLv<^tZXWF_Tird@dp*;er<;*bttWazQ)@$2@&8wQ%$i`G8JJf5 zWX6ss{{7Gup7z4*u}+gvC{kHG9QFrGZz7@KI8|ke6-!xd38_@uSD~P%r%>1opinrB zLe=4Z7OD>SE)=Ojd()IcW`7Hry$VGFezXsS@Fp1QXQ5!IccEZ)v3+f6hW*YbSgne* tC2lPS9WhnVxVs-)F~e_GjO%+WVLo5MfGT5U;(eC!_gN-V7pR$L`~xGfk52#q literal 0 HcmV?d00001 diff --git a/src/main/scala/chiselucl/examples/firrtl/Adder.fir b/examples/firrtl/Adder.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/Adder.fir rename to examples/firrtl/Adder.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/AsyncResetTester.fir b/examples/firrtl/AsyncResetTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/AsyncResetTester.fir rename to examples/firrtl/AsyncResetTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ChirrtlMems.fir b/examples/firrtl/ChirrtlMems.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ChirrtlMems.fir rename to examples/firrtl/ChirrtlMems.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/CustomTransform.fir b/examples/firrtl/CustomTransform.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/CustomTransform.fir rename to examples/firrtl/CustomTransform.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/DecoupledGCD.fir b/examples/firrtl/DecoupledGCD.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/DecoupledGCD.fir rename to examples/firrtl/DecoupledGCD.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/EmptyChirrtlMem.fir b/examples/firrtl/EmptyChirrtlMem.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/EmptyChirrtlMem.fir rename to examples/firrtl/EmptyChirrtlMem.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ExpandWhens.fir b/examples/firrtl/ExpandWhens.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ExpandWhens.fir rename to examples/firrtl/ExpandWhens.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/FPU.fir b/examples/firrtl/FPU.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/FPU.fir rename to examples/firrtl/FPU.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/GCDTester.fir b/examples/firrtl/GCDTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/GCDTester.fir rename to examples/firrtl/GCDTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/HasDeadCode.fir b/examples/firrtl/HasDeadCode.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/HasDeadCode.fir rename to examples/firrtl/HasDeadCode.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/HasLoops.fir b/examples/firrtl/HasLoops.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/HasLoops.fir rename to examples/firrtl/HasLoops.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/HwachaSequencer.fir b/examples/firrtl/HwachaSequencer.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/HwachaSequencer.fir rename to examples/firrtl/HwachaSequencer.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ICache.fir b/examples/firrtl/ICache.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ICache.fir rename to examples/firrtl/ICache.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ICache.lo.fir b/examples/firrtl/ICache.lo.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ICache.lo.fir rename to examples/firrtl/ICache.lo.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/LargeParamTester.fir b/examples/firrtl/LargeParamTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/LargeParamTester.fir rename to examples/firrtl/LargeParamTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/Legalize.fir b/examples/firrtl/Legalize.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/Legalize.fir rename to examples/firrtl/Legalize.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/MemTester.fir b/examples/firrtl/MemTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/MemTester.fir rename to examples/firrtl/MemTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/MultiExtModuleTester.fir b/examples/firrtl/MultiExtModuleTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/MultiExtModuleTester.fir rename to examples/firrtl/MultiExtModuleTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/NestedSubAccessTester.fir b/examples/firrtl/NestedSubAccessTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/NestedSubAccessTester.fir rename to examples/firrtl/NestedSubAccessTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/NodeType.fir b/examples/firrtl/NodeType.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/NodeType.fir rename to examples/firrtl/NodeType.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ParameterizedExtModuleTester.fir b/examples/firrtl/ParameterizedExtModuleTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ParameterizedExtModuleTester.fir rename to examples/firrtl/ParameterizedExtModuleTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/PipeTester.fir b/examples/firrtl/PipeTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/PipeTester.fir rename to examples/firrtl/PipeTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/Printf.fir b/examples/firrtl/Printf.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/Printf.fir rename to examples/firrtl/Printf.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/RenamedExtModuleTester.fir b/examples/firrtl/RenamedExtModuleTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/RenamedExtModuleTester.fir rename to examples/firrtl/RenamedExtModuleTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/RightShiftTester.fir b/examples/firrtl/RightShiftTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/RightShiftTester.fir rename to examples/firrtl/RightShiftTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/Rob.fir b/examples/firrtl/Rob.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/Rob.fir rename to examples/firrtl/Rob.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/RocketCore.fir b/examples/firrtl/RocketCore.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/RocketCore.fir rename to examples/firrtl/RocketCore.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/RocketCore.lo.fir b/examples/firrtl/RocketCore.lo.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/RocketCore.lo.fir rename to examples/firrtl/RocketCore.lo.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/SimpleExtModuleTester.fir b/examples/firrtl/SimpleExtModuleTester.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/SimpleExtModuleTester.fir rename to examples/firrtl/SimpleExtModuleTester.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/Trivial.fir b/examples/firrtl/Trivial.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/Trivial.fir rename to examples/firrtl/Trivial.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ZeroPortMem.fir b/examples/firrtl/ZeroPortMem.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ZeroPortMem.fir rename to examples/firrtl/ZeroPortMem.fir diff --git a/src/main/scala/chiselucl/examples/firrtl/ZeroWidthMem.fir b/examples/firrtl/ZeroWidthMem.fir similarity index 100% rename from src/main/scala/chiselucl/examples/firrtl/ZeroWidthMem.fir rename to examples/firrtl/ZeroWidthMem.fir diff --git a/src/main/scala/chiselucl/backend/RemoveTail.scala b/src/main/scala/chiselucl/transforms/RemoveTail.scala similarity index 94% rename from src/main/scala/chiselucl/backend/RemoveTail.scala rename to src/main/scala/chiselucl/transforms/RemoveTail.scala index 9001eef..e10fa14 100644 --- a/src/main/scala/chiselucl/backend/RemoveTail.scala +++ b/src/main/scala/chiselucl/transforms/RemoveTail.scala @@ -7,6 +7,8 @@ import firrtl._ import firrtl.ir._ import firrtl.Mappers._ +//TODO: Check with albert on keeping this transform + object RemoveTail { def removeTailE(expr: Expression): Expression = expr.map(removeTailE) match { case DoPrim(PrimOps.Tail, Seq(e), Seq(amt), tpe) => diff --git a/src/main/scala/chiselucl/backend/SimplyRegUpdate.scala b/src/main/scala/chiselucl/transforms/SimplyRegUpdate.scala similarity index 96% rename from src/main/scala/chiselucl/backend/SimplyRegUpdate.scala rename to src/main/scala/chiselucl/transforms/SimplyRegUpdate.scala index 0315561..5868790 100644 --- a/src/main/scala/chiselucl/backend/SimplyRegUpdate.scala +++ b/src/main/scala/chiselucl/transforms/SimplyRegUpdate.scala @@ -8,6 +8,8 @@ import firrtl.ir._ import firrtl.Utils.kind import firrtl.Mappers._ +//TODO: Check with Albert on keeping this transform + object SimplifyRegUpdate { def onStmt(namespace: Namespace)(stmt: Statement): Statement = stmt.map(onStmt(namespace)) match { case Connect(info, lhs, rhs) if kind(lhs) == RegKind => diff --git a/src/main/scala/chiselucl/backend/UclidEmitter.scala b/src/main/scala/chiselucl/transforms/UclidEmitter.scala similarity index 99% rename from src/main/scala/chiselucl/backend/UclidEmitter.scala rename to src/main/scala/chiselucl/transforms/UclidEmitter.scala index ff13f21..502c4ec 100644 --- a/src/main/scala/chiselucl/backend/UclidEmitter.scala +++ b/src/main/scala/chiselucl/transforms/UclidEmitter.scala @@ -66,9 +66,9 @@ class UclidEmitter(val debugOutput: Boolean = false) extends SeqTransform with E case Neg => s"-$arg0" case Not => s"~${arg0}" // TODO: Handle asUInt operator - case asUInt => arg0 + case AsUInt => arg0 // TODO: Handle asSInt operator - case asSInt => arg0 + case AsSInt => arg0 case _ => throwInternalError(s"Illegal unary operator: ${p.op}") } diff --git a/src/main/scala/chiselucl/uclid/package.scala b/src/main/scala/chiselucl/uclid/package.scala index 97f0632..09f1ce0 100644 --- a/src/main/scala/chiselucl/uclid/package.scala +++ b/src/main/scala/chiselucl/uclid/package.scala @@ -20,6 +20,7 @@ package object uclid { def apply(condition: Bool): Bool = apply(condition, None) def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { + condition.getClass.getMethods.map(m => println(m.getName)) name.foreach { condition.suggestName(_) } GuardSignal(condition) annotate(new ChiselAnnotation { def toFirrtl = UclidAssumptionAnnotation(condition.toTarget) }) @@ -28,7 +29,7 @@ package object uclid { } object Assert { - def apply(condition: Bool): Bool = apply(condition, None) + def apply(condition: Boolean): Bool = apply(condition, None) def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { name.foreach { condition.suggestName(_) } From dbc4337346a3e4da9a522a2963291cad3760421e Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 15:04:04 -0700 Subject: [PATCH 03/11] Added base for a general verification language --- .../chiselucl/verification/lang/package.scala | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 src/main/scala/chiselucl/verification/lang/package.scala diff --git a/src/main/scala/chiselucl/verification/lang/package.scala b/src/main/scala/chiselucl/verification/lang/package.scala new file mode 100644 index 0000000..dd163af --- /dev/null +++ b/src/main/scala/chiselucl/verification/lang/package.scala @@ -0,0 +1,39 @@ +package chiselucl +package verification + +import chisel3._ +import chisel3.experimental.{ChiselAnnotation, annotate, requireIsHardware} + +//TODO: Need to add more elements to this language so that we can +// guard signals more precisely + +package object lang { + + sealed trait VerificationFormula + + object Assume extends VerificationFormula { + def apply(condition: Bool): Bool = apply(condiition, None) + def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) + def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { + name.foreach { condition.suggestName(_) } + GuardSignal(condition) + //TODO: This needs to be modified to make UCLID agnostic + //annotate(new ChiselAnnotation { def toFirrtl = UclidAssumptionAnnotation(condition.toTarget) }) + condition + } + } + + object Assert extends VerificationFormula { + def apply(condition: Bool): Bool = apply(condition, None) + def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) + def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { + name.foreach { condition.suggestName(_) } + GuardSignal(condition) + //TODO: This needs to be modifies to make UCLID agnostic + //annotate(new ChiselAnnotation { def toFirrtl = UclidAssertAnnotation(condition.toTarget) }) + condition + } + + } + +} From 2c760c557ec60584f1ad31d2d9e9f29c64cf4ed6 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 15:17:11 -0700 Subject: [PATCH 04/11] Created annotations for circuit analysis passes; fixed compiler errors in verification lang --- .../annotations/InfoAnnotations.scala | 58 +++++++++++++++++++ src/main/scala/chiselucl/uclid/package.scala | 2 +- .../chiselucl/verification/lang/package.scala | 14 ++++- 3 files changed, 71 insertions(+), 3 deletions(-) create mode 100644 src/main/scala/chiselucl/annotations/InfoAnnotations.scala diff --git a/src/main/scala/chiselucl/annotations/InfoAnnotations.scala b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala new file mode 100644 index 0000000..1e7ddb6 --- /dev/null +++ b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala @@ -0,0 +1,58 @@ +// See LICESNSE for license details. + +package chiselucl +package annotations + +// Local imports +import chiselucl.verification.lang.VerificationFormula + +// Other imports + +import firrtl._ +import firrtl.ir._ +import firrtl.analyses.InstanceGraph +import firrtl.annotations.NoTargetAnnotation + +/** + * Base trait for annotations that contain information on + * components of the circuit. Extend this to pass information + * to the verification stages. + */ +trait VerificationInfoAnnotation extends NoTargetAnnotation + +/** + * Contains information on circuit structure to be used when + * constructing a solver query. + * + */ +case class CircuitInfoAnnotation( + name: String, + instGraph: InstanceGraph +) extends VerificationInfoAnnotation { + + /** + * Returns module names from highest module to leaf module. + */ + def getModuleNames: Seq[String] = instGraph.moduleOrder.map(_.name) + +} + +/** + * Collect information on relevant module state and assertions + * to be used when constructing a solver query. + * + */ +case class ModuleInfoAnnotation( + name: String, + nodes: Seq[DefNode], + wireDecls: Seq[DefWire], + instDecls: Seq[WDefInstance], + clocks: Set[Expression], + regResets: Set[String], + regDecls: Set[DefRegister], + memDecls: Set[DefMemory], + regAssigns: Seq[Connect], + combAssigns: Seq[Connect], + wireAssigns: Seq[Connect], + properties: Seq[VerificationFormula] +) extends VerificationInfoAnnotation diff --git a/src/main/scala/chiselucl/uclid/package.scala b/src/main/scala/chiselucl/uclid/package.scala index 09f1ce0..c626d84 100644 --- a/src/main/scala/chiselucl/uclid/package.scala +++ b/src/main/scala/chiselucl/uclid/package.scala @@ -29,7 +29,7 @@ package object uclid { } object Assert { - def apply(condition: Boolean): Bool = apply(condition, None) + def apply(condition: Bool): Bool = apply(condition, None) def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { name.foreach { condition.suggestName(_) } diff --git a/src/main/scala/chiselucl/verification/lang/package.scala b/src/main/scala/chiselucl/verification/lang/package.scala index dd163af..53fe4e7 100644 --- a/src/main/scala/chiselucl/verification/lang/package.scala +++ b/src/main/scala/chiselucl/verification/lang/package.scala @@ -2,7 +2,7 @@ package chiselucl package verification import chisel3._ -import chisel3.experimental.{ChiselAnnotation, annotate, requireIsHardware} +import chisel3.experimental.{requireIsHardware} //TODO: Need to add more elements to this language so that we can // guard signals more precisely @@ -11,8 +11,18 @@ package object lang { sealed trait VerificationFormula + object GuardSignal { + def apply[T <: Data](data: T)(implicit compileOptions: CompileOptions): Unit = { + if (compileOptions.checkSynthesizable) { + requireIsHardware(data, "Signal used in verification formula") + } + dontTouch(data) + } + } + + object Assume extends VerificationFormula { - def apply(condition: Bool): Bool = apply(condiition, None) + def apply(condition: Bool): Bool = apply(condition, None) def apply(condition: Bool, name: String): Bool = apply(condition, Some(name)) def apply(condition: Bool, name: Option[String])(implicit compileOptions: CompileOptions): Bool = { name.foreach { condition.suggestName(_) } From c805a4dbe4a2a32d665f00b7adaefd1186e13823 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 17:35:58 -0700 Subject: [PATCH 05/11] Created CollectCircuitInfo transform --- .../analysis/CollectCircuitInfo.scala | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala diff --git a/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala new file mode 100644 index 0000000..0b33264 --- /dev/null +++ b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala @@ -0,0 +1,23 @@ +// See LICENSE + + +package chiselucl +package analysis + +import chiselucl.annotations.{CircuitInfoAnnotation, ModuleInfoAnnotation} + +import firrtl._ +import firrtl.ir._ + + +class CollectCircuitInfo extends Transform { + def inputForm = LowForm + def outputForm = LowForm + + override def execute(cs: CircuitState): CircuitState = { + val circuitInfoAnno = Seq(CircuitInfoAnnotation(cs.circuit.main, new InstanceGraph(cs.circuit))) + cs.copy(annotations = circuitInfoAnno ++ cs.annotations) + } +} + + From c2503d2f60b1a6efa0fa6b2fc5d2853097bfe910 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Mon, 23 Mar 2020 18:55:22 -0700 Subject: [PATCH 06/11] Added CollectModuleInfo transform and decoupled UCLID logic; cleaned up CollectInfo.scala --- .../analysis/CollectCircuitInfo.scala | 6 +- .../analysis/CollectModuleInfo.scala | 114 ++++++++++++++++++ 2 files changed, 117 insertions(+), 3 deletions(-) create mode 100644 src/main/scala/chiselucl/analysis/CollectModuleInfo.scala diff --git a/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala index 0b33264..a42dd03 100644 --- a/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala +++ b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala @@ -1,13 +1,13 @@ -// See LICENSE +// See LICENSE for license details. package chiselucl package analysis -import chiselucl.annotations.{CircuitInfoAnnotation, ModuleInfoAnnotation} +import chiselucl.annotations.CircuitInfoAnnotation import firrtl._ -import firrtl.ir._ +import firrtl.analyses.InstanceGraph class CollectCircuitInfo extends Transform { diff --git a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala new file mode 100644 index 0000000..af7e56b --- /dev/null +++ b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala @@ -0,0 +1,114 @@ +// See LICESNSE for license details. + +package chiselucl +package analysis + +import chiselucl.annotations._ +import chiselucl.verification.lang._ + +import firrtl._ +import firrtl.ir._ +import firrtl.Utils._ +import firrtl.Mappers._ + +import scala.collection.mutable.{ListBuffer, HashSet} + +object CollectModuleInfo { + + def createModuleInfoAnnotation(m: Module): ModuleInfoAnnotation = { + val nodes = ListBuffer[DefNode]() + val wireDecls = ListBuffer[DefWire]() + val instDecls = ListBuffer[WDefInstance]() + val clocks = HashSet[Expression]() + val regResets = HashSet[String]() + val regDecls = HashSet[DefRegister]() + val memDecls = HashSet[DefMemory]() + val regAssigns = ListBuffer[Connect]() + val combAssigns = ListBuffer[Connect]() + val wireAssigns = ListBuffer[Connect]() + val properties = ListBuffer[VerificationFormula]() + + //TODO: Need to revisit this correctness of the collection + def processStatements(s: Statement): Statement = s map processStatements match { + case sx: DefNode => + nodes += sx + sx + case sx: DefRegister => + clocks += sx.clock + sx.reset match { + case wr: WRef => + regResets += wr.name + case UIntLiteral(v: BigInt, _) if (v == 0) => + case _ => + throwInternalError(s"Illegal reset signal ${sx.reset}") + } + regDecls += sx + sx + case sx @ Connect(_, lhs, rhs) => kind(lhs) match { + case RegKind => + regAssigns += sx + case PortKind => + combAssigns += sx + case MemKind => rhs.tpe match { + case ClockType => + clocks += rhs + case _ => + combAssigns += sx + } + case InstanceKind => lhs match { + case WSubField(WRef(instName,_,_,_), field, tpe, flow) => + combAssigns += sx + case _ => + throwInternalError(s"Only subfields of an instance may be on the lhs of a Connect involving an instance") + } + case _ => + throwInternalError(s"Only outputs, registers, mem fields, and inst subfields may be on the lhs of a Connect") + } + sx + case sx @ DefMemory(_, n, dt, _, wlat, rlat, rs, ws, rws, _) => + require(wlat == 1 && rlat == 0 && rws.size == 0, "This pass must run after VerilogMemDelays!") + require(dt.isInstanceOf[GroundType], "This pass must run after LowerTypes!") + memDecls += sx + sx + case sx @ WDefInstance(_,name,module,_) => + instDecls += sx + sx + case DefWire(_,_,_) => + // These are illegal for now + throw EmitterException("Using illegal statement!") + case sx => + sx + } + + processStatements(m.body) + + ModuleInfoAnnotation( + m.name, + nodes.toSeq, + wireDecls.toSeq, + instDecls.toSeq, + clocks.toSet, + regResets.toSet, + regDecls.toSet, + memDecls.toSet, + regAssigns.toSeq, + combAssigns.toSeq, + wireAssigns.toSeq, + properties.toSeq + ) + } +} + + +class CollectModuleInfo extends Transform { + def inputForm = LowForm + def outputForm = LowForm + + def execute(state: CircuitState): CircuitState = { + val moduleInfoAnnos = state.circuit.modules.flatMap { + case mod: Module => Some(CollectModuleInfo.createModuleInfoAnnotation(mod)) + case extMod: ExtModule => None + } + state.copy(annotations = moduleInfoAnnos ++ state.annotations) + } +} From 1fdd596eb411847869321dd6ff1994e0cb7c1256 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Tue, 24 Mar 2020 01:00:41 -0700 Subject: [PATCH 07/11] Added ExpandMemoryWires transform; minor changes to CollectModuleInfo --- .../analysis/CollectModuleInfo.scala | 3 +- .../analysis/ExpandMemoryWires.scala | 77 +++++++++++++++++++ 2 files changed, 79 insertions(+), 1 deletion(-) create mode 100644 src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala diff --git a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala index af7e56b..27d5662 100644 --- a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala +++ b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala @@ -1,4 +1,4 @@ -// See LICESNSE for license details. +// See LICENSE for license details. package chiselucl package analysis @@ -104,6 +104,7 @@ class CollectModuleInfo extends Transform { def inputForm = LowForm def outputForm = LowForm + def execute(state: CircuitState): CircuitState = { val moduleInfoAnnos = state.circuit.modules.flatMap { case mod: Module => Some(CollectModuleInfo.createModuleInfoAnnotation(mod)) diff --git a/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala new file mode 100644 index 0000000..dd9e0b3 --- /dev/null +++ b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala @@ -0,0 +1,77 @@ +// See LICENSE for license details. + +package chiselucl +package analysis + +import chiselucl.annotations._ + +import firrtl._ +import firrtl.ir._ +import firrtl.passes._ +import MemPortUtils.{memPortField} + + +import scala.collection.mutable.ListBuffer + +object ExpandMemoryWires { + + def expandWires(modInfo : ModuleInfoAnnotation) : ModuleInfoAnnotation = { + val newWires = ListBuffer[DefWire]() + + for (decl <- modInfo.memDecls) { + decl match { + case sx @ DefMemory(_, n, dt, _, wlat, rlat, rs, ws, rws, _) => + newWires += DefWire(NoInfo, s"havoc_$n", dt) + for (r <- rs) { + val data = memPortField(sx, r, "data") + val addr = memPortField(sx, r, "addr") + val en = memPortField(sx, r, "en") + newWires += DefWire(NoInfo, LowerTypes.loweredName(data), data.tpe) + newWires += DefWire(NoInfo, LowerTypes.loweredName(addr), addr.tpe) + newWires += DefWire(NoInfo, LowerTypes.loweredName(en), en.tpe) + } + for (w <- ws) { + val data = memPortField(sx, w, "data") + val addr = memPortField(sx, w, "addr") + val en = memPortField(sx, w, "en") + val mask = memPortField(sx, w, "mask") + newWires += DefWire(NoInfo, LowerTypes.loweredName(data), data.tpe) + newWires += DefWire(NoInfo, LowerTypes.loweredName(addr), addr.tpe) + newWires += DefWire(NoInfo, LowerTypes.loweredName(en), en.tpe) + newWires += DefWire(NoInfo, LowerTypes.loweredName(mask), mask.tpe) + } + case _ => // Do nothing + } + } + + ModuleInfoAnnotation( + modInfo.name, + modInfo.nodes, + newWires.toSeq ++ modInfo.wireDecls, + modInfo.instDecls, + modInfo.clocks, + modInfo.regResets, + modInfo.regDecls, + modInfo.memDecls, + modInfo.regAssigns, + modInfo.combAssigns, + modInfo.wireAssigns, + modInfo.properties + ) + } + +} + + +class ExpandMemoryWires extends Transform { + def inputForm = LowForm + def outputForm = LowForm + + def execute(state: CircuitState): CircuitState = { + val annos = state.annotations.map { + case modInfo: ModuleInfoAnnotation => ExpandMemoryWires.expandWires(modInfo) + case other => other + } + state.copy(annotations = annos) + } +} From 4bbd2d0a8db736ccc322bb40f390b0d906763686 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Tue, 24 Mar 2020 02:03:30 -0700 Subject: [PATCH 08/11] Split structure of ModuleInfoAnnotation; made other passes compatible with the change --- .../analysis/CollectModuleInfo.scala | 5 +- .../analysis/ExpandMemoryWires.scala | 5 +- .../annotations/InfoAnnotations.scala | 61 +++++++++++++++---- 3 files changed, 54 insertions(+), 17 deletions(-) diff --git a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala index 27d5662..cbc79fb 100644 --- a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala +++ b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala @@ -87,14 +87,15 @@ object CollectModuleInfo { nodes.toSeq, wireDecls.toSeq, instDecls.toSeq, - clocks.toSet, regResets.toSet, regDecls.toSet, memDecls.toSet, regAssigns.toSeq, combAssigns.toSeq, wireAssigns.toSeq, - properties.toSeq + properties.toSeq, + clocks.toSet, + None ) } } diff --git a/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala index dd9e0b3..13eef6c 100644 --- a/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala +++ b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala @@ -49,14 +49,15 @@ object ExpandMemoryWires { modInfo.nodes, newWires.toSeq ++ modInfo.wireDecls, modInfo.instDecls, - modInfo.clocks, modInfo.regResets, modInfo.regDecls, modInfo.memDecls, modInfo.regAssigns, modInfo.combAssigns, modInfo.wireAssigns, - modInfo.properties + modInfo.properties, + modInfo.clocks, + None ) } diff --git a/src/main/scala/chiselucl/annotations/InfoAnnotations.scala b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala index 1e7ddb6..50c5015 100644 --- a/src/main/scala/chiselucl/annotations/InfoAnnotations.scala +++ b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala @@ -37,22 +37,57 @@ case class CircuitInfoAnnotation( } +//TODO: Should we use named +trait Name { + def name: String +} + +trait StateInfo { + def nodes: Seq[DefNode] + def wireDecls: Seq[DefWire] + def instDecls: Seq[WDefInstance] + def regResets: Set[String] + def regDecls: Set[DefRegister] + def memDecls: Set[DefMemory] + def regAssigns: Seq[Connect] + def combAssigns: Seq[Connect] + def wireAssigns: Seq[Connect] +} + +trait PropertyInfo { + def properties: Seq[VerificationFormula] +} + +trait ClockInfo { + def clocks: Set[Expression] + def clockSets: Option[Set[Set[Expression]]] +} + + + + /** * Collect information on relevant module state and assertions * to be used when constructing a solver query. * */ case class ModuleInfoAnnotation( - name: String, - nodes: Seq[DefNode], - wireDecls: Seq[DefWire], - instDecls: Seq[WDefInstance], - clocks: Set[Expression], - regResets: Set[String], - regDecls: Set[DefRegister], - memDecls: Set[DefMemory], - regAssigns: Seq[Connect], - combAssigns: Seq[Connect], - wireAssigns: Seq[Connect], - properties: Seq[VerificationFormula] -) extends VerificationInfoAnnotation + override val name: String, + override val nodes: Seq[DefNode], + override val wireDecls: Seq[DefWire], + override val instDecls: Seq[WDefInstance], + override val regResets: Set[String], + override val regDecls: Set[DefRegister], + override val memDecls: Set[DefMemory], + override val regAssigns: Seq[Connect], + override val combAssigns: Seq[Connect], + override val wireAssigns: Seq[Connect], + override val properties: Seq[VerificationFormula], + override val clocks: Set[Expression], + override val clockSets: Option[Set[Set[Expression]]] +) extends VerificationInfoAnnotation with Name + with StateInfo + with ClockInfo + with PropertyInfo + + From 4db40523bbcc3548703a517cb82baae5aceb072e Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Tue, 24 Mar 2020 03:14:20 -0700 Subject: [PATCH 09/11] Added ComputeClockDomain pass (needs reimplementation); moving to emission --- .../analysis/ComputeClockDomain.scala | 84 +++++++++++++++++++ 1 file changed, 84 insertions(+) create mode 100644 src/main/scala/chiselucl/analysis/ComputeClockDomain.scala diff --git a/src/main/scala/chiselucl/analysis/ComputeClockDomain.scala b/src/main/scala/chiselucl/analysis/ComputeClockDomain.scala new file mode 100644 index 0000000..f7b0ccf --- /dev/null +++ b/src/main/scala/chiselucl/analysis/ComputeClockDomain.scala @@ -0,0 +1,84 @@ +// See LICENSE for license details. + +package chiselucl +package analysis + +import chiselucl.annotations._ + +import firrtl._ +import firrtl.ir._ +import firrtl.Utils._ + +import scala.collection.mutable.{LinkedHashMap, HashSet} + +object ComputeClockDomain { + + + // TODO: We have two possible approaches to computing equal clocks + // 1. Change this implementation to use disjoint sets with a peek + // 2. Analyze the actual collected clocks (this seems promising) + // + def addClockInfo(modInfo: ModuleInfoAnnotation): ModuleInfoAnnotation = { + val eqClocks = LinkedHashMap[Expression, HashSet[Expression]]() + + for (node<-modInfo.nodes) { + if (node.value.tpe == ClockType) { + node.value match { + case wr: WRef => + val clockSet = eqClocks.getOrElseUpdate(wr, new HashSet[Expression]()) + clockSet.add(WRef(node)) + case _ => throwInternalError(s"Cannot handle complex clock NodeDef") + } + } + } + + // Join equal clock sets + eqClocks.foreach({ + case (k1, set1) => + eqClocks.foreach({ + case (k2, set2) => + if (set1.contains(k2)) { + eqClocks.put(k1, set1.union(set2)) + eqClocks.remove(k2) + } + }) + }) + + val clockSets = new HashSet[Set[Expression]]() + eqClocks.foreach({ + case (k, set) => + set += k + clockSets += set.toSet + }) + + ModuleInfoAnnotation( + modInfo.name, + modInfo.nodes, + modInfo.wireDecls, + modInfo.instDecls, + modInfo.regResets, + modInfo.regDecls, + modInfo.memDecls, + modInfo.regAssigns, + modInfo.combAssigns, + modInfo.wireAssigns, + modInfo.properties, + modInfo.clocks, + Some(clockSets.toSet) + ) + } +} + + +class ComputeClockDomain extends Transform { + def inputForm = LowForm + def outputForm = LowForm + + def execute(state: CircuitState): CircuitState = { + val annos = state.annotations.map { + case modInfo: ModuleInfoAnnotation => ComputeClockDomain.addClockInfo(modInfo) + case other => other + } + state.copy(annotations = annos) + } +} From 3f8aac4f40041e87924feb30303fa604106ae667 Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Tue, 24 Mar 2020 14:33:07 -0700 Subject: [PATCH 10/11] Modified structure of verification stages --- src/main/scala/chiselucl/verification/lang/package.scala | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/main/scala/chiselucl/verification/lang/package.scala b/src/main/scala/chiselucl/verification/lang/package.scala index 53fe4e7..2e64d6c 100644 --- a/src/main/scala/chiselucl/verification/lang/package.scala +++ b/src/main/scala/chiselucl/verification/lang/package.scala @@ -7,6 +7,14 @@ import chisel3.experimental.{requireIsHardware} //TODO: Need to add more elements to this language so that we can // guard signals more precisely +//TODO: This needs to be moved to somewhere in the chisel/firrtl repos, since +// we want to expose a common verification front-end. Note that we +// also want people to be able to easily write their own verification +// frontends, so we might also want the verification passes to be +// aware of the specs they are using + +//TODO: Consult Albert on this + package object lang { sealed trait VerificationFormula From fa661a81ec47fb19702bd23f2173b682116546ed Mon Sep 17 00:00:00 2001 From: Pranav Gaddamadugu Date: Tue, 24 Mar 2020 16:18:08 -0700 Subject: [PATCH 11/11] Added scaffolding for emitting UCLID, need to figure out the emission API in FIRRTL --- .../uclid/stages/UclidEmitter.scala | 61 +++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 src/main/scala/chiselucl/verification/uclid/stages/UclidEmitter.scala diff --git a/src/main/scala/chiselucl/verification/uclid/stages/UclidEmitter.scala b/src/main/scala/chiselucl/verification/uclid/stages/UclidEmitter.scala new file mode 100644 index 0000000..0f0a15b --- /dev/null +++ b/src/main/scala/chiselucl/verification/uclid/stages/UclidEmitter.scala @@ -0,0 +1,61 @@ +// See LICENSE for license details. + +package chiselucl +package verification.uclid + +import chiselucl.annotations._ + +import firrtl._ +import firrtl.analyses._ +import firrtl.ir._ +import firrtl.passes._ +import firrtl.transforms._ + + +import java.io.Writer + +class IndentLevel { + var value: Int = 0 + def increase() = value += 2 + def decrease() = value -= 2 +} + +object UclidSerializer { + + def serializeModule(modInfo: ModuleInfoAnnotation)(implicit w : Writer): Unit = { + + } + + def serializeAllModules(circInfo: Seq[CircuitInfoAnnotation], modInfos: Seq[ModuleInfoAnnotation])(implicit w : Writer): Unit = { + + } +} + +class UclidEmitter(val debugOutput: Boolean = false) extends Transform with Emitter { + def inputForm = LowForm + def outputForm = LowForm + + val outputSuffix = ".ucl" + + //TODO: Need to figure out the emission interface + override def execute(state: CircuitState) = { + val modInfoAnnos = state.annotations.filter(_.isInstanceOf[ModuleInfoAnnotation]).asInstanceOf[Seq[ModuleInfoAnnotation]] + val circInfoAnnos = state.annotations.filter(_.isInstanceOf[CircuitInfoAnnotation]).asInstanceOf[Seq[CircuitInfoAnnotation]] + val newAnnos = state.annotations.flatMap { + case EmitCircuitAnnotation(_) => + val writer = new java.io.StringWriter + UclidSerializer.serializeAllModules(circInfoAnnos, modInfoAnnos)(writer) + Seq() + + case EmitAllModulesAnnotation(_) => + modInfoAnnos.map{ i => + val writer = new java.io.StringWriter + UclidSerializer.serializeModule(i)(writer) + Seq() + } + + case _ => Seq() + } + state.copy(annotations = newAnnos ++ state.annotations) + } +}