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
|
// SPDX-License-Identifier: Apache-2.0
package firrtl.backends.experimental.smt.end2end
class AssertAssumeStopSpec extends EndToEndSMTBaseSpec {
behavior.of("the SMT backend")
private def prefix(ii: Int): String =
s"""circuit AssertAssumStop$ii:
| module AssertAssumStop$ii:
| input clock: Clock
| input a: UInt<8>
| output b: UInt<8>
|
| b <= add(a, UInt(16))
|
|""".stripMargin
it should "support assertions" in {
val src = prefix(0) +
""" assert(clock, gt(b, a), lt(a, UInt(240)), "") : b_gt_a
|""".stripMargin
test(src, MCSuccess, kmax = 2)
}
it should "support assumptions" in {
val src = prefix(1) +
""" assert(clock, gt(b, a), UInt(1), "") : b_gt_a
|""".stripMargin
val srcWithAssume = prefix(2) +
""" assert(clock, gt(b, a), UInt(1), "") : b_gt_a
| assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
|""".stripMargin
// the assertion alone fails because of potential overflow
test(src, MCFail(0), kmax = 2)
// with the assumption that a is not too big, it works!
test(srcWithAssume, MCSuccess, kmax = 2)
}
it should "treat stop with ret =/= 0 as assertion" in {
val src = prefix(3) +
""" stop(clock, not(gt(b, a)), 1) : b_gt_a
|""".stripMargin
val srcWithAssume = prefix(4) +
""" stop(clock, not(gt(b, a)), 1) : b_gt_a
| assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
|""".stripMargin
// the assertion alone fails because of potential overflow
test(src, MCFail(0), kmax = 2)
// with the assumption that a is not too big, it works!
test(srcWithAssume, MCSuccess, kmax = 2)
}
it should "ignore stop with ret === 0" in {
val src = prefix(5) +
""" stop(clock, not(gt(b, a)), 1) : b_gt_a
| assume(clock, lt(a, UInt(240)), UInt(1), "") : a_lt_240
| stop(clock, UInt(1), 0) : always_stop
|""".stripMargin
test(src, MCSuccess, kmax = 2)
}
}
|
