Skip to content

A
abc
Commit ca6dd4ed by Alan Mishchenko
Options

Bug fix in &uif.

parent 1abd0457
Showing with 65 additions and 14 deletions
src/aig/gia/giaDup.c
......@@ -5301,7 +5301,7 @@ Gia_Man_t * Gia_ManDupUif( Gia_Man_t * p )
}
iUif = Gia_ManDupUifConstr( pNew, p, pvMap );
Gia_ManForEachCo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ManAppendAnd(pNew, pObj->Value, iUif) );
Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, pObj->Value, iUif) );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
Vec_WecFree( pvMap[0] );
......@@ -5336,23 +5336,31 @@ Gia_Man_t * Gia_ManDupBlackBox( Gia_Man_t * p )
Vec_Int_t * vMap = Gia_ManDupBlackBoxBuildMap( p );
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, k = 0;
int i, k = 0, iCi = 0, nCis = Gia_ManCiNum(p) + Vec_IntSum(vMap);
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
for ( i = 0; i < nCis; i++ )
Gia_ManAppendCi( pNew );
Gia_ManHashAlloc( pNew );
Gia_ManForEachObj1( p, pObj, i )
{
if ( Gia_ObjIsBuf(pObj) )
pObj->Value = Vec_IntEntry(vMap, k++) ? Gia_ManAppendCi(pNew) : Gia_ObjFanin0Copy(pObj); // out/in
{
if ( Vec_IntEntry(vMap, k++) ) // out
pObj->Value = Gia_ManCiLit(pNew, iCi++);
else
pObj->Value = Gia_ObjFanin0Copy(pObj);
}
else if ( Gia_ObjIsAnd(pObj) )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else if ( Gia_ObjIsCi(pObj) )
pObj->Value = Gia_ManAppendCi( pNew );
pObj->Value = Gia_ManCiLit(pNew, iCi++);
else if ( Gia_ObjIsCo(pObj) )
pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
}
assert( k == p->nBufs && iCi == nCis );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
Vec_IntFree( vMap );
......
src/base/abci/abc.c
......@@ -37157,6 +37157,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle );
else
pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
if ( pAbc->pGia->pCexSeq != NULL )
{
pAbc->Status = 0;
pAbc->nFrames = 0;
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
}
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
src/base/wln/wlnCom.c
......@@ -221,15 +221,18 @@ usage:
******************************************************************************/
int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose );
extern void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fInv, int fVerbose );
Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
char ** pArgvNew; int nArgcNew;
int c, fVerbose = 0;
int c, fInv = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ivh" ) ) != EOF )
{
switch ( c )
{
case 'i':
fInv ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
......@@ -251,11 +254,12 @@ int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandGraft(): This command expects one AIG file name on the command line.\n" );
return 1;
}
Wln_LibGraftOne( pLib, pArgvNew[0], pArgvNew[1], fVerbose );
Wln_LibGraftOne( pLib, pArgvNew[0], pArgvNew[1], fInv, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: %%graft [-vh] <module1_name> <module2_name>\n" );
Abc_Print( -2, "usage: %%graft [-ivh] <module1_name> <module2_name>\n" );
Abc_Print( -2, "\t replace instances of module1 by those of module2\n" );
Abc_Print( -2, "\t-i : toggle using inverse grafting [default = %s]\n", fInv? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......
src/base/wln/wlnRead.c
......@@ -48,6 +48,7 @@ struct Rtl_Lib_t_
Vec_Int_t * vTokens; // temp tokens
int pMap[MAX_MAP]; // temp map
Vec_Int_t * vMap; // mapping NameId into wires
Vec_Int_t * vInverses; // inverse equivalences
Vec_Int_t vAttrTemp; // temp
Vec_Int_t vTemp[TEMP_NUM]; // temp
};
......@@ -325,6 +326,7 @@ void Rtl_LibFree( Rtl_Lib_t * p )
for ( i = 0; i < TEMP_NUM; i++ )
ABC_FREE( p->vTemp[i].pArray );
Vec_IntFreeP( &p->vMap );
Vec_IntFreeP( &p->vInverses );
Vec_IntFreeP( &p->vTokens );
Abc_NamStop( p->pManName );
Vec_PtrFree( p->vNtks );
......@@ -1764,20 +1766,38 @@ void Rtl_NtkBlastConnect( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCon )
}
void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
{
extern void Rtl_NtkPrintBufs( Rtl_Ntk_t * p, Vec_Int_t * vBufs );
extern Gia_Man_t * Rtl_NtkBlast( Rtl_Ntk_t * p );
extern void Gia_ManDupRebuild( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vLits, int fBufs );
extern int Gia_ManFindFirst( Rtl_Ntk_t * p, int * pnOuts );
Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY );
int nIns = 0, nOuts = 0, nOuts1, iFirst1 = Gia_ManFindFirst( pModel, &nOuts1 );
int k, Par, Val, nBits = 0;
//printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
int k, Par, Val, iThis = -1, nBits = 0;
int fFound = 0;
//int fFound = p->pLib->vInverses && (iThis = Vec_IntFind(p->pLib->vInverses, pModel->NameId)) >= 0;
Vec_IntClear( &p->vBitTemp );
Rtl_CellForEachInput( p, pCell, Par, Val, k )
Rtl_NtkCollectSignalRange( p, Val );
// if ( pModel->pGia == NULL )
// pModel->pGia = Rtl_NtkBlast( pModel );
assert( pModel->pGia );
if ( pModel->fRoot )
if ( fFound )
{
// check if the previous one is the inverse one
int iThat = Vec_IntEntry( p->pLib->vInverses, iThis ^ 1 );
//printf( "Blasting %s -> %s...\n", Rtl_NtkName(p), Rtl_NtkName(pModel) );
//Rtl_NtkPrintBufs( p, pNew->vBarBufs );
if ( Vec_IntEntry(pNew->vBarBufs, Vec_IntSize(pNew->vBarBufs)-1) == Abc_Var2Lit(iThat, 1) &&
Vec_IntEntry(pNew->vBarBufs, Vec_IntSize(pNew->vBarBufs)-2) == Abc_Var2Lit(iThat, 0) )
{
//printf( "Found matching boundary.\n" );
}
nIns = nOuts1;
Vec_IntForEachEntry( &p->vBitTemp, Val, k )
Vec_IntWriteEntry( &p->vBitTemp, k, (k >= iFirst1 && k < iFirst1 + nOuts1) ? Gia_ManAppendBuf(pNew, Val) : Val );
Vec_IntPush( pNew->vBarBufs, (nIns << 16) | Abc_Var2Lit(pModel->NameId, 0) );
}
else if ( pModel->fRoot )
{
nIns = Vec_IntSize(&p->vBitTemp);
Vec_IntForEachEntry( &p->vBitTemp, Val, k )
......@@ -1788,7 +1808,7 @@ void Rtl_NtkBlastHierarchy( Gia_Man_t * pNew, Rtl_Ntk_t * p, int * pCell )
Gia_ManDupRebuild( pNew, pModel->pGia, &p->vBitTemp, !pModel->fRoot );
if ( !pModel->fRoot )
Vec_IntAppend( pNew->vBarBufs, pModel->pGia->vBarBufs );
if ( pModel->fRoot )
if ( pModel->fRoot || fFound )
{
nOuts = Vec_IntSize(&p->vBitTemp);
Vec_IntForEachEntry( &p->vBitTemp, Val, k )
......@@ -2616,7 +2636,7 @@ Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fVerbose )
SeeAlso []
***********************************************************************/
void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerbose )
void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fInv, int fVerbose )
{
int Name1 = Wln_ReadFindToken( pModule1, p->pManName );
int Name2 = Wln_ReadFindToken( pModule2, p->pManName );
......@@ -2633,6 +2653,16 @@ void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerb
Rtl_Ntk_t * pNtk1 = Rtl_LibNtk(p, iNtk1);
Rtl_Ntk_t * pNtk2 = Rtl_LibNtk(p, iNtk2);
assert( iNtk1 != iNtk2 );
if ( fInv )
{
printf( "Setting \"%s\" (appearing %d times) and \"%s\" (appearing %d times) as inverse-equivalent.\n",
Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
if ( p->vInverses == NULL )
p->vInverses = Vec_IntAlloc( 10 );
Vec_IntPushTwo( p->vInverses, pNtk1->NameId, pNtk2->NameId );
}
else
{
printf( "Replacing \"%s\" (appearing %d times) by \"%s\" (appearing %d times).\n",
Rtl_NtkName(pNtk1), Rtl_LibCountInsts(p, pNtk1), Rtl_NtkName(pNtk2), Rtl_LibCountInsts(p, pNtk2) );
pNtk1->iCopy = iNtk2;
......@@ -2640,6 +2670,7 @@ void Wln_LibGraftOne( Rtl_Lib_t * p, char * pModule1, char * pModule2, int fVerb
Rtl_LibUpdateBoxes( p );
Rtl_LibReorderModules( p );
}
}
}
/**Function*************************************************************
......
src/proof/cec/cecSatG3.c
......@@ -2125,6 +2125,8 @@ Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs,
{
Gia_Man_t * pNew = NULL;
Cec5_ManPerformSweeping( p, pPars, &pNew, 0, fCbs, approxLim, subBatchSz, adaRecycle );
if ( pNew == NULL )
pNew = Gia_ManDup( p );
return pNew;
}
......
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