ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bdcDec.c
Go to the documentation of this file.
1
20
21#include "bdcInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
45void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
46{
47 int v;
48 abctime clk = 0; // Suppress "might be used uninitialized"
49 if ( p->pPars->fVerbose )
50 clk = Abc_Clock();
51 // compute support
52 pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
53 Kit_TruthSupport( pIsf->puOff, p->nVars );
54 // go through the support variables
55 for ( v = 0; v < p->nVars; v++ )
56 {
57 if ( (pIsf->uSupp & (1 << v)) == 0 )
58 continue;
59 Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
60 Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
61 if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
62 continue;
63// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
64// continue;
65 // remove the variable
66 Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
67 Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
68// Kit_TruthExist( pIsf->puOn, p->nVars, v );
69// Kit_TruthExist( pIsf->puOff, p->nVars, v );
70 pIsf->uSupp &= ~(1 << v);
71 }
72 if ( p->pPars->fVerbose )
73 p->timeSupps += Abc_Clock() - clk;
74}
75
87void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
88{
89 int v;
90 abctime clk = 0; // Suppress "might be used uninitialized"
91 if ( p->pPars->fVerbose )
92 clk = Abc_Clock();
93 // go through the support variables
94 pIsf->uSupp = 0;
95 for ( v = 0; v < p->nVars; v++ )
96 {
97 if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
98 !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
99 continue;
100 if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
101 {
102 Kit_TruthExist( pIsf->puOn, p->nVars, v );
103 Kit_TruthExist( pIsf->puOff, p->nVars, v );
104 continue;
105 }
106 pIsf->uSupp |= (1 << v);
107 }
108 if ( p->pPars->fVerbose )
109 p->timeSupps += Abc_Clock() - clk;
110}
111
123int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type )
124{
125 unsigned * puTruth = p->puTemp1;
126 // get the truth table of the left branch
127 if ( Bdc_IsComplement(pFunc0) )
128 Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars );
129 else
130 Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars );
131 // split into parts
132 if ( Type == BDC_TYPE_OR )
133 {
134// Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
135// Right.R = bdd_exist( R, setRightRes );
136
137// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
138// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
139// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V ); Cudd_Ref( pR->Q );
140// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
141
142// assert( pR->R != b0 );
143// return (int)( pR->Q == b0 );
144
145 Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
146 Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
147 Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq );
148// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
149 assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
150 return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
151 }
152 else if ( Type == BDC_TYPE_AND )
153 {
154// Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
155// Right.Q = bdd_exist( Q, setRightRes );
156
157// if ( pR->Q ) Cudd_RecursiveDeref( dd, pR->Q );
158// if ( pR->R ) Cudd_RecursiveDeref( dd, pR->R );
159// pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V ); Cudd_Ref( pR->R );
160// pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V ); Cudd_Ref( pR->Q );
161
162// assert( pR->Q != b0 );
163// return (int)( pR->R == b0 );
164
165 Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars );
166 Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq );
167 Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq );
168// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
169 assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
170 return Kit_TruthIsConst0(pIsfR->puOff, p->nVars);
171 }
172 return 0;
173}
174
186static inline int Bdc_DecomposeGetCost( Bdc_Man_t * p, int nLeftVars, int nRightVars )
187{
188 assert( nLeftVars > 0 );
189 assert( nRightVars > 0 );
190 // compute the decomposition coefficient
191 if ( nLeftVars >= nRightVars )
192 return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
193 else // if ( nLeftVars < nRightVars )
194 return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
195}
196
208int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
209{
210 char pVars[16];
211 int v, nVars, Beg, End;
212
213 assert( pIsfL->uSupp == 0 );
214 assert( pIsfR->uSupp == 0 );
215
216 // fill in the variables
217 nVars = 0;
218 for ( v = 0; v < p->nVars; v++ )
219 if ( pIsf->uSupp & (1 << v) )
220 pVars[nVars++] = v;
221
222 // try variable pairs
223 for ( Beg = 0; Beg < nVars; Beg++ )
224 {
225 Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] );
226 for ( End = nVars - 1; End > Beg; End-- )
227 {
228 Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] );
229 if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
230 {
231 pIsfL->uUniq = (1 << pVars[Beg]);
232 pIsfR->uUniq = (1 << pVars[End]);
233 return 1;
234 }
235 }
236 }
237 return 0;
238}
239
251int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
252{
253 int v, VarCost;
254 int VarBest = -1; // Suppress "might be used uninitialized"
255 int Cost, VarCostBest = 0;
256
257 for ( v = 0; v < p->nVars; v++ )
258 {
259 if ( (pIsf->uSupp & (1 << v)) == 0 )
260 continue;
261// if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
262// Exist = Cudd_bddExistAbstract( dd, pF->R, Var ); Cudd_Ref( Exist );
263// if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
264
265 Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
266 if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
267 {
268 // measure the cost of this variable
269// VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
270// Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var ); Cudd_Ref( Univ );
271// VarCost = Kit_TruthCountOnes( Univ, p->nVars );
272// Cudd_RecursiveDeref( dd, Univ );
273
274 Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
275 VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
276 if ( VarCost == 0 )
277 VarCost = 1;
278 if ( VarCostBest < VarCost )
279 {
280 VarCostBest = VarCost;
281 VarBest = v;
282 }
283 }
284 }
285
286 // derive the components for weak-bi-decomposition if the variable is found
287 if ( VarCostBest )
288 {
289// funQLeftRes = Q & bdd_exist( R, setRightORweak );
290// Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest ); Cudd_Ref( Temp );
291// pL->Q = Cudd_bddAnd( dd, pF->Q, Temp ); Cudd_Ref( pL->Q );
292// Cudd_RecursiveDeref( dd, Temp );
293
294 Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
295 Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
296
297// pL->R = pF->R; Cudd_Ref( pL->R );
298// pL->V = VarBest; Cudd_Ref( pL->V );
299 Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
300 pIsfL->uUniq = (1 << VarBest);
301 pIsfR->uUniq = 0;
302
303// assert( pL->Q != b0 );
304// assert( pL->R != b0 );
305// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
306// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
307
308 // express cost in percents of the covered boolean space
309 Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
310 if ( Cost == 0 )
311 Cost = 1;
312 return Cost;
313 }
314 return 0;
315}
316
328int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
329{
330 unsigned uSupportRem;
331 int v, nLeftVars = 1, nRightVars = 1;
332 // clean the var sets
333 Bdc_IsfStart( p, pIsfL );
334 Bdc_IsfStart( p, pIsfR );
335 // check that the support is correct
336 assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) );
337 assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) );
338 // find initial variable sets
339 if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
340 return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
341 // prequantify the variables in the offset
342 Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq );
343 Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq );
344 // go through the remaining variables
345 uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq;
346 for ( v = 0; v < p->nVars; v++ )
347 {
348 if ( (uSupportRem & (1 << v)) == 0 )
349 continue;
350 // prequantify this variable
351 Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
352 Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
353 if ( nLeftVars < nRightVars )
354 {
355// if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
356// if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
357 if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
358 {
359// pL->V &= VarNew;
360 pIsfL->uUniq |= (1 << v);
361 nLeftVars++;
362 Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
363 }
364// else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
365 else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
366 {
367// pR->V &= VarNew;
368 pIsfR->uUniq |= (1 << v);
369 nRightVars++;
370 Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
371 }
372 }
373 else
374 {
375// if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
376 if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
377 {
378// pR->V &= VarNew;
379 pIsfR->uUniq |= (1 << v);
380 nRightVars++;
381 Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
382 }
383// else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
384 else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
385 {
386// pL->V &= VarNew;
387 pIsfL->uUniq |= (1 << v);
388 nLeftVars++;
389 Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
390 }
391 }
392 }
393
394 // derive the functions Q and R for the left branch
395// pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
396// pL->R = bdd_exist( pF->R, pR->V );
397
398// Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( Temp );
399// pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
400// Cudd_RecursiveDeref( dd, Temp );
401// pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( pL->R );
402
403 Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
404 Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq );
405 Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
406
407// assert( pL->Q != b0 );
408// assert( pL->R != b0 );
409// assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
410 assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
411 assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
412// assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
413
414 // derive the functions Q and R for the right branch
415// Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V ); Cudd_Ref( Temp );
416// pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
417// Cudd_RecursiveDeref( dd, Temp );
418// pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V ); Cudd_Ref( pR->R );
419
420 Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
421 Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
422 Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
423
424 assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
425 assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
426// assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
427
428 assert( pIsfL->uUniq );
429 assert( pIsfR->uUniq );
430 return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );
431}
432
444Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
445{
446 int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR;
447
448 Bdc_IsfClean( p->pIsfOL );
449 Bdc_IsfClean( p->pIsfOR );
450 Bdc_IsfClean( p->pIsfAL );
451 Bdc_IsfClean( p->pIsfAR );
452
453 // perform OR decomposition
454 WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
455
456 // perform AND decomposition
457 Bdc_IsfNot( pIsf );
458 WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
459 Bdc_IsfNot( pIsf );
460 Bdc_IsfNot( p->pIsfAL );
461 Bdc_IsfNot( p->pIsfAR );
462
463 // check the case when decomposition does not exist
464 if ( WeightOr == 0 && WeightAnd == 0 )
465 {
466 Bdc_IsfCopy( pIsfL, p->pIsfOL );
467 Bdc_IsfCopy( pIsfR, p->pIsfOR );
468 return BDC_TYPE_MUX;
469 }
470 // check the hash table
471 assert( WeightOr || WeightAnd );
472 WeightOrL = WeightOrR = 0;
473 if ( WeightOr )
474 {
475 if ( p->pIsfOL->uUniq )
476 {
477 Bdc_SuppMinimize( p, p->pIsfOL );
478 WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
479 }
480 if ( p->pIsfOR->uUniq )
481 {
482 Bdc_SuppMinimize( p, p->pIsfOR );
483 WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
484 }
485 }
486 WeightAndL = WeightAndR = 0;
487 if ( WeightAnd )
488 {
489 if ( p->pIsfAL->uUniq )
490 {
491 Bdc_SuppMinimize( p, p->pIsfAL );
492 WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
493 }
494 if ( p->pIsfAR->uUniq )
495 {
496 Bdc_SuppMinimize( p, p->pIsfAR );
497 WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
498 }
499 }
500
501 // check if there is any reuse for the components
502 if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
503 {
504 p->numReuse++;
505 p->numOrs++;
506 Bdc_IsfCopy( pIsfL, p->pIsfOL );
507 Bdc_IsfCopy( pIsfR, p->pIsfOR );
508 return BDC_TYPE_OR;
509 }
510 if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
511 {
512 p->numReuse++;
513 p->numAnds++;
514 Bdc_IsfCopy( pIsfL, p->pIsfAL );
515 Bdc_IsfCopy( pIsfR, p->pIsfAR );
516 return BDC_TYPE_AND;
517 }
518
519 // compare the two-component costs
520 if ( WeightOr > WeightAnd )
521 {
522 if ( WeightOr < BDC_SCALE )
523 p->numWeaks++;
524 p->numOrs++;
525 Bdc_IsfCopy( pIsfL, p->pIsfOL );
526 Bdc_IsfCopy( pIsfR, p->pIsfOR );
527 return BDC_TYPE_OR;
528 }
529 if ( WeightAnd < BDC_SCALE )
530 p->numWeaks++;
531 p->numAnds++;
532 Bdc_IsfCopy( pIsfL, p->pIsfAL );
533 Bdc_IsfCopy( pIsfR, p->pIsfAR );
534 return BDC_TYPE_AND;
535}
536
548int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
549{
550 int Var, VarMin, nSuppMin, nSuppCur;
551 unsigned uSupp0, uSupp1;
552 abctime clk = 0; // Suppress "might be used uninitialized"
553 if ( p->pPars->fVerbose )
554 clk = Abc_Clock();
555 VarMin = -1;
556 nSuppMin = 1000;
557 for ( Var = 0; Var < p->nVars; Var++ )
558 {
559 if ( (pIsf->uSupp & (1 << Var)) == 0 )
560 continue;
561 Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, Var );
562 Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var );
563 Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, Var );
564 Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var );
565 uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars );
566 uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars );
567 nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1);
568 if ( nSuppMin > nSuppCur )
569 {
570 nSuppMin = nSuppCur;
571 VarMin = Var;
572 break;
573 }
574 }
575 if ( VarMin >= 0 )
576 {
577 Kit_TruthCofactor0New( pIsfL->puOn, pIsf->puOn, p->nVars, VarMin );
578 Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin );
579 Kit_TruthCofactor1New( pIsfR->puOn, pIsf->puOn, p->nVars, VarMin );
580 Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin );
581 Bdc_SuppMinimize( p, pIsfL );
582 Bdc_SuppMinimize( p, pIsfR );
583 }
584 if ( p->pPars->fVerbose )
585 p->timeMuxes += Abc_Clock() - clk;
586 return VarMin;
587}
588
600int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc )
601{
602 unsigned * puTruth = p->puTemp1;
603 if ( Bdc_IsComplement(pFunc) )
604 Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
605 else
606 Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
607 return Bdc_TableCheckContainment( p, pIsf, puTruth );
608}
609
621Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type )
622{
623 Bdc_Fun_t * pFunc;
624 pFunc = Bdc_FunNew( p );
625 if ( pFunc == NULL )
626 return NULL;
627 pFunc->Type = Type;
628 pFunc->pFan0 = pFunc0;
629 pFunc->pFan1 = pFunc1;
630 pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
631 // get the truth table of the left branch
632 if ( Bdc_IsComplement(pFunc0) )
633 Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars );
634 else
635 Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars );
636 // get the truth table of the right branch
637 if ( Bdc_IsComplement(pFunc1) )
638 Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars );
639 else
640 Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars );
641 // compute the function of node
642 if ( pFunc->Type == BDC_TYPE_AND )
643 {
644 Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
645 }
646 else if ( pFunc->Type == BDC_TYPE_OR )
647 {
648 Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
649 // transform to AND gate
650 pFunc->Type = BDC_TYPE_AND;
651 pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
652 pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
653 Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
654 pFunc = Bdc_Not(pFunc);
655 }
656 else
657 assert( 0 );
658 // add to table
659 Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars );
660 Bdc_TableAdd( p, Bdc_Regular(pFunc) );
661 return pFunc;
662}
663
675Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
676{
677// int static Counter = 0;
678// int LocalCounter = Counter++;
679 Bdc_Type_t Type;
680 Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
681 Bdc_Isf_t IsfL, * pIsfL = &IsfL;
682 Bdc_Isf_t IsfB, * pIsfR = &IsfB;
683 int iVar;
684 abctime clk = 0; // Suppress "might be used uninitialized"
685/*
686printf( "Init function (%d):\n", LocalCounter );
687Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
688Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
689*/
690 // check computed results
691 assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
692 if ( p->pPars->fVerbose )
693 clk = Abc_Clock();
694 pFunc = Bdc_TableLookup( p, pIsf );
695 if ( p->pPars->fVerbose )
696 p->timeCache += Abc_Clock() - clk;
697 if ( pFunc )
698 return pFunc;
699 // decide on the decomposition type
700 if ( p->pPars->fVerbose )
701 clk = Abc_Clock();
702 Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
703 if ( p->pPars->fVerbose )
704 p->timeCheck += Abc_Clock() - clk;
705 if ( Type == BDC_TYPE_MUX )
706 {
707 if ( p->pPars->fVerbose )
708 clk = Abc_Clock();
709 iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
710 if ( p->pPars->fVerbose )
711 p->timeMuxes += Abc_Clock() - clk;
712 p->numMuxes++;
713 pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
714 pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
715 if ( pFunc0 == NULL || pFunc1 == NULL )
716 return NULL;
717 pFunc = Bdc_FunWithId( p, iVar + 1 );
718 pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
719 pFunc1 = Bdc_ManCreateGate( p, pFunc, pFunc1, BDC_TYPE_AND );
720 if ( pFunc0 == NULL || pFunc1 == NULL )
721 return NULL;
722 pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
723 }
724 else
725 {
726 pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
727 if ( pFunc0 == NULL )
728 return NULL;
729 // decompose the right branch
730 if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
731 {
732 p->nNodesNew--;
733 return pFunc0;
734 }
735 Bdc_SuppMinimize( p, pIsfR );
736 pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
737 if ( pFunc1 == NULL )
738 return NULL;
739 // create new gate
740 pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
741 }
742 return pFunc;
743}
744
748
749
750ABC_NAMESPACE_IMPL_END
751
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
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
Bdc_ManNodeVerify
int Bdc_ManNodeVerify(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Fun_t *pFunc)
Definition bdcDec.c:600
Bdc_DecomposeFindInitialVarSet
int Bdc_DecomposeFindInitialVarSet(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition bdcDec.c:208
Bdc_DecomposeUpdateRight
int Bdc_DecomposeUpdateRight(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR, Bdc_Fun_t *pFunc0, Bdc_Type_t Type)
Definition bdcDec.c:123
Bdc_ManDecompose_rec
Bdc_Fun_t * Bdc_ManDecompose_rec(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
MACRO DEFINITIONS ///.
Definition bdcDec.c:675
Bdc_DecomposeStepMux
int Bdc_DecomposeStepMux(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition bdcDec.c:548
Bdc_ManCreateGate
Bdc_Fun_t * Bdc_ManCreateGate(Bdc_Man_t *p, Bdc_Fun_t *pFunc0, Bdc_Fun_t *pFunc1, Bdc_Type_t Type)
Definition bdcDec.c:621
Bdc_SuppMinimize2
ABC_NAMESPACE_IMPL_START void Bdc_SuppMinimize2(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
DECLARATIONS ///.
Definition bdcDec.c:45
Bdc_SuppMinimize
void Bdc_SuppMinimize(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition bdcDec.c:87
Bdc_DecomposeOr
int Bdc_DecomposeOr(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition bdcDec.c:328
Bdc_DecomposeStep
Bdc_Type_t Bdc_DecomposeStep(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition bdcDec.c:444
Bdc_DecomposeWeakOr
int Bdc_DecomposeWeakOr(Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
Definition bdcDec.c:251
Bdc_TableAdd
void Bdc_TableAdd(Bdc_Man_t *p, Bdc_Fun_t *pFunc)
Definition bdcTable.c:101
Bdc_TableCheckContainment
int Bdc_TableCheckContainment(Bdc_Man_t *p, Bdc_Isf_t *pIsf, unsigned *puTruth)
DECLARATIONS ///.
Definition bdcTable.c:45
Bdc_Isf_t
struct Bdc_Isf_t_ Bdc_Isf_t
Definition bdcInt.h:72
Bdc_Type_t
Bdc_Type_t
BASIC TYPES ///.
Definition bdcInt.h:48
BDC_TYPE_OR
@ BDC_TYPE_OR
Definition bdcInt.h:53
BDC_TYPE_AND
@ BDC_TYPE_AND
Definition bdcInt.h:52
BDC_TYPE_MUX
@ BDC_TYPE_MUX
Definition bdcInt.h:55
BDC_SCALE
#define BDC_SCALE
INCLUDES ///.
Definition bdcInt.h:41
Bdc_TableLookup
Bdc_Fun_t * Bdc_TableLookup(Bdc_Man_t *p, Bdc_Isf_t *pIsf)
Definition bdcTable.c:62
Bdc_Fun_t
typedefABC_NAMESPACE_HEADER_START struct Bdc_Fun_t_ Bdc_Fun_t
INCLUDES ///.
Definition bdc.h:42
Bdc_Man_t
struct Bdc_Man_t_ Bdc_Man_t
Definition bdc.h:43
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
Kit_TruthSupport
unsigned Kit_TruthSupport(unsigned *pTruth, int nVars)
Definition kitTruth.c:346
Kit_TruthCofactor1New
void Kit_TruthCofactor1New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:573
Kit_TruthCofactor0New
void Kit_TruthCofactor0New(unsigned *pOut, unsigned *pIn, int nVars, int iVar)
Definition kitTruth.c:521
Kit_TruthForallNew
void Kit_TruthForallNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:867
Kit_TruthVarIsVacuous
int Kit_TruthVarIsVacuous(unsigned *pOnset, unsigned *pOffset, int nVars, int iVar)
Definition kitTruth.c:625
Kit_TruthVarInSupport
int Kit_TruthVarInSupport(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:270
Kit_TruthExistSet
void Kit_TruthExistSet(unsigned *pRes, unsigned *pTruth, int nVars, unsigned uMask)
Definition kitTruth.c:793
Kit_TruthExist
void Kit_TruthExist(unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:684
Kit_TruthExistNew
void Kit_TruthExistNew(unsigned *pRes, unsigned *pTruth, int nVars, int iVar)
Definition kitTruth.c:738
Bdc_Isf_t_::puOn
unsigned * puOn
Definition bdcInt.h:77
Bdc_Isf_t_::uUniq
unsigned uUniq
Definition bdcInt.h:76
Bdc_Isf_t_::uSupp
unsigned uSupp
Definition bdcInt.h:75
Bdc_Isf_t_::puOff
unsigned * puOff
Definition bdcInt.h:78
assert
#define assert(ex)
Definition util_old.h:213