From cb77b061e835044b4f3a2b718fb7ce3971b5d06e Mon Sep 17 00:00:00 2001 From: mergify[bot] Date: Tue, 1 Feb 2022 20:55:35 +0000 Subject: Optional clock param for memory ports (#2333) (#2382) Warn if clock at memory instantiation differs from clock bound at port creation and port clock is not manually passed Co-authored-by: Jack Koenig (cherry picked from commit 465805ec7b2696a985eaa12cf9c6868f11ac2931) Co-authored-by: Aditya Naik <91489422+adkian-sifive@users.noreply.github.com>--- core/src/main/scala/chisel3/Mem.scala | 161 ++++++++++++++++++--- .../internal/sourceinfo/SourceInfoTransform.scala | 4 + src/test/scala/chiselTests/MultiClockSpec.scala | 110 +++++++++++++- 3 files changed, 255 insertions(+), 20 deletions(-) diff --git a/core/src/main/scala/chisel3/Mem.scala b/core/src/main/scala/chisel3/Mem.scala index ff5072ad..4b7c0815 100644 --- a/core/src/main/scala/chisel3/Mem.scala +++ b/core/src/main/scala/chisel3/Mem.scala @@ -56,6 +56,7 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) with SourceInfoDoc { _parent.foreach(_.addId(this)) + private val clockInst: Clock = Builder.forcedClock // REVIEW TODO: make accessors (static/dynamic, read/write) combinations consistent. /** Creates a read accessor into the memory with static addressing. See the @@ -63,17 +64,17 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) */ def apply(x: BigInt): T = macro SourceInfoTransform.xArg - /** Creates a read accessor into the memory with static addressing. See the - * class documentation of the memory for more detailed information. - */ - def apply(x: Int): T = macro SourceInfoTransform.xArg - /** @group SourceInfoTransformMacro */ def do_apply(idx: BigInt)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = { require(idx >= 0 && idx < length) - apply(idx.asUInt) + apply(idx.asUInt, Builder.forcedClock) } + /** Creates a read accessor into the memory with static addressing. See the + * class documentation of the memory for more detailed information. + */ + def apply(x: Int): T = macro SourceInfoTransform.xArg + /** @group SourceInfoTransformMacro */ def do_apply(idx: Int)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = do_apply(BigInt(idx))(sourceInfo, compileOptions) @@ -85,7 +86,12 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) /** @group SourceInfoTransformMacro */ def do_apply(idx: UInt)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = - makePort(sourceInfo, idx, MemPortDirection.INFER) + do_apply_impl(idx, Builder.forcedClock, MemPortDirection.INFER, true) + + def apply(x: UInt, y: Clock): T = macro SourceInfoTransform.xyArg + + def do_apply(idx: UInt, clock: Clock)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = + do_apply_impl(idx, clock, MemPortDirection.INFER, false) /** Creates a read accessor into the memory with dynamic addressing. See the * class documentation of the memory for more detailed information. @@ -94,16 +100,71 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) /** @group SourceInfoTransformMacro */ def do_read(idx: UInt)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = - makePort(sourceInfo, idx, MemPortDirection.READ) + do_apply_impl(idx, Builder.forcedClock, MemPortDirection.READ, true) + + /** Creates a read accessor into the memory with dynamic addressing. + * Takes a clock parameter to bind a clock that may be different + * from the implicit clock. See the class documentation of the memory + * for more detailed information. + */ + def read(x: UInt, y: Clock): T = macro SourceInfoTransform.xyArg + + /** @group SourceInfoTransformMacro */ + def do_read(idx: UInt, clock: Clock)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = + do_apply_impl(idx, clock, MemPortDirection.READ, false) + + protected def do_apply_impl( + idx: UInt, + clock: Clock, + dir: MemPortDirection, + warn: Boolean + )( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions + ): T = { + if (warn && clock != clockInst) { + Builder.warning( + "The clock used to initialize the memory is different than the one used to initialize the port. " + + "If this is intentional, please pass the clock explicitly when creating the port. This behavior will be an error in 3.6.0" + ) + } + makePort(sourceInfo, idx, dir, clock) + } /** Creates a write accessor into the memory. * * @param idx memory element index to write into * @param data new data to write */ - def write(idx: UInt, data: T)(implicit compileOptions: CompileOptions): Unit = { + def write(idx: UInt, data: T)(implicit compileOptions: CompileOptions): Unit = + write_impl(idx, data, Builder.forcedClock, true) + + /** Creates a write accessor into the memory with a clock + * that may be different from the implicit clock. + * + * @param idx memory element index to write into + * @param data new data to write + * @param clock clock to bind to this accessor + */ + def write(idx: UInt, data: T, clock: Clock)(implicit compileOptions: CompileOptions): Unit = + write_impl(idx, data, clock, false) + + private def write_impl( + idx: UInt, + data: T, + clock: Clock, + warn: Boolean + )( + implicit compileOptions: CompileOptions + ): Unit = { + if (warn && clock != clockInst) { + Builder.warning( + "The clock used to initialize the memory is different than the one used to initialize the port. " + + "If this is intentional, please pass the clock explicitly when creating the port. This behavior will be an error in 3.6.0" + ) + } implicit val sourceInfo = UnlocatableSourceInfo - makePort(UnlocatableSourceInfo, idx, MemPortDirection.WRITE) := data + makePort(UnlocatableSourceInfo, idx, MemPortDirection.WRITE, clock) := data } /** Creates a masked write accessor into the memory. @@ -122,9 +183,49 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) )( implicit evidence: T <:< Vec[_], compileOptions: CompileOptions + ): Unit = + masked_write_impl(idx, data, mask, Builder.forcedClock, true) + + /** Creates a masked write accessor into the memory with a clock + * that may be different from the implicit clock. + * + * @param idx memory element index to write into + * @param data new data to write + * @param mask write mask as a Seq of Bool: a write to the Vec element in + * memory is only performed if the corresponding mask index is true. + * @param clock clock to bind to this accessor + * + * @note this is only allowed if the memory's element data type is a Vec + */ + def write( + idx: UInt, + data: T, + mask: Seq[Bool], + clock: Clock + )( + implicit evidence: T <:< Vec[_], + compileOptions: CompileOptions + ): Unit = + masked_write_impl(idx, data, mask, clock, false) + + private def masked_write_impl( + idx: UInt, + data: T, + mask: Seq[Bool], + clock: Clock, + warn: Boolean + )( + implicit evidence: T <:< Vec[_], + compileOptions: CompileOptions ): Unit = { implicit val sourceInfo = UnlocatableSourceInfo - val accessor = makePort(sourceInfo, idx, MemPortDirection.WRITE).asInstanceOf[Vec[Data]] + if (warn && clock != clockInst) { + Builder.warning( + "The clock used to initialize the memory is different than the one used to initialize the port. " + + "If this is intentional, please pass the clock explicitly when creating the port. This behavior will be an error in 3.6.0" + ) + } + val accessor = makePort(sourceInfo, idx, MemPortDirection.WRITE, clock).asInstanceOf[Vec[Data]] val dataVec = data.asInstanceOf[Vec[Data]] if (accessor.length != dataVec.length) { Builder.error(s"Mem write data must contain ${accessor.length} elements (found ${dataVec.length})") @@ -139,7 +240,8 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) private def makePort( sourceInfo: SourceInfo, idx: UInt, - dir: MemPortDirection + dir: MemPortDirection, + clock: Clock )( implicit compileOptions: CompileOptions ): T = { @@ -147,7 +249,7 @@ sealed abstract class MemBase[T <: Data](val t: T, val length: BigInt) val i = Vec.truncateIndex(idx, length)(sourceInfo, compileOptions) val port = pushCommand( - DefMemPort(sourceInfo, t.cloneTypeFull, Node(this), dir, i.ref, Builder.forcedClock.ref) + DefMemPort(sourceInfo, t.cloneTypeFull, Node(this), dir, i.ref, clock.ref) ).id // Bind each element of port to being a MemoryPort port.bind(MemoryPortBinding(Builder.forcedUserModule, Builder.currentWhen)) @@ -244,23 +346,44 @@ object SyncReadMem { */ sealed class SyncReadMem[T <: Data] private (t: T, n: BigInt, val readUnderWrite: SyncReadMem.ReadUnderWrite) extends MemBase[T](t, n) { + + override def read(x: UInt): T = macro SourceInfoTransform.xArg + + /** @group SourceInfoTransformMacro */ + override def do_read(idx: UInt)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = + do_read(idx = idx, en = true.B) + def read(x: UInt, en: Bool): T = macro SourceInfoTransform.xEnArg /** @group SourceInfoTransformMacro */ - def do_read(addr: UInt, enable: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = { + def do_read(idx: UInt, en: Bool)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = + _read_impl(idx, en, Builder.forcedClock, true) + + def read(idx: UInt, en: Bool, clock: Clock): T = macro SourceInfoTransform.xyzArg + + /** @group SourceInfoTransformMacro */ + def do_read(idx: UInt, en: Bool, clock: Clock)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions): T = + _read_impl(idx, en, clock, false) + + /** @group SourceInfoTransformMacro */ + private def _read_impl( + addr: UInt, + enable: Bool, + clock: Clock, + warn: Boolean + )( + implicit sourceInfo: SourceInfo, + compileOptions: CompileOptions + ): T = { val a = Wire(UInt()) a := DontCare var port: Option[T] = None when(enable) { a := addr - port = Some(super.do_read(a)) + port = Some(super.do_apply_impl(a, clock, MemPortDirection.READ, warn)) } port.get } - - /** @group SourceInfoTransformMacro */ - override def do_read(idx: UInt)(implicit sourceInfo: SourceInfo, compileOptions: CompileOptions) = - do_read(addr = idx, enable = true.B) // note: we implement do_read(addr) for SyncReadMem in terms of do_read(addr, en) in order to ensure that // `mem.read(addr)` will always behave the same as `mem.read(addr, true.B)` } diff --git a/macros/src/main/scala/chisel3/internal/sourceinfo/SourceInfoTransform.scala b/macros/src/main/scala/chisel3/internal/sourceinfo/SourceInfoTransform.scala index 01e0acd6..3e310774 100644 --- a/macros/src/main/scala/chisel3/internal/sourceinfo/SourceInfoTransform.scala +++ b/macros/src/main/scala/chisel3/internal/sourceinfo/SourceInfoTransform.scala @@ -200,6 +200,10 @@ class SourceInfoTransform(val c: Context) extends AutoSourceTransform { q"$thisObj.$doFuncTerm($x, $y)($implicitSourceInfo, $implicitCompileOptions)" } + def xyzArg(idx: c.Tree, en: c.Tree, clock: c.Tree): c.Tree = { + q"$thisObj.$doFuncTerm($idx, $en, $clock)($implicitSourceInfo, $implicitCompileOptions)" + } + def xEnArg(x: c.Tree, en: c.Tree): c.Tree = { q"$thisObj.$doFuncTerm($x, $en)($implicitSourceInfo, $implicitCompileOptions)" } diff --git a/src/test/scala/chiselTests/MultiClockSpec.scala b/src/test/scala/chiselTests/MultiClockSpec.scala index 2553f3b3..381b4009 100644 --- a/src/test/scala/chiselTests/MultiClockSpec.scala +++ b/src/test/scala/chiselTests/MultiClockSpec.scala @@ -113,7 +113,7 @@ class MultiClockMemTest extends BasicTester { when(done) { stop() } } -class MultiClockSpec extends ChiselFlatSpec { +class MultiClockSpec extends ChiselFlatSpec with Utils { "withClock" should "scope the clock of registers" in { assertTesterPasses(new ClockDividerTest) @@ -129,6 +129,114 @@ class MultiClockSpec extends ChiselFlatSpec { }) } + "Differing clocks at memory and port instantiation" should "warn" in { + class modMemDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { Mem(4, UInt(8.W)) } + val port0 = mem(0.U) + } + val (logMemDifferingClock, _) = grabLog(ChiselStage.elaborate(new modMemDifferingClock)) + logMemDifferingClock should include("memory is different") + + class modSyncReadMemDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { SyncReadMem(4, UInt(8.W)) } + val port0 = mem(0.U) + } + val (logSyncReadMemDifferingClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemDifferingClock)) + logSyncReadMemDifferingClock should include("memory is different") + } + + "Differing clocks at memory and write accessor instantiation" should "warn" in { + class modMemWriteDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { Mem(4, UInt(8.W)) } + mem(1.U) := 1.U + } + val (logMemWriteDifferingClock, _) = grabLog(ChiselStage.elaborate(new modMemWriteDifferingClock)) + logMemWriteDifferingClock should include("memory is different") + + class modSyncReadMemWriteDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { SyncReadMem(4, UInt(8.W)) } + mem.write(1.U, 1.U) + } + val (logSyncReadMemWriteDifferingClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemWriteDifferingClock)) + logSyncReadMemWriteDifferingClock should include("memory is different") + } + + "Differing clocks at memory and read accessor instantiation" should "warn" in { + class modMemReadDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { Mem(4, UInt(8.W)) } + val readVal = mem.read(0.U) + } + val (logMemReadDifferingClock, _) = grabLog(ChiselStage.elaborate(new modMemReadDifferingClock)) + logMemReadDifferingClock should include("memory is different") + + class modSyncReadMemReadDifferingClock extends Module { + val myClock = IO(Input(Clock())) + val mem = withClock(myClock) { SyncReadMem(4, UInt(8.W)) } + val readVal = mem.read(0.U) + } + val (logSyncReadMemReadDifferingClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemReadDifferingClock)) + logSyncReadMemReadDifferingClock should include("memory is different") + } + + "Passing clock parameter to memory port instantiation" should "not warn" in { + class modMemPortClock extends Module { + val myClock = IO(Input(Clock())) + val mem = Mem(4, UInt(8.W)) + val port0 = mem(0.U, myClock) + } + val (logMemPortClock, _) = grabLog(ChiselStage.elaborate(new modMemPortClock)) + (logMemPortClock should not).include("memory is different") + + class modSyncReadMemPortClock extends Module { + val myClock = IO(Input(Clock())) + val mem = SyncReadMem(4, UInt(8.W)) + val port0 = mem(0.U, myClock) + } + val (logSyncReadMemPortClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemPortClock)) + (logSyncReadMemPortClock should not).include("memory is different") + } + + "Passing clock parameter to memory write accessor" should "not warn" in { + class modMemWriteClock extends Module { + val myClock = IO(Input(Clock())) + val mem = Mem(4, UInt(8.W)) + mem.write(0.U, 0.U, myClock) + } + val (logMemWriteClock, _) = grabLog(ChiselStage.elaborate(new modMemWriteClock)) + (logMemWriteClock should not).include("memory is different") + + class modSyncReadMemWriteClock extends Module { + val myClock = IO(Input(Clock())) + val mem = SyncReadMem(4, UInt(8.W)) + mem.write(0.U, 0.U, myClock) + } + val (logSyncReadMemWriteClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemWriteClock)) + (logSyncReadMemWriteClock should not).include("memory is different") + } + + "Passing clock parameter to memory read accessor" should "not warn" in { + class modMemReadClock extends Module { + val myClock = IO(Input(Clock())) + val mem = Mem(4, UInt(8.W)) + val readVal = mem.read(0.U, myClock) + } + val (logMemReadClock, _) = grabLog(ChiselStage.elaborate(new modMemReadClock)) + (logMemReadClock should not).include("memory is different") + + class modSyncReadMemReadClock extends Module { + val myClock = IO(Input(Clock())) + val mem = SyncReadMem(4, UInt(8.W)) + val readVal = mem.read(0.U, myClock) + } + val (logSyncReadMemReadClock, _) = grabLog(ChiselStage.elaborate(new modSyncReadMemReadClock)) + (logSyncReadMemReadClock should not).include("memory is different") + } + "withReset" should "scope the reset of registers" in { assertTesterPasses(new WithResetTest) } -- cgit v1.2.3