ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
wlc.c
Go to the documentation of this file.
1
20
21#include "wlc.h"
22#include "sat/bsat/satStore.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
33
34
46void Wlc_GenerateCodeMax4( int nBits )
47{
48 int nWidth, nSteps, i;
49 FILE * pFile = fopen( "max4.v", "wb" );
50 if ( pFile == NULL )
51 return;
52
53 for ( nSteps = 0, nWidth = 1; nWidth < nBits; nWidth *= 3, nSteps++ );
54
55 fprintf( pFile, "module max4 ( a, b, c, d, res, addr );\n\n" );
56 fprintf( pFile, " input [%d:0] a, b, c, d;\n", nBits-1 );
57 fprintf( pFile, " output [%d:0] res;\n", nBits-1 );
58 fprintf( pFile, " output [1:0] addr;\n\n" );
59
60 fprintf( pFile, " wire [%d:0] A = a;\n", nWidth-1 );
61 fprintf( pFile, " wire [%d:0] B = b;\n", nWidth-1 );
62 fprintf( pFile, " wire [%d:0] C = c;\n", nWidth-1 );
63 fprintf( pFile, " wire [%d:0] D = d;\n\n", nWidth-1 );
64
65 fprintf( pFile, " wire AB, AC, AD, BC, BD, CD;\n\n" );
66
67 fprintf( pFile, " comp( A, B, AB );\n" );
68 fprintf( pFile, " comp( A, C, AC );\n" );
69 fprintf( pFile, " comp( A, D, AD );\n" );
70 fprintf( pFile, " comp( B, C, BC );\n" );
71 fprintf( pFile, " comp( B, D, BD );\n" );
72 fprintf( pFile, " comp( C, D, CD );\n\n" );
73
74 fprintf( pFile, " assign addr = AB ? (CD ? (AC ? 2\'b00 : 2\'b10) : (AD ? 2\'b00 : 2\'b11)) : (CD ? (BC ? 2\'b01 : 2\'b10) : (BD ? 2\'b01 : 2\'b11));\n\n" );
75 fprintf( pFile, " assign res = addr[1] ? (addr[1] ? d : c) : (addr[0] ? b : a);\n\n" );
76 fprintf( pFile, "endmodule\n\n\n" );
77
78
79 fprintf( pFile, "module comp ( a, b, res );\n\n" );
80 fprintf( pFile, " input [%d:0] a, b;\n", nWidth-1 );
81 fprintf( pFile, " output res;\n" );
82 fprintf( pFile, " wire res2;\n\n" );
83
84 fprintf( pFile, " wire [%d:0] A = a & ~b;\n", nWidth-1 );
85 fprintf( pFile, " wire [%d:0] B = ~a & b;\n\n", nWidth-1 );
86
87 fprintf( pFile, " comp0( A, B, res, res2 );\n\n" );
88
89 fprintf( pFile, "endmodule\n\n\n" );
90
91
92 for ( i = 0; i < nSteps; i++ )
93 {
94 fprintf( pFile, "module comp%d ( a, b, yes, no );\n\n", i );
95 fprintf( pFile, " input [%d:0] a, b;\n", nWidth-1 );
96 fprintf( pFile, " output yes, no;\n\n", nWidth/3-1 );
97
98 fprintf( pFile, " wire [2:0] y, n;\n\n" );
99
100 if ( i == nSteps - 1 )
101 {
102 fprintf( pFile, " assign y = a;\n" );
103 fprintf( pFile, " assign n = b;\n\n" );
104 }
105 else
106 {
107 fprintf( pFile, " wire [%d:0] A0 = a[%d:%d];\n", nWidth/3-1, nWidth/3-1, 0 );
108 fprintf( pFile, " wire [%d:0] A1 = a[%d:%d];\n", nWidth/3-1, 2*nWidth/3-1, nWidth/3 );
109 fprintf( pFile, " wire [%d:0] A2 = a[%d:%d];\n\n", nWidth/3-1, nWidth-1, 2*nWidth/3 );
110
111 fprintf( pFile, " wire [%d:0] B0 = b[%d:%d];\n", nWidth/3-1, nWidth/3-1, 0 );
112 fprintf( pFile, " wire [%d:0] B1 = b[%d:%d];\n", nWidth/3-1, 2*nWidth/3-1, nWidth/3 );
113 fprintf( pFile, " wire [%d:0] B2 = b[%d:%d];\n\n", nWidth/3-1, nWidth-1, 2*nWidth/3 );
114
115 fprintf( pFile, " comp%d( A0, B0, y[0], n[0] );\n", i+1 );
116 fprintf( pFile, " comp%d( A1, B1, y[1], n[1] );\n", i+1 );
117 fprintf( pFile, " comp%d( A2, B2, y[2], n[2] );\n\n", i+1 );
118 }
119
120 fprintf( pFile, " assign yes = y[0] | (~y[0] & ~n[0] & y[1]) | (~y[0] & ~n[0] & ~y[1] & ~n[1] & y[2]);\n" );
121 fprintf( pFile, " assign no = n[0] | (~y[0] & ~n[0] & n[1]) | (~y[0] & ~n[0] & ~y[1] & ~n[1] & n[2]);\n\n" );
122
123 fprintf( pFile, "endmodule\n\n\n" );
124
125 nWidth /= 3;
126 }
127 fclose( pFile );
128}
129
130
142void Wlc_BlastFullAdderCtrlCnf( sat_solver * pSat, int a, int ac, int b, int c, int * pc, int * ps, int * piVars )
143{
144 int Cnf[12][6] = { // xabc cs // abc cs
145
146 { -1, 0, 0, 0, 0, 0 }, // -000 00 // 000 00
147 { -1, 0, 0, 1, 0, 1 }, // -001 01 // 001 01
148 { -1, 0, 1, 0, 0, 1 }, // -010 01 // 010 01
149 { -1, 0, 1, 1, 1, 0 }, // -011 10 // 011 10
150
151 { 0,-1, 0, 0, 0, 0 }, // 0-00 00
152 { 0,-1, 0, 1, 0, 1 }, // 0-01 01
153 { 0,-1, 1, 0, 0, 1 }, // 0-10 01
154 { 0,-1, 1, 1, 1, 0 }, // 0-11 10
155
156 { 1, 1, 0, 0, 0, 1 }, // 1100 01 // 100 01
157 { 1, 1, 0, 1, 1, 0 }, // 1101 10 // 101 10
158 { 1, 1, 1, 0, 1, 0 }, // 1110 10 // 110 10
159 { 1, 1, 1, 1, 1, 1 } // 1111 11 // 111 11
160 };
161
162 int pVars[6] = {a, ac, b, c, *piVars, *piVars+1};
163 int i, v, nLits, pLits[6];
164 for ( i = 0; i < 12; i++ )
165 {
166 nLits = 0;
167 for ( v = 0; v < 6; v++ )
168 {
169 if ( Cnf[i][v] == -1 )
170 continue;
171 if ( pVars[v] == 0 ) // const 0
172 {
173 if ( Cnf[i][v] == 0 )
174 continue;
175 if ( Cnf[i][v] == 1 )
176 break;
177 }
178 if ( pVars[v] == -1 ) // const -1
179 {
180 if ( Cnf[i][v] == 0 )
181 break;
182 if ( Cnf[i][v] == 1 )
183 continue;
184 }
185 pLits[nLits++] = Abc_Var2Lit( pVars[v], Cnf[i][v] );
186 }
187 if ( v < 6 )
188 continue;
189 assert( nLits > 2 );
190 sat_solver_addclause( pSat, pLits, pLits + nLits );
191 }
192 *pc = (*piVars)++;
193 *ps = (*piVars)++;
194}
195void Wlc_BlastMultiplierCnf( sat_solver * pSat, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vTemp, Vec_Int_t * vRes, int * piVars )
196{
197 int * pRes, * pArgC, * pArgS, a, b, Carry = 0;
198 assert( nArgA > 0 && nArgB > 0 );
199 // prepare result
200 Vec_IntFill( vRes, nArgA + nArgB, 0 );
201 pRes = Vec_IntArray( vRes );
202 // prepare intermediate storage
203 Vec_IntFill( vTemp, 2 * nArgA, 0 );
204 pArgC = Vec_IntArray( vTemp );
205 pArgS = pArgC + nArgA;
206 // create matrix
207 for ( b = 0; b < nArgB; b++ )
208 for ( a = 0; a < nArgA; a++ )
209 Wlc_BlastFullAdderCtrlCnf( pSat, pArgA[a], pArgB[b], pArgS[a], pArgC[a], &pArgC[a], a ? &pArgS[a-1] : &pRes[b], piVars );
210 // final addition
211 pArgS[nArgA-1] = 0;
212 for ( a = 0; a < nArgA; a++ )
213 Wlc_BlastFullAdderCtrlCnf( pSat, -1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], piVars );
214}
215sat_solver * Wlc_BlastMultiplierCnfMain( int nBits )
216{
217 Vec_Int_t * vRes1 = Vec_IntAlloc( 2*nBits );
218 Vec_Int_t * vRes2 = Vec_IntAlloc( 2*nBits );
219 Vec_Int_t * vTemp = Vec_IntAlloc( 2*nBits );
220
221 int * pArgA = ABC_ALLOC( int, nBits );
222 int * pArgB = ABC_ALLOC( int, nBits );
223 int i, Ent1, Ent2, nVars = 1 + 2*nBits;
224 int nVarsAll = 1 + 4*nBits + 4*nBits*(nBits + 1);
225
226 sat_solver * pSat = sat_solver_new();
227 sat_solver_setnvars( pSat, nVarsAll );
228
229 for ( i = 0; i < nBits; i++ )
230 pArgA[i] = 1 + i, pArgB[i] = 1 + nBits + i;
231 Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes1, &nVars );
232
233 for ( i = 0; i < nBits; i++ )
234 pArgA[i] = 1 + nBits + i, pArgB[i] = 1 + i;
235 Wlc_BlastMultiplierCnf( pSat, pArgA, pArgB, nBits, nBits, vTemp, vRes2, &nVars );
236
237 Vec_IntClear( vTemp );
238 Vec_IntForEachEntryTwo( vRes1, vRes2, Ent1, Ent2, i )
239 {
240 Vec_IntPush( vTemp, Abc_Var2Lit(nVars, 0) );
241 sat_solver_add_xor( pSat, Ent1, Ent2, nVars++, 0 );
242 }
243 assert( nVars == nVarsAll );
244 sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) );
245
246 ABC_FREE( pArgA );
247 ABC_FREE( pArgB );
248 Vec_IntFree( vRes1 );
249 Vec_IntFree( vRes2 );
250 Vec_IntFree( vTemp );
251 return pSat;
252}
253void Wlc_BlastMultiplierCnfTest( int nBits )
254{
255 abctime clk = Abc_Clock();
256 sat_solver * pSat = Wlc_BlastMultiplierCnfMain( nBits );
257 int i, status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
258 Sat_SolverWriteDimacs( pSat, "test_mult.cnf", NULL, NULL, 0 );
259 for ( i = 0; i < sat_solver_nvars(pSat); i++ )
260 printf( "%d=%d ", i, sat_solver_var_value(pSat, i) );
261 printf( "\n" );
262
263 printf( "Verifying for %d bits: %s ", nBits, status == l_True ? "SAT" : "UNSAT" );
264 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
265 sat_solver_delete( pSat );
266}
267
279Vec_Int_t * Wlc_ManGenAdderN( Gia_Man_t * p, int nLits, int * pLitsA, int * pLitsB, int Carry )
280{
281 extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps );
282 Vec_Int_t * vRes = Vec_IntStart( nLits + 1 );
283 int i, * pRes = Vec_IntArray(vRes);
284 for ( i = 0; i < nLits; i++ )
285 Wlc_BlastFullAdder( p, pLitsA[i], pLitsB[i], Carry, &Carry, &pRes[i] );
286 pRes[nLits] = Carry;
287 return vRes;
288}
289Vec_Int_t * Wlc_ManGenAdder2_rec( Gia_Man_t * p, int nLits, int * pLitsA, int * pLitsB, int Carry, int Size )
290{
291 Vec_Int_t * vRes, * vRes0, * vRes1, * vRes2; int i, iCtrl;
292 if ( nLits == Size )
293 return Wlc_ManGenAdderN( p, nLits, pLitsA, pLitsB, Carry );
294 vRes0 = Wlc_ManGenAdder2_rec( p, nLits/2, pLitsA, pLitsB, Carry, Size );
295 vRes1 = Wlc_ManGenAdder2_rec( p, nLits/2, pLitsA + nLits/2, pLitsB + nLits/2, 0, Size );
296 vRes2 = Wlc_ManGenAdder2_rec( p, nLits/2, pLitsA + nLits/2, pLitsB + nLits/2, 1, Size );
297 vRes = Vec_IntAlloc( nLits + 1 );
298 Vec_IntAppend( vRes, vRes0 );
299 iCtrl = Vec_IntPop( vRes );
300 for ( i = 0; i <= nLits/2; i++ )
301 Vec_IntPush( vRes, Gia_ManHashMux(p, iCtrl, Vec_IntEntry(vRes2, i), Vec_IntEntry(vRes1, i)) );
302 assert( Vec_IntSize(vRes) == nLits + 1 );
303 Vec_IntFree( vRes0 );
304 Vec_IntFree( vRes1 );
305 Vec_IntFree( vRes2 );
306 return vRes;
307}
308Gia_Man_t * Wlc_ManGenAdder2( int nBits, int Size, int fSigned )
309{
310 Gia_Man_t * pTemp, * pNew; int n, i, iLit, nBitsAll;
311 Vec_Int_t * vOuts, * vLits = Vec_IntAlloc( 1000 );
312 pNew = Gia_ManStart( 1000 );
313 pNew->pName = Abc_UtilStrsav( "adder" );
314 for ( nBitsAll = Size; nBitsAll < nBits; nBitsAll *= 2 )
315 ;
316 for ( n = 0; n < 2; n++ )
317 {
318 for ( i = 0; i < nBits; i++ )
319 Vec_IntPush( vLits, Gia_ManAppendCi(pNew) );
320 for ( ; i < nBitsAll; i++ )
321 Vec_IntPush( vLits, fSigned ? Vec_IntEntry(vLits, nBits-1) : 0 );
322 }
323 Gia_ManHashAlloc( pNew );
324 vOuts = Wlc_ManGenAdder2_rec( pNew, nBitsAll, Vec_IntEntryP(vLits, 0), Vec_IntEntryP(vLits, Vec_IntSize(vLits)/2), 0, Size );
325 Gia_ManHashStop( pNew );
326 Vec_IntForEachEntry( vOuts, iLit, i )
327 Gia_ManAppendCo( pNew, iLit );
328 Vec_IntFree( vLits );
329 Vec_IntFree( vOuts );
330 pNew = Gia_ManCleanup( pTemp = pNew );
331 Gia_ManStop( pTemp );
332 return pNew;
333}
334
335Vec_Int_t * Wlc_ManGenAdder_rec( Gia_Man_t * p, int nLits, int * pLitsA, int * pLitsB, int Carry, int Size )
336{
337 Vec_Int_t * vRes, * vRes0, * vRes1, * vRes2, * vRes3, * vRes4; int i, iCtrl;
338 if ( nLits == Size )
339 return Wlc_ManGenAdderN( p, nLits, pLitsA, pLitsB, Carry );
340 assert( nLits % 3 == 0 );
341 vRes0 = Wlc_ManGenAdder_rec( p, nLits/3, pLitsA + 0*nLits/3, pLitsB + 0*nLits/3, Carry, Size );
342 vRes1 = Wlc_ManGenAdder_rec( p, nLits/3, pLitsA + 1*nLits/3, pLitsB + 1*nLits/3, 0, Size );
343 vRes2 = Wlc_ManGenAdder_rec( p, nLits/3, pLitsA + 1*nLits/3, pLitsB + 1*nLits/3, 1, Size );
344 vRes3 = Wlc_ManGenAdder_rec( p, nLits/3, pLitsA + 2*nLits/3, pLitsB + 2*nLits/3, 0, Size );
345 vRes4 = Wlc_ManGenAdder_rec( p, nLits/3, pLitsA + 2*nLits/3, pLitsB + 2*nLits/3, 1, Size );
346 vRes = Vec_IntAlloc( nLits + 1 );
347 Vec_IntAppend( vRes, vRes0 );
348 iCtrl = Vec_IntPop( vRes );
349 for ( i = 0; i <= nLits/3; i++ )
350 Vec_IntPush( vRes, Gia_ManHashMux(p, iCtrl, Vec_IntEntry(vRes2, i), Vec_IntEntry(vRes1, i)) );
351 iCtrl = Vec_IntPop( vRes );
352 for ( i = 0; i <= nLits/3; i++ )
353 Vec_IntPush( vRes, Gia_ManHashMux(p, iCtrl, Vec_IntEntry(vRes4, i), Vec_IntEntry(vRes3, i)) );
354 assert( Vec_IntSize(vRes) == nLits + 1 );
355 Vec_IntFree( vRes0 );
356 Vec_IntFree( vRes1 );
357 Vec_IntFree( vRes2 );
358 Vec_IntFree( vRes3 );
359 Vec_IntFree( vRes4 );
360 return vRes;
361}
362Gia_Man_t * Wlc_ManGenAdder( int nBits )
363{
364 Gia_Man_t * pTemp, * pNew; int n, i, iLit, nBitsAll;
365 Vec_Int_t * vOuts, * vLits = Vec_IntAlloc( 1000 );
366 pNew = Gia_ManStart( 1000 );
367 pNew->pName = Abc_UtilStrsav( "adder" );
368 for ( nBitsAll = 3; nBitsAll < nBits; nBitsAll *= 3 )
369 ;
370 for ( n = 0; n < 2; n++ )
371 {
372 for ( i = 0; i < nBits; i++ )
373 Vec_IntPush( vLits, Gia_ManAppendCi(pNew) );
374 for ( ; i < nBitsAll; i++ )
375 Vec_IntPush( vLits, 0 );
376 }
377 Gia_ManHashAlloc( pNew );
378 vOuts = Wlc_ManGenAdder_rec( pNew, nBitsAll, Vec_IntEntryP(vLits, 0), Vec_IntEntryP(vLits, Vec_IntSize(vLits)/2), 0, 3 );
379 Gia_ManHashStop( pNew );
380 Vec_IntForEachEntryStop( vOuts, iLit, i, nBits+1 )
381 Gia_ManAppendCo( pNew, iLit );
382 Vec_IntFree( vLits );
383 Vec_IntFree( vOuts );
384 pNew = Gia_ManCleanup( pTemp = pNew );
385 Gia_ManStop( pTemp );
386 return pNew;
387}
388
400void Wlc_BuildOne32( Gia_Man_t * p, int * pLitIn, int * pLitOut )
401{
402 Wlc_BlastFullAdder( p, pLitIn[0], pLitIn[1], pLitIn[2], &pLitIn[5], &pLitOut[0] );
403 Wlc_BlastFullAdder( p, pLitIn[3], pLitIn[4], pLitIn[5], &pLitOut[2], &pLitOut[1] );
404}
405void Wlc_BuildOne51( Gia_Man_t * p, int * pLitIn, int * pLitOut )
406{
407 int Lit00, Lit01, Lit11;
408 Wlc_BlastFullAdder( p, pLitIn[0], pLitIn[1], pLitIn[2], &Lit01, &Lit00 );
409 Wlc_BlastFullAdder( p, pLitIn[3], pLitIn[4], Lit00, &Lit11, &pLitOut[0] );
410 Wlc_BlastFullAdder( p, pLitIn[5], Lit01, Lit11, &pLitOut[2], &pLitOut[1] );
411}
412void Wlc_BuildOne6( Gia_Man_t * p, int * pLitIn, int Const1, int * pLitOut )
413{
414 int Lit00, Lit01, Lit10, Lit11, Lit12;
415 Wlc_BlastFullAdder( p, pLitIn[0], pLitIn[1], pLitIn[2], &Lit01, &Lit00 );
416 Wlc_BlastFullAdder( p, pLitIn[3], pLitIn[4], pLitIn[5], &Lit11, &Lit10 );
417 Wlc_BlastFullAdder( p, Lit00, Lit10, Const1, &Lit12, &pLitOut[0] );
418 Wlc_BlastFullAdder( p, Lit01, Lit11, Lit12, &pLitOut[2],&pLitOut[1] );
419}
420Vec_Wec_t * Wlc_ManGenTree_iter( Gia_Man_t * p, Vec_Wec_t * vBits, int * pCounter )
421{
422 Vec_Wec_t * vBitsNew = Vec_WecStart( Vec_WecSize(vBits) );
423 int i, k, pLitsIn[16], pLitsOut[16], Count = 0, fSimple = Vec_WecMaxLevelSize(vBits) <= 3;
424 for ( i = 0; i < Vec_WecSize(vBits)-1; i++ )
425 {
426 Vec_Int_t * vBits0 = Vec_WecEntry(vBits, i);
427 Vec_Int_t * vBits1 = Vec_WecEntry(vBits, i+1);
428 if ( fSimple )
429 {
430 assert( Vec_IntSize(vBits0) <= 3 );
431 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
432 pLitsIn[k] = Vec_IntPop( vBits0 );
433 for ( ; k < 3; k++ )
434 pLitsIn[k] = 0;
435 assert( k == 3 );
436 Wlc_BlastFullAdder( p, pLitsIn[0], pLitsIn[1], pLitsIn[2], &pLitsOut[1], &pLitsOut[0] );
437 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
438 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
439 Count += 2;
440 continue;
441 }
442 while ( Vec_IntSize(vBits0) >= 6 )
443 {
444 for ( k = 0; k < 6; k++ )
445 pLitsIn[k] = Vec_IntPop( vBits0 );
446 assert( k == 6 );
447 Wlc_BuildOne6( p, pLitsIn, 0, pLitsOut );
448 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
449 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
450 Vec_WecPush( vBitsNew, i+2, pLitsOut[2] );
451 Count += 3;
452 }
453 if ( Vec_IntSize(vBits0) == 5 && Vec_IntSize(vBits1) > 0 )
454 {
455 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
456 pLitsIn[k] = Vec_IntPop( vBits0 );
457 pLitsIn[k++] = Vec_IntPop( vBits1 );
458 assert( k == 6 );
459 Wlc_BuildOne51( p, pLitsIn, pLitsOut );
460 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
461 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
462 Vec_WecPush( vBitsNew, i+2, pLitsOut[2] );
463 Count += 3;
464 }
465 if ( Vec_IntSize(vBits0) == 5 && Vec_IntSize(vBits1) == 0 )
466 {
467 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
468 pLitsIn[k] = Vec_IntPop( vBits0 );
469 pLitsIn[k++] = 0;
470 assert( k == 6 );
471 Wlc_BuildOne6( p, pLitsIn, 0, pLitsOut );
472 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
473 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
474 Vec_WecPush( vBitsNew, i+2, pLitsOut[2] );
475 Count += 3;
476 }
477 if ( Vec_IntSize(vBits0) == 4 && Vec_IntSize(vBits1) > 0 )
478 {
479 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
480 pLitsIn[k] = Vec_IntPop( vBits0 );
481 pLitsIn[k++] = 0;
482 pLitsIn[k++] = Vec_IntPop( vBits1 );
483 assert( k == 6 );
484 Wlc_BuildOne51( p, pLitsIn, pLitsOut );
485 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
486 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
487 Vec_WecPush( vBitsNew, i+2, pLitsOut[2] );
488 Count += 3;
489 }
490 if ( Vec_IntSize(vBits0) == 3 && Vec_IntSize(vBits1) >= 2 )
491 {
492 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
493 pLitsIn[k] = Vec_IntPop( vBits0 );
494 pLitsIn[k++] = Vec_IntPop( vBits1 );
495 pLitsIn[k++] = Vec_IntPop( vBits1 );
496 assert( k == 5 );
497 Wlc_BuildOne32( p, pLitsIn, pLitsOut );
498 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
499 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
500 Vec_WecPush( vBitsNew, i+2, pLitsOut[2] );
501 Count += 3;
502 }
503 if ( Vec_IntSize(vBits0) >= 3 )
504 {
505 for ( k = 0; k < 3; k++ )
506 pLitsIn[k] = Vec_IntPop( vBits0 );
507 assert( k == 3 );
508 Wlc_BlastFullAdder( p, pLitsIn[0], pLitsIn[1], pLitsIn[2], &pLitsOut[1], &pLitsOut[0] );
509 Vec_WecPush( vBitsNew, i+0, pLitsOut[0] );
510 Vec_WecPush( vBitsNew, i+1, pLitsOut[1] );
511 Count += 2;
512 }
513/*
514 if ( Vec_IntSize(vBits0) == 2 )
515 {
516 Vec_IntClear( vBits0 );
517 Vec_WecPush( vBitsNew, i+0, 0 );
518 Vec_WecPush( vBitsNew, i+1, 0 );
519 Count += 2;
520 }
521*/
522 for ( k = 0; Vec_IntSize(vBits0) > 0; k++ )
523 Vec_WecPush( vBitsNew, i, Vec_IntPop(vBits0) );
524 }
525 if ( pCounter )
526 *pCounter = Count;
527 return vBitsNew;
528}
529void Wlc_ManGenTreeOne( Gia_Man_t * pNew, Vec_Wec_t * vBits0, int fMult, int fVerbose )
530{
531 extern int Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits, int Carry ); // result is in pAdd0
532
533 Vec_Wec_t * vTemp, * vBits = Vec_WecDup( vBits0 );
534 Vec_Int_t * vOuts = Vec_IntAlloc( 1000 ), * vOuts2;
535 Vec_Int_t * vLits0 = Vec_IntAlloc( 1000 );
536 Vec_Int_t * vLits1 = Vec_IntAlloc( 1000 );
537 int i, iLit, nBitsAll = 0, CounterAll = 0, Counter = 1;
538 for ( i = 0; Counter && i < 1000; i++ )
539 {
540 if ( fVerbose ) printf( "LEVEL %d\n", i );
541 if ( fVerbose ) Vec_WecPrint( vBits, 0 );
542 if ( Vec_WecMaxLevelSize(vBits) <= 2 )
543 break;
544 vBits = Wlc_ManGenTree_iter( pNew, vTemp = vBits, &Counter );
545 Vec_WecFree( vTemp );
546 CounterAll += Counter;
547 }
548 printf( "Total count = %d.\n", CounterAll );
549 if ( !fMult )
550 {
551 int Carry;
552/*
553 Vec_WecForEachLevel( vBits, vOuts2, i )
554 {
555 if ( i == 10 )
556 break;
557 if ( i == 0 )
558 {
559 assert( Vec_IntSize(vOuts2) == 1 );
560 Vec_IntPush( vOuts, Vec_IntPop(vOuts2) );
561 continue;
562 }
563 assert( Vec_IntSize(vOuts2) == 1 || Vec_IntSize(vOuts2) == 2 );
564 Vec_IntPush( vLits0, Vec_IntPop(vOuts2) );
565 if ( Vec_IntSize(vOuts2) == 1 )
566 Vec_IntPush( vLits1, Vec_IntPop(vOuts2) );
567 else
568 {
569 Vec_IntPush( vLits1, 0 );
570 }
571 }
572 assert( Vec_IntSize(vLits0) == 9 );
573 assert( Vec_IntSize(vLits1) == 9 );
574*/
575 Vec_WecForEachLevel( vBits, vOuts2, i )
576 {
577 if ( Vec_IntSize(vOuts2) == 0 )
578 break;
579 assert( Vec_IntSize(vOuts2) == 1 || Vec_IntSize(vOuts2) == 2 );
580 Vec_IntPush( vLits0, Vec_IntPop(vOuts2) );
581 if ( Vec_IntSize(vOuts2) == 1 )
582 Vec_IntPush( vLits1, Vec_IntPop(vOuts2) );
583 else
584 Vec_IntPush( vLits1, 0 );
585 }
586 printf( "The adder size is %d.\n", Vec_IntSize(vLits0) );
587 Vec_IntShrink( vLits0, 11 );
588 Vec_IntShrink( vLits1, 11 );
589
590// vOuts2 = Wlc_ManGenAdder_rec( pNew, 9, Vec_IntArray(vLits0), Vec_IntArray(vLits1), 0, 3 );
591// Vec_IntAppend( vOuts, vOuts2 );
592// Vec_IntFree( vOuts2 );
593
594 Carry = Wlc_BlastAdder( pNew, Vec_IntArray(vLits0), Vec_IntArray(vLits1), 11, 0 );
595 Vec_IntAppend( vOuts, vLits0 );
596 Vec_IntPush( vOuts, Carry );
597
598
599 Gia_ManAppendCo( pNew, Vec_IntEntry(vOuts, 11) );
600 }
601 else
602 {
603 Vec_WecForEachLevel( vBits, vOuts2, i )
604 {
605 if ( Vec_IntSize(vOuts2) == 0 )
606 break;
607 assert( Vec_IntSize(vOuts2) == 1 || Vec_IntSize(vOuts2) == 2 );
608 Vec_IntPush( vLits0, Vec_IntPop(vOuts2) );
609 if ( Vec_IntSize(vOuts2) == 1 )
610 Vec_IntPush( vLits1, Vec_IntPop(vOuts2) );
611 else
612 Vec_IntPush( vLits1, 0 );
613 }
614 printf( "The adder size is %d.\n", Vec_IntSize(vLits0) );
615 Vec_IntShrink( vLits0, Gia_ManCiNum(pNew)+1 ); // mult
616 Vec_IntShrink( vLits1, Gia_ManCiNum(pNew)+1 ); // mult
617
618 for ( nBitsAll = 3; nBitsAll < Vec_IntSize(vLits0); nBitsAll *= 3 )
619 ;
620 for ( i = Vec_IntSize(vLits0); i < nBitsAll; i++ )
621 {
622 Vec_IntPush( vLits0, 0 );
623 Vec_IntPush( vLits1, 0 );
624 }
625 assert( Vec_IntSize(vLits0) == nBitsAll );
626 assert( Vec_IntSize(vLits1) == nBitsAll );
627
628 vOuts2 = Wlc_ManGenAdder_rec( pNew, nBitsAll, Vec_IntArray(vLits0), Vec_IntArray(vLits1), 0, 3 );
629 Vec_IntAppend( vOuts, vOuts2 );
630 Vec_IntFree( vOuts2 );
631 //Carry = Wlc_BlastAdder( pNew, Vec_IntArray(vLits0), Vec_IntArray(vLits1), nBitsAll, 0 );
632 //Vec_IntAppend( vOuts, vLits0 );
633 //Vec_IntPush( vOuts, Carry );
634
635 Vec_IntShrink( vOuts, Gia_ManCiNum(pNew) ); // mult
636 //Vec_IntShrink( vOuts, Gia_ManCiNum(pNew)/2 );
637
638 Vec_IntForEachEntry( vOuts, iLit, i )
639 Gia_ManAppendCo( pNew, iLit );
640 }
641
642 Vec_IntFree( vOuts );
643 Vec_IntFree( vLits0 );
644 Vec_IntFree( vLits1 );
645 Vec_WecFree( vBits );
646}
647Gia_Man_t * Wlc_ManGenTree( int nInputs, int Value, int nBits, int fVerbose )
648{
649 Gia_Man_t * pTemp, * pNew; int i, Counter = 0;
650 Vec_Wec_t * vBits = Vec_WecStart( nBits+2 );
651 for ( i = 0; i < nBits+2; i++ )
652 Vec_WecPush( vBits, i, (Value >> i) & 1 );
653 pNew = Gia_ManStart( 1000 );
654 pNew->pName = Abc_UtilStrsav( "tree" );
655 for ( i = 0; i < nInputs; i++ )
656 Vec_WecPush( vBits, 0, Gia_ManAppendCi(pNew) );
657 Gia_ManHashAlloc( pNew );
658 Wlc_ManGenTreeOne( pNew, vBits, 0, fVerbose );
659 Gia_ManHashStop( pNew );
660 Vec_WecFree( vBits );
661 pNew = Gia_ManCleanup( pTemp = pNew );
662 Gia_ManStop( pTemp );
663 return pNew;
664}
665
666
678Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose )
679{
680 extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose );
681 Vec_Int_t * vIns = Vec_IntAlloc( 2*nInputs );
682 Gia_Man_t * pTemp, * pNew;
683 Vec_Wec_t * vProds; int i;
684 pNew = Gia_ManStart( 1000 );
685 pNew->pName = Abc_UtilStrsav( "tree" );
686
687 for ( i = 0; i < 2*nInputs; i++ )
688 Vec_IntPush( vIns, Gia_ManAppendCi(pNew) );
689 //for ( i = 0; i < nInputs; i++ )
690 // Vec_IntPush( vIns, Gia_ManAppendCi(pNew) );
691 //for ( i = 0; i < nInputs; i++ )
692 // Vec_IntPush( vIns, Vec_IntEntry(vIns, i) );
693
694 Gia_ManHashAlloc( pNew );
695 Wlc_BlastBooth( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds, 0 );
696 Wlc_ManGenTreeOne( pNew, vProds, 1, fVerbose );
697 Gia_ManHashStop( pNew );
698 Vec_WecFree( vProds );
699 Vec_IntFree( vIns );
700 pNew = Gia_ManCleanup( pTemp = pNew );
701 Gia_ManStop( pTemp );
702 return pNew;
703}
704
716void Extra_PrintTernary( FILE * pFile, word * pFunc, word * pCare, int nBits )
717{
718 int i;
719 for ( i = nBits-1; i >= 0; i-- )
720 if ( Abc_TtGetBit(pCare, i) )
721 fprintf( pFile, "%c", '0' + Abc_TtGetBit(pFunc, i) );
722 else
723 fprintf( pFile, "-" );
724 fprintf( pFile, "\n" );
725}
726void Wlc_AdderTreeGen( int n )
727{
728 word Care[1<<10] = {0};
729 word Truth[8][1<<10] = {{0}};
730 int nIns = 0, pIns[16][2] = {{0}};
731 int i, k, x, Res, Mint, nMints = 1 << (n*n);
732 assert( n >= 2 && n <= 4 );
733 for ( x = 0; x < 2*n; x++ )
734 {
735 for ( i = 0; i < n; i++ )
736 for ( k = 0; k < n; k++ )
737 if ( i + k == x )
738 pIns[nIns][0] = i, pIns[nIns][1] = k, nIns++;
739 }
740 for ( x = 0; x < nIns; x++ )
741 printf( "(%d, %d) ", pIns[x][0], pIns[x][1] );
742 printf( "\n" );
743 for ( i = 0; i < (1<<n); i++ )
744 for ( k = 0; k < (1<<n); k++ )
745 {
746 Mint = 0;
747 for ( x = 0; x < nIns; x++ )
748 if ( ((i >> pIns[x][0]) & 1) && ((k >> pIns[x][1]) & 1) )
749 Mint |= 1 << x;
750 assert( Mint < (1<<16) );
751 Abc_TtSetBit( Care, Mint );
752
753 Res = i * k;
754 for ( x = 0; x < 2*n; x++ )
755 if ( (Res >> x) & 1 )
756 Abc_TtSetBit( Truth[x], Mint );
757 }
758 if ( n == 2 )
759 {
760 Care[0] = Abc_Tt6Stretch( Care[0], n*n );
761 for ( i = 0; i < 2*n; i++ )
762 Truth[i][0] = Abc_Tt6Stretch( Truth[i][0], n*n );
763 nMints = 64;
764 }
765 for ( x = 0; x < nMints; x++ )
766 printf( "%d", Abc_TtGetBit(Care, x) );
767 printf( "\n\n" );
768 for ( i = 0; i < 2*n; i++, printf( "\n" ) )
769 for ( x = 0; x < nMints; x++ )
770 printf( "%d", Abc_TtGetBit(Truth[i], x) );
771 if ( 1 )
772 {
773 FILE * pFile = fopen( "tadd.truth", "wb" );
774 for ( i = 0; i < 2*n; i++ )
775 Extra_PrintTernary( pFile, Truth[i], Care, nMints );
776 fclose( pFile );
777 }
778}
779
783
784
785ABC_NAMESPACE_IMPL_END
786
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
l_True
#define l_True
Definition bmcBmcS.c:35
sat_solver_addclause
#define sat_solver_addclause
Definition cecSatG2.c:37
sat_solver_add_xor
#define sat_solver_add_xor
Definition cecSatG2.c:39
sat_solver
#define sat_solver
Definition cecSatG2.c:34
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
p
Cube * p
Definition exorList.c:222
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition giaHash.c:692
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
sat_solver_new
sat_solver * sat_solver_new(void)
Definition satSolver.c:1137
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition satSolver.c:1272
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition satSolver.c:2369
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition satSolver.c:1341
Sat_SolverWriteDimacs
void Sat_SolverWriteDimacs(sat_solver *p, char *pFileName, lit *assumptionsBegin, lit *assumptionsEnd, int incrementVars)
Definition satUtil.c:74
Gia_Man_t_::pName
char * pName
Definition gia.h:99
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_IntForEachEntryStop
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition vecInt.h:58
Vec_IntForEachEntryTwo
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition vecInt.h:66
Vec_WecForEachLevel
#define Vec_WecForEachLevel(vGlob, vVec, i)
MACRO DEFINITIONS ///.
Definition vecWec.h:55
Vec_Wec_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Wec_t_ Vec_Wec_t
INCLUDES ///.
Definition vecWec.h:42
Wlc_BlastAdder
int Wlc_BlastAdder(Gia_Man_t *pNew, int *pAdd0, int *pAdd1, int nBits, int Carry)
Definition wlcBlast.c:429
Wlc_BlastBooth
void Wlc_BlastBooth(Gia_Man_t *pNew, int *pArgA, int *pArgB, int nArgA, int nArgB, Vec_Int_t *vRes, int fSigned, int fCla, Vec_Wec_t **pvProds, int fVerbose)
Definition wlcBlast.c:1242
Wlc_BlastFullAdder
void Wlc_BlastFullAdder(Gia_Man_t *pNew, int a, int b, int c, int *pc, int *ps)
Definition wlcBlast.c:401
Wlc_GenerateCodeMax4
ABC_NAMESPACE_IMPL_START void Wlc_GenerateCodeMax4(int nBits)
DECLARATIONS ///.
Definition wlc.c:46
Extra_PrintTernary
void Extra_PrintTernary(FILE *pFile, word *pFunc, word *pCare, int nBits)
Definition wlc.c:716
Wlc_AdderTreeGen
void Wlc_AdderTreeGen(int n)
Definition wlc.c:726
Wlc_ManGenAdder2_rec
Vec_Int_t * Wlc_ManGenAdder2_rec(Gia_Man_t *p, int nLits, int *pLitsA, int *pLitsB, int Carry, int Size)
Definition wlc.c:289
Wlc_ManGenTree
Gia_Man_t * Wlc_ManGenTree(int nInputs, int Value, int nBits, int fVerbose)
Definition wlc.c:647
Wlc_ManGenAdder2
Gia_Man_t * Wlc_ManGenAdder2(int nBits, int Size, int fSigned)
Definition wlc.c:308
Wlc_ManGenAdderN
Vec_Int_t * Wlc_ManGenAdderN(Gia_Man_t *p, int nLits, int *pLitsA, int *pLitsB, int Carry)
Definition wlc.c:279
Wlc_BlastMultiplierCnfMain
sat_solver * Wlc_BlastMultiplierCnfMain(int nBits)
Definition wlc.c:215
Wlc_ManGenTree_iter
Vec_Wec_t * Wlc_ManGenTree_iter(Gia_Man_t *p, Vec_Wec_t *vBits, int *pCounter)
Definition wlc.c:420
Wlc_BlastMultiplierCnf
void Wlc_BlastMultiplierCnf(sat_solver *pSat, int *pArgA, int *pArgB, int nArgA, int nArgB, Vec_Int_t *vTemp, Vec_Int_t *vRes, int *piVars)
Definition wlc.c:195
Wlc_ManGenTreeOne
void Wlc_ManGenTreeOne(Gia_Man_t *pNew, Vec_Wec_t *vBits0, int fMult, int fVerbose)
Definition wlc.c:529
Wlc_ManGenProd
Gia_Man_t * Wlc_ManGenProd(int nInputs, int fVerbose)
Definition wlc.c:678
Wlc_BuildOne6
void Wlc_BuildOne6(Gia_Man_t *p, int *pLitIn, int Const1, int *pLitOut)
Definition wlc.c:412
Wlc_BuildOne32
void Wlc_BuildOne32(Gia_Man_t *p, int *pLitIn, int *pLitOut)
Definition wlc.c:400
Wlc_BlastMultiplierCnfTest
void Wlc_BlastMultiplierCnfTest(int nBits)
Definition wlc.c:253
Wlc_ManGenAdder_rec
Vec_Int_t * Wlc_ManGenAdder_rec(Gia_Man_t *p, int nLits, int *pLitsA, int *pLitsB, int Carry, int Size)
Definition wlc.c:335
Wlc_BuildOne51
void Wlc_BuildOne51(Gia_Man_t *p, int *pLitIn, int *pLitOut)
Definition wlc.c:405
Wlc_BlastFullAdderCtrlCnf
void Wlc_BlastFullAdderCtrlCnf(sat_solver *pSat, int a, int ac, int b, int c, int *pc, int *ps, int *piVars)
Definition wlc.c:142
Wlc_ManGenAdder
Gia_Man_t * Wlc_ManGenAdder(int nBits)
Definition wlc.c:362