blob: 4d96631e1d3d685dfd58964f43895fd3159b24af (
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
62
63
64
65
66
67
68
69
|
// SPDX-License-Identifier: Apache-2.0
package firrtl.backends.experimental.smt
import org.scalatest.flatspec.AnyFlatSpec
class SMTLibSpec extends AnyFlatSpec {
behavior.of("SMTLib backend")
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), "") : a_eq_b
|""".stripMargin
val expected =
"""(declare-sort m_s 0)
|; firrtl-smt2-input a 8
|(declare-fun a_f (m_s) (_ BitVec 8))
|; firrtl-smt2-output b 16
|(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
|; firrtl-smt2-assert a_eq_b 1
|(define-fun a_eq_b_f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
|(define-fun m_t ((state m_s) (state_n m_s)) Bool true)
|(define-fun m_i ((state m_s)) Bool true)
|(define-fun m_a ((state m_s)) Bool (a_eq_b_f state))
|(define-fun m_u ((state m_s)) Bool true)
|""".stripMargin
assert(SMTBackendHelpers.toSMTLibStr(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]
|(declare-sort m_s 0)
|; firrtl-smt2-input a 8
|; @[a 0:0]
|(declare-fun a_f (m_s) (_ BitVec 8))
|; firrtl-smt2-output b 16
|; @[b 0:0], @[b_a 0:0]
|(define-fun b_f ((state m_s)) (_ BitVec 16) ((_ zero_extend 8) (a_f state)))
|; firrtl-smt2-assert assert_0 1
|; @[assert 0:0]
|(define-fun assert_0_f ((state m_s)) Bool (= ((_ zero_extend 8) (a_f state)) (b_f state)))
|(define-fun m_t ((state m_s) (state_n m_s)) Bool true)
|(define-fun m_i ((state m_s)) Bool true)
|(define-fun m_a ((state m_s)) Bool (assert_0_f state))
|(define-fun m_u ((state m_s)) Bool true)
|""".stripMargin
assert(SMTBackendHelpers.toSMTLibStr(src) == expected)
}
}
|
