blob: 20fe6811fd0566e61b3964aed34db365a1ac9f11 (
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
|
(benchmark umulov1bw016.smt
:source {
We verify the correctness of an unsigned multiplication
overflow detection unit, which is described in
"Combined Unsigned and Two's Complement Saturating Multipliers"
by M. Schulte et al.
Bit-width: 4
Contributed by Robert Brummayer (robert.brummayer@gmail.com).
}
:status unsat
:category { industrial }
:logic QF_BV
:difficulty { 0 }
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v2 BitVec[4]))
:formula
(let (?e3 bv0[4])
(let (?e4 (concat ?e3 v1))
(let (?e5 (concat ?e3 v2))
(let (?e6 (bvmul ?e4 ?e5))
(let (?e7 (extract[7:4] ?e6))
(let (?e8 (ite (= ?e7 ?e3) bv1[1] bv0[1]))
(let (?e32 (extract[3:3] v2))
(let (?e34 (extract[2:2] v2))
(let (?e35 (bvand (bvnot ?e32) (bvnot ?e34)))
(let (?e36 (extract[1:1] v2))
(let (?e37 (bvand ?e35 (bvnot ?e36)))
(let (?e38 (extract[1:1] v1))
(let (?e39 (bvand ?e38 ?e32))
(let (?e40 (extract[2:2] v1))
(let (?e41 (bvand ?e40 (bvnot ?e35)))
(let (?e42 (bvand (bvnot ?e39) (bvnot ?e41)))
(let (?e43 (extract[3:3] v1))
(let (?e44 (bvand ?e43 (bvnot ?e37)))
(let (?e45 (bvand ?e42 (bvnot ?e44)))
(let (?e82 bv0[1])
(let (?e83 (concat ?e82 v1))
(let (?e84 (concat ?e82 v2))
(let (?e85 (bvmul ?e83 ?e84))
(let (?e86 (extract[4:4] ?e85))
(let (?e87 (bvand ?e45 (bvnot ?e86)))
(let (?e88 (ite (= (bvnot ?e8) (bvnot ?e87)) bv1[1] bv0[1]))
(not (= (bvnot ?e88) bv0[1]))
)))))))))))))))))))))))))))
|
