src/aig/fra/fraBmc.c File Reference

#include "fra.h"
Include dependency graph for fraBmc.c:

Go to the source code of this file.

Data Structures

struct  Fra_Bmc_t_

Functions

static Aig_Obj_t * Bmc_ObjFrames (Aig_Obj_t *pObj, int i)
static void Bmc_ObjSetFrames (Aig_Obj_t *pObj, int i, Aig_Obj_t *pNode)
static Aig_Obj_t * Bmc_ObjFraig (Aig_Obj_t *pObj)
static void Bmc_ObjSetFraig (Aig_Obj_t *pObj, Aig_Obj_t *pNode)
static Aig_Obj_t * Bmc_ObjChild0Frames (Aig_Obj_t *pObj, int i)
static Aig_Obj_t * Bmc_ObjChild1Frames (Aig_Obj_t *pObj, int i)
int Fra_BmcNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
int Fra_BmcNodeIsConst (Aig_Obj_t *pObj)
void Fra_BmcFilterImplications (Fra_Man_t *p, Fra_Bmc_t *pBmc)
Fra_Bmc_t * Fra_BmcStart (Aig_Man_t *pAig, int nPref, int nDepth)
void Fra_BmcStop (Fra_Bmc_t *p)
Aig_Man_t * Fra_BmcFrames (Fra_Bmc_t *p)
void Fra_BmcPerform (Fra_Man_t *p, int nPref, int nDepth)

Function Documentation

static Aig_Obj_t* Bmc_ObjChild0Frames ( Aig_Obj_t *  pObj,
int  i 
) [inline, static]

Definition at line 51 of file fraBmc.c.

00051 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }

static Aig_Obj_t* Bmc_ObjChild1Frames ( Aig_Obj_t *  pObj,
int  i 
) [inline, static]

Definition at line 52 of file fraBmc.c.

00052 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }

static Aig_Obj_t* Bmc_ObjFraig ( Aig_Obj_t *  pObj  )  [inline, static]

Definition at line 48 of file fraBmc.c.

00048 { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id];  }

static Aig_Obj_t* Bmc_ObjFrames ( Aig_Obj_t *  pObj,
int  i 
) [inline, static]

Definition at line 45 of file fraBmc.c.

00045 { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i];  }

static void Bmc_ObjSetFraig ( Aig_Obj_t *  pObj,
Aig_Obj_t *  pNode 
) [inline, static]

Definition at line 49 of file fraBmc.c.

00049 { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; }

static void Bmc_ObjSetFrames ( Aig_Obj_t *  pObj,
int  i,
Aig_Obj_t *  pNode 
) [inline, static]

Definition at line 46 of file fraBmc.c.

00046 { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; }

void Fra_BmcFilterImplications ( Fra_Man_t *  p,
Fra_Bmc_t *  pBmc 
)

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

Synopsis [Refines implications using BMC.]

Description [The input is the combinational FRAIG manager, which is used to FRAIG the timeframes. ]

SideEffects []

SeeAlso []

Definition at line 118 of file fraBmc.c.

00119 {
00120     Aig_Obj_t * pLeft, * pRight;
00121     Aig_Obj_t * pLeftT, * pRightT;
00122     Aig_Obj_t * pLeftF, * pRightF;
00123     int i, f, Imp, Left, Right;
00124     int fComplL, fComplR;
00125     assert( p->nFramesAll == 1 );
00126     assert( p->pManAig == pBmc->pAigFrames );
00127     Vec_IntForEachEntry( pBmc->vImps, Imp, i )
00128     {
00129         if ( Imp == 0 )
00130             continue;
00131         Left  = Fra_ImpLeft(Imp);
00132         Right = Fra_ImpRight(Imp);
00133         // get the corresponding nodes
00134         pLeft  = Aig_ManObj( pBmc->pAig, Left );
00135         pRight = Aig_ManObj( pBmc->pAig, Right );
00136         // iterate through the timeframes
00137         for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
00138         {
00139             // get timeframe nodes
00140             pLeftT  = Bmc_ObjFrames( pLeft, f );
00141             pRightT = Bmc_ObjFrames( pRight, f );
00142             // get the corresponding FRAIG nodes
00143             pLeftF  = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
00144             pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
00145             // get the complemented attributes
00146             fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
00147             fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
00148             // check equality
00149             if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
00150             {
00151                 if ( fComplL == fComplR ) // x => x  - always true
00152                     continue;
00153                 assert( fComplL != fComplR );
00154                 // consider 4 possibilities:
00155                 // NOT(1) => 1    or   0 => 1  - always true
00156                 // 1 => NOT(1)    or   1 => 0  - never true
00157                 // NOT(x) => x    or   x       - not always true
00158                 // x => NOT(x)    or   NOT(x)  - not always true
00159                 if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
00160                     continue;
00161                 // disproved implication
00162                 Vec_IntWriteEntry( pBmc->vImps, i, 0 ); 
00163                 break;
00164             }
00165             // check the implication 
00166             if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
00167             {
00168                 Vec_IntWriteEntry( pBmc->vImps, i, 0 );
00169                 break;
00170             }
00171         }
00172     }
00173     Fra_ImpCompactArray( pBmc->vImps );
00174 }

Aig_Man_t* Fra_BmcFrames ( Fra_Bmc_t *  p  ) 

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

Synopsis [Constructs initialized timeframes of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file fraBmc.c.

00234 {
00235     Aig_Man_t * pAigFrames;
00236     Aig_Obj_t * pObj, * pObjNew;
00237     Aig_Obj_t ** pLatches;
00238     int i, k, f;
00239 
00240     // start the fraig package
00241     pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
00242     pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
00243     // create PI nodes for the frames
00244     for ( f = 0; f < p->nFramesAll; f++ )
00245         Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
00246     for ( f = 0; f < p->nFramesAll; f++ )
00247         Aig_ManForEachPiSeq( p->pAig, pObj, i )
00248             Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) );
00249     // set initial state for the latches
00250     Aig_ManForEachLoSeq( p->pAig, pObj, i )
00251         Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
00252 
00253     // add timeframes
00254     pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
00255     for ( f = 0; f < p->nFramesAll; f++ )
00256     {
00257         // add internal nodes of this frame
00258         Aig_ManForEachNode( p->pAig, pObj, i )
00259         {
00260             pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) );
00261             Bmc_ObjSetFrames( pObj, f, pObjNew );
00262         }
00263         if ( f == p->nFramesAll - 1 )
00264             break;
00265         // save the latch input values
00266         k = 0;
00267         Aig_ManForEachLiSeq( p->pAig, pObj, i )
00268             pLatches[k++] = Bmc_ObjChild0Frames(pObj,f);
00269         assert( k == Aig_ManRegNum(p->pAig) );
00270         // insert them to the latch output values
00271         k = 0;
00272         Aig_ManForEachLoSeq( p->pAig, pObj, i )
00273             Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
00274         assert( k == Aig_ManRegNum(p->pAig) );
00275     }
00276     free( pLatches );
00277     // add POs to all the dangling nodes
00278     Aig_ManForEachObj( pAigFrames, pObjNew, i )
00279         if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
00280             Aig_ObjCreatePo( pAigFrames, pObjNew );
00281 
00282     // return the new manager
00283     return pAigFrames;
00284 }

int Fra_BmcNodeIsConst ( Aig_Obj_t *  pObj  ) 

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

Synopsis [Returns 1 if the node is costant.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file fraBmc.c.

00101 {
00102     Fra_Man_t * p = pObj->pData;
00103     return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
00104 }

int Fra_BmcNodesAreEqual ( Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Returns 1 if the nodes are equivalent.]

Description []

SideEffects []

SeeAlso []

Definition at line 69 of file fraBmc.c.

00070 {
00071     Fra_Man_t * p = pObj0->pData;
00072     Aig_Obj_t * pObjFrames0, * pObjFrames1;
00073     Aig_Obj_t * pObjFraig0, * pObjFraig1;
00074     int i;
00075     for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
00076     {
00077         pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
00078         pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
00079         if ( pObjFrames0 == pObjFrames1 )
00080             continue;
00081         pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
00082         pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
00083         if ( pObjFraig0 != pObjFraig1 )
00084             return 0;
00085     }
00086     return 1;
00087 }

void Fra_BmcPerform ( Fra_Man_t *  p,
int  nPref,
int  nDepth 
)

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

Synopsis [Performs BMC for the given AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file fraBmc.c.

00298 {
00299     Aig_Obj_t * pObj;
00300     int i, nImpsOld, clk = clock();
00301     assert( p->pBmc == NULL );
00302     // derive and fraig the frames
00303     p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
00304     p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
00305     // if implications are present, configure the AIG manager to check them
00306     if ( p->pCla->vImps )
00307     {
00308         p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications;
00309         p->pBmc->pAigFrames->pImpData = p->pBmc;
00310         p->pBmc->vImps = p->pCla->vImps;
00311         nImpsOld = Vec_IntSize(p->pCla->vImps);
00312     } 
00313     p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
00314     p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
00315     p->pBmc->pAigFrames->pObjCopies = NULL;
00316     // annotate frames nodes with pointers to the manager
00317     Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
00318         pObj->pData = p;
00319     // report the results
00320     if ( p->pPars->fVerbose )
00321     {
00322         printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
00323             Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
00324             Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
00325         PRT( "Time", clock() - clk );
00326         printf( "Before BMC: " );  
00327 //        Fra_ClassesPrint( p->pCla, 0 );
00328         printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
00329             Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
00330         if ( p->pCla->vImps )
00331             printf( "Imp = %5d. ", nImpsOld );
00332         printf( "\n" );
00333     }
00334     // refine the classes
00335     p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
00336     p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
00337     Fra_ClassesRefine( p->pCla );
00338     Fra_ClassesRefine1( p->pCla, 1, NULL );
00339     p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
00340     p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
00341     // report the results
00342     if ( p->pPars->fVerbose )
00343     {
00344         printf( "After  BMC: " );  
00345 //        Fra_ClassesPrint( p->pCla, 0 );
00346         printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
00347             Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
00348         if ( p->pCla->vImps )
00349             printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
00350         printf( "\n" );
00351     }
00352     // free the BMC manager
00353     Fra_BmcStop( p->pBmc );  
00354     p->pBmc = NULL;
00355 }

Fra_Bmc_t* Fra_BmcStart ( Aig_Man_t *  pAig,
int  nPref,
int  nDepth 
)

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

Synopsis [Starts the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 188 of file fraBmc.c.

00189 {
00190     Fra_Bmc_t * p;
00191     p = ALLOC( Fra_Bmc_t, 1 );
00192     memset( p, 0, sizeof(Fra_Bmc_t) );
00193     p->pAig = pAig;
00194     p->nPref = nPref;
00195     p->nDepth = nDepth;
00196     p->nFramesAll = nPref + nDepth;
00197     p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
00198     memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
00199     return p;
00200 }

void Fra_BmcStop ( Fra_Bmc_t *  p  ) 

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

Synopsis [Stops the BMC manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file fraBmc.c.

00214 {
00215     Aig_ManStop( p->pAigFrames );
00216     Aig_ManStop( p->pAigFraig );
00217     free( p->pObjToFrames );
00218     free( p->pObjToFraig );
00219     free( p );
00220 }

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