summaryrefslogtreecommitdiffstats
path: root/src/aig/ssw/sswDyn.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-01-21 04:30:10 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-01-21 04:30:10 -0800
commit8014f25f6db719fa62336f997963532a14c568f6 (patch)
treec691ee91a3a2d452a2bd24ac89a8c717beaa7af7 /src/aig/ssw/sswDyn.c
parentc44cc5de9429e6b4f1c05045fcf43c9cb96437b5 (diff)
downloadabc-8014f25f6db719fa62336f997963532a14c568f6.tar.gz
abc-8014f25f6db719fa62336f997963532a14c568f6.tar.bz2
abc-8014f25f6db719fa62336f997963532a14c568f6.zip
Major restructuring of the code.
Diffstat (limited to 'src/aig/ssw/sswDyn.c')
-rw-r--r--src/aig/ssw/sswDyn.c489
1 files changed, 0 insertions, 489 deletions
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
deleted file mode 100644
index 7bdb2652..00000000
--- a/src/aig/ssw/sswDyn.c
+++ /dev/null
@@ -1,489 +0,0 @@
-/**CFile****************************************************************
-
- FileName [sswDyn.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Inductive prover with constraints.]
-
- Synopsis [Dynamic loading of constraints.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - September 1, 2008.]
-
- Revision [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sswInt.h"
-#include "bar.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Label PIs nodes of the frames corresponding to PIs of AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
-{
- Aig_Obj_t * pObj, * pObjFrames;
- int f, i;
- Aig_ManConst1( p->pFrames )->fMarkA = 1;
- Aig_ManConst1( p->pFrames )->fMarkB = 1;
- for ( f = 0; f < p->nFrames; f++ )
- {
- Saig_ManForEachPi( p->pAig, pObj, i )
- {
- pObjFrames = Ssw_ObjFrame( p, pObj, f );
- assert( Aig_ObjIsPi(pObjFrames) );
- assert( pObjFrames->fMarkB == 0 );
- pObjFrames->fMarkA = 1;
- pObjFrames->fMarkB = 1;
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects new POs in p->vNewPos.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
-{
- assert( !Aig_IsComplement(pObj) );
- if ( pObj->fMarkA )
- return;
- pObj->fMarkA = 1;
- if ( Aig_ObjIsPi(pObj) )
- {
- Vec_PtrPush( vNewPis, pObj );
- return;
- }
- assert( Aig_ObjIsNode(pObj) );
- Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
- Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
-}
-
-/**Function*************************************************************
-
- Synopsis [Collects new POs in p->vNewPos.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
-{
- Aig_Obj_t * pFanout;
- int iFanout = -1, i;
- assert( !Aig_IsComplement(pObj) );
- if ( pObj->fMarkB )
- return;
- pObj->fMarkB = 1;
- if ( pObj->Id > p->nSRMiterMaxId )
- return;
- if ( Aig_ObjIsPo(pObj) )
- {
- // skip if it is a register input PO
- if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
- return;
- // add the number of this constraint
- Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
- return;
- }
- // visit the fanouts
- assert( p->pFrames->pFanData != NULL );
- Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
- Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
-}
-
-/**Function*************************************************************
-
- Synopsis [Loads logic cones and relevant constraints.]
-
- Description [Both pRepr and pObj are objects of the AIG.
- The result is the current SAT solver loaded with the logic cones
- for pRepr and pObj corresponding to them in the frames,
- as well as all the relevant constraints.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
-{
- Aig_Obj_t * pObjFrames, * pReprFrames;
- Aig_Obj_t * pTemp, * pObj0, * pObj1;
- int i, iConstr, RetValue;
-
- assert( pRepr != pObj );
- // get the corresponding frames nodes
- pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
- pObjFrames = Aig_Regular( Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
- assert( pReprFrames != pObjFrames );
- /*
- // compute the AIG support
- Vec_PtrClear( p->vNewLos );
- Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
- Ssw_ManCollectPis_rec( pObj, p->vNewLos );
- // add logic cones for register outputs
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
- {
- pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
- Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
- }
-*/
- // add cones for the nodes
- Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
- Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
-
- // compute the frames support
- Vec_PtrClear( p->vNewLos );
- Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
- Ssw_ManCollectPis_rec( pObjFrames, p->vNewLos );
- // these nodes include both nodes corresponding to PIs and LOs
- // (the nodes corresponding to PIs should be labeled with fMarkB!)
-
- // collect the related constraint POs
- Vec_IntClear( p->vNewPos );
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vNewLos, pTemp, i )
- Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
- // check if the corresponding pairs are added
- Vec_IntForEachEntry( p->vNewPos, iConstr, i )
- {
- pObj0 = Aig_ManPo( p->pFrames, 2*iConstr );
- pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
-// if ( pObj0->fMarkB && pObj1->fMarkB )
- if ( pObj0->fMarkB || pObj1->fMarkB )
- {
- pObj0->fMarkB = 1;
- pObj1->fMarkB = 1;
- Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
- }
- }
- if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
- {
- RetValue = sat_solver_simplify(p->pMSat->pSat);
- assert( RetValue != 0 );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Tranfers simulation information from FRAIG to AIG.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
-{
- Aig_Obj_t * pObj, * pObjFraig;
- unsigned * pInfo;
- int i, f, nFrames;
-
- // transfer simulation information
- Aig_ManForEachPi( p->pAig, pObj, i )
- {
- pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
- if ( pObjFraig == Aig_ManConst0(p->pFrames) )
- {
- Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
- continue;
- }
- assert( !Aig_IsComplement(pObjFraig) );
- assert( Aig_ObjIsPi(pObjFraig) );
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
- Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
- }
- // set random simulation info for the second frame
- for ( f = 1; f < p->nFrames; f++ )
- {
- Saig_ManForEachPi( p->pAig, pObj, i )
- {
- pObjFraig = Ssw_ObjFrame( p, pObj, f );
- assert( !Aig_IsComplement(pObjFraig) );
- assert( Aig_ObjIsPi(pObjFraig) );
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
- Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
- }
- }
- // create random info
- nFrames = Ssw_SmlNumFrames( p->pSml );
- for ( ; f < nFrames; f++ )
- {
- Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs one round of simulation with counter-examples.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
-{
- int RetValue1, RetValue2, clk = clock();
- // transfer PI simulation information from storage
-// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
- Ssw_ManSweepTransferDyn( p );
- // simulate internal nodes
-// Ssw_SmlSimulateOneFrame( p->pSml );
- Ssw_SmlSimulateOne( p->pSml );
- // check equivalence classes
- RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
- RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
- // prepare simulation info for the next round
- Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
- p->nPatterns = 0;
- p->nSimRounds++;
-p->timeSimSat += clock() - clk;
- return RetValue1 > 0 || RetValue2 > 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs one round of simulation with counter-examples.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_ManSweepResimulateDynLocal( Ssw_Man_t * p, int f )
-{
- Aig_Obj_t * pObj, * pRepr, ** ppClass;
- int i, k, nSize, RetValue1, RetValue2, clk = clock();
- p->nSimRounds++;
- // transfer PI simulation information from storage
-// Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
- Ssw_ManSweepTransferDyn( p );
- // determine const1 cands and classes to be simulated
- Vec_PtrClear( p->vResimConsts );
- Vec_PtrClear( p->vResimClasses );
- Aig_ManIncrementTravId( p->pAig );
- for ( i = p->iNodeStart; i < p->iNodeLast + p->pPars->nResimDelta; i++ )
- {
- if ( i >= Aig_ManObjNumMax( p->pAig ) )
- break;
- pObj = Aig_ManObj( p->pAig, i );
- if ( pObj == NULL )
- continue;
- if ( Ssw_ObjIsConst1Cand(p->pAig, pObj) )
- {
- Vec_PtrPush( p->vResimConsts, pObj );
- continue;
- }
- pRepr = Aig_ObjRepr(p->pAig, pObj);
- if ( pRepr == NULL )
- continue;
- if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
- continue;
- Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
- Vec_PtrPush( p->vResimClasses, pRepr );
- }
- // simulate internal nodes
-// Ssw_SmlSimulateOneFrame( p->pSml );
-// Ssw_SmlSimulateOne( p->pSml );
- // resimulate dynamically
-// Aig_ManIncrementTravId( p->pAig );
-// Aig_ObjIsTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
- p->nVisCounter++;
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimConsts, pObj, i )
- Ssw_SmlSimulateOneDyn_rec( p->pSml, pObj, p->nFrames-1, p->pVisited, p->nVisCounter );
- // resimulate the cone of influence of the cand classes
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
- {
- ppClass = Ssw_ClassesReadClass( p->ppClasses, pRepr, &nSize );
- for ( k = 0; k < nSize; k++ )
- Ssw_SmlSimulateOneDyn_rec( p->pSml, ppClass[k], p->nFrames-1, p->pVisited, p->nVisCounter );
- }
-
- // check equivalence classes
-// RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
-// RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
- // refine these nodes
- RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vResimConsts, 1 );
- RetValue2 = 0;
- Vec_PtrForEachEntry( Aig_Obj_t *, p->vResimClasses, pRepr, i )
- RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRepr, 1 );
-
- // prepare simulation info for the next round
- Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
- p->nPatterns = 0;
- p->nSimRounds++;
-p->timeSimSat += clock() - clk;
- return RetValue1 > 0 || RetValue2 > 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Performs fraiging for the internal nodes.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Ssw_ManSweepDyn( Ssw_Man_t * p )
-{
- Bar_Progress_t * pProgress = NULL;
- Aig_Obj_t * pObj, * pObjNew;
- int clk, i, f;
-
- // perform speculative reduction
-clk = clock();
- // create timeframes
- p->pFrames = Ssw_FramesWithClasses( p );
- Aig_ManFanoutStart( p->pFrames );
- p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );
-
- // map constants and PIs of the last frame
- f = p->pPars->nFramesK;
- Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
- Saig_ManForEachPi( p->pAig, pObj, i )
- Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
- Aig_ManSetPioNumbers( p->pFrames );
- // label nodes corresponding to primary inputs
- Ssw_ManLabelPiNodes( p );
-p->timeReduce += clock() - clk;
-
- // prepare simulation info
- assert( p->vSimInfo == NULL );
- p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
- Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
-
- // sweep internal nodes
- p->fRefined = 0;
- Ssw_ClassesClearRefined( p->ppClasses );
- if ( p->pPars->fVerbose )
- pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
- p->iNodeStart = 0;
- Aig_ManForEachObj( p->pAig, pObj, i )
- {
- if ( p->iNodeStart == 0 )
- p->iNodeStart = i;
- if ( p->pPars->fVerbose )
- Bar_ProgressUpdate( pProgress, i, NULL );
- if ( Saig_ObjIsLo(p->pAig, pObj) )
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
- else if ( Aig_ObjIsNode(pObj) )
- {
- pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
- Ssw_ObjSetFrame( p, pObj, f, pObjNew );
- p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, NULL );
- }
- // check if it is time to recycle the solver
- if ( p->pMSat->pSat == NULL ||
- (p->pPars->nSatVarMax2 &&
- p->pMSat->nSatVars > p->pPars->nSatVarMax2 &&
- p->nRecycleCalls > p->pPars->nRecycleCalls2) )
- {
- // resimulate
- if ( p->nPatterns > 0 )
- {
- p->iNodeLast = i;
- if ( p->pPars->fLocalSim )
- Ssw_ManSweepResimulateDynLocal( p, f );
- else
- Ssw_ManSweepResimulateDyn( p, f );
- p->iNodeStart = i+1;
- }
-// printf( "Recycling SAT solver with %d vars and %d calls.\n",
-// p->pMSat->nSatVars, p->nRecycleCalls );
-// Aig_ManCleanMarkAB( p->pAig );
- Aig_ManCleanMarkAB( p->pFrames );
- // label nodes corresponding to primary inputs
- Ssw_ManLabelPiNodes( p );
- // replace the solver
- if ( p->pMSat )
- {
- p->nVarsMax = ABC_MAX( p->nVarsMax, p->pMSat->nSatVars );
- p->nCallsMax = ABC_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
- Ssw_SatStop( p->pMSat );
- p->nRecycles++;
- p->nRecyclesTotal++;
- p->nRecycleCalls = 0;
- }
- p->pMSat = Ssw_SatStart( 0 );
- assert( p->nPatterns == 0 );
- }
- // resimulate
- if ( p->nPatterns == 32 )
- {
- p->iNodeLast = i;
- if ( p->pPars->fLocalSim )
- Ssw_ManSweepResimulateDynLocal( p, f );
- else
- Ssw_ManSweepResimulateDyn( p, f );
- p->iNodeStart = i+1;
- }
- }
- // resimulate
- if ( p->nPatterns > 0 )
- {
- p->iNodeLast = i;
- if ( p->pPars->fLocalSim )
- Ssw_ManSweepResimulateDynLocal( p, f );
- else
- Ssw_ManSweepResimulateDyn( p, f );
- }
- // collect stats
- if ( p->pPars->fVerbose )
- Bar_ProgressStop( pProgress );
-
- // cleanup
-// Ssw_ClassesCheck( p->ppClasses );
- return p->fRefined;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-