ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
darScript.c
Go to the documentation of this file.
1
20
21#include "darInt.h"
22#include "proof/dch/dch.h"
23#include "aig/gia/gia.h"
24#include "aig/gia/giaAig.h"
25
26ABC_NAMESPACE_IMPL_START
27
28
32
36
48Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
49{
50 Aig_Man_t * pTemp;
51 Dar_RwrPar_t Pars, * pPars = &Pars;
52 Dar_ManDefaultRwrParams( pPars );
53 pAig = Aig_ManDupDfs( pAig );
54 Dar_ManRewrite( pAig, pPars );
55 pAig = Aig_ManDupDfs( pTemp = pAig );
56 Aig_ManStop( pTemp );
57 return pAig;
58}
59
71Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
72//alias rwsat "st; rw -l; b -l; rw -l; rf -l"
73{
74 Aig_Man_t * pTemp;
75 abctime Time = pAig->Time2Quit;
76
77 Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
78 Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
79
80 Dar_ManDefaultRwrParams( pParsRwr );
81 Dar_ManDefaultRefParams( pParsRef );
82
83 pParsRwr->fUpdateLevel = 0;
84 pParsRef->fUpdateLevel = 0;
85
86 pParsRwr->fVerbose = fVerbose;
87 pParsRef->fVerbose = fVerbose;
88//printf( "1" );
89 pAig = Aig_ManDupDfs( pAig );
90 if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
91
92//printf( "2" );
93 // balance
94 if ( fBalance )
95 {
96 pAig->Time2Quit = Time;
97 pAig = Dar_ManBalance( pTemp = pAig, 0 );
98 Aig_ManStop( pTemp );
99 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
100 if ( Time && Abc_Clock() > Time )
101 { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
102 }
103
104//Aig_ManDumpBlif( pAig, "inter.blif", NULL, NULL );
105//printf( "3" );
106 // rewrite
107 pAig->Time2Quit = Time;
108 Dar_ManRewrite( pAig, pParsRwr );
109 pAig = Aig_ManDupDfs( pTemp = pAig );
110 Aig_ManStop( pTemp );
111 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
112 if ( Time && Abc_Clock() > Time )
113 { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
114
115//printf( "4" );
116 // refactor
117 pAig->Time2Quit = Time;
118 Dar_ManRefactor( pAig, pParsRef );
119 pAig = Aig_ManDupDfs( pTemp = pAig );
120 Aig_ManStop( pTemp );
121 if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
122 if ( Time && Abc_Clock() > Time )
123 { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
124
125//printf( "5" );
126 // balance
127 if ( fBalance )
128 {
129 pAig->Time2Quit = Time;
130 pAig = Dar_ManBalance( pTemp = pAig, 0 );
131 Aig_ManStop( pTemp );
132 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
133 if ( Time && Abc_Clock() > Time )
134 { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
135 }
136
137//printf( "6" );
138 // rewrite
139 pAig->Time2Quit = Time;
140 Dar_ManRewrite( pAig, pParsRwr );
141 pAig = Aig_ManDupDfs( pTemp = pAig );
142 Aig_ManStop( pTemp );
143 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
144 if ( Time && Abc_Clock() > Time )
145 { if ( pAig ) Aig_ManStop( pAig ); return NULL; }
146
147//printf( "7" );
148 return pAig;
149}
150
162Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
163//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
164{
165 Aig_Man_t * pTemp;
166
167 Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
168 Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
169
170 Dar_ManDefaultRwrParams( pParsRwr );
171 Dar_ManDefaultRefParams( pParsRef );
172
173 pParsRwr->fUpdateLevel = fUpdateLevel;
174 pParsRef->fUpdateLevel = fUpdateLevel;
175
176 pParsRwr->fPower = fPower;
177
178 pParsRwr->fVerbose = 0;//fVerbose;
179 pParsRef->fVerbose = 0;//fVerbose;
180
181 pAig = Aig_ManDupDfs( pAig );
182 if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
183/*
184 // balance
185 if ( fBalance )
186 {
187 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
188 Aig_ManStop( pTemp );
189 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
190 }
191*/
192 // rewrite
193 Dar_ManRewrite( pAig, pParsRwr );
194 pAig = Aig_ManDupDfs( pTemp = pAig );
195 Aig_ManStop( pTemp );
196 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
197
198 // refactor
199 Dar_ManRefactor( pAig, pParsRef );
200 pAig = Aig_ManDupDfs( pTemp = pAig );
201 Aig_ManStop( pTemp );
202 if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
203
204 // balance
205 if ( fBalance )
206 {
207 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
208 Aig_ManStop( pTemp );
209 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
210 }
211
212 pParsRwr->fUseZeros = 1;
213 pParsRef->fUseZeros = 1;
214
215 // rewrite
216 Dar_ManRewrite( pAig, pParsRwr );
217 pAig = Aig_ManDupDfs( pTemp = pAig );
218 Aig_ManStop( pTemp );
219 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
220
221 return pAig;
222}
223
235Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose )
236//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
237{
238 Aig_Man_t * pTemp;
239
240 Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
241 Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
242
243 Dar_ManDefaultRwrParams( pParsRwr );
244 Dar_ManDefaultRefParams( pParsRef );
245
246 pParsRwr->fUpdateLevel = fUpdateLevel;
247 pParsRef->fUpdateLevel = fUpdateLevel;
248 pParsRwr->fFanout = fFanout;
249 pParsRwr->fPower = fPower;
250
251 pParsRwr->fVerbose = 0;//fVerbose;
252 pParsRef->fVerbose = 0;//fVerbose;
253
254 pAig = Aig_ManDupDfs( pAig );
255 if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
256/*
257 // balance
258 if ( fBalance )
259 {
260 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
261 Aig_ManStop( pTemp );
262 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
263 }
264*/
265 // rewrite
266// Dar_ManRewrite( pAig, pParsRwr );
267 pParsRwr->fUpdateLevel = 0; // disable level update
268 Dar_ManRewrite( pAig, pParsRwr );
269 pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
270
271 pAig = Aig_ManDupDfs( pTemp = pAig );
272 Aig_ManStop( pTemp );
273 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
274
275 // refactor
276 Dar_ManRefactor( pAig, pParsRef );
277 pAig = Aig_ManDupDfs( pTemp = pAig );
278 Aig_ManStop( pTemp );
279 if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
280
281 // balance
282// if ( fBalance )
283 {
284 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
285 Aig_ManStop( pTemp );
286 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
287 }
288
289 // rewrite
290 Dar_ManRewrite( pAig, pParsRwr );
291 pAig = Aig_ManDupDfs( pTemp = pAig );
292 Aig_ManStop( pTemp );
293 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
294
295 pParsRwr->fUseZeros = 1;
296 pParsRef->fUseZeros = 1;
297
298 // rewrite
299 Dar_ManRewrite( pAig, pParsRwr );
300 pAig = Aig_ManDupDfs( pTemp = pAig );
301 Aig_ManStop( pTemp );
302 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
303
304 // balance
305 if ( fBalance )
306 {
307 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
308 Aig_ManStop( pTemp );
309 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
310 }
311
312 // refactor
313 Dar_ManRefactor( pAig, pParsRef );
314 pAig = Aig_ManDupDfs( pTemp = pAig );
315 Aig_ManStop( pTemp );
316 if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
317
318 // rewrite
319 Dar_ManRewrite( pAig, pParsRwr );
320 pAig = Aig_ManDupDfs( pTemp = pAig );
321 Aig_ManStop( pTemp );
322 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
323
324 // balance
325 if ( fBalance )
326 {
327 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
328 Aig_ManStop( pTemp );
329 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
330 }
331 return pAig;
332}
333
345Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
346//alias resyn "b; rw; rwz; b; rwz; b"
347//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
348{
349 Vec_Ptr_t * vAigs;
350
351 vAigs = Vec_PtrAlloc( 3 );
352 pAig = Aig_ManDupDfs(pAig);
353 Vec_PtrPush( vAigs, pAig );
354
355 pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
356 Vec_PtrPush( vAigs, pAig );
357//Aig_ManPrintStats( pAig );
358
359 pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
360 Vec_PtrPush( vAigs, pAig );
361//Aig_ManPrintStats( pAig );
362
363 pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
364 return vAigs;
365}
366
378Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose )
379{
380 Aig_Man_t * pMan, * pTemp;
381 Vec_Ptr_t * vAigs;
382 int i;
383 abctime clk;
384
385clk = Abc_Clock();
386// vAigs = Dar_ManChoiceSynthesisExt();
387 vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, 0, fVerbose );
388
389 // swap the first and last network
390 // this should lead to the primary choice being "better" because of synthesis
391 // (it is also important when constructing choices)
392 if ( !fConstruct )
393 {
394 pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
395 Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
396 Vec_PtrWriteEntry( vAigs, 0, pMan );
397 }
398
399if ( fVerbose )
400{
401ABC_PRT( "Synthesis time", Abc_Clock() - clk );
402}
403clk = Abc_Clock();
404 if ( fConstruct )
405 pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
406 else
407 pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
408 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
409 Aig_ManStop( pTemp );
410 Vec_PtrFree( vAigs );
411if ( fVerbose )
412{
413ABC_PRT( "Choicing time ", Abc_Clock() - clk );
414}
415 return pMan;
416// return NULL;
417}
418
419
431Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
432//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
433{
434 Aig_Man_t * pTemp;
435
436 Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
437 Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
438
439 Dar_ManDefaultRwrParams( pParsRwr );
440 Dar_ManDefaultRefParams( pParsRef );
441
442 pParsRwr->fUpdateLevel = fUpdateLevel;
443 pParsRef->fUpdateLevel = fUpdateLevel;
444
445 pParsRwr->fPower = fPower;
446
447 pParsRwr->fVerbose = 0;//fVerbose;
448 pParsRef->fVerbose = 0;//fVerbose;
449
450// pAig = Aig_ManDupDfs( pAig );
451 if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
452
453 // rewrite
454 Dar_ManRewrite( pAig, pParsRwr );
455 pAig = Aig_ManDupDfs( pTemp = pAig );
456 Aig_ManStop( pTemp );
457 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
458
459 // refactor
460 Dar_ManRefactor( pAig, pParsRef );
461 pAig = Aig_ManDupDfs( pTemp = pAig );
462 Aig_ManStop( pTemp );
463 if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
464
465 // balance
466 if ( fBalance )
467 {
468 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
469 Aig_ManStop( pTemp );
470 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
471 }
472
473 pParsRwr->fUseZeros = 1;
474 pParsRef->fUseZeros = 1;
475
476 // rewrite
477 Dar_ManRewrite( pAig, pParsRwr );
478 pAig = Aig_ManDupDfs( pTemp = pAig );
479 Aig_ManStop( pTemp );
480 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
481
482 return pAig;
483}
484
496Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose )
497//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
498{
499 Aig_Man_t * pTemp;
500
501 Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
502 Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
503
504 Dar_ManDefaultRwrParams( pParsRwr );
505 Dar_ManDefaultRefParams( pParsRef );
506
507 pParsRwr->fUpdateLevel = fUpdateLevel;
508 pParsRef->fUpdateLevel = fUpdateLevel;
509 pParsRwr->fFanout = fFanout;
510 pParsRwr->fPower = fPower;
511
512 pParsRwr->fVerbose = 0;//fVerbose;
513 pParsRef->fVerbose = 0;//fVerbose;
514
515// pAig = Aig_ManDupDfs( pAig );
516 if ( fVerbose ) printf( "Starting: " ), Aig_ManPrintStats( pAig );
517
518 // skip if lighter synthesis is requested
519 if ( !fLightSynth )
520 {
521 // rewrite
522 //Dar_ManRewrite( pAig, pParsRwr );
523// pParsRwr->fUpdateLevel = 0; // disable level update // this change was requested in July and later disabled
524 Dar_ManRewrite( pAig, pParsRwr );
525// pParsRwr->fUpdateLevel = fUpdateLevel; // reenable level update if needed
526
527 pAig = Aig_ManDupDfs( pTemp = pAig );
528 Aig_ManStop( pTemp );
529 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
530
531 // refactor
532 Dar_ManRefactor( pAig, pParsRef );
533 pAig = Aig_ManDupDfs( pTemp = pAig );
534 Aig_ManStop( pTemp );
535 if ( fVerbose ) printf( "Refactor: " ), Aig_ManPrintStats( pAig );
536 }
537
538 // balance
539 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
540 Aig_ManStop( pTemp );
541 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
542
543 // skip if lighter synthesis is requested
544 if ( !fLightSynth )
545 {
546 // rewrite
547 Dar_ManRewrite( pAig, pParsRwr );
548 pAig = Aig_ManDupDfs( pTemp = pAig );
549 Aig_ManStop( pTemp );
550 if ( fVerbose ) printf( "Rewrite: " ), Aig_ManPrintStats( pAig );
551 }
552
553 pParsRwr->fUseZeros = 1;
554 pParsRef->fUseZeros = 1;
555
556 // rewrite
557 Dar_ManRewrite( pAig, pParsRwr );
558 pAig = Aig_ManDupDfs( pTemp = pAig );
559 Aig_ManStop( pTemp );
560 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
561
562 // skip if lighter synthesis is requested
563 if ( !fLightSynth )
564 {
565 // balance
566 if ( fBalance )
567 {
568 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
569 Aig_ManStop( pTemp );
570 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
571 }
572 }
573
574 // refactor
575 Dar_ManRefactor( pAig, pParsRef );
576 pAig = Aig_ManDupDfs( pTemp = pAig );
577 Aig_ManStop( pTemp );
578 if ( fVerbose ) printf( "RefactorZ: " ), Aig_ManPrintStats( pAig );
579
580 // skip if lighter synthesis is requested
581 if ( !fLightSynth )
582 {
583 // rewrite
584 Dar_ManRewrite( pAig, pParsRwr );
585 pAig = Aig_ManDupDfs( pTemp = pAig );
586 Aig_ManStop( pTemp );
587 if ( fVerbose ) printf( "RewriteZ: " ), Aig_ManPrintStats( pAig );
588 }
589
590 // balance
591 if ( fBalance )
592 {
593 pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
594 Aig_ManStop( pTemp );
595 if ( fVerbose ) printf( "Balance: " ), Aig_ManPrintStats( pAig );
596 }
597 return pAig;
598}
599
611int Dar_NewChoiceSynthesisGuard( Aig_Man_t * pAig )
612{
613 Aig_Obj_t * pObj;
614 int i, Count = 0;
615 Aig_ManForEachNode( pAig, pObj, i )
616 if ( Aig_ObjRefs(pObj) > 1000 )
617 Count += Aig_ObjRefs(pObj) / 1000;
618 return (int)(Count > 10);
619}
620
632Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose )
633//alias resyn "b; rw; rwz; b; rwz; b"
634//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
635{
636 Vec_Ptr_t * vGias;
637 Gia_Man_t * pGia, * pTemp;
638 int i;
639
640 if ( fUpdateLevel && Dar_NewChoiceSynthesisGuard(pAig) )
641 {
642 if ( fVerbose )
643 printf( "Warning: Due to high fanout count of some nodes, level updating is disabled.\n" );
644 fUpdateLevel = 0;
645 }
646
647 vGias = Vec_PtrAlloc( 3 );
648 pGia = Gia_ManFromAig(pAig);
649 Vec_PtrPush( vGias, pGia );
650
651 pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
652 pGia = Gia_ManFromAig(pAig);
653 Vec_PtrPush( vGias, pGia );
654//Aig_ManPrintStats( pAig );
655
656 pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
657 pGia = Gia_ManFromAig(pAig);
658 Vec_PtrPush( vGias, pGia );
659//Aig_ManPrintStats( pAig );
660
661 Aig_ManStop( pAig );
662
663 // swap around the first and the last
664 pTemp = (Gia_Man_t *)Vec_PtrPop( vGias );
665 Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
666 Vec_PtrWriteEntry( vGias, 0, pTemp );
667
668// Aig_Man_t * pAig;
669// int i;
670// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
671// Vec_PtrForEachEntry( Aig_Man_t *, p->vAigs, pAig, i )
672// Aig_ManPrintStats( pAig );
673
674 // derive the miter
675 pGia = Gia_ManChoiceMiter( vGias );
676
677 // cleanup
678 Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i )
679 Gia_ManStop( pTemp );
680 Vec_PtrFree( vGias );
681 return pGia;
682}
683
695/*
696Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
697{
698 extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
699 extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
700
701 int fVerbose = pPars->fVerbose;
702 int fConstruct = 0;
703 Aig_Man_t * pMan, * pTemp;
704 Vec_Ptr_t * vAigs;
705 int i;
706 abctime clk;
707
708clk = Abc_Clock();
709// vAigs = Dar_ManChoiceSynthesisExt();
710// vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
711 vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
712
713 // swap the first and last network
714 // this should lead to the primary choice being "better" because of synthesis
715 // (it is also important when constructing choices)
716 if ( !fConstruct )
717 {
718 pMan = Vec_PtrPop( vAigs );
719 Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
720 Vec_PtrWriteEntry( vAigs, 0, pMan );
721 }
722
723if ( fVerbose )
724{
725//ABC_PRT( "Synthesis time", Abc_Clock() - clk );
726}
727 pPars->timeSynth = Abc_Clock() - clk;
728
729clk = Abc_Clock();
730 // perform choice computation
731 if ( pPars->fUseGia )
732 pMan = Cec_ComputeChoices( vAigs, pPars );
733 else
734 pMan = Dch_ComputeChoices( vAigs, pPars );
735
736 // reconstruct the network
737 pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
738 Aig_ManStop( pTemp );
739 // duplicate the timing manager
740 pTemp = Vec_PtrEntry( vAigs, 0 );
741 if ( pTemp->pManTime )
742 {
743 extern void * Tim_ManDup( void * p, int fDiscrete );
744 pMan->pManTime = Tim_ManDup( pTemp->pManTime, 0 );
745 }
746 // reset levels
747 Aig_ManChoiceLevel( pMan );
748 ABC_FREE( pMan->pName );
749 ABC_FREE( pMan->pSpec );
750 pMan->pName = Abc_UtilStrsav( pTemp->pName );
751 pMan->pSpec = Abc_UtilStrsav( pTemp->pSpec );
752
753 // cleanup
754 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
755 Aig_ManStop( pTemp );
756 Vec_PtrFree( vAigs );
757
758if ( fVerbose )
759{
760//ABC_PRT( "Choicing time ", Abc_Clock() - clk );
761}
762 return pMan;
763// return NULL;
764}
765*/
766
778Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
779{
780// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
781 extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
782 int fVerbose = pPars->fVerbose;
783 Aig_Man_t * pMan, * pTemp;
784 Vec_Ptr_t * vAigs;
785 Vec_Ptr_t * vPios;
786 void * pManTime;
787 char * pName, * pSpec;
788 int i;
789 abctime clk;
790
791clk = Abc_Clock();
792 vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
793pPars->timeSynth = Abc_Clock() - clk;
794 // swap the first and last network
795 // this should lead to the primary choice being "better" because of synthesis
796 // (it is also important when constructing choices)
797 pMan = (Aig_Man_t *)Vec_PtrPop( vAigs );
798 Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
799 Vec_PtrWriteEntry( vAigs, 0, pMan );
800
801 // derive the total AIG
802 pMan = Dch_DeriveTotalAig( vAigs );
803 // cleanup
804 Vec_PtrForEachEntry( Aig_Man_t *, vAigs, pTemp, i )
805 Aig_ManStop( pTemp );
806 Vec_PtrFree( vAigs );
807
808 // compute choices
809 pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
810 Aig_ManStop( pTemp );
811
812 // save useful things
813 pManTime = pAig->pManTime; pAig->pManTime = NULL;
814 pName = Abc_UtilStrsav( pAig->pName );
815 pSpec = Abc_UtilStrsav( pAig->pSpec );
816
817 // create guidence
818 vPios = Aig_ManOrderPios( pMan, pAig );
819 Aig_ManStop( pAig );
820
821 // reconstruct the network
822 pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
823 Aig_ManStop( pTemp );
824 Vec_PtrFree( vPios );
825
826 // reset levels
827 pMan->pManTime = pManTime;
828 Aig_ManChoiceLevel( pMan );
829
830 // copy names
831 ABC_FREE( pMan->pName );
832 ABC_FREE( pMan->pSpec );
833 pMan->pName = pName;
834 pMan->pSpec = pSpec;
835 return pMan;
836}
837
849Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
850{
851 extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
852 extern Aig_Man_t * Cec_ComputeChoicesNew2( Gia_Man_t * pGia, int nConfs, int fVerbose );
853 extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
854// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
855 extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
856// int fVerbose = pPars->fVerbose;
857 Aig_Man_t * pMan, * pTemp;
858 Gia_Man_t * pGia;
859 Vec_Ptr_t * vPios;
860 void * pManTime;
861 char * pName, * pSpec;
862 abctime clk;
863
864 // save useful things
865 pManTime = pAig->pManTime; pAig->pManTime = NULL;
866 pName = Abc_UtilStrsav( pAig->pName );
867 pSpec = Abc_UtilStrsav( pAig->pSpec );
868
869 // perform synthesis
870clk = Abc_Clock();
871 pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, pPars->fVerbose );
872pPars->timeSynth = Abc_Clock() - clk;
873
874 // perform choice computation
875 if ( pPars->fUseNew )
876 pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
877 else if ( pPars->fUseNew2 )
878 pMan = Cec_ComputeChoicesNew2( pGia, pPars->nBTLimit, pPars->fVerbose );
879 else if ( pPars->fUseGia )
880 pMan = Cec_ComputeChoices( pGia, pPars );
881 else
882 {
883 pMan = Gia_ManToAigSkip( pGia, 3 );
884 pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
885 Aig_ManStop( pTemp );
886 }
887 Gia_ManStop( pGia );
888
889 // create guidence
890 vPios = Aig_ManOrderPios( pMan, pAig );
891 Aig_ManStop( pAig );
892
893 // reconstruct the network
894 pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
895 Aig_ManStop( pTemp );
896 Vec_PtrFree( vPios );
897
898 // reset levels
899 pMan->pManTime = pManTime;
900 Aig_ManChoiceLevel( pMan );
901
902 // copy names
903 ABC_FREE( pMan->pName );
904 ABC_FREE( pMan->pSpec );
905 pMan->pName = pName;
906 pMan->pSpec = pSpec;
907 return pMan;
908}
909
910
914
915
916ABC_NAMESPACE_IMPL_END
917
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
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
Aig_ManOrderPios
Vec_Ptr_t * Aig_ManOrderPios(Aig_Man_t *p, Aig_Man_t *pOrder)
Definition aigDup.c:626
Aig_ManDupDfs
Aig_Man_t * Aig_ManDupDfs(Aig_Man_t *p)
Definition aigDup.c:563
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManChoiceConstructive
Aig_Man_t * Aig_ManChoiceConstructive(Vec_Ptr_t *vAigs, int fVerbose)
Definition aigPart.c:1564
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManDupDfsGuided
Aig_Man_t * Aig_ManDupDfsGuided(Aig_Man_t *p, Vec_Ptr_t *vPios)
Definition aigDup.c:694
Aig_ManChoicePartitioned
Aig_Man_t * Aig_ManChoicePartitioned(Vec_Ptr_t *vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose)
Definition aigPart.c:1247
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManChoiceLevel
int Aig_ManChoiceLevel(Aig_Man_t *p)
Definition aigDfs.c:595
Cec_ComputeChoicesNew
Aig_Man_t * Cec_ComputeChoicesNew(Gia_Man_t *pGia, int nConfs, int fVerbose)
Definition cecChoice.c:415
Cec_ComputeChoices
Aig_Man_t * Cec_ComputeChoices(Gia_Man_t *pGia, Dch_Pars_t *pPars)
Definition cecChoice.c:385
Cec_ComputeChoicesNew2
Aig_Man_t * Cec_ComputeChoicesNew2(Gia_Man_t *pGia, int nConfs, int fVerbose)
Definition cecChoice.c:425
Dar_NewChoiceSynthesis
Gia_Man_t * Dar_NewChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose)
Definition darScript.c:632
Dar_ManCompress2
Aig_Man_t * Dar_ManCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fVerbose)
Definition darScript.c:235
Dar_ManChoiceNew
Aig_Man_t * Dar_ManChoiceNew(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition darScript.c:849
Dar_ManChoiceNewAig
Aig_Man_t * Dar_ManChoiceNewAig(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition darScript.c:778
Dar_NewCompress2
Aig_Man_t * Dar_NewCompress2(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose)
Definition darScript.c:496
Dar_ManRwsat
Aig_Man_t * Dar_ManRwsat(Aig_Man_t *pAig, int fBalance, int fVerbose)
DECLARATIONS ///.
Definition darScript.c:71
Dar_NewCompress
Aig_Man_t * Dar_NewCompress(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition darScript.c:431
Dar_NewChoiceSynthesisGuard
int Dar_NewChoiceSynthesisGuard(Aig_Man_t *pAig)
Definition darScript.c:611
Dar_ManRewriteDefault
ABC_NAMESPACE_IMPL_START Aig_Man_t * Dar_ManRewriteDefault(Aig_Man_t *pAig)
DECLARATIONS ///.
Definition darScript.c:48
Dar_ManChoiceSynthesis
Vec_Ptr_t * Dar_ManChoiceSynthesis(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition darScript.c:345
Dar_ManChoice
Aig_Man_t * Dar_ManChoice(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fConstruct, int nConfMax, int nLevelMax, int fVerbose)
Definition darScript.c:378
Dar_ManCompress
Aig_Man_t * Dar_ManCompress(Aig_Man_t *pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose)
Definition darScript.c:162
Dar_ManRefactor
int Dar_ManRefactor(Aig_Man_t *pAig, Dar_RefPar_t *pPars)
Definition darRefact.c:496
Dar_RwrPar_t
typedefABC_NAMESPACE_HEADER_START struct Dar_RwrPar_t_ Dar_RwrPar_t
INCLUDES ///.
Definition dar.h:42
Dar_ManDefaultRwrParams
void Dar_ManDefaultRwrParams(Dar_RwrPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition darCore.c:51
Dar_ManBalance
Aig_Man_t * Dar_ManBalance(Aig_Man_t *p, int fUpdateLevel)
Definition darBalance.c:554
Dar_RefPar_t
struct Dar_RefPar_t_ Dar_RefPar_t
Definition dar.h:43
Dar_ManRewrite
int Dar_ManRewrite(Aig_Man_t *pAig, Dar_RwrPar_t *pPars)
Definition darCore.c:79
Dar_ManDefaultRefParams
void Dar_ManDefaultRefParams(Dar_RefPar_t *pPars)
FUNCTION DEFINITIONS ///.
Definition darRefact.c:85
Dch_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Dch_Pars_t_ Dch_Pars_t
INCLUDES ///.
Definition dch.h:43
Dch_ComputeChoices
Aig_Man_t * Dch_ComputeChoices(Aig_Man_t *pAig, Dch_Pars_t *pPars)
Definition dchCore.c:89
Dch_DeriveTotalAig
Aig_Man_t * Dch_DeriveTotalAig(Vec_Ptr_t *vAigs)
MACRO DEFINITIONS ///.
Definition dchAig.c:65
Gia_ManFromAig
Gia_Man_t * Gia_ManFromAig(Aig_Man_t *p)
INCLUDES ///.
Definition giaAig.c:76
Gia_ManToAigSkip
Aig_Man_t * Gia_ManToAigSkip(Gia_Man_t *p, int nOutDelta)
Definition giaAig.c:365
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManChoiceMiter
Gia_Man_t * Gia_ManChoiceMiter(Vec_Ptr_t *vGias)
Definition giaDup.c:3763
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Dar_RefPar_t_::fVerbose
int fVerbose
Definition dar.h:67
Dar_RefPar_t_::fUseZeros
int fUseZeros
Definition dar.h:66
Dar_RefPar_t_::fUpdateLevel
int fUpdateLevel
Definition dar.h:65
Gia_Man_t_::fVerbose
int fVerbose
Definition gia.h:203
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55