blob: 32976d308ad36d64d021c5fc4949ba9c9f35e6f6 (
plain)
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
|
// SPDX-License-Identifier: Apache-2.0
package firrtl.backends.experimental.smt
private class Btor2Spec extends SMTBackendBaseSpec {
it should "convert a hello world module" in {
val src =
"""circuit m:
| module m:
| input clock: Clock
| input a: UInt<8>
| output b: UInt<16>
| b <= a
| assert(clock, eq(a, b), UInt(1), "")
|""".stripMargin
val expected =
"""1 sort bitvec 8
|2 input 1 a
|3 sort bitvec 16
|4 uext 3 2 8
|5 output 4 ; b
|6 sort bitvec 1
|7 uext 3 2 8
|8 eq 6 7 4
|9 not 6 8
|10 bad 9 ; assert_
|""".stripMargin
assert(toBotr2Str(src) == expected)
}
it should "include FileInfo in the output" in {
val src =
"""circuit m: @[circuit 0:0]
| module m: @[module 0:0]
| input clock: Clock @[clock 0:0]
| input a: UInt<8> @[a 0:0]
| output b: UInt<16> @[b 0:0]
| b <= a @[b_a 0:0]
| assert(clock, eq(a, b), UInt(1), "") @[assert 0:0]
|""".stripMargin
val expected =
"""; @ module 0:0
|1 sort bitvec 8
|2 input 1 a ; @ a 0:0
|3 sort bitvec 16
|4 uext 3 2 8
|5 output 4 ; b @ b 0:0, b_a 0:0
|6 sort bitvec 1
|7 uext 3 2 8
|8 eq 6 7 4
|9 not 6 8
|10 bad 9 ; assert_ @ assert 0:0
|""".stripMargin
assert(toBotr2Str(src) == expected)
}
}
|
