1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
// SPDX-License-Identifier: Apache-2.0
package chiselTest
import chisel3._
import chisel3.experimental._
import chiseltest._
import chiseltest.formal._
import firrtl.annotations.MemoryArrayInitAnnotation
import org.scalatest.flatspec.AnyFlatSpec
class MemFormalSpec extends AnyFlatSpec with ChiselScalatestTester with Formal {
behavior.of("SyncReadMem read enable")
private def check(mod: Boolean => ReadEnTestModule, alwaysEnabeld: Boolean = false): Unit = {
// we first check that the read is enabled when it should be
verify(mod(true), Seq(BoundedCheck(4)))
if (!alwaysEnabeld) {
// now we check that it is disabled, when it should be
// however, note that this check is not exhaustive/complete!
assertThrows[FailedBoundedCheckException] {
verify(mod(false), Seq(BoundedCheck(4)))
}
}
}
it should "always be true when calling read(addr)" in {
check(new ReadEnTestModule(_) { out := mem.read(addr) }, true)
}
it should "always be true when calling read(addr, true.B)" in {
check(new ReadEnTestModule(_) { out := mem.read(addr, true.B) }, true)
}
it should "always be false when calling read(addr, false.B)" in {
check(new ReadEnTestModule(_) {
out := mem.read(addr, false.B)
shouldRead := false.B
shouldNotRead := true.B
})
}
it should "be enabled by iff en=1 when calling read(addr, en)" in {
check(new ReadEnTestModule(_) {
val en = IO(Input(Bool()))
out := mem.read(addr, en)
shouldRead := en
shouldNotRead := !en
})
}
}
abstract class ReadEnTestModule(testShouldRead: Boolean) extends Module {
val addr = IO(Input(UInt(5.W)))
val out = IO(Output(UInt(8.W)))
out := DontCare
// these can be overwritten by the concrete test
val shouldRead = WireInit(true.B)
val shouldNotRead = WireInit(false.B)
// we initialize the memory, so that the output should always equivalent to the read address
val mem = SyncReadMem(32, chiselTypeOf(out))
annotate(new ChiselAnnotation {
override def toFirrtl = MemoryArrayInitAnnotation(mem.toTarget, values = Seq.tabulate(32)(BigInt(_)))
})
// the first cycle after reset, the data will be arbitrary
val firstCycle = RegNext(false.B, init = true.B)
if (testShouldRead) {
when(!firstCycle && RegNext(shouldRead)) {
verification.assert(out === RegNext(addr))
}
} else {
when(!firstCycle && RegNext(shouldNotRead)) {
// this can only fail if the read enable is false and an arbitrary value is provided
// note that this test is not complete!!
verification.assert(out === 200.U)
}
}
}
|
