diff options
Diffstat (limited to 'src/sat/pdr/pdrClass.c')
| -rw-r--r-- | src/sat/pdr/pdrClass.c | 223 |
1 files changed, 0 insertions, 223 deletions
diff --git a/src/sat/pdr/pdrClass.c b/src/sat/pdr/pdrClass.c deleted file mode 100644 index 3e990958..00000000 --- a/src/sat/pdr/pdrClass.c +++ /dev/null @@ -1,223 +0,0 @@ -/**CFile**************************************************************** - - FileName [pdrClass.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Property driven reachability.] - - Synopsis [Equivalence classes of register outputs.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - November 20, 2010.] - - Revision [$Id: pdrClass.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "pdrInt.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs duplication with the variable map.] - - Description [Var map contains -1 if const0 and <reg_num> otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Aig_Man_t * Pdr_ManRehashWithMap( Aig_Man_t * pAig, Vec_Int_t * vMap ) -{ - Aig_Man_t * pFrames; - Aig_Obj_t * pObj; - int i, iReg; - assert( Vec_IntSize(vMap) == Aig_ManRegNum(pAig) ); - // start the fraig package - pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) ); - pFrames->pName = Aig_UtilStrsav( pAig->pName ); - pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec ); - // create CI mapping - Aig_ManCleanData( pAig ); - Aig_ManConst1(pAig)->pData = Aig_ManConst1(pFrames); - Aig_ManForEachPi( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePi(pFrames); - Saig_ManForEachLo( pAig, pObj, i ) - { - iReg = Vec_IntEntry(vMap, i); - if ( iReg == -1 ) - pObj->pData = Aig_ManConst0(pFrames); - else - pObj->pData = Saig_ManLo(pAig, iReg)->pData; - } - // add internal nodes of this frame - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - // add output nodes - Aig_ManForEachPo( pAig, pObj, i ) - pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) ); - // finish off - Aig_ManCleanup( pFrames ); - Aig_ManSetRegNum( pFrames, Aig_ManRegNum(pAig) ); - return pFrames; -} - -/**Function************************************************************* - - Synopsis [Creates mapping of registers.] - - Description [Var map contains -1 if const0 and <reg_num> otherwise.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Pdr_ManCreateMap( Aig_Man_t * p ) -{ - Aig_Obj_t * pObj; - Vec_Int_t * vMap; - int * pLit2Id, Lit, i; - pLit2Id = ABC_ALLOC( int, Aig_ManObjNumMax(p) * 2 ); - for ( i = 0; i < Aig_ManObjNumMax(p) * 2; i++ ) - pLit2Id[i] = -1; - vMap = Vec_IntAlloc( Aig_ManRegNum(p) ); - Saig_ManForEachLi( p, pObj, i ) - { - if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p) ) - { - Vec_IntPush( vMap, -1 ); - continue; - } - Lit = 2 * Aig_ObjFaninId0(pObj) + Aig_ObjFaninC0(pObj); - if ( pLit2Id[Lit] < 0 ) // the first time - pLit2Id[Lit] = i; - Vec_IntPush( vMap, pLit2Id[Lit] ); - } - ABC_FREE( pLit2Id ); - return vMap; -} - -/**Function************************************************************* - - Synopsis [Counts reduced registers.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pdr_ManCountMap( Vec_Int_t * vMap ) -{ - int i, Entry, Counter = 0; - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry != i ) - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Counts reduced registers.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_ManPrintMap( Vec_Int_t * vMap ) -{ - Vec_Int_t * vMarks; - int f, i, iClass, Entry, Counter = 0; - printf( " Consts: " ); - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry == -1 ) - printf( "%d ", i ); - printf( "\n" ); - vMarks = Vec_IntAlloc( 100 ); - Vec_IntForEachEntry( vMap, iClass, f ) - { - if ( iClass == -1 ) - continue; - if ( iClass == f ) - continue; - // check previous classes - if ( Vec_IntFind( vMarks, iClass ) >= 0 ) - continue; - Vec_IntPush( vMarks, iClass ); - // print class - printf( " Class %d : ", iClass ); - Vec_IntForEachEntry( vMap, Entry, i ) - if ( Entry == iClass ) - printf( "%d ", i ); - printf( "\n" ); - } - Vec_IntFree( vMarks ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pdr_ManEquivClasses( Aig_Man_t * pAig ) -{ - Vec_Int_t * vMap; - Aig_Man_t * pTemp; - int f, nFrames = 100; - assert( Saig_ManRegNum(pAig) > 0 ); - // start the map - vMap = Vec_IntAlloc( 0 ); - Vec_IntFill( vMap, Aig_ManRegNum(pAig), -1 ); - // iterate and print changes - for ( f = 0; f < nFrames; f++ ) - { - // implement variable map - pTemp = Pdr_ManRehashWithMap( pAig, vMap ); - // report the result - printf( "F =%4d : Total = %6d. Nodes = %6d. RedRegs = %6d. Prop = %s\n", - f+1, Aig_ManNodeNum(pAig), Aig_ManNodeNum(pTemp), Pdr_ManCountMap(vMap), - Aig_ObjChild0(Aig_ManPo(pTemp,0)) == Aig_ManConst0(pTemp) ? "proof" : "unknown" ); - // recreate the map - Pdr_ManPrintMap( vMap ); - Vec_IntFree( vMap ); - vMap = Pdr_ManCreateMap( pTemp ); - Aig_ManStop( pTemp ); - if ( Pdr_ManCountMap(vMap) == 0 ) - break; - } - Vec_IntFree( vMap ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - |