ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
exor.c
Go to the documentation of this file.
1
20
47
48#include "exor.h"
49#include "base/abc/abc.h"
50
51ABC_NAMESPACE_IMPL_START
52
56
57// information about the cube cover
58cinfo g_CoverInfo;
59
60extern int s_fDecreaseLiterals;
61
65
69
70
82/*
83static int QCost[16][16] =
84{
85 { 1}, // 0
86 { 1, 2}, // 1
87 { 5, 5, 6}, // 2
88 { 14, 14, 16, 18}, // 3
89 { 20, 20, 20, 22, 24}, // 4
90 { 32, 32, 32, 34, 36, 38}, // 5
91 { 44, 44, 44, 44, 46, 48, 50}, // 6
92 { 56, 56, 56, 56, 58, 60, 62, 64}, // 7
93 { 0 }
94};
95*/
96int GetQCost( int nVars, int nNegs )
97{
98 int Extra;
99 assert( nVars >= nNegs );
100 if ( nVars == 0 )
101 return 1;
102 if ( nVars == 1 )
103 {
104 if ( nNegs == 0 ) return 1;
105 if ( nNegs == 1 ) return 2;
106 }
107 if ( nVars == 2 )
108 {
109 if ( nNegs <= 1 ) return 5;
110 if ( nNegs == 2 ) return 6;
111 }
112 if ( nVars == 3 )
113 {
114 if ( nNegs <= 1 ) return 14;
115 if ( nNegs == 2 ) return 16;
116 if ( nNegs == 3 ) return 18;
117 }
118 Extra = nNegs - nVars/2;
119 return 20 + 12 * (nVars - 4) + (Extra > 0 ? 2 * Extra : 0);
120
121}
122void GetQCostTest()
123{
124 int i, k, Limit = 10;
125 for ( i = 0; i < Limit; i++ )
126 {
127 for ( k = 0; k <= i; k++ )
128 printf( "%4d ", GetQCost(i, k) );
129 printf( "\n" );
130 }
131}
132int ComputeQCost( Vec_Int_t * vCube )
133{
134 int i, Entry, nLitsN = 0;
135 Vec_IntForEachEntry( vCube, Entry, i )
136 nLitsN += Abc_LitIsCompl(Entry);
137 return GetQCost( Vec_IntSize(vCube), nLitsN );
138}
139int ComputeQCostBits( Cube * p )
140{
141 extern varvalue GetVar( Cube* pC, int Var );
142 int v, nLits = 0, nLitsN = 0;
143 for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
144 {
145 int Value = GetVar( p, v );
146 if ( Value == VAR_NEG )
147 nLitsN++;
148 else if ( Value == VAR_POS )
149 nLits++;
150 }
151 nLits += nLitsN;
152 return GetQCost( nLits, nLitsN );
153}
154int ToffoliGateCount( int controls, int lines )
155{
156 switch ( controls )
157 {
158 case 0u:
159 case 1u:
160 return 0;
161 break;
162 case 2u:
163 return 1;
164 break;
165 case 3u:
166 return 4;
167 break;
168 case 4u:
169 return ( ( ( lines + 1 ) / 2 ) >= controls ) ? 8 : 10;
170 break;
171 default:
172 return ( ( ( lines + 1 ) / 2 ) >= controls ) ? 4 * ( controls - 2 ) : 8 * ( controls - 3 );
173 }
174}
175int ComputeQCostTcount( Vec_Int_t * vCube )
176{
177 return 7 * ToffoliGateCount( Vec_IntSize( vCube ), g_CoverInfo.nVarsIn + 1 );
178}
179int ComputeQCostTcountBits( Cube * p )
180{
181 extern varvalue GetVar( Cube* pC, int Var );
182 int v, nLits = 0;
183 for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
184 if ( GetVar( p, v ) != VAR_ABS )
185 nLits++;
186 return 7 * ToffoliGateCount( nLits, g_CoverInfo.nVarsIn + 1 );
187
188 /* maybe just: 7 * ToffoliGateCount( p->a, g_CoverInfo.nVarsIn + 1 ); */
189}
190
191
203int ReduceEsopCover()
204{
206 // SIMPLIFICATION
208
209 int nIterWithoutImprovement = 0;
210 int nIterCount = 0;
211 int GainTotal;
212 int z;
213
214 do
215 {
216//START:
217 if ( g_CoverInfo.Verbosity == 2 )
218 printf( "\nITERATION #%d\n\n", ++nIterCount );
219 else if ( g_CoverInfo.Verbosity == 1 )
220 printf( "." );
221
222 GainTotal = 0;
223 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
224 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
225
226 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
227 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
228
229 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
230 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
231
232 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
233 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
234
235 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
236 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
237
238 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
239 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
240
241 if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) )
242 {
243 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
244 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
245 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
246 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
247 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
248 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
249 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
250 GainTotal += IterativelyApplyExorLink4( 1|2|0 );
251
252 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
253 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
254 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
255 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
256 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
257 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
258 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
259 GainTotal += IterativelyApplyExorLink4( 1|2|0 );
260 }
261
262 if ( GainTotal )
263 nIterWithoutImprovement = 0;
264 else
265 nIterWithoutImprovement++;
266
267// if ( g_CoverInfo.Quality >= 2 && nIterWithoutImprovement == 2 )
268// s_fDecreaseLiterals = 1;
269 }
270 while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
271
272
273 // improve the literal count
274 s_fDecreaseLiterals = 1;
275 for ( z = 0; z < 1; z++ )
276 {
277 if ( g_CoverInfo.Verbosity == 2 )
278 printf( "\nITERATION #%d\n\n", ++nIterCount );
279 else if ( g_CoverInfo.Verbosity == 1 )
280 printf( "." );
281
282 GainTotal = 0;
283 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
284 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
285
286 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
287 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
288
289 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
290 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
291
292 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
293 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
294
295 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
296 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
297
298// if ( GainTotal )
299// {
300// nIterWithoutImprovement = 0;
301// goto START;
302// }
303 }
304
305
306/* ////////////////////////////////////////////////////////////////////
307 // Print statistics
308 printf( "\nShallow simplification time is ";
309 cout << (float)(clk2 - clk1)/(float)(CLOCKS_PER_SEC) << " sec\n" );
310 printf( "Deep simplification time is ";
311 cout << (float)(Abc_Clock() - clk2)/(float)(CLOCKS_PER_SEC) << " sec\n" );
312 printf( "Cover after iterative simplification = " << s_nCubesInUse << endl;
313 printf( "Reduced by initial cube writing = " << g_CoverInfo.nCubesBefore-nCubesAfterWriting << endl;
314 printf( "Reduced by shallow simplification = " << nCubesAfterWriting-nCubesAfterShallow << endl;
315 printf( "Reduced by deep simplification = " << nCubesAfterWriting-s_nCubesInUse << endl;
316
317// printf( "\nThe total number of cubes created = " << g_CoverInfo.cIDs << endl;
318// printf( "Total number of places in a queque = " << s_nPosAlloc << endl;
319// printf( "Minimum free places in queque-2 = " << s_nPosMax[0] << endl;
320// printf( "Minimum free places in queque-3 = " << s_nPosMax[1] << endl;
321// printf( "Minimum free places in queque-4 = " << s_nPosMax[2] << endl;
322*/
323
324 // write the number of cubes into cover information
325 assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc );
326
327// printf( "\nThe output cover is\n" );
328// PrintCoverDebug( cout );
329
330 return 0;
331}
332
334// quite a good script
336/*
337 long clk1 = Abc_Clock();
338 int nIterWithoutImprovement = 0;
339 do
340 {
341 PrintQuequeStats();
342 GainTotal = 0;
343 GainTotal += IterativelyApplyExorLink( DIST2, 0|2|0 );
344 GainTotal += IterativelyApplyExorLink( DIST3, 0|2|0 );
345 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
346 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
347
348 if ( nIterWithoutImprovement > 2 )
349 {
350 GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
351 GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 );
352 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
353 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
354 }
355
356 if ( nIterWithoutImprovement > 6 )
357 {
358 GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
359 GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
360 GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
361 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
362 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
363 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
364 }
365
366 if ( GainTotal )
367 nIterWithoutImprovement = 0;
368 else
369 nIterWithoutImprovement++;
370 }
371 while ( nIterWithoutImprovement < 12 );
372
373 nCubesAfterShallow = s_nCubesInUse;
374
375*/
376
377/*
378 // alu4 - 439
379 long clk1 = Abc_Clock();
380 int nIterWithoutImprovement = 0;
381 do
382 {
383 PrintQuequeStats();
384 GainTotal = 0;
385 GainTotal += IterativelyApplyExorLink( DIST2, 1|0|0 );
386 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
387 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
388 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
389 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
390 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
391
392 if ( nIterWithoutImprovement > 2 )
393 {
394 GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
395 GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 );
396 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
397 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
398 }
399
400 if ( nIterWithoutImprovement > 6 )
401 {
402 GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
403 GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
404 GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
405 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
406 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
407 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
408 }
409
410 if ( GainTotal )
411 nIterWithoutImprovement = 0;
412 else
413 nIterWithoutImprovement++;
414 }
415 while ( nIterWithoutImprovement < 12 );
416*/
417
418/*
419// alu4 - 412 cubes, 700 sec
420
421 long clk1 = Abc_Clock();
422 int nIterWithoutImprovement = 0;
423 int nIterCount = 0;
424 do
425 {
426 printf( "\nITERATION #" << ++nIterCount << endl << endl;
427
428 GainTotal = 0;
429 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
430 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
431 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
432 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
433 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
434 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
435
436 if ( nIterWithoutImprovement > 3 )
437 {
438 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
439 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
440 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
441 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
442 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
443 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
444 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
445 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
446 }
447
448 if ( nIterWithoutImprovement > 7 )
449 {
450 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
451 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
452 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
453 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
454 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
455 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
456 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
457 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
458 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
459 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
460 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
461 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
462 }
463
464 if ( GainTotal )
465 nIterWithoutImprovement = 0;
466 else
467 nIterWithoutImprovement++;
468 }
469 while ( nIterWithoutImprovement < 12 );
470*/
471
472/*
473// pretty good script
474// alu4 = 424 in 250 sec
475
476 long clk1 = Abc_Clock();
477 int nIterWithoutImprovement = 0;
478 int nIterCount = 0;
479 do
480 {
481 printf( "\nITERATION #" << ++nIterCount << " |";
482 for ( int k = 0; k < nIterWithoutImprovement; k++ )
483 printf( "*";
484 for ( ; k < 11; k++ )
485 printf( "_";
486 printf( "|" << endl << endl;
487
488 GainTotal = 0;
489 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
490 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
491 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
492 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
493 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
494
495 if ( nIterWithoutImprovement > 2 )
496 {
497 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
498 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
499 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
500 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
501 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
502 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
503 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
504 }
505
506 if ( nIterWithoutImprovement > 4 )
507 {
508 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
509 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
510 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
511 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
512 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
513 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
514 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
515 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
516 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
517 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
518 }
519
520 if ( GainTotal )
521 nIterWithoutImprovement = 0;
522 else
523 nIterWithoutImprovement++;
524 }
525 while ( nIterWithoutImprovement < 7 );
526*/
527
528/*
529alu4 = 435 70 secs
530
531 long clk1 = Abc_Clock();
532 int nIterWithoutImprovement = 0;
533 int nIterCount = 0;
534
535 do
536 {
537 printf( "\nITERATION #" << ++nIterCount << endl << endl;
538
539 GainTotal = 0;
540 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
541 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
542
543 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
544 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
545
546 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
547 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
548
549 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
550 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
551
552 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
553 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
554
555 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
556 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
557
558
559 if ( GainTotal )
560 nIterWithoutImprovement = 0;
561 else
562 nIterWithoutImprovement++;
563 }
564 while ( nIterWithoutImprovement < 4 );
565*/
566
567/*
568 // the best previous
569
570 long clk1 = Abc_Clock();
571 int nIterWithoutImprovement = 0;
572 int nIterCount = 0;
573 int GainTotal;
574 do
575 {
576 if ( g_CoverInfo.Verbosity == 2 )
577 printf( "\nITERATION #" << ++nIterCount << endl << endl;
578 else if ( g_CoverInfo.Verbosity == 1 )
579 cout << '.';
580
581 GainTotal = 0;
582 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
583 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
584
585 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
586 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
587
588 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
589 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
590
591 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
592 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
593
594 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
595 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
596
597 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
598 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
599
600 if ( nIterWithoutImprovement > 1 )
601 {
602 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
603 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
604 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
605 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
606 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
607 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
608 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
609 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
610
611 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
612 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
613 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
614 GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
615 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
616 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
617 GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
618 GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
619 }
620
621 if ( GainTotal )
622 nIterWithoutImprovement = 0;
623 else
624 nIterWithoutImprovement++;
625 }
626// while ( nIterWithoutImprovement < 20 );
627// while ( nIterWithoutImprovement < 7 );
628 while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
629
630*/
631
632/*
633// the last tried
634
635 long clk1 = Abc_Clock();
636 int nIterWithoutImprovement = 0;
637 int nIterCount = 0;
638 int GainTotal;
639 do
640 {
641 if ( g_CoverInfo.Verbosity == 2 )
642 printf( "\nITERATION #" << ++nIterCount << endl << endl;
643 else if ( g_CoverInfo.Verbosity == 1 )
644 cout << '.';
645
646 GainTotal = 0;
647 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
648 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
649
650 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
651 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
652
653 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
654 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
655
656 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
657 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
658
659 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
660 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
661
662 if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) )
663 {
664 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
665 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
666 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
667 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
668 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
669 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
670 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
671 GainTotal += IterativelyApplyExorLink4( 1|2|0 );
672
673 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
674 GainTotal += IterativelyApplyExorLink3( 1|2|0 );
675 GainTotal += IterativelyApplyExorLink2( 1|2|0 );
676 GainTotal += IterativelyApplyExorLink3( 1|2|4 );
677 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
678 GainTotal += IterativelyApplyExorLink4( 1|2|4 );
679 GainTotal += IterativelyApplyExorLink2( 1|2|4 );
680 GainTotal += IterativelyApplyExorLink4( 1|2|0 );
681 }
682
683 if ( GainTotal )
684 nIterWithoutImprovement = 0;
685 else
686 nIterWithoutImprovement++;
687 }
688 while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
689*/
690
702void AddCubesToStartingCover( Vec_Wec_t * vEsop )
703{
704 Vec_Int_t * vCube;
705 Cube * pNew;
706 int * s_Level2Var;
707 int * s_LevelValues;
708 int c, i, k, Lit, Out;
709
710 s_Level2Var = ABC_ALLOC( int, g_CoverInfo.nVarsIn );
711 s_LevelValues = ABC_ALLOC( int, g_CoverInfo.nVarsIn );
712
713 for ( i = 0; i < g_CoverInfo.nVarsIn; i++ )
714 s_Level2Var[i] = i;
715
716 g_CoverInfo.nLiteralsBefore = 0;
717 g_CoverInfo.QCostBefore = 0;
718 Vec_WecForEachLevel( vEsop, vCube, c )
719 {
720 // get the output of this cube
721 Out = -Vec_IntPop(vCube) - 1;
722
723 // fill in the cube with blanks
724 for ( i = 0; i < g_CoverInfo.nVarsIn; i++ )
725 s_LevelValues[i] = VAR_ABS;
726 Vec_IntForEachEntry( vCube, Lit, k )
727 {
728 if ( Abc_LitIsCompl(Lit) )
729 s_LevelValues[Abc_Lit2Var(Lit)] = VAR_NEG;
730 else
731 s_LevelValues[Abc_Lit2Var(Lit)] = VAR_POS;
732 }
733
734 // get the new cube
735 pNew = GetFreeCube();
736 // consider the need to clear the cube
737 if ( pNew->pCubeDataIn[0] ) // this is a recycled cube
738 {
739 for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
740 pNew->pCubeDataIn[i] = 0;
741 for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
742 pNew->pCubeDataOut[i] = 0;
743 }
744
745 InsertVarsWithoutClearing( pNew, s_Level2Var, g_CoverInfo.nVarsIn, s_LevelValues, Out );
746 // set literal counts
747 pNew->a = Vec_IntSize(vCube);
748 pNew->z = 1;
749 pNew->q = ComputeQCost(vCube);
750 // set the ID
751 pNew->ID = g_CoverInfo.cIDs++;
752 // skip through zero-ID
753 if ( g_CoverInfo.cIDs == 256 )
754 g_CoverInfo.cIDs = 1;
755
756 // add this cube to storage
757 CheckForCloseCubes( pNew, 1 );
758
759 g_CoverInfo.nLiteralsBefore += Vec_IntSize(vCube);
760 g_CoverInfo.QCostBefore += ComputeQCost(vCube);
761 }
762 ABC_FREE( s_Level2Var );
763 ABC_FREE( s_LevelValues );
764
765 assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc );
766}
767
779int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
780{
781 abctime clk1;
782 int RemainderBits;
783 int TotalWords;
784 int MemTemp, MemTotal;
785
787 // STEPS of HEURISTIC ESOP MINIMIZATION
790 // STEP 1: determine the size of the starting cover
792 assert( nIns > 0 );
793 // inputs
794 RemainderBits = (nIns*2)%(sizeof(unsigned)*8);
795 TotalWords = (nIns*2)/(sizeof(unsigned)*8) + (RemainderBits > 0);
796 g_CoverInfo.nVarsIn = nIns;
797 g_CoverInfo.nWordsIn = TotalWords;
798 // outputs
799 RemainderBits = (nOuts)%(sizeof(unsigned)*8);
800 TotalWords = (nOuts)/(sizeof(unsigned)*8) + (RemainderBits > 0);
801 g_CoverInfo.nVarsOut = nOuts;
802 g_CoverInfo.nWordsOut = TotalWords;
803 g_CoverInfo.cIDs = 1;
804
805 // cubes
806 clk1 = Abc_Clock();
807// g_CoverInfo.nCubesBefore = CountTermsInPseudoKroneckerCover( g_Func.dd, nOuts );
808 g_CoverInfo.nCubesBefore = Vec_WecSize(vEsop);
809 g_CoverInfo.TimeStart = Abc_Clock() - clk1;
810
811 if ( g_CoverInfo.Verbosity )
812 {
813 printf( "Starting cover generation time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) );
814 printf( "The number of cubes in the starting cover is %d\n", g_CoverInfo.nCubesBefore );
815 }
816
817 if ( g_CoverInfo.nCubesBefore > g_CoverInfo.nCubesMax )
818 {
819 printf( "\nThe size of the starting cover is more than %d cubes. Quitting...\n", g_CoverInfo.nCubesMax );
820 return 0;
821 }
822
824 // STEP 2: prepare internal data structures
826 g_CoverInfo.nCubesAlloc = g_CoverInfo.nCubesBefore + ADDITIONAL_CUBES;
827
828 // allocate cube cover
829 MemTotal = 0;
830 MemTemp = AllocateCover( g_CoverInfo.nCubesAlloc, g_CoverInfo.nWordsIn, g_CoverInfo.nWordsOut );
831 if ( MemTemp == 0 )
832 {
833 printf( "Unexpected memory allocation problem. Quitting...\n" );
834 return 0;
835 }
836 else
837 MemTotal += MemTemp;
838
839 // allocate cube sets
840 MemTemp = AllocateCubeSets( g_CoverInfo.nVarsIn, g_CoverInfo.nVarsOut );
841 if ( MemTemp == 0 )
842 {
843 printf( "Unexpected memory allocation problem. Quitting...\n" );
844 return 0;
845 }
846 else
847 MemTotal += MemTemp;
848
849 // allocate adjacency queques
850 MemTemp = AllocateQueques( g_CoverInfo.nCubesAlloc*g_CoverInfo.nCubesAlloc/CUBE_PAIR_FACTOR );
851 if ( MemTemp == 0 )
852 {
853 printf( "Unexpected memory allocation problem. Quitting...\n" );
854 return 0;
855 }
856 else
857 MemTotal += MemTemp;
858
859 if ( g_CoverInfo.Verbosity )
860 printf( "Dynamically allocated memory is %dK\n", MemTotal/1000 );
861
863 // STEP 3: write the cube cover into the allocated storage
866 clk1 = Abc_Clock();
867 if ( g_CoverInfo.Verbosity )
868 printf( "Generating the starting cover...\n" );
869 AddCubesToStartingCover( vEsop );
871
873 // STEP 4: iteratively improve the cover
875 if ( g_CoverInfo.Verbosity )
876 printf( "Performing minimization...\n" );
877 clk1 = Abc_Clock();
878 ReduceEsopCover();
879 g_CoverInfo.TimeMin = Abc_Clock() - clk1;
880// g_Func.TimeMin = (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC);
881 if ( g_CoverInfo.Verbosity )
882 {
883 printf( "\nMinimization time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) );
884 printf( "\nThe number of cubes after minimization is %d\n", g_CoverInfo.nCubesInUse );
885 }
886
888 // STEP 5: save the cover into file
890 // if option is MULTI_OUTPUT, the output is written into the output file;
891 // if option is SINGLE_NODE, the output is added to the input file
892 // and written into the output file; in this case, the minimized nodes is
893 // also stored in the temporary file "temp.blif" for verification
894
895 // create the file name and write the output
896 {
897 char Buffer[1000];
898 sprintf( Buffer, "%s", pFileNameOut ? pFileNameOut : "temp.esop" );
899 WriteResultIntoFile( Buffer );
900 if ( g_CoverInfo.Verbosity )
901 printf( "Minimized cover has been written into file <%s>\n", Buffer );
902 }
903
905 // STEP 6: delocate memory
907 DelocateCubeSets();
908 DelocateCover();
909 DelocateQueques();
910
911 // return success
912 return 1;
913}
914
915
927int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity, int nCubesMax, int fUseQCost )
928{
929 memset( &g_CoverInfo, 0, sizeof(cinfo) );
930 g_CoverInfo.Quality = Quality;
931 g_CoverInfo.Verbosity = Verbosity;
932 g_CoverInfo.nCubesMax = nCubesMax;
933 g_CoverInfo.fUseQCost = fUseQCost;
934 if ( fUseQCost )
935 s_fDecreaseLiterals = 1;
936 if ( g_CoverInfo.Verbosity )
937 {
938 printf( "\nEXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" );
939 printf( "by Alan Mishchenko, Portland State University, July-September 2000\n\n" );
940 printf( "Incoming ESOP has %d inputs, %d outputs, and %d cubes.\n", nIns, nOuts, Vec_WecSize(vEsop) );
941 }
942 PrepareBitSetModule();
943 if ( Exorcism( vEsop, nIns, nOuts, pFileNameOut ) == 0 )
944 {
945 printf( "Something went wrong when minimizing the cover\n" );
946 return 0;
947 }
948 return 1;
949}
950
951Vec_Wec_t * Abc_ExorcismNtk2Esop( Abc_Ntk_t * pNtk )
952{
953 Vec_Wec_t * vEsop = NULL;
954 Abc_Obj_t * pNode, * pFanin, * pDriver;
955 char * pCube;
956 int nIns, nOuts, nProducts, nFanins, i, k;
957
958 nIns = Abc_NtkCiNum( pNtk );
959 nOuts = Abc_NtkCoNum( pNtk );
960
961 nProducts = 0;
962 Abc_NtkForEachCo( pNtk, pNode, i )
963 {
964 pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
965 if ( !Abc_ObjIsNode(pDriver) )
966 {
967 nProducts++;
968 continue;
969 }
970 if ( Abc_NodeIsConst(pDriver) )
971 {
972 if ( Abc_NodeIsConst1(pDriver) )
973 nProducts++;
974 continue;
975 }
976 nProducts += Abc_SopGetCubeNum((char *)pDriver->pData);
977 }
978
979 Abc_NtkForEachCi( pNtk, pNode, i )
980 pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)i;
981
982 vEsop = Vec_WecAlloc( nProducts+1 );
983
984 Abc_NtkForEachCo( pNtk, pNode, i )
985 {
986 pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
987 if ( Abc_NodeIsConst(pDriver) ) continue;
988
989 nFanins = Abc_ObjFaninNum(pDriver);
990 Abc_SopForEachCube( (char *)pDriver->pData, nFanins, pCube )
991 {
992 Vec_Int_t *vCubeIn = Vec_WecPushLevel( vEsop );
993 Vec_IntGrow( vCubeIn, nIns+2 );
994
995 Abc_ObjForEachFanin( pDriver, pFanin, k )
996 {
997 pFanin = Abc_ObjFanin0Ntk(pFanin);
998 assert( (int)(ABC_PTRUINT_T)pFanin->pCopy < nIns );
999 if ( pCube[k] == '0' )
1000 {
1001 Vec_IntPush( vCubeIn, 2*k + 1 );
1002 }
1003 else if ( pCube[k] == '1' )
1004 {
1005 Vec_IntPush( vCubeIn, 2*k );
1006 }
1007 }
1008 Vec_IntPush( vCubeIn, -( i + 1 ) );
1009 }
1010 }
1011
1012 return vEsop;
1013}
1014
1015
1019
1020
1021ABC_NAMESPACE_IMPL_END
1022
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_NtkForEachCo
#define Abc_NtkForEachCo(pNtk, pCo, i)
Definition abc.h:522
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
Abc_Ntk_t
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
Abc_NodeIsConst
ABC_DLL int Abc_NodeIsConst(Abc_Obj_t *pNode)
Definition abcObj.c:867
Abc_SopForEachCube
#define Abc_SopForEachCube(pSop, nFanins, pCube)
Definition abc.h:538
Abc_NtkForEachCi
#define Abc_NtkForEachCi(pNtk, pCi, i)
Definition abc.h:518
Abc_SopGetCubeNum
ABC_DLL int Abc_SopGetCubeNum(char *pSop)
Definition abcSop.c:537
Abc_NodeIsConst1
ABC_DLL int Abc_NodeIsConst1(Abc_Obj_t *pNode)
Definition abcObj.c:916
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
GetVar
varvalue GetVar(Cube *pC, int Var)
INLINE FUNCTION DEFINITIONS ///.
Definition exorBits.c:188
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Abc_ExorcismNtk2Esop
Vec_Wec_t * Abc_ExorcismNtk2Esop(Abc_Ntk_t *pNtk)
Definition exor.c:951
Exorcism
int Exorcism(Vec_Wec_t *vEsop, int nIns, int nOuts, char *pFileNameOut)
Definition exor.c:779
Abc_ExorcismMain
int Abc_ExorcismMain(Vec_Wec_t *vEsop, int nIns, int nOuts, char *pFileNameOut, int Quality, int Verbosity, int nCubesMax, int fUseQCost)
Definition exor.c:927
s_fDecreaseLiterals
int s_fDecreaseLiterals
Definition exorList.c:247
GetQCostTest
void GetQCostTest()
Definition exor.c:122
AddCubesToStartingCover
void AddCubesToStartingCover(Vec_Wec_t *vEsop)
Definition exor.c:702
ComputeQCostTcountBits
int ComputeQCostTcountBits(Cube *p)
Definition exor.c:179
ComputeQCostTcount
int ComputeQCostTcount(Vec_Int_t *vCube)
Definition exor.c:175
ComputeQCostBits
int ComputeQCostBits(Cube *p)
Definition exor.c:139
ReduceEsopCover
int ReduceEsopCover()
Definition exor.c:203
ComputeQCost
int ComputeQCost(Vec_Int_t *vCube)
Definition exor.c:132
GetQCost
int GetQCost(int nVars, int nNegs)
EXTERNAL FUNCTIONS ///.
Definition exor.c:96
g_CoverInfo
ABC_NAMESPACE_IMPL_START cinfo g_CoverInfo
GLOBAL VARIABLES ///.
Definition exor.c:58
ToffoliGateCount
int ToffoliGateCount(int controls, int lines)
Definition exor.c:154
AllocateCover
int AllocateCover(int nCubes, int nWordsIn, int nWordsOut)
CUBE COVER MEMORY MANAGEMENT //.
Definition exorCubes.c:90
DelocateQueques
void DelocateQueques()
Definition exorList.c:1139
PrepareBitSetModule
void PrepareBitSetModule()
FUNCTION DEFINITIONS ///.
Definition exorBits.c:144
IterativelyApplyExorLink4
int IterativelyApplyExorLink4(char fDistEnable)
Definition exorList.c:524
AllocateCubeSets
int AllocateCubeSets(int nVarsIn, int nVarsOut)
CUBE SET MANIPULATION PROCEDURES ///.
Definition exorList.c:792
AllocateQueques
int AllocateQueques(int nPlaces)
Definition exorList.c:1112
DelocateCubeSets
void DelocateCubeSets()
Definition exorList.c:816
InsertVarsWithoutClearing
void InsertVarsWithoutClearing(Cube *pC, int *pVars, int nVarsIn, int *pVarValues, int Output)
Definition exorBits.c:388
WriteResultIntoFile
int WriteResultIntoFile(char *pFileName)
Definition exorUtil.c:182
Cube
struct cube Cube
ADDITIONAL_CUBES
@ ADDITIONAL_CUBES
Definition exor.h:67
CUBE_PAIR_FACTOR
@ CUBE_PAIR_FACTOR
Definition exor.h:70
IterativelyApplyExorLink3
int IterativelyApplyExorLink3(char fDistEnable)
Definition exorList.c:405
IterativelyApplyExorLink2
int IterativelyApplyExorLink2(char fDistEnable)
FUNCTIONS OF THIS MODULE ///.
Definition exorList.c:277
GetFreeCube
Cube * GetFreeCube()
Definition exorCubes.c:174
DelocateCover
void DelocateCover()
Definition exorCubes.c:147
cinfo
struct cinfo_tag cinfo
CheckForCloseCubes
int CheckForCloseCubes(Cube *p, int fAddCube)
Definition exorList.c:643
varvalue
varvalue
VARVALUE and CUBEDIST enum typedefs ///.
Definition exor.h:178
VAR_POS
@ VAR_POS
Definition exor.h:178
VAR_NEG
@ VAR_NEG
Definition exor.h:178
VAR_ABS
@ VAR_ABS
Definition exor.h:178
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition abc.h:148
cube::a
short a
Definition exor.h:126
cube::z
short z
Definition exor.h:127
cube::q
short q
Definition exor.h:128
cube::ID
byte ID
Definition exor.h:125
cube::pCubeDataOut
drow * pCubeDataOut
Definition exor.h:130
cube::pCubeDataIn
drow * pCubeDataIn
Definition exor.h:129
assert
#define assert(ex)
Definition util_old.h:213
memset
char * memset()
sprintf
char * sprintf()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
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