Commit 5cf9d6dd by Alan Mishchenko

Experiments with mini AIG manager.

parent ae1dddbc
...@@ -73,7 +73,7 @@ static void Mini_AigGrow( Mini_Aig_t * p, int nCapMin ) ...@@ -73,7 +73,7 @@ static void Mini_AigGrow( Mini_Aig_t * p, int nCapMin )
} }
static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 ) static void Mini_AigPush( Mini_Aig_t * p, int Lit0, int Lit1 )
{ {
if ( p->nSize >= p->nCap + 1 ) if ( p->nSize + 2 > p->nCap )
{ {
if ( p->nCap < MINI_AIG_START_SIZE ) if ( p->nCap < MINI_AIG_START_SIZE )
Mini_AigGrow( p, MINI_AIG_START_SIZE ); Mini_AigGrow( p, MINI_AIG_START_SIZE );
...@@ -110,7 +110,7 @@ static int Mini_AigLitIsConst0( int Lit ) { return Lit == 0 ...@@ -110,7 +110,7 @@ static int Mini_AigLitIsConst0( int Lit ) { return Lit == 0
static int Mini_AigLitIsConst1( int Lit ) { return Lit == 1; } static int Mini_AigLitIsConst1( int Lit ) { return Lit == 1; }
static int Mini_AigLitIsConst( int Lit ) { return Lit == 0 || Lit == 1; } static int Mini_AigLitIsConst( int Lit ) { return Lit == 0 || Lit == 1; }
static int Mini_AigNumNodes( Mini_Aig_t * p ) { return p->nSize/2; } static int Mini_AigNodeNum( Mini_Aig_t * p ) { return p->nSize/2; }
static int Mini_AigNodeIsConst( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id == 0; } static int Mini_AigNodeIsConst( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id == 0; }
static int Mini_AigNodeIsPi( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) == MINI_AIG_NULL; } static int Mini_AigNodeIsPi( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) == MINI_AIG_NULL; }
static int Mini_AigNodeIsPo( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) == MINI_AIG_NULL; } static int Mini_AigNodeIsPo( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ); return Id > 0 && Mini_AigNodeFanin0( p, Id ) != MINI_AIG_NULL && Mini_AigNodeFanin1( p, Id ) == MINI_AIG_NULL; }
...@@ -118,15 +118,12 @@ static int Mini_AigNodeIsAnd( Mini_Aig_t * p, int Id ) { assert( Id >= 0 ...@@ -118,15 +118,12 @@ static int Mini_AigNodeIsAnd( Mini_Aig_t * p, int Id ) { assert( Id >= 0
// constructor/destructor // constructor/destructor
static Mini_Aig_t * Mini_AigStart( int nCap ) static Mini_Aig_t * Mini_AigStart()
{ {
Mini_Aig_t * p; Mini_Aig_t * p;
assert( nCap > 0 );
p = MINI_AIG_ALLOC( Mini_Aig_t, 1 ); p = MINI_AIG_ALLOC( Mini_Aig_t, 1 );
if ( nCap < MINI_AIG_START_SIZE )
nCap = MINI_AIG_START_SIZE;
p->nSize = 0; p->nSize = 0;
p->nCap = nCap; p->nCap = MINI_AIG_START_SIZE;
p->pArray = MINI_AIG_ALLOC( int, p->nCap ); p->pArray = MINI_AIG_ALLOC( int, p->nCap );
Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL ); Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
return p; return p;
...@@ -142,14 +139,14 @@ static void Mini_AigStop( Mini_Aig_t * p ) ...@@ -142,14 +139,14 @@ static void Mini_AigStop( Mini_Aig_t * p )
// (constant node is created when AIG manager is created) // (constant node is created when AIG manager is created)
static int Mini_AigCreatePi( Mini_Aig_t * p ) static int Mini_AigCreatePi( Mini_Aig_t * p )
{ {
int Lit = Mini_AigNumNodes(p); int Lit = Mini_AigNodeNum(p);
Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL ); Mini_AigPush( p, MINI_AIG_NULL, MINI_AIG_NULL );
return Lit; return Lit;
} }
static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 ) static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 )
{ {
int Lit = Mini_AigNumNodes(p); int Lit = Mini_AigNodeNum(p);
assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNumNodes(p) ); assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNodeNum(p) );
Mini_AigPush( p, Lit0, MINI_AIG_NULL ); Mini_AigPush( p, Lit0, MINI_AIG_NULL );
return Lit; return Lit;
} }
...@@ -157,9 +154,9 @@ static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 ) ...@@ -157,9 +154,9 @@ static int Mini_AigCreatePo( Mini_Aig_t * p, int Lit0 )
// boolean operations // boolean operations
static int Mini_AigAnd( Mini_Aig_t * p, int Lit0, int Lit1 ) static int Mini_AigAnd( Mini_Aig_t * p, int Lit0, int Lit1 )
{ {
int Lit = Mini_AigNumNodes(p); int Lit = Mini_AigNodeNum(p);
assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNumNodes(p) ); assert( Lit0 >= 0 && Lit0 < 2 * Mini_AigNodeNum(p) );
assert( Lit1 >= 0 && Lit1 < 2 * Mini_AigNumNodes(p) ); assert( Lit1 >= 0 && Lit1 < 2 * Mini_AigNodeNum(p) );
Mini_AigPush( p, Lit0, Lit1 ); Mini_AigPush( p, Lit0, Lit1 );
return Lit; return Lit;
} }
...@@ -178,6 +175,12 @@ static int Mini_AigXor( Mini_Aig_t * p, int Lit0, int Lit1 ) ...@@ -178,6 +175,12 @@ static int Mini_AigXor( Mini_Aig_t * p, int Lit0, int Lit1 )
return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 ); return Mini_AigMux( p, Lit0, Mini_AigLitNot(Lit1), Lit1 );
} }
#define Mini_AigForEachPi( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPi(p, i) ) else
#define Mini_AigForEachPo( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsPo(p, i) ) else
#define Mini_AigForEachAnd( p, i ) for (i = 1; i < Mini_AigNodeNum(p); i++) if ( !Mini_AigNodeIsAnd(p, i) ) else
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
...@@ -29,9 +29,6 @@ ABC_NAMESPACE_IMPL_START ...@@ -29,9 +29,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
static Mini_Aig_t * Abc_NtkToMini( Abc_Ntk_t * pNtk );
static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Mini_Aig_t * p );
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS /// /// FUNCTION DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -50,20 +47,15 @@ static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Mini_Aig_t * p ); ...@@ -50,20 +47,15 @@ static Abc_Ntk_t * Abc_NtkFromMini( Abc_Ntk_t * pNtkOld, Mini_Aig_t * p );
Abc_Obj_t * Abc_NodeFanin0Copy( Abc_Ntk_t * pNtk, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id ) Abc_Obj_t * Abc_NodeFanin0Copy( Abc_Ntk_t * pNtk, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id )
{ {
int Lit = Mini_AigNodeFanin0( p, Id ); int Lit = Mini_AigNodeFanin0( p, Id );
Lit = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); int AbcLit = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) );
return Abc_ObjNotCond( Abc_NtkObj(pNtk, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); return Abc_ObjFromLit( pNtk, AbcLit );
} }
Abc_Obj_t * Abc_NodeFanin1Copy( Abc_Ntk_t * pNtk, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id ) Abc_Obj_t * Abc_NodeFanin1Copy( Abc_Ntk_t * pNtk, Vec_Int_t * vCopies, Mini_Aig_t * p, int Id )
{ {
int Lit = Mini_AigNodeFanin1( p, Id ); int Lit = Mini_AigNodeFanin1( p, Id );
Lit = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); int AbcLit = Abc_LitNotCond( Vec_IntEntry(vCopies, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) );
return Abc_ObjNotCond( Abc_NtkObj(pNtk, Abc_Lit2Var(Lit)), Abc_LitIsCompl(Lit) ); return Abc_ObjFromLit( pNtk, AbcLit );
}
int Abc_NodeToLit( Abc_Obj_t * pObj )
{
return Abc_LitNotCond( Abc_ObjId(Abc_ObjRegular(pObj)), Abc_ObjIsComplement(pObj) );
} }
Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p ) Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
{ {
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
...@@ -71,12 +63,12 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p ) ...@@ -71,12 +63,12 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
Vec_Int_t * vCopies; Vec_Int_t * vCopies;
int i, nNodes; int i, nNodes;
// get the number of nodes // get the number of nodes
nNodes = Mini_AigNumNodes(p); nNodes = Mini_AigNodeNum(p);
// create ABC network // create ABC network
pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); pNtk = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
// create mapping from MiniAIG into ABC objects // create mapping from MiniAIG objects into ABC objects
vCopies = Vec_IntAlloc( nNodes ); vCopies = Vec_IntAlloc( nNodes );
Vec_IntPush( vCopies, Abc_LitNot(Abc_NodeToLit(Abc_AigConst1(pNtk))) ); Vec_IntPush( vCopies, Abc_LitNot(Abc_ObjToLit(Abc_AigConst1(pNtk))) );
// iterate through the objects // iterate through the objects
for ( i = 1; i < nNodes; i++ ) for ( i = 1; i < nNodes; i++ )
{ {
...@@ -87,7 +79,7 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p ) ...@@ -87,7 +79,7 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
else if ( Mini_AigNodeIsAnd( p, i ) ) else if ( Mini_AigNodeIsAnd( p, i ) )
pObj = Abc_AigAnd((Abc_Aig_t *)pNtk->pManFunc, Abc_NodeFanin0Copy(pNtk, vCopies, p, i), Abc_NodeFanin1Copy(pNtk, vCopies, p, i)); pObj = Abc_AigAnd((Abc_Aig_t *)pNtk->pManFunc, Abc_NodeFanin0Copy(pNtk, vCopies, p, i), Abc_NodeFanin1Copy(pNtk, vCopies, p, i));
else assert( 0 ); else assert( 0 );
Vec_IntPush( vCopies, Abc_NodeToLit(pObj) ); Vec_IntPush( vCopies, Abc_ObjToLit(pObj) );
} }
Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc ); Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc );
Vec_IntFree( vCopies ); Vec_IntFree( vCopies );
...@@ -109,26 +101,34 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p ) ...@@ -109,26 +101,34 @@ Abc_Ntk_t * Abc_NtkFromMiniAig( Mini_Aig_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NodeFanin0Copy2( Abc_Obj_t * pObj )
{
return Abc_LitNotCond( Abc_ObjFanin0(pObj)->iTemp, Abc_ObjFaninC0(pObj) );
}
int Abc_NodeFanin1Copy2( Abc_Obj_t * pObj )
{
return Abc_LitNotCond( Abc_ObjFanin1(pObj)->iTemp, Abc_ObjFaninC1(pObj) );
}
Mini_Aig_t * Abc_NtkToMiniAig( Abc_Ntk_t * pNtk ) Mini_Aig_t * Abc_NtkToMiniAig( Abc_Ntk_t * pNtk )
{ {
Mini_Aig_t * p = NULL; Mini_Aig_t * p;
/*
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
int i; int i;
assert( Abc_NtkIsStrash(pNtk) );
// create the manager // create the manager
p = Hop_ManStart(); p = Mini_AigStart();
// transfer the pointers to the basic nodes // create mapping from MiniAIG into ABC objects
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Hop_ManConst1(p); Abc_NtkCleanCopy( pNtk );
Abc_AigConst1(pNtk)->iTemp = Mini_AigLitConst1();
// create primary inputs
Abc_NtkForEachCi( pNtk, pObj, i ) Abc_NtkForEachCi( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Hop_ObjCreatePi(p); pObj->iTemp = Mini_AigCreatePi(p);
// perform the conversion of the internal nodes (assumes DFS ordering) // create internal nodes
Abc_NtkForEachNode( pNtk, pObj, i ) Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = (Abc_Obj_t *)Hop_And( p, (Hop_Obj_t *)Abc_ObjChild0Copy(pObj), (Hop_Obj_t *)Abc_ObjChild1Copy(pObj) ); pObj->iTemp = Mini_AigAnd( p, Abc_NodeFanin0Copy2(pObj), Abc_NodeFanin1Copy2(pObj) );
// create the POs // create primary outputs
Abc_NtkForEachCo( pNtk, pObj, i ) Abc_NtkForEachCo( pNtk, pObj, i )
Hop_ObjCreatePo( p, (Hop_Obj_t *)Abc_ObjChild0Copy(pObj) ); pObj->iTemp = Mini_AigCreatePo( p, Abc_NodeFanin0Copy2(pObj) );
Hop_ManCleanup( p );
*/
return p; return p;
} }
...@@ -143,16 +143,25 @@ Mini_Aig_t * Abc_NtkToMiniAig( Abc_Ntk_t * pNtk ) ...@@ -143,16 +143,25 @@ Mini_Aig_t * Abc_NtkToMiniAig( Abc_Ntk_t * pNtk )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Abc_NtkInputMiniAig( Mini_Aig_t * p ) void Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * p )
{ {
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
Abc_Frame_t * pAbc = Abc_FrameReadGlobalFrame();
if ( pAbc == NULL ) if ( pAbc == NULL )
printf( "ABC framework is not initialized by calling Abc_Start()\n" ); printf( "ABC framework is not initialized by calling Abc_Start()\n" );
pNtk = Abc_NtkFromMiniAig( p ); pNtk = Abc_NtkFromMiniAig( (Mini_Aig_t *)p );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
// Abc_NtkDelete( pNtk ); // Abc_NtkDelete( pNtk );
} }
void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc )
{
Abc_Ntk_t * pNtk;
if ( pAbc == NULL )
printf( "ABC framework is not initialized by calling Abc_Start()\n" );
pNtk = Abc_FrameReadNtk( pAbc );
if ( pNtk == NULL )
printf( "Current network in ABC framework is not defined.\n" );
return Abc_NtkToMiniAig( pNtk );
}
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
...@@ -131,6 +131,10 @@ extern ABC_DLL void Abc_FrameSetCex( Abc_Cex_t * pCex ); ...@@ -131,6 +131,10 @@ extern ABC_DLL void Abc_FrameSetCex( Abc_Cex_t * pCex );
extern ABC_DLL void Abc_FrameSetNFrames( int nFrames ); extern ABC_DLL void Abc_FrameSetNFrames( int nFrames );
extern ABC_DLL void Abc_FrameSetStatus( int Status ); extern ABC_DLL void Abc_FrameSetStatus( int Status );
/*=== mainFrame.c ===========================================================*/
extern ABC_DLL void Abc_NtkInputMiniAig( Abc_Frame_t * pAbc, void * p );
extern ABC_DLL void * Abc_NtkOutputMiniAig( Abc_Frame_t * pAbc );
ABC_NAMESPACE_HEADER_END ABC_NAMESPACE_HEADER_END
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment