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/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 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 0000000..1e31b0f Binary files /dev/null and b/examples/firrtl/.RocketCore.fir.swp differ 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/analysis/CollectCircuitInfo.scala b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala new file mode 100644 index 0000000..a42dd03 --- /dev/null +++ b/src/main/scala/chiselucl/analysis/CollectCircuitInfo.scala @@ -0,0 +1,23 @@ +// See LICENSE for license details. + + +package chiselucl +package analysis + +import chiselucl.annotations.CircuitInfoAnnotation + +import firrtl._ +import firrtl.analyses.InstanceGraph + + +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) + } +} + + diff --git a/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala new file mode 100644 index 0000000..cbc79fb --- /dev/null +++ b/src/main/scala/chiselucl/analysis/CollectModuleInfo.scala @@ -0,0 +1,116 @@ +// See LICENSE 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, + regResets.toSet, + regDecls.toSet, + memDecls.toSet, + regAssigns.toSeq, + combAssigns.toSeq, + wireAssigns.toSeq, + properties.toSeq, + clocks.toSet, + None + ) + } +} + + +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) + } +} 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) + } +} diff --git a/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala new file mode 100644 index 0000000..13eef6c --- /dev/null +++ b/src/main/scala/chiselucl/analysis/ExpandMemoryWires.scala @@ -0,0 +1,78 @@ +// 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.regResets, + modInfo.regDecls, + modInfo.memDecls, + modInfo.regAssigns, + modInfo.combAssigns, + modInfo.wireAssigns, + modInfo.properties, + modInfo.clocks, + None + ) + } + +} + + +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) + } +} diff --git a/src/main/scala/chiselucl/annotations/InfoAnnotations.scala b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala new file mode 100644 index 0000000..50c5015 --- /dev/null +++ b/src/main/scala/chiselucl/annotations/InfoAnnotations.scala @@ -0,0 +1,93 @@ +// 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) + +} + +//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( + 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 + + 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..c626d84 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) }) 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..2e64d6c --- /dev/null +++ b/src/main/scala/chiselucl/verification/lang/package.scala @@ -0,0 +1,57 @@ +package chiselucl +package verification + +import chisel3._ +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 + + 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(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 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 + } + + } + +} 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) + } +}