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
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
#!/usr/bin/env python2
import sys, getopt
def usage():
print "usage: adder [-h] [-n <n>]"
sys.exit(0)
def die(msg):
assert msg != None
print msg
sys.exit(1)
def is_power_of_2 (x):
assert x > 0
return (x & (x - 1)) == 0
def next_power_of_2 (x):
assert x > 0
x -= 1
i = 1
while i < 32:
x = x | (x >> i)
i *= 2
return x + 1
def log2 (x):
result = 0
assert x > 0
assert is_power_of_2 (x)
while x > 1:
x >>= 1
result += 1
assert result >= 0
return result
n = 32
id = 1
def add_seq (list, ext):
global id
assert list != None
assert len (list) >= 2
assert ext >= 0
print "(let (?e" + str(id) + " (zero_extend[" + str(ext) + \
"] " + list[0] + "))"
last = "?e" + str(id)
id += 1
for i in range(1, len(list)):
print "(let (?e" + str(id) + " (bvadd " + last + " (zero_extend[" + \
str(ext) + "] " + list[i] + ")))"
last = "?e" + str(id)
id += 1
return last, ext + 1
def add_par (list):
global id
bw = 1
assert list != None
assert len (list) >= 2
while len(list) != 1:
i = 0
next = []
while i < len(list):
if i != len(list) - 1:
print "(let (?e" + str(id) + " (bvadd (zero_extend[1] " + \
list[i] + ") (zero_extend[1] " + list[i + 1] + ")))"
else:
print "(let (?e" + str(id) + " (zero_extend[1] " + list[i] + "))"
last = "?e" + str(id)
next.append(last)
id += 1
i += 2
list = next
bw += 1
return last, bw
try:
opts, args = getopt.getopt(sys.argv[1:], "hn:")
except getopt.GetoptError, err:
print str(err)
usage()
for o, a in opts:
if o in ("-h"):
usage()
elif o in ("-n"):
n = int (a)
if n < 2:
die ("n must be >= 2")
num_bits_n = log2 (next_power_of_2 (n + 1))
print "(benchmark adderEqCheck" + str(n)
print ":source {"
print "Equivalence checking of adder circuits on " + str(n) + " inputs of BW 1"
print "We verifiy the equivalence of tree-like and linear circuit layout"
print "Contributed by Robert Brummayer (robert.brummayer@gmail.com)"
print "}"
print ":status unsat"
print ":logic QF_BV"
list = []
for i in range(n):
print ":extrafuns ((v" + str(i) + " BitVec[1]))"
list.append("v" + str(i))
print ":formula"
result_simple, bw_simple = add_seq (list, num_bits_n - 1)
result_par, bw_par = add_par (list)
if bw_par < bw_simple:
ext = bw_simple - bw_par
print "(not (= " + result_simple + " (zero_extend[" + str(ext) + "] " + \
result_par + ")))"
elif bw_par > bw_simple:
ext = bw_par - bw_simple
print "(not (= (zero_extend[" + str(ext) + "] " + result_simple + ") " + \
result_par + "))"
else:
print "(not (= " + result_simple + " " + result_par + "))"
pars = ""
for i in range(id):
pars = pars + ")"
print pars
|
