ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
cutPre22.c
Go to the documentation of this file.
1
20
21#include "cutInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
30#define CUT_CELL_MVAR 9
31
32typedef struct Cut_Cell_t_ Cut_Cell_t;
33typedef struct Cut_CMan_t_ Cut_CMan_t;
34
35struct Cut_Cell_t_
36{
37 Cut_Cell_t * pNext; // pointer to the next cell in the table
38 Cut_Cell_t * pNextVar; // pointer to the next cell of this support size
39 Cut_Cell_t * pParent; // pointer to the cell used to derive this one
40 int nUsed; // the number of times the cell is used
41 char Box[4]; // functions in the boxes
42 unsigned nVars : 4; // the number of variables
43 unsigned CrossBar0 : 4; // the variable set equal
44 unsigned CrossBar1 : 4; // the variable set equal
45 unsigned CrossBarPhase : 2; // the phase of the cross bar (0, 1, or 2)
46 unsigned CanonPhase : 18; // the canonical phase
47 char CanonPerm[CUT_CELL_MVAR+3]; // semicanonical permutation
48 short Store[2*CUT_CELL_MVAR]; // minterm counts in the cofactors
49 unsigned uTruth[1<<(CUT_CELL_MVAR-5)]; // the current truth table
50};
51
52struct Cut_CMan_t_
53{
54 // storage for canonical cells
55 Extra_MmFixed_t * pMem;
56 st__table * tTable;
57 Cut_Cell_t * pSameVar[CUT_CELL_MVAR+1];
58 // elementary truth tables
59 unsigned uInputs[CUT_CELL_MVAR][1<<(CUT_CELL_MVAR-5)];
60 // temporary truth tables
61 unsigned uTemp1[22][1<<(CUT_CELL_MVAR-5)];
62 unsigned uTemp2[22][1<<(CUT_CELL_MVAR-5)];
63 unsigned uTemp3[22][1<<(CUT_CELL_MVAR-5)];
64 unsigned uFinal[1<<(CUT_CELL_MVAR-5)];
65 unsigned puAux[1<<(CUT_CELL_MVAR-5)];
66 // statistical variables
67 int nTotal;
68 int nGood;
69 int nVarCounts[CUT_CELL_MVAR+1];
70 int nSymGroups[CUT_CELL_MVAR+1];
71 int nSymGroupsE[CUT_CELL_MVAR+1];
72 abctime timeCanon;
73 abctime timeSupp;
74 abctime timeTable;
75 int nCellFound;
76 int nCellNotFound;
77};
78
79// NP-classes of functions of 3 variables (22)
80//static char * s_NP3[22] = {
81// " 0\n", // 00 const 0 // 0 vars
82// " 1\n", // 01 const 1 // 0 vars
83// "1 1\n", // 02 a // 1 vars
84// "11 1\n", // 03 ab // 2 vars
85// "11 0\n", // 04 (ab)' // 2 vars
86// "10 1\n01 1\n", // 05 a<+>b // 2 vars
87// "111 1\n", // 06 0s abc // 3 vars
88// "111 0\n", // 07 (abc)' //
89// "11- 1\n1-1 1\n", // 08 1p a(b+c) //
90// "11- 0\n1-1 0\n", // 09 (a(b+c))' //
91// "111 1\n100 1\n010 1\n001 1\n", // 10 2s a<+>b<+>c //
92// "10- 0\n1-0 0\n011 0\n", // 11 3p a<+>bc //
93// "101 1\n110 1\n", // 12 4p a(b<+>c) //
94// "101 0\n110 0\n", // 13 (a(b<+>c))' //
95// "11- 1\n1-1 1\n-11 1\n", // 14 5s ab+bc+ac //
96// "111 1\n000 1\n", // 15 6s abc+a'b'c' //
97// "111 0\n000 0\n", // 16 (abc+a'b'c')' //
98// "11- 1\n-11 1\n0-1 1\n", // 17 7 ab+bc+a'c //
99// "011 1\n101 1\n110 1\n", // 18 8s a'bc+ab'c+abc' //
100// "011 0\n101 0\n110 0\n", // 19 (a'bc+ab'c+abc')' //
101// "100 1\n-11 1\n", // 20 9p ab'c'+bc //
102// "100 0\n-11 0\n" // 21 (ab'c'+bc)' //
103//};
104
105// NP-classes of functions of 3 variables (22)
106static char * s_NP3Names[22] = {
107 " const 0 ",
108 " const 1 ",
109 " a ",
110 " ab ",
111 " (ab)' ",
112 " a<+>b ",
113 "0s abc ",
114 " (abc)' ",
115 "1p a(b+c) ",
116 " (a(b+c))' ",
117 "2s a<+>b<+>c ",
118 "3p a<+>bc ",
119 "4p a(b<+>c) ",
120 " (a(b<+>c))' ",
121 "5s ab+bc+ac ",
122 "6s abc+a'b'c' ",
123 " (abc+a'b'c')' ",
124 "7 ab+bc+a'c ",
125 "8s a'bc+ab'c+abc' ",
126 " (a'bc+ab'c+abc')' ",
127 "9p ab'c'+bc ",
128 " (ab'c'+bc)' "
129};
130
131// the number of variables in each function
132//static int s_NP3VarNums[22] = { 0, 0, 1, 2, 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3 };
133
134// NPN classes of functions of exactly 3 inputs (10)
135static int s_NPNe3[10] = { 6, 8, 10, 11, 12, 14, 15, 17, 18, 20 };
136
137// NPN classes of functions of exactly 3 inputs that are symmetric (5)
138//static int s_NPNe3s[10] = { 6, 10, 14, 15, 18 };
139
140// NPN classes of functions of exactly 3 inputs (4)
141//static int s_NPNe3p[10] = { 8, 11, 12, 20 };
142
143static Cut_CMan_t * Cut_CManStart();
144static void Cut_CManStop( Cut_CMan_t * p );
145static void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type );
146static void Cut_CellCanonicize( Cut_CMan_t * p, Cut_Cell_t * pCell );
147static int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell );
148static void Cut_CellSuppMin( Cut_Cell_t * pCell );
149static void Cut_CellCrossBar( Cut_Cell_t * pCell );
150
151
152static Cut_CMan_t * s_pCMan = NULL;
153
157
169void Cut_CellLoad()
170{
171 FILE * pFile;
172 char * pFileName = "cells22_daomap_iwls.txt";
173 char pString[1000];
174 Cut_CMan_t * p;
175 Cut_Cell_t * pCell;
176 int Length; //, i;
177 pFile = fopen( pFileName, "r" );
178 if ( pFile == NULL )
179 {
180 printf( "Cannot open file \"%s\".\n", pFileName );
181 return;
182 }
183 // start the manager
184 p = Cut_CManStart();
185 // load truth tables
186 while ( fgets(pString, 1000, pFile) )
187 {
188 Length = strlen(pString);
189 pString[Length--] = 0;
190 if ( Length == 0 )
191 continue;
192 // derive the cell
193 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
194 memset( pCell, 0, sizeof(Cut_Cell_t) );
195 pCell->nVars = Abc_Base2Log(Length*4);
196 pCell->nUsed = 1;
197// Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
198 Extra_ReadHexadecimal( pCell->uTruth, pString, pCell->nVars );
199 Cut_CellSuppMin( pCell );
200/*
201 // set the elementary permutation
202 for ( i = 0; i < (int)pCell->nVars; i++ )
203 pCell->CanonPerm[i] = i;
204 // canonicize
205 pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
206*/
207 // add to the table
208 p->nTotal++;
209
210// Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars ); printf( "\n" );
211// if ( p->nTotal == 500 )
212// break;
213
214 if ( !Cut_CellTableLookup( p, pCell ) ) // new cell
215 p->nGood++;
216 }
217 printf( "Read %d cells from file \"%s\". Added %d cells to the table.\n", p->nTotal, pFileName, p->nGood );
218 fclose( pFile );
219// return p;
220}
221
233void Cut_CellPrecompute()
234{
235 Cut_CMan_t * p;
236 Cut_Cell_t * pCell, * pTemp;
237 int i1, i2, i3, i, j, k, c;
238 abctime clk = Abc_Clock(); //, clk2 = Abc_Clock();
239
240 p = Cut_CManStart();
241
242 // precompute truth tables
243 for ( i = 0; i < 22; i++ )
244 Cut_CellTruthElem( p->uInputs[0], p->uInputs[1], p->uInputs[2], p->uTemp1[i], 9, i );
245 for ( i = 0; i < 22; i++ )
246 Cut_CellTruthElem( p->uInputs[3], p->uInputs[4], p->uInputs[5], p->uTemp2[i], 9, i );
247 for ( i = 0; i < 22; i++ )
248 Cut_CellTruthElem( p->uInputs[6], p->uInputs[7], p->uInputs[8], p->uTemp3[i], 9, i );
249/*
250 if ( k == 8 && ((i1 == 6 && i2 == 14 && i3 == 20) || (i1 == 20 && i2 == 6 && i3 == 14)) )
251 {
252 Extra_PrintBinary( stdout, &pCell->CanonPhase, pCell->nVars+1 ); printf( " : " );
253 for ( i = 0; i < pCell->nVars; i++ )
254 printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
255 Extra_PrintHexadecimal( stdout, pCell->uTruth, pCell->nVars );
256 printf( "\n" );
257 }
258*/
259/*
260 // go through symmetric roots
261 for ( k = 0; k < 5; k++ )
262 for ( i1 = 0; i1 < 22; i1++ )
263 for ( i2 = i1; i2 < 22; i2++ )
264 for ( i3 = i2; i3 < 22; i3++ )
265 {
266 // derive the cell
267 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
268 memset( pCell, 0, sizeof(Cut_Cell_t) );
269 pCell->nVars = 9;
270 pCell->Box[0] = s_NPNe3s[k];
271 pCell->Box[1] = i1;
272 pCell->Box[2] = i2;
273 pCell->Box[3] = i3;
274 // fill in the truth table
275 Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3s[k] );
276 // canonicize
277 Cut_CellCanonicize( pCell );
278
279 // add to the table
280 p->nTotal++;
281 if ( Cut_CellTableLookup( p, pCell ) ) // already exists
282 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
283 else
284 p->nGood++;
285 }
286
287 // go through partially symmetric roots
288 for ( k = 0; k < 4; k++ )
289 for ( i1 = 0; i1 < 22; i1++ )
290 for ( i2 = 0; i2 < 22; i2++ )
291 for ( i3 = i2; i3 < 22; i3++ )
292 {
293 // derive the cell
294 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
295 memset( pCell, 0, sizeof(Cut_Cell_t) );
296 pCell->nVars = 9;
297 pCell->Box[0] = s_NPNe3p[k];
298 pCell->Box[1] = i1;
299 pCell->Box[2] = i2;
300 pCell->Box[3] = i3;
301 // fill in the truth table
302 Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3p[k] );
303 // canonicize
304 Cut_CellCanonicize( pCell );
305
306 // add to the table
307 p->nTotal++;
308 if ( Cut_CellTableLookup( p, pCell ) ) // already exists
309 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
310 else
311 p->nGood++;
312 }
313
314 // go through non-symmetric functions
315 for ( i1 = 0; i1 < 22; i1++ )
316 for ( i2 = 0; i2 < 22; i2++ )
317 for ( i3 = 0; i3 < 22; i3++ )
318 {
319 // derive the cell
320 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
321 memset( pCell, 0, sizeof(Cut_Cell_t) );
322 pCell->nVars = 9;
323 pCell->Box[0] = 17;
324 pCell->Box[1] = i1;
325 pCell->Box[2] = i2;
326 pCell->Box[3] = i3;
327 // fill in the truth table
328 Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, 17 );
329 // canonicize
330 Cut_CellCanonicize( pCell );
331
332 // add to the table
333 p->nTotal++;
334 if ( Cut_CellTableLookup( p, pCell ) ) // already exists
335 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
336 else
337 p->nGood++;
338 }
339*/
340
341 // go through non-symmetric functions
342 for ( k = 0; k < 10; k++ )
343 for ( i1 = 0; i1 < 22; i1++ )
344 for ( i2 = 0; i2 < 22; i2++ )
345 for ( i3 = 0; i3 < 22; i3++ )
346 {
347 // derive the cell
348 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
349 memset( pCell, 0, sizeof(Cut_Cell_t) );
350 pCell->nVars = 9;
351 pCell->Box[0] = s_NPNe3[k];
352 pCell->Box[1] = i1;
353 pCell->Box[2] = i2;
354 pCell->Box[3] = i3;
355 // set the elementary permutation
356 for ( i = 0; i < (int)pCell->nVars; i++ )
357 pCell->CanonPerm[i] = i;
358 // fill in the truth table
359 Cut_CellTruthElem( p->uTemp1[i1], p->uTemp2[i2], p->uTemp3[i3], pCell->uTruth, 9, s_NPNe3[k] );
360 // minimize the support
361 Cut_CellSuppMin( pCell );
362
363 // canonicize
364 pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
365
366 // add to the table
367 p->nTotal++;
368 if ( Cut_CellTableLookup( p, pCell ) ) // already exists
369 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
370 else
371 {
372 p->nGood++;
373 p->nVarCounts[pCell->nVars]++;
374
375 if ( pCell->nVars )
376 for ( i = 0; i < (int)pCell->nVars-1; i++ )
377 {
378 if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
379 continue;
380 // i and i+1 can be symmetric
381 // find the end of this group
382 for ( j = i+1; j < (int)pCell->nVars; j++ )
383 if ( pCell->Store[2*i] != pCell->Store[2*j] )
384 break;
385
386 if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
387 p->nSymGroupsE[j-i]++;
388 else
389 p->nSymGroups[j-i]++;
390 i = j - 1;
391 }
392/*
393 if ( pCell->nVars == 3 )
394 {
395 Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
396 for ( i = 0; i < (int)pCell->nVars; i++ )
397 printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
398 printf( "\n" );
399 }
400*/
401 }
402 }
403
404 printf( "BASIC: Total = %d. Good = %d. Entry = %d. ", (int)p->nTotal, (int)p->nGood, (int)sizeof(Cut_Cell_t) );
405 ABC_PRT( "Time", Abc_Clock() - clk );
406 printf( "Cells: " );
407 for ( i = 0; i <= 9; i++ )
408 printf( "%d=%d ", i, p->nVarCounts[i] );
409 printf( "\nDiffs: " );
410 for ( i = 0; i <= 9; i++ )
411 printf( "%d=%d ", i, p->nSymGroups[i] );
412 printf( "\nEquals: " );
413 for ( i = 0; i <= 9; i++ )
414 printf( "%d=%d ", i, p->nSymGroupsE[i] );
415 printf( "\n" );
416
417 // continue adding new cells using support
418 for ( k = CUT_CELL_MVAR; k > 3; k-- )
419 {
420 for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
421 for ( i1 = 0; i1 < k; i1++ )
422 for ( i2 = i1+1; i2 < k; i2++ )
423 for ( c = 0; c < 3; c++ )
424 {
425 // derive the cell
426 pCell = (Cut_Cell_t *)Extra_MmFixedEntryFetch( p->pMem );
427 memset( pCell, 0, sizeof(Cut_Cell_t) );
428 pCell->nVars = pTemp->nVars;
429 pCell->pParent = pTemp;
430 // set the elementary permutation
431 for ( i = 0; i < (int)pCell->nVars; i++ )
432 pCell->CanonPerm[i] = i;
433 // fill in the truth table
434 Extra_TruthCopy( pCell->uTruth, pTemp->uTruth, pTemp->nVars );
435 // create the cross-bar
436 pCell->CrossBar0 = i1;
437 pCell->CrossBar1 = i2;
438 pCell->CrossBarPhase = c;
439 Cut_CellCrossBar( pCell );
440 // minimize the support
441//clk2 = Abc_Clock();
442 Cut_CellSuppMin( pCell );
443//p->timeSupp += Abc_Clock() - clk2;
444 // canonicize
445//clk2 = Abc_Clock();
446 pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
447//p->timeCanon += Abc_Clock() - clk2;
448
449 // add to the table
450//clk2 = Abc_Clock();
451 p->nTotal++;
452 if ( Cut_CellTableLookup( p, pCell ) ) // already exists
453 Extra_MmFixedEntryRecycle( p->pMem, (char *)pCell );
454 else
455 {
456 p->nGood++;
457 p->nVarCounts[pCell->nVars]++;
458
459 for ( i = 0; i < (int)pCell->nVars-1; i++ )
460 {
461 if ( pCell->Store[2*i] != pCell->Store[2*(i+1)] ) // i and i+1 cannot be symmetric
462 continue;
463 // i and i+1 can be symmetric
464 // find the end of this group
465 for ( j = i+1; j < (int)pCell->nVars; j++ )
466 if ( pCell->Store[2*i] != pCell->Store[2*j] )
467 break;
468
469 if ( pCell->Store[2*i] == pCell->Store[2*i+1] )
470 p->nSymGroupsE[j-i]++;
471 else
472 p->nSymGroups[j-i]++;
473 i = j - 1;
474 }
475/*
476 if ( pCell->nVars == 3 )
477 {
478 Extra_PrintBinary( stdout, pCell->uTruth, 32 ); printf( "\n" );
479 for ( i = 0; i < (int)pCell->nVars; i++ )
480 printf( "%d=%d/%d ", pCell->CanonPerm[i], pCell->Store[2*i], pCell->Store[2*i+1] );
481 printf( "\n" );
482 }
483*/
484 }
485//p->timeTable += Abc_Clock() - clk2;
486 }
487
488 printf( "VAR %d: Total = %d. Good = %d. Entry = %d. ", k, p->nTotal, p->nGood, (int)sizeof(Cut_Cell_t) );
489 ABC_PRT( "Time", Abc_Clock() - clk );
490 printf( "Cells: " );
491 for ( i = 0; i <= 9; i++ )
492 printf( "%d=%d ", i, p->nVarCounts[i] );
493 printf( "\nDiffs: " );
494 for ( i = 0; i <= 9; i++ )
495 printf( "%d=%d ", i, p->nSymGroups[i] );
496 printf( "\nEquals: " );
497 for ( i = 0; i <= 9; i++ )
498 printf( "%d=%d ", i, p->nSymGroupsE[i] );
499 printf( "\n" );
500 }
501// printf( "\n" );
502 ABC_PRT( "Supp ", p->timeSupp );
503 ABC_PRT( "Canon", p->timeCanon );
504 ABC_PRT( "Table", p->timeTable );
505// Cut_CManStop( p );
506}
507
519int Cut_CellTableLookup( Cut_CMan_t * p, Cut_Cell_t * pCell )
520{
521 Cut_Cell_t ** pSlot, * pTemp;
522 unsigned Hash;
523 Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum( pCell->nVars ) );
524 if ( ! st__find_or_add( p->tTable, (char *)(ABC_PTRUINT_T)Hash, (char ***)&pSlot ) )
525 *pSlot = NULL;
526 for ( pTemp = *pSlot; pTemp; pTemp = pTemp->pNext )
527 {
528 if ( pTemp->nVars != pCell->nVars )
529 continue;
530 if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
531 return 1;
532 }
533 // the entry is new
534 pCell->pNext = *pSlot;
535 *pSlot = pCell;
536 // add it to the variable support list
537 pCell->pNextVar = p->pSameVar[pCell->nVars];
538 p->pSameVar[pCell->nVars] = pCell;
539 return 0;
540}
541
553void Cut_CellSuppMin( Cut_Cell_t * pCell )
554{
555 static unsigned uTemp[1<<(CUT_CELL_MVAR-5)];
556 unsigned * pIn, * pOut, * pTemp;
557 int i, k, Counter, Temp;
558
559 // go backward through the support variables and remove redundant
560 for ( k = pCell->nVars - 1; k >= 0; k-- )
561 if ( !Extra_TruthVarInSupport(pCell->uTruth, pCell->nVars, k) )
562 {
563 // shift all the variables above this one
564 Counter = 0;
565 pIn = pCell->uTruth; pOut = uTemp;
566 for ( i = k; i < (int)pCell->nVars - 1; i++ )
567 {
568 Extra_TruthSwapAdjacentVars( pOut, pIn, pCell->nVars, i );
569 pTemp = pIn; pIn = pOut; pOut = pTemp;
570 // swap the support vars
571 Temp = pCell->CanonPerm[i];
572 pCell->CanonPerm[i] = pCell->CanonPerm[i+1];
573 pCell->CanonPerm[i+1] = Temp;
574 Counter++;
575 }
576 // return the function back into its place
577 if ( Counter & 1 )
578 Extra_TruthCopy( pOut, pIn, pCell->nVars );
579 // remove one variable
580 pCell->nVars--;
581// Extra_PrintBinary( stdout, pCell->uTruth, (1<<pCell->nVars) ); printf( "\n" );
582 }
583}
584
596void Cut_CellCrossBar( Cut_Cell_t * pCell )
597{
598 static unsigned uTemp0[1<<(CUT_CELL_MVAR-5)];
599 static unsigned uTemp1[1<<(CUT_CELL_MVAR-5)];
600 Extra_TruthCopy( uTemp0, pCell->uTruth, pCell->nVars );
601 Extra_TruthCopy( uTemp1, pCell->uTruth, pCell->nVars );
602 if ( pCell->CanonPhase == 0 )
603 {
604 Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
605 Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
606 Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
607 Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
608 }
609 else if ( pCell->CanonPhase == 1 )
610 {
611 Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar0 );
612 Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar1 );
613 Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar0 );
614 Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar1 );
615 }
616 else if ( pCell->CanonPhase == 2 )
617 {
618 Extra_TruthCofactor0( uTemp0, pCell->nVars, pCell->CrossBar0 );
619 Extra_TruthCofactor1( uTemp0, pCell->nVars, pCell->CrossBar1 );
620 Extra_TruthCofactor1( uTemp1, pCell->nVars, pCell->CrossBar0 );
621 Extra_TruthCofactor0( uTemp1, pCell->nVars, pCell->CrossBar1 );
622 }
623 else assert( 0 );
624 Extra_TruthMux( pCell->uTruth, uTemp0, uTemp1, pCell->nVars, pCell->CrossBar0 );
625}
626
638void Cut_CellTruthElem( unsigned * InA, unsigned * InB, unsigned * InC, unsigned * pOut, int nVars, int Type )
639{
640 int nWords = Extra_TruthWordNum( nVars );
641 int i;
642
643 assert( Type < 22 );
644 switch ( Type )
645 {
646 // " 0\n", // 00 const 0
647 case 0:
648 for ( i = 0; i < nWords; i++ )
649 pOut[i] = 0;
650 return;
651 // " 1\n", // 01 const 1
652 case 1:
653 for ( i = 0; i < nWords; i++ )
654 pOut[i] = 0xFFFFFFFF;
655 return;
656 // "1 1\n", // 02 a
657 case 2:
658 for ( i = 0; i < nWords; i++ )
659 pOut[i] = InA[i];
660 return;
661 // "11 1\n", // 03 ab
662 case 3:
663 for ( i = 0; i < nWords; i++ )
664 pOut[i] = InA[i] & InB[i];
665 return;
666 // "11 0\n", // 04 (ab)'
667 case 4:
668 for ( i = 0; i < nWords; i++ )
669 pOut[i] = ~(InA[i] & InB[i]);
670 return;
671 // "10 1\n01 1\n", // 05 a<+>b
672 case 5:
673 for ( i = 0; i < nWords; i++ )
674 pOut[i] = InA[i] ^ InB[i];
675 return;
676 // "111 1\n", // 06 + abc
677 case 6:
678 for ( i = 0; i < nWords; i++ )
679 pOut[i] = InA[i] & InB[i] & InC[i];
680 return;
681 // "111 0\n", // 07 (abc)'
682 case 7:
683 for ( i = 0; i < nWords; i++ )
684 pOut[i] = ~(InA[i] & InB[i] & InC[i]);
685 return;
686 // "11- 1\n1-1 1\n", // 08 + a(b+c)
687 case 8:
688 for ( i = 0; i < nWords; i++ )
689 pOut[i] = InA[i] & (InB[i] | InC[i]);
690 return;
691 // "11- 0\n1-1 0\n", // 09 (a(b+c))'
692 case 9:
693 for ( i = 0; i < nWords; i++ )
694 pOut[i] = ~(InA[i] & (InB[i] | InC[i]));
695 return;
696 // "111 1\n100 1\n010 1\n001 1\n", // 10 + a<+>b<+>c
697 case 10:
698 for ( i = 0; i < nWords; i++ )
699 pOut[i] = InA[i] ^ InB[i] ^ InC[i];
700 return;
701 // "10- 0\n1-0 0\n011 0\n", // 11 + a<+>bc
702 case 11:
703 for ( i = 0; i < nWords; i++ )
704 pOut[i] = InA[i] ^ (InB[i] & InC[i]);
705 return;
706 // "101 1\n110 1\n", // 12 + a(b<+>c)
707 case 12:
708 for ( i = 0; i < nWords; i++ )
709 pOut[i] = InA[i] & (InB[i] ^ InC[i]);
710 return;
711 // "101 0\n110 0\n", // 13 (a(b<+>c))'
712 case 13:
713 for ( i = 0; i < nWords; i++ )
714 pOut[i] = ~(InA[i] & (InB[i] ^ InC[i]));
715 return;
716 // "11- 1\n1-1 1\n-11 1\n", // 14 + ab+bc+ac
717 case 14:
718 for ( i = 0; i < nWords; i++ )
719 pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (InA[i] & InC[i]);
720 return;
721 // "111 1\n000 1\n", // 15 + abc+a'b'c'
722 case 15:
723 for ( i = 0; i < nWords; i++ )
724 pOut[i] = (InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]);
725 return;
726 // "111 0\n000 0\n", // 16 (abc+a'b'c')'
727 case 16:
728 for ( i = 0; i < nWords; i++ )
729 pOut[i] = ~((InA[i] & InB[i] & InC[i]) | (~InA[i] & ~InB[i] & ~InC[i]));
730 return;
731 // "11- 1\n-11 1\n0-1 1\n", // 17 + ab+bc+a'c
732 case 17:
733 for ( i = 0; i < nWords; i++ )
734 pOut[i] = (InA[i] & InB[i]) | (InB[i] & InC[i]) | (~InA[i] & InC[i]);
735 return;
736 // "011 1\n101 1\n110 1\n", // 18 + a'bc+ab'c+abc'
737 case 18:
738 for ( i = 0; i < nWords; i++ )
739 pOut[i] = (~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]);
740 return;
741 // "011 0\n101 0\n110 0\n", // 19 (a'bc+ab'c+abc')'
742 case 19:
743 for ( i = 0; i < nWords; i++ )
744 pOut[i] = ~((~InA[i] & InB[i] & InC[i]) | (InA[i] & ~InB[i] & InC[i]) | (InA[i] & InB[i] & ~InC[i]));
745 return;
746 // "100 1\n-11 1\n", // 20 + ab'c'+bc
747 case 20:
748 for ( i = 0; i < nWords; i++ )
749 pOut[i] = (InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]);
750 return;
751 // "100 0\n-11 0\n" // 21 (ab'c'+bc)'
752 case 21:
753 for ( i = 0; i < nWords; i++ )
754 pOut[i] = ~((InA[i] & ~InB[i] & ~InC[i]) | (InB[i] & InC[i]));
755 return;
756 }
757}
758
759
771Cut_CMan_t * Cut_CManStart()
772{
773 Cut_CMan_t * p;
774 int i, k;
775 // start the manager
776 assert( sizeof(unsigned) == 4 );
777 p = ABC_ALLOC( Cut_CMan_t, 1 );
778 memset( p, 0, sizeof(Cut_CMan_t) );
779 // start the table and the memory manager
780 p->tTable = st__init_table( st__ptrcmp, st__ptrhash);;
781 p->pMem = Extra_MmFixedStart( sizeof(Cut_Cell_t) );
782 // set elementary truth tables
783 for ( k = 0; k < CUT_CELL_MVAR; k++ )
784 for ( i = 0; i < (1<<CUT_CELL_MVAR); i++ )
785 if ( i & (1 << k) )
786 p->uInputs[k][i>>5] |= (1 << (i&31));
787 s_pCMan = p;
788 return p;
789}
790
802void Cut_CManStop( Cut_CMan_t * p )
803{
804 st__free_table( p->tTable );
805 Extra_MmFixedStop( p->pMem );
806 ABC_FREE( p );
807}
819int Cut_CellIsRunning()
820{
821 return s_pCMan != NULL;
822}
823
835void Cut_CellDumpToFile()
836{
837 FILE * pFile;
838 Cut_CMan_t * p = s_pCMan;
839 Cut_Cell_t * pTemp;
840 char * pFileName = "celllib22.txt";
841 int NumUsed[10][5] = {{0}};
842 int BoxUsed[22][5] = {{0}};
843 int i, k, Counter;
844 abctime clk = Abc_Clock();
845
846 if ( p == NULL )
847 {
848 printf( "Cut_CellDumpToFile: Cell manager is not defined.\n" );
849 return;
850 }
851
852 // count the number of cells used
853 for ( k = CUT_CELL_MVAR; k >= 0; k-- )
854 {
855 for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
856 {
857 if ( pTemp->nUsed == 0 )
858 NumUsed[k][0]++;
859 else if ( pTemp->nUsed < 10 )
860 NumUsed[k][1]++;
861 else if ( pTemp->nUsed < 100 )
862 NumUsed[k][2]++;
863 else if ( pTemp->nUsed < 1000 )
864 NumUsed[k][3]++;
865 else
866 NumUsed[k][4]++;
867
868 for ( i = 0; i < 4; i++ )
869 if ( pTemp->nUsed == 0 )
870 BoxUsed[ (int)pTemp->Box[i] ][0]++;
871 else if ( pTemp->nUsed < 10 )
872 BoxUsed[ (int)pTemp->Box[i] ][1]++;
873 else if ( pTemp->nUsed < 100 )
874 BoxUsed[ (int)pTemp->Box[i] ][2]++;
875 else if ( pTemp->nUsed < 1000 )
876 BoxUsed[ (int)pTemp->Box[i] ][3]++;
877 else
878 BoxUsed[ (int)pTemp->Box[i] ][4]++;
879 }
880 }
881
882 printf( "Functions found = %10d. Functions not found = %10d.\n", p->nCellFound, p->nCellNotFound );
883 for ( k = 0; k <= CUT_CELL_MVAR; k++ )
884 {
885 printf( "%3d : ", k );
886 for ( i = 0; i < 5; i++ )
887 printf( "%8d ", NumUsed[k][i] );
888 printf( "\n" );
889 }
890 printf( "Box usage:\n" );
891 for ( k = 0; k < 22; k++ )
892 {
893 printf( "%3d : ", k );
894 for ( i = 0; i < 5; i++ )
895 printf( "%8d ", BoxUsed[k][i] );
896 printf( " %s", s_NP3Names[k] );
897 printf( "\n" );
898 }
899
900 pFile = fopen( pFileName, "w" );
901 if ( pFile == NULL )
902 {
903 printf( "Cut_CellDumpToFile: Cannout open output file.\n" );
904 return;
905 }
906
907 Counter = 0;
908 for ( k = 0; k <= CUT_CELL_MVAR; k++ )
909 {
910 for ( pTemp = p->pSameVar[k]; pTemp; pTemp = pTemp->pNextVar )
911 if ( pTemp->nUsed > 0 )
912 {
913 Extra_PrintHexadecimal( pFile, pTemp->uTruth, (k <= 5? 5 : k) );
914 fprintf( pFile, "\n" );
915 Counter++;
916 }
917 fprintf( pFile, "\n" );
918 }
919 fclose( pFile );
920
921 printf( "Library composed of %d functions is written into file \"%s\". ", Counter, pFileName );
922
923 ABC_PRT( "Time", Abc_Clock() - clk );
924}
925
926
940int Cut_CellTruthLookup( unsigned * pTruth, int nVars )
941{
942 Cut_CMan_t * p = s_pCMan;
943 Cut_Cell_t * pTemp;
944 Cut_Cell_t Cell, * pCell = &Cell;
945 unsigned Hash;
946 int i;
947
948 // cell manager is not defined
949 if ( p == NULL )
950 {
951 printf( "Cut_CellTruthLookup: Cell manager is not defined.\n" );
952 return 0;
953 }
954
955 // canonicize
956 memset( pCell, 0, sizeof(Cut_Cell_t) );
957 pCell->nVars = nVars;
958 Extra_TruthCopy( pCell->uTruth, pTruth, nVars );
959 Cut_CellSuppMin( pCell );
960 // set the elementary permutation
961 for ( i = 0; i < (int)pCell->nVars; i++ )
962 pCell->CanonPerm[i] = i;
963 // canonicize
964 pCell->CanonPhase = Extra_TruthSemiCanonicize( pCell->uTruth, p->puAux, pCell->nVars, pCell->CanonPerm, pCell->Store );
965
966
967 // check if the cell exists
968 Hash = Extra_TruthHash( pCell->uTruth, Extra_TruthWordNum(pCell->nVars) );
969 if ( st__lookup( p->tTable, (char *)(ABC_PTRUINT_T)Hash, (char **)&pTemp ) )
970 {
971 for ( ; pTemp; pTemp = pTemp->pNext )
972 {
973 if ( pTemp->nVars != pCell->nVars )
974 continue;
975 if ( Extra_TruthIsEqual(pTemp->uTruth, pCell->uTruth, pCell->nVars) )
976 {
977 pTemp->nUsed++;
978 p->nCellFound++;
979 return 1;
980 }
981 }
982 }
983 p->nCellNotFound++;
984 return 0;
985}
986
987
991
992
993ABC_NAMESPACE_IMPL_END
994
nWords
int nWords
Definition abcNpn.c:127
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
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
CUT_CELL_MVAR
#define CUT_CELL_MVAR
DECLARATIONS ///.
Definition cutExpand.c:30
Cut_CellPrecompute
void Cut_CellPrecompute()
Definition cutPre22.c:233
Cut_CellTruthLookup
int Cut_CellTruthLookup(unsigned *pTruth, int nVars)
Definition cutPre22.c:940
Cut_CellLoad
void Cut_CellLoad()
FUNCTION DEFINITIONS ///.
Definition cutPre22.c:169
CUT_CELL_MVAR
#define CUT_CELL_MVAR
DECLARATIONS ///.
Definition cutPre22.c:30
Cut_CellIsRunning
int Cut_CellIsRunning()
Definition cutPre22.c:819
Cut_CellDumpToFile
void Cut_CellDumpToFile()
Definition cutPre22.c:835
Cut_Cell_t
struct Cut_Cell_t_ Cut_Cell_t
Definition cutPre22.c:32
Cut_CMan_t
struct Cut_CMan_t_ Cut_CMan_t
Definition cutPre22.c:33
p
Cube * p
Definition exorList.c:222
Extra_MmFixedEntryFetch
char * Extra_MmFixedEntryFetch(Extra_MmFixed_t *p)
Definition extraUtilMemory.c:202
Extra_TruthCofactor1
void Extra_TruthCofactor1(unsigned *pTruth, int nVars, int iVar)
Definition extraUtilTruth.c:399
Extra_MmFixedStop
void Extra_MmFixedStop(Extra_MmFixed_t *p)
Definition extraUtilMemory.c:180
Extra_TruthHash
unsigned Extra_TruthHash(unsigned *pIn, int nWords)
Definition extraUtilTruth.c:902
Extra_TruthVarInSupport
int Extra_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition extraUtilTruth.c:301
Extra_TruthMux
void Extra_TruthMux(unsigned *pOut, unsigned *pCof0, unsigned *pCof1, int nVars, int iVar)
Definition extraUtilTruth.c:611
Extra_MmFixedStart
Extra_MmFixed_t * Extra_MmFixedStart(int nEntrySize)
Definition extraUtilMemory.c:122
Extra_ReadHexadecimal
int Extra_ReadHexadecimal(unsigned Sign[], char *pString, int nVars)
Definition extraUtilFile.c:559
Extra_PrintHexadecimal
void Extra_PrintHexadecimal(FILE *pFile, unsigned Sign[], int nVars)
Definition extraUtilFile.c:584
Extra_TruthSemiCanonicize
unsigned Extra_TruthSemiCanonicize(unsigned *pInOut, unsigned *pAux, int nVars, char *pCanonPerm, short *pStore)
Definition extraUtilTruth.c:999
Extra_MmFixed_t
struct Extra_MmFixed_t_ Extra_MmFixed_t
Definition extra.h:147
Extra_MmFixedEntryRecycle
void Extra_MmFixedEntryRecycle(Extra_MmFixed_t *p, char *pEntry)
Definition extraUtilMemory.c:253
Extra_TruthCofactor0
void Extra_TruthCofactor0(unsigned *pTruth, int nVars, int iVar)
Definition extraUtilTruth.c:450
Extra_TruthSwapAdjacentVars
void Extra_TruthSwapAdjacentVars(unsigned *pOut, unsigned *pIn, int nVars, int Start)
Definition extraUtilTruth.c:114
st__ptrhash
int st__ptrhash(const char *, int)
Definition st.c:467
st__find_or_add
int st__find_or_add(st__table *table, char *key, char ***slot)
Definition st.c:230
st__ptrcmp
int st__ptrcmp(const char *, const char *)
Definition st.c:479
st__lookup
int st__lookup(st__table *table, const char *key, char **value)
Definition st.c:114
st__init_table
st__table * st__init_table(st__compare_func_type compare, st__hash_func_type hash)
Definition st.c:72
st__free_table
void st__free_table(st__table *table)
Definition st.c:81
Cut_CMan_t_
Definition cutPre22.c:53
Cut_CMan_t_::nGood
int nGood
Definition cutPre22.c:68
Cut_CMan_t_::pMem
Extra_MmFixed_t * pMem
Definition cutPre22.c:55
Cut_CMan_t_::uTemp3
unsigned uTemp3[22][1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:63
Cut_CMan_t_::timeSupp
abctime timeSupp
Definition cutPre22.c:73
Cut_CMan_t_::timeCanon
abctime timeCanon
Definition cutPre22.c:72
Cut_CMan_t_::nSymGroups
int nSymGroups[CUT_CELL_MVAR+1]
Definition cutPre22.c:70
Cut_CMan_t_::pSameVar
Cut_Cell_t * pSameVar[CUT_CELL_MVAR+1]
Definition cutPre22.c:57
Cut_CMan_t_::nTotal
int nTotal
Definition cutPre22.c:67
Cut_CMan_t_::puAux
unsigned puAux[1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:65
Cut_CMan_t_::uTemp2
unsigned uTemp2[22][1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:62
Cut_CMan_t_::uFinal
unsigned uFinal[1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:64
Cut_CMan_t_::nCellFound
int nCellFound
Definition cutPre22.c:75
Cut_CMan_t_::nVarCounts
int nVarCounts[CUT_CELL_MVAR+1]
Definition cutPre22.c:69
Cut_CMan_t_::tTable
st__table * tTable
Definition cutPre22.c:56
Cut_CMan_t_::nCellNotFound
int nCellNotFound
Definition cutPre22.c:76
Cut_CMan_t_::uInputs
unsigned uInputs[CUT_CELL_MVAR][1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:59
Cut_CMan_t_::uTemp1
unsigned uTemp1[22][1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:61
Cut_CMan_t_::timeTable
abctime timeTable
Definition cutPre22.c:74
Cut_CMan_t_::nSymGroupsE
int nSymGroupsE[CUT_CELL_MVAR+1]
Definition cutPre22.c:71
Cut_Cell_t_
Definition cutPre22.c:36
Cut_Cell_t_::nVars
unsigned nVars
Definition cutPre22.c:42
Cut_Cell_t_::CrossBarPhase
unsigned CrossBarPhase
Definition cutPre22.c:45
Cut_Cell_t_::CrossBar1
unsigned CrossBar1
Definition cutPre22.c:44
Cut_Cell_t_::CanonPhase
unsigned CanonPhase
Definition cutPre22.c:46
Cut_Cell_t_::pNext
Cut_Cell_t * pNext
Definition cutPre22.c:37
Cut_Cell_t_::Store
short Store[2 *CUT_CELL_MVAR]
Definition cutPre22.c:48
Cut_Cell_t_::nUsed
int nUsed
Definition cutPre22.c:40
Cut_Cell_t_::pParent
Cut_Cell_t * pParent
Definition cutPre22.c:39
Cut_Cell_t_::pNextVar
Cut_Cell_t * pNextVar
Definition cutPre22.c:38
Cut_Cell_t_::Box
char Box[4]
Definition cutPre22.c:41
Cut_Cell_t_::uTruth
unsigned uTruth[1<<(CUT_CELL_MVAR-5)]
Definition cutPre22.c:49
Cut_Cell_t_::CanonPerm
char CanonPerm[CUT_CELL_MVAR+3]
Definition cutPre22.c:47
Cut_Cell_t_::CrossBar0
unsigned CrossBar0
Definition cutPre22.c:43
st__table
Definition st.h:52
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
strlen
int strlen()