From e54d9691616b9a0326e2fdb3156bb4eeb8abfcd7 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 30 Sep 2007 08:01:00 -0700 Subject: Version abc70930 --- src/aig/fra/fraCore.c | 428 -------------------------------------------------- 1 file changed, 428 deletions(-) delete mode 100644 src/aig/fra/fraCore.c (limited to 'src/aig/fra/fraCore.c') diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c deleted file mode 100644 index b390edbe..00000000 --- a/src/aig/fra/fraCore.c +++ /dev/null @@ -1,428 +0,0 @@ -/**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 $] - -***********************************************************************/ - -#include "fra.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/* - Speculating reduction in the sequential case leads to an interesting - situation when a counter-ex may not refine any classes. This happens - for non-constant equivalence classes. In such cases the representative - of the class (proved by simulation to be non-constant) may be reduced - to a constant during the speculative reduction. The fraig-representative - of this representative node is a constant node, even though this is a - non-constant class. Experiments have shown that this situation happens - very often at the beginning of the refinement iteration when there are - many spurious candidate equivalence classes (especially if heavy-duty - simulatation of BMC was node used at the beginning). As a result, the - SAT solver run may return a counter-ex that distinguishes the given - representative node from the constant-1 node but this counter-ex - does not distinguish the nodes in the non-costant class... This is why - there is no check of refinment after a counter-ex in the sequential case. -*/ - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Reports the status of the miter.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Fra_FraigMiterStatus( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj, * pObjNew; - int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0; - if ( p->pData ) - return 0; - Aig_ManForEachPoSeq( p, pObj, i ) - { - pObjNew = Aig_ObjChild0(pObj); - // check if the output is constant 0 - if ( pObjNew == Aig_ManConst0(p) ) - { - CountConst0++; - continue; - } - // check if the output is constant 1 - if ( pObjNew == Aig_ManConst1(p) ) - { - CountNonConst0++; - continue; - } - // check if the output can be constant 0 - if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) ) - { - CountNonConst0++; - continue; - } - CountUndecided++; - } -/* - if ( p->pParams->fVerbose ) - { - printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) ); - printf( "Const0 = %d. ", CountConst0 ); - printf( "NonConst0 = %d. ", CountNonConst0 ); - printf( "Undecided = %d. ", CountUndecided ); - printf( "\n" ); - } -*/ - if ( CountNonConst0 ) - return 0; - if ( CountUndecided ) - return -1; - return 1; -} - -/**Function************************************************************* - - Synopsis [Write speculative miter for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) -{ - static int Counter = 0; - char FileName[20]; - Aig_Man_t * pTemp; - Aig_Obj_t * pNode; - int i; - // create manager with the logic for these two nodes - pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig ); - // dump the logic into a file - sprintf( FileName, "aig\\%03d.blif", ++Counter ); - Aig_ManDumpBlif( pTemp, FileName ); - printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName ); - // clean up - Aig_ManStop( pTemp ); - Aig_ManForEachObj( p->pManFraig, pNode, i ) - pNode->pData = p; -} - -/**Function************************************************************* - - Synopsis [Verifies the generated counter-ex.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex ) -{ - Aig_Obj_t * pObj, ** ppClass; - int i, c; - assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) ); - // make sure the input pattern is not used - Aig_ManForEachObj( p->pManAig, pObj, i ) - assert( !pObj->fMarkB ); - // simulate the cex through the AIG - Aig_ManConst1(p->pManAig)->fMarkB = 1; - Aig_ManForEachPi( p->pManAig, pObj, i ) - pObj->fMarkB = Vec_IntEntry(vCex, i); - Aig_ManForEachNode( p->pManAig, pObj, i ) - pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & - (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj)); - Aig_ManForEachPo( p->pManAig, pObj, i ) - pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj); - // check if the classes hold - Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i ) - { - if ( pObj->fPhase != pObj->fMarkB ) - printf( "The node %d is not constant under cex!\n", pObj->Id ); - } - Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i ) - { - for ( c = 1; ppClass[c]; c++ ) - if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) ) - printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id ); -// for ( c = 0; ppClass[c]; c++ ) -// if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) ) -// printf( "A member of non-constant class has a constant repr!\n" ); - } - // clean the simulation pattern - Aig_ManForEachObj( p->pManAig, pObj, i ) - pObj->fMarkB = 0; -} - -/**Function************************************************************* - - Synopsis [Performs fraiging for one node.] - - Description [Returns the fraiged node.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) -{ - Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; - int RetValue; - assert( !Aig_IsComplement(pObj) ); - // get representative of this class - pObjRepr = Fra_ClassObjRepr( pObj ); - if ( pObjRepr == NULL || // this is a unique node - (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node - return; - // get the fraiged node - pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK ); - // get the fraiged representative - pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK ); - // if the fraiged nodes are the same, return - if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) ) - { - p->nSatCallsSkipped++; - return; - } - assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) ); - // if they are proved different, the c-ex will be in p->pPatWords - RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); - if ( RetValue == 1 ) // proved equivalent - { -// if ( p->pPars->fChoicing ) -// Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) ); - // the nodes proved equal - pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); - Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 ); - return; - } - if ( RetValue == -1 ) // failed - { - if ( p->vTimeouts == NULL ) - p->vTimeouts = Vec_PtrAlloc( 100 ); - Vec_PtrPush( p->vTimeouts, pObj ); - if ( !p->pPars->fSpeculate ) - return; - assert( 0 ); - // speculate - p->nSpeculs++; - pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); - Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 ); - Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) ); - return; - } - // disprove the nodes - p->pCla->fRefinement = 1; - // if we do not include the node into those disproved, we may end up - // merging this node with another representative, for which proof has timed out - if ( p->vTimeouts ) - Vec_PtrPush( p->vTimeouts, pObj ); - // verify that the counter-example satisfies all the constraints -// if ( p->vCex ) -// Fra_FraigVerifyCounterEx( p, p->vCex ); - // simulate the counter-example and return the Fraig node - Fra_SmlResimulate( p ); - if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr ) - printf( "Fra_FraigNode(): Error in class refinement!\n" ); - assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr ); -} - -/**Function************************************************************* - - Synopsis [Performs fraiging for the internal nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Fra_FraigSweep( Fra_Man_t * p ) -{ - Bar_Progress_t * pProgress; - Aig_Obj_t * pObj, * pObjNew; - int i, k = 0, Pos = 0; - // fraig latch outputs - Aig_ManForEachLoSeq( p->pManAig, pObj, i ) - { - Fra_FraigNode( p, pObj ); - if ( p->pPars->fUseImps ) - Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos ); - } - if ( p->pPars->fLatchCorr ) - return; - // fraig internal nodes - pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) ); - Aig_ManForEachNode( p->pManAig, pObj, i ) - { - Bar_ProgressUpdate( pProgress, i, NULL ); - // derive and remember the new fraig node - pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) ); - Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew ); - Aig_Regular(pObjNew)->pData = p; - // quit if simulation detected a counter-example for a PO - if ( p->pManFraig->pData ) - continue; - // perform fraiging - Fra_FraigNode( p, pObj ); - if ( p->pPars->fUseImps ) - Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos ); - } - Bar_ProgressStop( pProgress ); - // try to prove the outputs of the miter - p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); -// Fra_MiterStatus( p->pManFraig ); -// if ( p->pPars->fProve && p->pManFraig->pData == NULL ) -// Fra_MiterProve( p ); - // compress implications after processing all of them - if ( p->pPars->fUseImps ) - Fra_ImpCompactArray( p->pCla->vImps ); -} - -/**Function************************************************************* - - Synopsis [Performs fraiging of the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ) -{ - Fra_Man_t * p; - Aig_Man_t * pManAigNew; - int clk; - if ( Aig_ManNodeNum(pManAig) == 0 ) - return Aig_ManDup(pManAig, 1); -clk = clock(); - assert( Aig_ManLatchNum(pManAig) == 0 ); - p = Fra_ManStart( pManAig, pPars ); - p->pManFraig = Fra_ManPrepareComb( p ); - p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords ); - Fra_SmlSimulate( p, 0 ); -// if ( p->pPars->fChoicing ) -// Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) ); - // collect initial states - p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); - p->nNodesBeg = Aig_ManNodeNum(pManAig); - p->nRegsBeg = Aig_ManRegNum(pManAig); - // perform fraig sweep - Fra_FraigSweep( p ); - // call back the procedure to check implications - if ( pManAig->pImpFunc ) - pManAig->pImpFunc( p, pManAig->pImpData ); - // finalize the fraiged manager - Fra_ManFinalizeComb( p ); - if ( p->pPars->fChoicing ) - { -int clk2 = clock(); - Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - pManAigNew = Aig_ManDupRepr( p->pManAig, 1 ); - Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) ); - Aig_ManTransferRepr( pManAigNew, p->pManAig ); - Aig_ManMarkValidChoices( pManAigNew ); - Aig_ManStop( p->pManFraig ); - p->pManFraig = NULL; -p->timeTrav += clock() - clk2; - } - else - { - Aig_ManCleanup( p->pManFraig ); - pManAigNew = p->pManFraig; - p->pManFraig = NULL; - } -p->timeTotal = clock() - clk; - // collect final stats - p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); - p->nNodesEnd = Aig_ManNodeNum(pManAigNew); - p->nRegsEnd = Aig_ManRegNum(pManAigNew); - Fra_ManStop( p ); - return pManAigNew; -} - -/**Function************************************************************* - - Synopsis [Performs choicing of the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ) -{ - Fra_Par_t Pars, * pPars = &Pars; - Fra_ParamsDefault( pPars ); - pPars->nBTLimitNode = nConfMax; - pPars->fChoicing = 1; - pPars->fDoSparse = 1; - pPars->fSpeculate = 0; - pPars->fProve = 0; - pPars->fVerbose = 0; - return Fra_FraigPerform( pManAig, pPars ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ) -{ - Aig_Man_t * pFraig; - Fra_Par_t Pars, * pPars = &Pars; - Fra_ParamsDefault( pPars ); - pPars->nBTLimitNode = nConfMax; - pPars->fChoicing = 0; - pPars->fDoSparse = 1; - pPars->fSpeculate = 0; - pPars->fProve = 0; - pPars->fVerbose = 0; - pFraig = Fra_FraigPerform( pManAig, pPars ); - return pFraig; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -- cgit v1.2.3