diff options
Diffstat (limited to 'src/aig/fra/fraInd.c')
| -rw-r--r-- | src/aig/fra/fraInd.c | 205 |
1 files changed, 205 insertions, 0 deletions
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c new file mode 100644 index 00000000..1bfe1cb4 --- /dev/null +++ b/src/aig/fra/fraInd.c @@ -0,0 +1,205 @@ +/**CFile**************************************************************** + + FileName [fraInd.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [New FRAIG package.] + + Synopsis [Inductive prover.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 30, 2007.] + + Revision [$Id: fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "fra.h" +#include "cnf.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prepares the inductive case with speculative reduction.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) +{ + Aig_Man_t * pManFraig; + Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter; + Aig_Obj_t ** pLatches; + int i, k, f; + assert( p->pManFraig == NULL ); + assert( Aig_ManInitNum(p->pManAig) > 0 ); + assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); + + // start the fraig package + pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames ); + pManFraig->vInits = Vec_IntDup(p->pManAig->vInits); + // create PI nodes for the frames + for ( f = 0; f < p->nFrames; f++ ) + { + Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) ); + Aig_ManForEachPiSeq( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) ); + } + // create latches for the first frame + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); + + // add timeframes + pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) ); + for ( f = 0; f < p->nFrames - 1; f++ ) + { + // add internal nodes of this frame + Aig_ManForEachNode( p->pManAig, pObj, i ) + { + pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) ); + Fra_ObjSetFraig( pObj, f, pObjNew ); + // skip nodes without representative + if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL ) + continue; + assert( pObjRepr->Id < pObj->Id ); + // get the new node of the representative + pObjReprNew = Fra_ObjFraig( pObjRepr, f ); + // if this is the same node, no need to add constraints + if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) ) + continue; + // these are different nodes + // perform speculative reduction + Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) ); + // add the constraint + pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew ); + pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) ); + Aig_ObjCreatePo( pManFraig, pMiter ); + } + // save the latch input values + k = 0; + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + pLatches[k++] = Fra_ObjChild0Fra(pObj,f); + assert( k == Aig_ManInitNum(p->pManAig) ); + // insert them to the latch output values + k = 0; + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, f+1, pLatches[k++] ); + assert( k == Aig_ManInitNum(p->pManAig) ); + } + free( pLatches ); + // mark the asserts + pManFraig->nAsserts = Aig_ManPoNum(pManFraig); + // add the POs for the latch inputs + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) ); + + // set the pointer to the manager + Aig_ManForEachObj( p->pManAig, pObj, i ) + pObj->pData = p; + // set the pointers to the manager + Aig_ManForEachObj( pManFraig, pObj, i ) + pObj->pData = p; + // make sure the satisfying assignment is node assigned + assert( pManFraig->pData == NULL ); + return pManFraig; +} + +/**Function************************************************************* + + Synopsis [Performs choicing of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose ) +{ + Fra_Man_t * p; + Fra_Par_t Pars, * pPars = &Pars; + Aig_Obj_t * pObj; + Cnf_Dat_t * pCnf; + Aig_Man_t * pManAigNew; + int nIter, i; + + if ( Aig_ManNodeNum(pManAig) == 0 ) + return Aig_ManDup(pManAig, 1); + assert( Aig_ManLatchNum(pManAig) == 0 ); + assert( Aig_ManInitNum(pManAig) > 0 ); + + // get parameters + Fra_ParamsDefaultSeq( pPars ); + pPars->nTimeFrames = nFrames; + pPars->fVerbose = fVerbose; + + // start the fraig manager for this run + p = Fra_ManStart( pManAig, pPars ); + // derive and refine e-classes using the 1st init frame + Fra_Simulate( p, 1 ); + + // refine e-classes using sequential simulation + + // iterate the inductive case + p->pCla->fRefinement = 1; + for ( nIter = 0; p->pCla->fRefinement; nIter++ ) + { + // mark the classes as non-refined + p->pCla->fRefinement = 0; + // derive non-init K-timeframes while implementing e-classes + p->pManFraig = Fra_FramesWithClasses( p ); + if ( fVerbose ) + printf( "Iter = %3d. Original = %6d. Reduced = %6d.\n", + nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts ); + + // perform AIG rewriting on the speculated frames + + // convert the manager to SAT solver (the last nLatches outputs are inputs) + pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) ); + p->pSat = Cnf_DataWriteIntoSolver( pCnf ); + // transfer variable numbers + Aig_ManForEachPi( p->pManAig, pObj, i ) + Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); + Aig_ManForEachLiSeq( p->pManAig, pObj, i ) + { + Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); + Fra_ObjSetFaninVec( pObj, (void *)1 ); + } + Cnf_DataFree( pCnf ); + + // perform sweeping + Fra_FraigSweep( p ); + assert( Vec_PtrSize(p->vTimeouts) == 0 ); + Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; + sat_solver_delete( p->pSat ); p->pSat = NULL; + } + + // move the classes into representatives + Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); + // implement the classes + pManAigNew = Aig_ManDupRepr( pManAig ); + Fra_ManStop( p ); + return pManAigNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |