src/aig/bdc/bdcDec.c File Reference

#include "bdcInt.h"
Include dependency graph for bdcDec.c:

Go to the source code of this file.

Functions

static Bdc_Type_t Bdc_DecomposeStep (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
static int Bdc_DecomposeUpdateRight (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR, unsigned *puTruth, Bdc_Type_t Type)
Bdc_Fun_t * Bdc_ManDecompose_rec (Bdc_Man_t *p, Bdc_Isf_t *pIsf)
static int Bdc_DecomposeGetCost (Bdc_Man_t *p, int nLeftVars, int nRightVars)
int Bdc_DecomposeFindInitialVarSet (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
int Bdc_DecomposeWeakOr (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)
int Bdc_DecomposeOr (Bdc_Man_t *p, Bdc_Isf_t *pIsf, Bdc_Isf_t *pIsfL, Bdc_Isf_t *pIsfR)

Function Documentation

int Bdc_DecomposeFindInitialVarSet ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf,
Bdc_Isf_t *  pIsfL,
Bdc_Isf_t *  pIsfR 
)

Function*************************************************************

Synopsis [Checks existence of weak OR-bidecomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file bdcDec.c.

00182 {
00183     char pVars[16];
00184         int v, nVars, Beg, End;
00185 
00186         assert( pIsfL->uSupp == 0 );
00187         assert( pIsfR->uSupp == 0 );
00188 
00189         // fill in the variables
00190     nVars = 0;
00191         for ( v = 0; v < p->nVars; v++ )
00192         if ( pIsf->uSupp & (1 << v) )
00193             pVars[nVars++] = v;
00194 
00195     // try variable pairs
00196     for ( Beg = 0; Beg < nVars; Beg++ )
00197     {
00198         Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pVars[Beg] ); 
00199         for ( End = nVars - 1; End > Beg; End-- )
00200         {
00201             Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] ); 
00202             if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
00203             {
00204                         pIsfL->uSupp = (1 << Beg);
00205                         pIsfR->uSupp = (1 << End);
00206                         pIsfL->Var = Beg;
00207                         pIsfR->Var = End;
00208                 return 1;
00209             }
00210         }
00211     }
00212     return 0;
00213 }

static int Bdc_DecomposeGetCost ( Bdc_Man_t *  p,
int  nLeftVars,
int  nRightVars 
) [inline, static]

Function*************************************************************

Synopsis [Checks existence of OR-bidecomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file bdcDec.c.

00160 {
00161         assert( nLeftVars > 0 );
00162         assert( nRightVars > 0 );
00163         // compute the decomposition coefficient
00164         if ( nLeftVars >= nRightVars )
00165                 return BDC_SCALE * (p->nVars * nRightVars + nLeftVars);
00166         else // if ( nLeftVars < nRightVars )
00167                 return BDC_SCALE * (p->nVars * nLeftVars + nRightVars);
00168 }

int Bdc_DecomposeOr ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf,
Bdc_Isf_t *  pIsfL,
Bdc_Isf_t *  pIsfR 
)

Function*************************************************************

Synopsis [Checks existence of OR-bidecomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 298 of file bdcDec.c.

00299 {
00300     unsigned uSuppRem;
00301         int v, nLeftVars = 1, nRightVars = 1; 
00302     // clean the var sets
00303     Bdc_IsfClean( pIsfL );
00304     Bdc_IsfClean( pIsfR );
00305     // find initial variable sets
00306     if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
00307         return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
00308     // prequantify the variables in the offset
00309     Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var ); 
00310     Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var );
00311     // go through the remaining variables
00312     uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp;
00313     assert( Kit_WordCountOnes(uSuppRem) > 0 );
00314     for ( v = 0; v < p->nVars; v++ )
00315     {
00316         if ( (uSuppRem & (1 << v)) == 0 )
00317             continue;
00318         // prequantify this variable
00319         Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
00320         Kit_TruthExistNew( p->puTemp4, p->puTemp2, p->nVars, v );
00321                 if ( nLeftVars < nRightVars )
00322                 {
00323 //                      if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
00324 //                      if ( VerifyORCondition( dd, pF->Q, pF->R, pL->V, pR->V, VarNew ) )
00325                         if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
00326                         {
00327 //                              pL->V &= VarNew;
00328                 pIsfL->uSupp |= (1 << v);
00329                                 nLeftVars++;
00330                         }
00331 //                      else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
00332                         else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
00333                         {
00334 //                              pR->V &= VarNew;
00335                 pIsfR->uSupp |= (1 << v);
00336                                 nRightVars++;
00337                         }
00338                 }
00339                 else
00340                 {
00341 //                      if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
00342                         if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
00343                         {
00344 //                              pR->V &= VarNew;
00345                 pIsfR->uSupp |= (1 << v);
00346                                 nRightVars++;
00347                         }
00348 //                      else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
00349                         else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
00350                         {
00351 //                              pL->V &= VarNew;
00352                 pIsfL->uSupp |= (1 << v);
00353                                 nLeftVars++;
00354                         }
00355                 }
00356     }
00357 
00358         // derive the functions Q and R for the left branch
00359 //      pL->Q = bdd_appex( pF->Q, bdd_exist( pF->R, pL->V ), bddop_and, pR->V );
00360 //      pL->R = bdd_exist( pF->R, pR->V );
00361 
00362 //      Temp = Cudd_bddExistAbstract( dd, pF->R, pL->V );      Cudd_Ref( Temp );
00363 //      pL->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pR->V ); Cudd_Ref( pL->Q );
00364 //      Cudd_RecursiveDeref( dd, Temp );
00365 //      pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V );     Cudd_Ref( pL->R );
00366 
00367     Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
00368     Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp );
00369     Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
00370 
00371         // derive the functions Q and R for the right branch
00372 //      Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V );      Cudd_Ref( Temp );
00373 //      pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
00374 //      Cudd_RecursiveDeref( dd, Temp );
00375 //      pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V );     Cudd_Ref( pR->R );
00376 
00377 /*
00378     Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
00379     Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
00380     Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
00381 */
00382 
00383 //      assert( pL->Q != b0 );
00384 //      assert( pL->R != b0 );
00385 //      assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
00386     assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
00387     assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
00388     assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
00389 
00390         return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );                
00391 }

Bdc_Type_t Bdc_DecomposeStep ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf,
Bdc_Isf_t *  pIsfL,
Bdc_Isf_t *  pIsfR 
) [static]

CFile****************************************************************

FileName [bdcDec.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Truth-table-based bi-decomposition engine.]

Synopsis [Decomposition procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - January 30, 2007.]

Revision [

Id
bdcDec.c,v 1.00 2007/01/30 00:00:00 alanmi Exp

] DECLARATIONS ///

Function*************************************************************

Synopsis [Performs one step of bi-decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 404 of file bdcDec.c.

00405 {
00406     int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR;
00407 
00408     Bdc_IsfClean( p->pIsfOL );
00409     Bdc_IsfClean( p->pIsfOR );
00410     Bdc_IsfClean( p->pIsfAL );
00411     Bdc_IsfClean( p->pIsfAR );
00412 
00413     // perform OR decomposition
00414     CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
00415 
00416     // perform AND decomposition
00417     Bdc_IsfNot( pIsf );
00418     CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
00419     Bdc_IsfNot( pIsf );
00420     Bdc_IsfNot( p->pIsfAL );
00421     Bdc_IsfNot( p->pIsfAR );
00422 
00423     // check the hash table
00424     Bdc_SuppMinimize( p, p->pIsfOL );
00425     CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
00426     Bdc_SuppMinimize( p, p->pIsfOR );
00427     CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
00428     Bdc_SuppMinimize( p, p->pIsfAL );
00429     CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
00430     Bdc_SuppMinimize( p, p->pIsfAR );
00431     CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
00432 
00433     // check if there is any reuse for the components
00434     if ( CostOrL + CostOrR < CostAndL + CostAndR )
00435     {
00436         Bdc_IsfCopy( pIsfL, p->pIsfOL );
00437         Bdc_IsfCopy( pIsfR, p->pIsfOR );
00438         return BDC_TYPE_OR;
00439     }
00440     if ( CostOrL + CostOrR > CostAndL + CostAndR )
00441     {
00442         Bdc_IsfCopy( pIsfL, p->pIsfAL );
00443         Bdc_IsfCopy( pIsfR, p->pIsfAR );
00444         return BDC_TYPE_AND; 
00445     }
00446 
00447     // compare the two-component costs
00448     if ( CostOr < CostAnd )
00449     {
00450         Bdc_IsfCopy( pIsfL, p->pIsfOL );
00451         Bdc_IsfCopy( pIsfR, p->pIsfOR );
00452         return BDC_TYPE_OR;
00453     }
00454     return BDC_TYPE_AND;
00455 }

int Bdc_DecomposeUpdateRight ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf,
Bdc_Isf_t *  pIsfL,
Bdc_Isf_t *  pIsfR,
unsigned *  puTruth,
Bdc_Type_t  Type 
) [static]

Function*************************************************************

Synopsis [Updates the ISF of the right after the left was decompoosed.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file bdcDec.c.

00106 {
00107         if ( Type == BDC_TYPE_OR ) 
00108         {
00109 //              Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
00110 //              Right.R = bdd_exist( R, setRightRes );
00111 
00112 //              if ( pR->Q )  Cudd_RecursiveDeref( dd, pR->Q );
00113 //              if ( pR->R )  Cudd_RecursiveDeref( dd, pR->R );
00114 //              pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Cudd_Not(CompSpecF), pL->V );   Cudd_Ref( pR->Q );
00115 //              pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V );                      Cudd_Ref( pR->R );
00116 
00117 //              assert( pR->R != b0 );
00118 //              return (int)( pR->Q == b0 );
00119 
00120         Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
00121         Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); 
00122         Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
00123         assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
00124         return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
00125         }
00126         else if ( Type == BDC_TYPE_AND )
00127         {
00128 //              Right.R = bdd_appex( R, CompSpecLeftF, bddop_and, setRightRes );
00129 //              Right.Q = bdd_exist( Q, setRightRes );
00130 
00131 //              if ( pR->Q )  Cudd_RecursiveDeref( dd, pR->Q );
00132 //              if ( pR->R )  Cudd_RecursiveDeref( dd, pR->R );
00133 //              pR->R = Cudd_bddAndAbstract( dd, pF->R, CompSpecF, pL->V );                 Cudd_Ref( pR->R );
00134 //              pR->Q = Cudd_bddExistAbstract( dd, pF->Q, pL->V );                      Cudd_Ref( pR->Q );
00135 
00136 //              assert( pR->Q != b0 );
00137 //              return (int)( pR->R == b0 );
00138 
00139         Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
00140         Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); 
00141         Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
00142         assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
00143         return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
00144         }
00145         return 0;
00146 }

int Bdc_DecomposeWeakOr ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf,
Bdc_Isf_t *  pIsfL,
Bdc_Isf_t *  pIsfR 
)

Function*************************************************************

Synopsis [Checks existence of weak OR-bidecomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 226 of file bdcDec.c.

00227 {
00228         int v, VarCost, VarBest, Cost, VarCostBest = 0;
00229 
00230     for ( v = 0; v < p->nVars; v++ )
00231         {
00232         Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
00233 //              if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
00234 //              Exist = Cudd_bddExistAbstract( dd, pF->R, Var );   Cudd_Ref( Exist );
00235 //              if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
00236         if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
00237                 {
00238                         // measure the cost of this variable
00239 //                      VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
00240 
00241 //                      Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var );   Cudd_Ref( Univ );
00242 //                      VarCost = Kit_TruthCountOnes( Univ, p->nVars );
00243 //                      Cudd_RecursiveDeref( dd, Univ );
00244 
00245             Kit_TruthForallNew( p->puTemp2, pIsf->puOn, p->nVars, v );
00246             VarCost = Kit_TruthCountOnes( p->puTemp2, p->nVars );
00247                         if ( VarCost == 0 )
00248                                 VarCost = 1;
00249                         if ( VarCostBest < VarCost )
00250                         {
00251                                 VarCostBest = VarCost;
00252                                 VarBest = v;
00253                         }
00254                 }
00255         }
00256 
00257         // derive the components for weak-bi-decomposition if the variable is found
00258         if ( VarCostBest )
00259         {
00260 //              funQLeftRes = Q & bdd_exist( R, setRightORweak );
00261 
00262 //              Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest );     Cudd_Ref( Temp );
00263 //              pL->Q = Cudd_bddAnd( dd, pF->Q, Temp );                         Cudd_Ref( pL->Q );
00264 //              Cudd_RecursiveDeref( dd, Temp );
00265 
00266         Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, VarBest );
00267         Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
00268 
00269 //              pL->R = pF->R;                                              Cudd_Ref( pL->R );
00270 //              pL->V = VarBest;                                        Cudd_Ref( pL->V );
00271         Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
00272         pIsfL->Var = VarBest;
00273 
00274 //              assert( pL->Q != b0 );
00275 //              assert( pL->R != b0 );
00276 //              assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
00277 
00278                 // express cost in percents of the covered boolean space
00279                 Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
00280                 if ( Cost == 0 )
00281                         Cost = 1;
00282         return Cost;
00283         }
00284     return 0;
00285 }

Bdc_Fun_t* Bdc_ManDecompose_rec ( Bdc_Man_t *  p,
Bdc_Isf_t *  pIsf 
)

FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Performs one step of bi-decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file bdcDec.c.

00046 {
00047     Bdc_Fun_t * pFunc;
00048     Bdc_Isf_t IsfL, * pIsfL = &IsfL;
00049     Bdc_Isf_t IsfB, * pIsfR = &IsfB;
00050     // check computed results
00051     if ( pFunc = Bdc_TableLookup( p, pIsf ) )
00052         return pFunc;
00053     // decide on the decomposition type
00054     pFunc = Bdc_FunNew( p );
00055     if ( pFunc == NULL )
00056         return NULL;
00057     pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
00058     // decompose the left branch
00059     pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL );
00060     if ( pFunc->pFan0 == NULL )
00061         return NULL;
00062     // decompose the right branch
00063     if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) )
00064     {
00065         p->nNodes--;
00066         return pFunc->pFan0;
00067     }
00068     pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL );
00069     if ( pFunc->pFan1 == NULL )
00070         return NULL;
00071     // compute the function of node
00072     pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
00073     if ( pFunc->Type == BDC_TYPE_AND )
00074         Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
00075     else if ( pFunc->Type == BDC_TYPE_OR )
00076         Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
00077     else 
00078         assert( 0 );
00079     // verify correctness
00080     assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) );
00081     // convert from OR to AND
00082     if ( pFunc->Type == BDC_TYPE_OR )
00083     {
00084         pFunc->Type = BDC_TYPE_AND;
00085         pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
00086         pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
00087         Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
00088         pFunc = Bdc_Not(pFunc);
00089     }
00090     Bdc_TableAdd( p, Bdc_Regular(pFunc) );
00091     return pFunc;
00092 }

Generated on Tue Jan 5 12:18:13 2010 for abc70930 by  doxygen 1.6.1