Skip to content

A
abc
Commit d9760b04 by Alan Mishchenko
Options

Version abc80209

parent f2d4f6c2
Showing with 95 additions and 23 deletions
src/aig/aig/aig.h
......@@ -517,7 +517,8 @@ extern void Aig_ObjOrderInsert( Aig_Man_t * p, int ObjId );
extern void Aig_ObjOrderRemove( Aig_Man_t * p, int ObjId );
extern void Aig_ObjOrderAdvance( Aig_Man_t * p );
/*=== aigPart.c =========================================================*/
extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan );
extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p );
extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
......
src/aig/aig/aigPart.c
......@@ -258,7 +258,7 @@ Vec_Int_t * Part_ManTransferEntry( Part_One_t * p )
Synopsis [Computes supports of the POs in the multi-output AIG.]
Description [Returns the array of integer arrays containing indices
of the primary inputs.]
of the primary inputsf or each primary output.]
SideEffects [Adds the integer PO number at end of each array.]
......@@ -346,6 +346,40 @@ Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan )
/**Function*************************************************************
Synopsis [Computes the set of outputs for each input.]
Description [Returns the array of integer arrays containing indices
of the primary outputsf for each primary input.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Aig_ManSupportsInverse( Aig_Man_t * p )
{
Vec_Ptr_t * vSupps, * vSuppsInv;
Vec_Int_t * vSupp;
int i, k, iIn, iOut;
// get structural supports for each output
vSupps = Aig_ManSupports( p );
// start the inverse supports
vSuppsInv = Vec_PtrAlloc( Aig_ManPiNum(p) );
for ( i = 0; i < Aig_ManPiNum(p); i++ )
Vec_PtrPush( vSuppsInv, Vec_IntAlloc(8) );
// transforms the supports into the inverse supports
Vec_PtrForEachEntry( vSupps, vSupp, i )
{
iOut = Vec_IntPop( vSupp );
Vec_IntForEachEntry( vSupp, iIn, k )
Vec_IntPush( Vec_PtrEntry(vSuppsInv, iIn), iOut );
}
Vec_VecFree( (Vec_Vec_t *)vSupps );
return vSuppsInv;
}
/**Function*************************************************************
Synopsis [Start char-bases support representation.]
Description []
......
src/aig/fra/fraClaus.c
......@@ -515,7 +515,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
nCountConst = nCountImps = 0;
CostMax = p->nSimWords * 32;
/*
// add the property
{
Aig_Obj_t * pObj;
......@@ -528,7 +528,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
nCountConst++;
// printf( "Added the target property to the set of clauses to be inductively checked.\n" );
}
*/
pSeq->nWordsPref = p->nSimWordsPref;
Aig_ManForEachLoSeq( p->pAig, pObj1, i )
......
src/base/abci/abcDar.c
......@@ -95,8 +95,8 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
if ( fRegisters )
{
pMan->nRegs = Abc_NtkLatchNum(pNtk);
// pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
pMan->vFlopNums = NULL;
pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
// pMan->vFlopNums = NULL;
}
// transfer the pointers to the basic nodes
Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
......@@ -154,6 +154,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Obj_t * pObjNew;
Aig_Obj_t * pObj;
int i;
assert( pMan->nAsserts == 0 );
// assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
......@@ -207,7 +208,8 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObjNew, * pLatch;
Aig_Obj_t * pObj, * pObjLo, * pObjLi;
int i, iNodeId;
int i, iNodeId, nDigits;
assert( pMan->nAsserts == 0 );
// assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) );
// perform strashing
pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
......@@ -237,19 +239,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_ObjAddFanin( pObjLo->pData, pObjNew );
Abc_LatchSetInit0( pObjNew );
}
if ( pMan->vFlopNums == NULL )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
{
pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
}
}
// rebuild the AIG
vNodes = Aig_ManDfs( pMan );
Vec_PtrForEachEntry( vNodes, pObj, i )
......@@ -261,8 +250,8 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
// connect the PO nodes
Aig_ManForEachPo( pMan, pObj, i )
{
if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
break;
// if ( pMan->nAsserts && i == Aig_ManPoNum(pMan) - pMan->nAsserts )
// break;
iNodeId = Nm_ManFindIdByNameTwoTypes( pNtkNew->pManName, Abc_ObjName(Abc_NtkCo(pNtkNew, i)), ABC_OBJ_PI, ABC_OBJ_BO );
if ( iNodeId >= 0 )
pObjNew = Abc_NtkObj( pNtkNew, iNodeId );
......@@ -270,6 +259,29 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
pObjNew = (Abc_Obj_t *)Aig_ObjChild0Copy(pObj);
Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjNew );
}
if ( pMan->vFlopNums == NULL )
Abc_NtkAddDummyBoxNames( pNtkNew );
else
{
assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) );
nDigits = Extra_Base10Log( Abc_NtkLatchNum(pNtkNew) );
Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
{
pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) );
iNodeId = Nm_ManFindIdByName( pNtkNew->pManName, Abc_ObjName(Abc_ObjFanout0(pLatch)), ABC_OBJ_PO );
if ( iNodeId >= 0 )
{
Abc_ObjAssignName( pObjNew, Abc_ObjNameDummy("l", i, nDigits), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjNameDummy("li", i, nDigits), NULL );
Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjNameDummy("lo", i, nDigits), NULL );
//printf( "happening %s -> %s\n", Abc_ObjName(Abc_ObjFanin0(pObjNew)), Abc_ObjName(Abc_ObjFanout0(pObjNew)) );
continue;
}
Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL );
Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL );
Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL );
}
}
// if there are assertions, add them
if ( pMan->nAsserts > 0 )
Aig_ManForEachAssert( pMan, pObj, i )
......
src/opt/mfs/mfsCore.c
......@@ -175,6 +175,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
p->pCare = Abc_NtkToDar( pTemp, 0 );
Abc_NtkDelete( pTemp );
p->vSuppsInv = Aig_ManSupportsInverse( p->pCare );
}
// if ( pPars->fVerbose )
{
......
src/opt/mfs/mfsInt.h
......@@ -49,6 +49,7 @@ struct Mfs_Man_t_
Mfs_Par_t * pPars;
Abc_Ntk_t * pNtk;
Aig_Man_t * pCare;
Vec_Ptr_t * vSuppsInv;
int nFaninMax;
// intermeditate data for the node
Vec_Ptr_t * vRoots; // the roots of the window
......
src/opt/mfs/mfsMan.c
......@@ -155,6 +155,8 @@ void Mfs_ManStop( Mfs_Man_t * p )
Mfs_ManPrint( p );
if ( p->pCare )
Aig_ManStop( p->pCare );
if ( p->vSuppsInv )
Vec_VecFree( (Vec_Vec_t *)p->vSuppsInv );
Mfs_ManClean( p );
Int_ManFree( p->pMan );
Vec_IntFree( p->vMem );
......
src/opt/mfs/mfsStrash.c
......@@ -179,7 +179,8 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
Aig_Man_t * pMan;
Abc_Obj_t * pFanin;
Aig_Obj_t * pObjAig, * pPi, * pPo;
int i;
Vec_Int_t * vOuts;
int i, k, iOut;
// start the new manager
pMan = Aig_ManStart( 1000 );
// construct the root node's AIG cone
......@@ -197,6 +198,25 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
pPi->pData = pFanin->pCopy;
}
// construct the constraints
Vec_PtrForEachEntry( p->vSupp, pFanin, i )
{
vOuts = Vec_PtrEntry( p->vSuppsInv, (int)pFanin->pData );
Vec_IntForEachEntry( vOuts, iOut, k )
{
pPo = Aig_ManPo( p->pCare, iOut );
if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
continue;
Aig_ObjSetTravIdCurrent( p->pCare, pPo );
if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
continue;
pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
if ( pObjAig == NULL )
continue;
pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
Aig_ObjCreatePo( pMan, pObjAig );
}
}
/*
Aig_ManForEachPo( p->pCare, pPo, i )
{
// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
......@@ -208,6 +228,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
Aig_ObjCreatePo( pMan, pObjAig );
}
*/
}
if ( p->pPars->fResub )
{
......
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