src/aig/fra/fraCore.c File Reference

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

Go to the source code of this file.

Functions

int Fra_FraigMiterStatus (Aig_Man_t *p)
static void Fra_FraigNodeSpeculate (Fra_Man_t *p, Aig_Obj_t *pObj, Aig_Obj_t *pObjFraig, Aig_Obj_t *pObjReprFraig)
void Fra_FraigVerifyCounterEx (Fra_Man_t *p, Vec_Int_t *vCex)
static void Fra_FraigNode (Fra_Man_t *p, Aig_Obj_t *pObj)
void Fra_FraigSweep (Fra_Man_t *p)
Aig_Man_t * Fra_FraigPerform (Aig_Man_t *pManAig, Fra_Par_t *pPars)
Aig_Man_t * Fra_FraigChoice (Aig_Man_t *pManAig, int nConfMax)
Aig_Man_t * Fra_FraigEquivence (Aig_Man_t *pManAig, int nConfMax)

Function Documentation

Aig_Man_t* Fra_FraigChoice ( Aig_Man_t *  pManAig,
int  nConfMax 
)

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

Synopsis [Performs choicing of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 385 of file fraCore.c.

00386 {
00387     Fra_Par_t Pars, * pPars = &Pars; 
00388     Fra_ParamsDefault( pPars );
00389     pPars->nBTLimitNode = nConfMax;
00390     pPars->fChoicing    = 1;
00391     pPars->fDoSparse    = 1;
00392     pPars->fSpeculate   = 0;
00393     pPars->fProve       = 0;
00394     pPars->fVerbose     = 0;
00395     return Fra_FraigPerform( pManAig, pPars );
00396 }

Aig_Man_t* Fra_FraigEquivence ( Aig_Man_t *  pManAig,
int  nConfMax 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file fraCore.c.

00410 {
00411     Aig_Man_t * pFraig;
00412     Fra_Par_t Pars, * pPars = &Pars; 
00413     Fra_ParamsDefault( pPars );
00414     pPars->nBTLimitNode = nConfMax;
00415     pPars->fChoicing    = 0;
00416     pPars->fDoSparse    = 1;
00417     pPars->fSpeculate   = 0;
00418     pPars->fProve       = 0;
00419     pPars->fVerbose     = 0;
00420     pFraig = Fra_FraigPerform( pManAig, pPars );
00421     return pFraig;
00422 }

int Fra_FraigMiterStatus ( Aig_Man_t *  p  ) 

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

FileName [fraCore.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id
fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

] DECLARATIONS /// FUNCTION DEFINITIONS ///Function*************************************************************

Synopsis [Reports the status of the miter.]

Description []

SideEffects []

SeeAlso []

Definition at line 59 of file fraCore.c.

00060 {
00061     Aig_Obj_t * pObj, * pObjNew;
00062     int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
00063     if ( p->pData )
00064         return 0;
00065     Aig_ManForEachPoSeq( p, pObj, i )
00066     {
00067         pObjNew = Aig_ObjChild0(pObj);
00068         // check if the output is constant 0
00069         if ( pObjNew == Aig_ManConst0(p) )
00070         {
00071             CountConst0++;
00072             continue;
00073         }
00074         // check if the output is constant 1
00075         if ( pObjNew == Aig_ManConst1(p) )
00076         {
00077             CountNonConst0++;
00078             continue;
00079         }
00080         // check if the output can be constant 0
00081         if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
00082         {
00083             CountNonConst0++;
00084             continue;
00085         }
00086         CountUndecided++;
00087     }
00088 /*
00089     if ( p->pParams->fVerbose )
00090     {
00091         printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
00092         printf( "Const0 = %d.  ", CountConst0 );
00093         printf( "NonConst0 = %d.  ", CountNonConst0 );
00094         printf( "Undecided = %d.  ", CountUndecided );
00095         printf( "\n" );
00096     }
00097 */
00098     if ( CountNonConst0 )
00099         return 0;
00100     if ( CountUndecided )
00101         return -1;
00102     return 1;
00103 }

static void Fra_FraigNode ( Fra_Man_t *  p,
Aig_Obj_t *  pObj 
) [inline, static]

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

Synopsis [Performs fraiging for one node.]

Description [Returns the fraiged node.]

SideEffects []

SeeAlso []

Definition at line 194 of file fraCore.c.

00195 { 
00196     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
00197     int RetValue;
00198     assert( !Aig_IsComplement(pObj) );
00199     // get representative of this class
00200     pObjRepr = Fra_ClassObjRepr( pObj );
00201     if ( pObjRepr == NULL || // this is a unique node
00202        (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
00203         return;
00204     // get the fraiged node
00205     pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK );
00206     // get the fraiged representative
00207     pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
00208     // if the fraiged nodes are the same, return
00209     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
00210     {
00211         p->nSatCallsSkipped++;
00212         return;
00213     }
00214     assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
00215     // if they are proved different, the c-ex will be in p->pPatWords
00216     RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
00217     if ( RetValue == 1 )  // proved equivalent
00218     {
00219 //        if ( p->pPars->fChoicing )
00220 //            Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
00221         // the nodes proved equal
00222         pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
00223         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
00224         return;
00225     }
00226     if ( RetValue == -1 ) // failed
00227     {
00228         if ( p->vTimeouts == NULL )
00229             p->vTimeouts = Vec_PtrAlloc( 100 );
00230         Vec_PtrPush( p->vTimeouts, pObj );
00231         if ( !p->pPars->fSpeculate )
00232             return;
00233         assert( 0 );
00234         // speculate
00235         p->nSpeculs++;
00236         pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
00237         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
00238         Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
00239         return;
00240     }
00241     // disprove the nodes
00242     p->pCla->fRefinement = 1;
00243     // if we do not include the node into those disproved, we may end up 
00244     // merging this node with another representative, for which proof has timed out
00245     if ( p->vTimeouts )
00246         Vec_PtrPush( p->vTimeouts, pObj );
00247     // verify that the counter-example satisfies all the constraints
00248 //    if ( p->vCex )
00249 //        Fra_FraigVerifyCounterEx( p, p->vCex );
00250     // simulate the counter-example and return the Fraig node
00251     Fra_SmlResimulate( p );
00252     if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
00253         printf( "Fra_FraigNode(): Error in class refinement!\n" );
00254     assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
00255 }

static void Fra_FraigNodeSpeculate ( Fra_Man_t *  p,
Aig_Obj_t *  pObj,
Aig_Obj_t *  pObjFraig,
Aig_Obj_t *  pObjReprFraig 
) [inline, static]

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

Synopsis [Write speculative miter for one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 116 of file fraCore.c.

00117 { 
00118     static int Counter = 0;
00119     char FileName[20];
00120     Aig_Man_t * pTemp;
00121     Aig_Obj_t * pNode;
00122     int i;
00123     // create manager with the logic for these two nodes
00124     pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
00125     // dump the logic into a file
00126     sprintf( FileName, "aig\\%03d.blif", ++Counter );
00127     Aig_ManDumpBlif( pTemp, FileName );
00128     printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
00129     // clean up
00130     Aig_ManStop( pTemp );
00131     Aig_ManForEachObj( p->pManFraig, pNode, i )
00132         pNode->pData = p;
00133 }

Aig_Man_t* Fra_FraigPerform ( Aig_Man_t *  pManAig,
Fra_Par_t *  pPars 
)

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

Synopsis [Performs fraiging of the AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 321 of file fraCore.c.

00322 {
00323     Fra_Man_t * p;
00324     Aig_Man_t * pManAigNew;
00325     int clk;
00326     if ( Aig_ManNodeNum(pManAig) == 0 )
00327         return Aig_ManDup(pManAig, 1);
00328 clk = clock();
00329     assert( Aig_ManLatchNum(pManAig) == 0 );
00330     p = Fra_ManStart( pManAig, pPars );
00331     p->pManFraig = Fra_ManPrepareComb( p );
00332     p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
00333     Fra_SmlSimulate( p, 0 );
00334 //    if ( p->pPars->fChoicing )
00335 //        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
00336     // collect initial states
00337     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
00338     p->nNodesBeg = Aig_ManNodeNum(pManAig);
00339     p->nRegsBeg  = Aig_ManRegNum(pManAig);
00340     // perform fraig sweep
00341     Fra_FraigSweep( p );
00342     // call back the procedure to check implications
00343     if ( pManAig->pImpFunc )
00344         pManAig->pImpFunc( p, pManAig->pImpData );
00345     // finalize the fraiged manager
00346     Fra_ManFinalizeComb( p );
00347     if ( p->pPars->fChoicing )
00348     {
00349 int clk2 = clock();
00350         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
00351         pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
00352         Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
00353         Aig_ManTransferRepr( pManAigNew, p->pManAig );
00354         Aig_ManMarkValidChoices( pManAigNew );
00355         Aig_ManStop( p->pManFraig );
00356         p->pManFraig = NULL;
00357 p->timeTrav += clock() - clk2;
00358     }
00359     else
00360     {
00361         Aig_ManCleanup( p->pManFraig );
00362         pManAigNew = p->pManFraig;
00363         p->pManFraig = NULL;
00364     }
00365 p->timeTotal = clock() - clk;
00366     // collect final stats
00367     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
00368     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
00369     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
00370     Fra_ManStop( p );
00371     return pManAigNew;
00372 }

void Fra_FraigSweep ( Fra_Man_t *  p  ) 

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

Synopsis [Performs fraiging for the internal nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 268 of file fraCore.c.

00269 {
00270     Bar_Progress_t * pProgress;
00271     Aig_Obj_t * pObj, * pObjNew;
00272     int i, k = 0, Pos = 0;
00273     // fraig latch outputs
00274     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
00275     {
00276         Fra_FraigNode( p, pObj );
00277         if ( p->pPars->fUseImps )
00278             Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
00279     }
00280     if ( p->pPars->fLatchCorr )
00281         return;
00282     // fraig internal nodes
00283     pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
00284     Aig_ManForEachNode( p->pManAig, pObj, i )
00285     {
00286         Bar_ProgressUpdate( pProgress, i, NULL );
00287         // derive and remember the new fraig node
00288         pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
00289         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
00290         Aig_Regular(pObjNew)->pData = p;
00291         // quit if simulation detected a counter-example for a PO
00292         if ( p->pManFraig->pData )
00293             continue;
00294         // perform fraiging
00295         Fra_FraigNode( p, pObj );
00296         if ( p->pPars->fUseImps )
00297             Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
00298     }
00299     Bar_ProgressStop( pProgress );
00300     // try to prove the outputs of the miter
00301     p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
00302 //    Fra_MiterStatus( p->pManFraig );
00303 //    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
00304 //        Fra_MiterProve( p );
00305     // compress implications after processing all of them
00306     if ( p->pPars->fUseImps )
00307         Fra_ImpCompactArray( p->pCla->vImps );
00308 }

void Fra_FraigVerifyCounterEx ( Fra_Man_t *  p,
Vec_Int_t *  vCex 
)

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

Synopsis [Verifies the generated counter-ex.]

Description []

SideEffects []

SeeAlso []

Definition at line 146 of file fraCore.c.

00147 {
00148     Aig_Obj_t * pObj, ** ppClass;
00149     int i, c;
00150     assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
00151     // make sure the input pattern is not used
00152     Aig_ManForEachObj( p->pManAig, pObj, i )
00153         assert( !pObj->fMarkB );
00154     // simulate the cex through the AIG
00155     Aig_ManConst1(p->pManAig)->fMarkB = 1;
00156     Aig_ManForEachPi( p->pManAig, pObj, i )
00157         pObj->fMarkB = Vec_IntEntry(vCex, i);
00158     Aig_ManForEachNode( p->pManAig, pObj, i )
00159         pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
00160                        (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
00161     Aig_ManForEachPo( p->pManAig, pObj, i )
00162         pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
00163     // check if the classes hold
00164     Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
00165     {
00166         if ( pObj->fPhase != pObj->fMarkB )
00167             printf( "The node %d is not constant under cex!\n", pObj->Id );
00168     }
00169     Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
00170     {
00171         for ( c = 1; ppClass[c]; c++ )
00172             if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
00173                 printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
00174 //        for ( c = 0; ppClass[c]; c++ )
00175 //            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
00176 //                printf( "A member of non-constant class has a constant repr!\n" );
00177     }
00178     // clean the simulation pattern
00179     Aig_ManForEachObj( p->pManAig, pObj, i )
00180         pObj->fMarkB = 0;
00181 }

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