Skip to content

Commit e1e997a

Browse files
peterschrammelpeterschrammel
committed
Missing operators for IMul1; IMul1 passes through the typechecker
1 parent 9cfa2ff commit e1e997a

File tree

5 files changed

+319
-0
lines changed

5 files changed

+319
-0
lines changed

‎regression/systemc/BitvectorSc7/main.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,15 @@ typedef sc_uint<4> uint256_t;
88

99
void check()
1010
{
11+
#if 0
12+
uint1_t abc;
13+
#endif
14+
1115
uint1_t result;
1216
result.range(0,0) = result.range(0,0);
1317

1418
uint1_t spec(0), impl(1);
19+
1520
assert(impl == spec);
1621
}
1722

@@ -20,6 +25,7 @@ int main(int argc, char *argv[])
2025
#if 1
2126
uint1_t abc;
2227
#endif
28+
2329
check();
2430

2531
return 0;

‎regression/systemc/IMul1/main.cpp

Lines changed: 254 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,254 @@
1+
// Simple Masc example: integer multiplication
2+
// John O'Leary, 28 May 2013
3+
4+
#include <cassert>
5+
#include "../systemc_util.cpp"
6+
#include "../sc_uint_base.cpp"
7+
#include "../sc_uint.h"
8+
#include "../masc.h"
9+
10+
#ifndef __CPROVER__
11+
#include <iostream>
12+
#include <bitset>
13+
using namespace std;
14+
//using namespace sc_dt;
15+
#endif
16+
17+
18+
// Masc begin
19+
20+
// This Masc code describes a 32x32 -> 64 unsigned integer multiplier
21+
// Adapted from significand_multiplier_r4_param in Warren Ferguson's
22+
// library of Verilog reference models.
23+
24+
typedef sc_uint<32> ui32;
25+
typedef sc_uint<64> ui64;
26+
typedef sc_uint<35> ui35;
27+
typedef sc_uint<3> ui3;
28+
typedef sc_uint<33> ui33; //big
29+
typedef sc_uint<67> ui67; //big
30+
31+
// Step 1: construct an array of radix-4 digits for a source multiplier.
32+
33+
// For each 3-bit slice x[2*k+1:2*k-1] of the multiplier, we compute a
34+
// 3-bit sign-magnitude encoding of x[2*k-1] + x[2*k] - 2 * x[2*k+1]:
35+
36+
ui3 Encode(ui3 slice) {
37+
ui3 enc;
38+
switch (slice.to_uint()) {
39+
case 4:
40+
enc = 6; // -2 -> 110
41+
break;
42+
case 5: case 6:
43+
enc = 5; // -1 -> 101
44+
break;
45+
case 7: case 0:
46+
enc = 0; // 0 -> 000
47+
break;
48+
case 1: case 2:
49+
enc = 1; // +1 -> 001
50+
break;
51+
case 3:
52+
enc = 2; // +2 -> 010
53+
break;
54+
default:
55+
assert(false);
56+
}
57+
return enc;
58+
}
59+
60+
array<ui3, 17> Booth (ui32 x) {
61+
62+
// Pad the multiplier with 2 leading zeroes and 1 trailing zero:
63+
ui35 x35(x.to_uint()); // << 1;
64+
x35 <<= 1;
65+
66+
// Compute the booth encodings:
67+
array<ui3, 17> a;
68+
for (int k=0; k<17; k++) {
69+
a[k] = Encode(x35.range(2*k+2, 2*k));
70+
}
71+
return a;
72+
}
73+
74+
// Step 2: Form the partial products.
75+
76+
array<ui33, 17> PartialProducts (array<ui3, 17> m21, ui32 y) {
77+
array<ui33, 17> pp;
78+
79+
for (int k=0; k<17; k++) {
80+
ui33 row;
81+
switch (m21[k].range(1,0).to_uint()) {
82+
case 2:
83+
row = y; // << 1;
84+
row <<= 1;
85+
break;
86+
case 1:
87+
row = y;
88+
break;
89+
default:
90+
row = 0;
91+
}
92+
pp[k] = m21[k][2] ? ~row : row;
93+
}
94+
95+
return pp;
96+
}
97+
98+
// Step 3: Construct the table of aligned partial products.
99+
100+
array<ui64, 17> Align(array<ui3, 17> bds, array<ui33, 17> pps) {
101+
102+
// Extract the sign bits from the booth encodings:
103+
array<bool, 17> sb;
104+
array<bool, 18> psb;
105+
for (int k=0; k<17; k++) {
106+
sb[k] = bds[k][2];
107+
psb[k+1] = bds[k][2];
108+
}
109+
110+
// Build the table:
111+
array<ui64, 17> tble;
112+
for (int k=0; k<17; k++) {
113+
ui67 tmp = 0;
114+
tmp.range(2*k+32, 2*k) = pps[k];
115+
if (k == 0) {
116+
tmp[33] = sb[k];
117+
tmp[34] = sb[k];
118+
tmp[35] = !sb[k];
119+
}
120+
else {
121+
tmp[2*k-2] = psb[k];
122+
tmp[2*k+33] = !sb[k];
123+
tmp[2*k+34] = 1;
124+
}
125+
126+
tble[k] = tmp.range(63, 0);
127+
}
128+
129+
return tble;
130+
}
131+
132+
// Step 4: Sum the rows of the table of aligned partial products
133+
134+
// The compression tree is constucted from two basic modules:
135+
136+
tuple<ui64, ui64> Compress32(ui64 in0, ui64 in1, ui64 in2) {
137+
ui64 out0 = in0 ^ in1 ^ in2;
138+
ui64 out1 = in0 & in1 | in0 &in2 | in1 & in2;
139+
out1 <<= 1;
140+
return tuple<ui64, ui64>(out0, out1);
141+
}
142+
143+
tuple<ui64, ui64> Compress42(ui64 in0, ui64 in1, ui64 in2, ui64 in3) {
144+
ui64 temp = (in1 & in2 | in1 & in3 | in2 & in3);// << 1;
145+
temp <<= 1;
146+
ui64 out0 = in0 ^ in1 ^ in2 ^ in3 ^ temp;
147+
ui64 out1 = (in0 & ~(in0 ^ in1 ^ in2 ^ in3)) | (temp & (in0 ^ in1 ^ in2 ^ in3));
148+
out1 <<= 1;
149+
return tuple<ui64, ui64>(out0, out1);
150+
}
151+
152+
ui64 Sum(array<ui64, 17> in) {
153+
154+
// level 1 consists of 4 4:2 compressors
155+
array<ui64, 8> A1;
156+
for (uint i=0; i<4; i++) {
157+
tie(A1[2*i+0], A1[2*i+1]) = Compress42(in[4*i], in[4*i+1], in[4*i+2], in[4*i+3]);
158+
}
159+
160+
// level 2 consists of 2 4:2 compressors
161+
array<ui64, 4> A2;
162+
for (uint i=0; i<2; i++) {
163+
tie(A2[2*i+0], A2[2*i+1]) = Compress42(A1[4*i], A1[4*i+1], A1[4*i+2], A1[4*i+3]);
164+
}
165+
166+
// level 3 consists of 1 4:2 compressor
167+
array<ui64, 2> A3;
168+
tie(A3[0], A3[1]) = Compress42(A2[0], A2[1], A2[2], A2[3]);
169+
170+
// level 4 consists of 1 3:2 compressor
171+
array<ui64, 2> A4;
172+
tie(A4[0], A4[1]) = Compress32(A3[0], A3[1], in[16]);
173+
174+
// The final sum:
175+
return A4[0] + A4[1];
176+
}
177+
178+
// Stitch it together
179+
180+
ui64 Imul(ui32 s1, ui32 s2) {
181+
182+
#ifndef __CPROVER__
183+
cout << "Operands:" << endl;
184+
cout << hex << s1 << endl;
185+
cout << hex << s1 << endl;
186+
#endif
187+
188+
array<ui3, 17> bd = Booth(s1);
189+
190+
#ifndef __CPROVER__
191+
cout << "Booth digits:" << endl;
192+
for (int i=0; i<17; i++) {
193+
cout << i << ": " << bd[i][2] << bd[i][1] << bd[i][0] << endl;
194+
}
195+
#endif
196+
197+
array<ui33, 17> pp = PartialProducts(bd, s2);
198+
199+
#ifndef __CPROVER__
200+
cout << "Partial products:" << endl;
201+
for (int i=0; i<17; i++) {
202+
cout << i << ": " << hex << pp[i] << endl;
203+
}
204+
#endif
205+
206+
array<ui64, 17> tble = Align (bd, pp);
207+
208+
#ifndef __CPROVER__
209+
cout << "Aligned partial products:" << endl;
210+
for (int i=0; i<17; i++) {
211+
cout << i << ": " << hex << tble[i] << endl;
212+
}
213+
#endif
214+
215+
ui64 prod = Sum(tble);
216+
217+
218+
#ifndef __CPROVER__
219+
cout << "Product:" << endl;
220+
cout << hex << prod << endl;
221+
#endif
222+
223+
return prod;
224+
225+
}
226+
227+
tuple<bool, ui64, ui64>ImulTest(ui32 s1, ui32 s2) {
228+
ui64 spec_result; //= s1 * s2;
229+
spec_result = s1 * s2;
230+
ui64 imul_result = Imul(s1, s2);
231+
#ifndef __CPROVER__
232+
cout << "Expected:" << endl;
233+
cout << hex << spec_result << endl;
234+
#endif
235+
return tuple<bool, ui64, ui64>(spec_result == imul_result, spec_result, imul_result);
236+
}
237+
238+
// Masc end
239+
240+
int main(int argc, char *argv[])
241+
{
242+
{
243+
ui32 src1(4);
244+
ui32 src2(4);
245+
ui64 spec_result;
246+
ui64 imul_result;
247+
bool passed;
248+
tie(passed, spec_result, imul_result) = ImulTest(src1, src2);
249+
assert(passed);
250+
}
251+
252+
return 0;
253+
}
254+

‎regression/systemc/IMul1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.cpp
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^VERIFICATION SUCCESSFUL$
7+
--
8+
^warning: ignoring

‎regression/systemc/sc_uint.h

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,31 @@ class sc_uint : public sc_uint_base
8282
return sc_uint_base::operator>>=(v);
8383
}
8484

85+
sc_uint<W> operator <<= (int v)
86+
{
87+
return sc_uint_base::operator<<=(v);
88+
}
89+
90+
sc_uint<W> operator~ ()
91+
{
92+
return sc_uint_base::operator~();
93+
}
94+
95+
sc_uint<W> operator^ (const sc_uint_base &other)
96+
{
97+
return sc_uint<W>(sc_uint_base::operator^(other));
98+
}
99+
100+
sc_uint<W> operator| (const sc_uint_base &other)
101+
{
102+
return sc_uint<W>(sc_uint_base::operator|(other));
103+
}
104+
105+
sc_uint<W> operator& (const sc_uint_base &other)
106+
{
107+
return sc_uint<W>(sc_uint_base::operator&(other));
108+
}
109+
85110
};
86111

87112
#ifndef __CPROVER__

‎regression/systemc/sc_uint_base.h

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,11 +114,37 @@ class sc_uint_base
114114
return *this;
115115
}
116116

117+
sc_uint_base operator<<=(int v) //uint_type v
118+
{
119+
val <<= v;
120+
return *this;
121+
}
122+
117123
sc_uint_base operator+(const sc_uint_base &other)
118124
{
119125
return sc_uint_base(val+other.val, m_len);
120126
}
121127

128+
sc_uint_base operator~()
129+
{
130+
return sc_uint_base(~val, m_len);
131+
}
132+
133+
sc_uint_base operator^(const sc_uint_base &other)
134+
{
135+
return sc_uint_base(val^other.val, m_len);
136+
}
137+
138+
sc_uint_base operator|(const sc_uint_base &other)
139+
{
140+
return sc_uint_base(val|other.val, m_len);
141+
}
142+
143+
sc_uint_base operator&(const sc_uint_base &other)
144+
{
145+
return sc_uint_base(val&other.val, m_len);
146+
}
147+
122148
sc_uint_base operator*(const sc_uint_base &other)
123149
{
124150
return sc_uint_base(val*other.val, m_len);

0 commit comments

Comments
 (0)