Skip to content

A
abc
Commit 1c0ea102 by Alan Mishchenko
Options

Adding new utility procedures.

parent a3ada00d
Showing with 159 additions and 45 deletions
src/base/acb/acb.h
......@@ -1023,7 +1023,7 @@ extern Vec_Int_t * Acb_ObjCollectTfiVec( Acb_Ntk_t * p, Vec_Int_t * vObjs );
extern Vec_Int_t * Acb_ObjCollectTfoVec( Acb_Ntk_t * p, Vec_Int_t * vObjs );
extern int Acb_NtkCountPiBuffers( Acb_Ntk_t * p, Vec_Int_t * vObjs );
extern int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs );
extern int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjs, int nGates[5] );
extern int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed, int nGates[5] );
extern int Acb_ObjComputeLevelD( Acb_Ntk_t * p, int iObj );
extern int Acb_NtkComputeLevelD( Acb_Ntk_t * p, Vec_Int_t * vTfo );
......
src/base/acb/acbFunc.c
......@@ -1905,6 +1905,42 @@ Vec_Int_t * Acb_GetUsedDivs( Vec_Int_t * vDivs, Vec_Int_t * vUsed )
Vec_IntPush( vRes, iObj );
return vRes;
}
Vec_Int_t * Acb_GetDerefedNodes( Acb_Ntk_t * p )
{
Vec_Ptr_t * vNames = Abc_FrameReadSignalNames();
if ( vNames != NULL )
{
Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
Vec_Int_t * vMap = Vec_IntStartFull( Abc_NamObjNumMax(p->pDesign->pStrs) );
int i, iObj; char * pName;
Acb_NtkForEachObj( p, iObj )
if ( Acb_ObjName(p, iObj) )
Vec_IntWriteEntry( vMap, Acb_ObjName(p, iObj), iObj );
Vec_PtrForEachEntry( char *, vNames, pName, i )
{
int NameId = Abc_NamStrFindOrAdd( p->pDesign->pStrs, pName, NULL );
if ( NameId == 0 )
{
printf( "Cannot find name ID for name %s\n", pName );
Vec_IntFree( vMap );
Vec_IntFree( vNodes );
return NULL;
}
else if ( Vec_IntEntry(vMap, NameId) == -1 )
{
printf( "Cannot find obj ID for name %s\n", pName );
Vec_IntFree( vMap );
Vec_IntFree( vNodes );
return NULL;
}
else
Vec_IntPush( vNodes, Vec_IntEntry(vMap, NameId) );
}
Vec_IntFree( vMap );
return vNodes;
}
return NULL;
}
Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUsed, Vec_Ptr_t * vSops, Vec_Ptr_t * vGias, Vec_Int_t * vTars )
{
extern Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops );
......@@ -1912,15 +1948,19 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
Vec_Wec_t * vGates = vGias ? Abc_GiaSynthesize(vGias, NULL) : Abc_SopSynthesize(vSops); Vec_Int_t * vGate;
int nOuts = vGias ? Vec_PtrSize(vGias) : Vec_PtrSize(vSops);
int i, k, iObj, nWires = Vec_WecSize(vGates) - Vec_IntSize(vUsed) - nOuts, fFirst = 1;
int nGates[5] = {0}, nInvs = 0, nBufs = 0, nNodes = 0, nConst[2] = {0};
int nGates1[5] = {0}, nGates0[5] = {0};
Vec_Ptr_t * vNames = Acb_GenerateSignalNames( p, vDivs, vUsed, nWires, vTars, vGates );
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
Vec_Int_t * vSup = Acb_GetUsedDivs( vDivs, vUsed );
Vec_Int_t * vDrf = Acb_GetDerefedNodes( p );
Vec_Int_t * vTfi = Acb_ObjCollectTfiVec( p, vSup );
Vec_Int_t * vTfo = Acb_ObjCollectTfoVec( p, vTars );
int nPiCount = Acb_NtkCountPiBuffers( p, vSup );
int nPoCount = Acb_NtkCountPoDrivers( p, vTars );
int nMffc = Acb_NtkFindMffcSize( p, vSup, nGates );
int nMffc = vDrf ? Vec_IntSize(vTars) + Acb_NtkFindMffcSize( p, vSup, vDrf, nGates1 ) : 0;
int * pCounts = Abc_FrameReadGateCounts();
for ( i = 0; i < 5; i++ )
nGates1[i] += pCounts[i];
Vec_IntFree( vSup );
Vec_WecForEachLevelStartStop( vGates, vGate, i, Vec_IntSize(vUsed), Vec_IntSize(vUsed)+nWires )
{
......@@ -1928,20 +1968,23 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
{
char * pName = Acb_Oper2Name(Vec_IntEntry(vGate, 0));
if ( !strcmp(pName, "buf") )
nBufs++;
nGates0[2]++;
else if ( !strcmp(pName, "not") )
nInvs++;
nGates0[3]++;
else
nNodes += Vec_IntSize(vGate) - 3;
nGates0[4] += Vec_IntSize(vGate) - 3;
}
else
nConst[Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T]++;
nGates0[Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T]++;
}
Vec_StrPrintF( vStr, "// Patch : in = %d out = %d : pi_in = %d po_out = %d : tfi = %d tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
Vec_StrPrintF( vStr, "// Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nConst[0], nConst[1], nBufs, nInvs, nNodes );
Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates[0], nGates[1], nGates[2], nGates[3], nGates[4] );
Vec_StrPrintF( vStr, "// TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n\n", nWires-nMffc, nConst[0]-nGates[0], nConst[1]-nGates[1], nBufs-nGates[2], nInvs-nGates[3], nNodes-nGates[4] );
Vec_StrPrintF( vStr, "// Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] );
if ( vDrf != NULL )
Vec_StrPrintF( vStr, "// Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] );
if ( vDrf != NULL )
Vec_StrPrintF( vStr, "// TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0], nGates0[1]-nGates1[1], nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] );
Vec_StrPrintF( vStr, "\n" );
Vec_StrAppend( vStr, "module patch (" );
......@@ -2003,9 +2046,13 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
// printf( "Summary of the results\n" );
printf( "\n" );
printf( "Patch : in = %d out = %d : pi_in = %d po_out = %d : tfi = %d tfo = %d\n", Vec_IntSize(vUsed), nOuts, nPiCount, nPoCount, Vec_IntSize(vTfi), Vec_IntSize(vTfo) );
printf( "Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nConst[0], nConst[1], nBufs, nInvs, nNodes );
printf( "Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates[0], nGates[1], nGates[2], nGates[3], nGates[4] );
printf( "TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires-nMffc, nConst[0]-nGates[0], nConst[1]-nGates[1], nBufs-nGates[2], nInvs-nGates[3], nNodes-nGates[4] );
printf( "Added : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires, nGates0[0], nGates0[1], nGates0[2], nGates0[3], nGates0[4] );
if ( vDrf != NULL )
printf( "Removed : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nMffc, nGates1[0], nGates1[1], nGates1[2], nGates1[3], nGates1[4] );
if ( vDrf != NULL )
printf( "TOTAL : gate =%4d : c0 =%2d c1 =%2d buf =%3d inv =%3d two-input =%4d\n", nWires-nMffc, nGates0[0]-nGates1[0], nGates0[1]-nGates1[1], nGates0[2]-nGates1[2], nGates0[3]-nGates1[3], nGates0[4]-nGates1[4] );
printf( "\n" );
Vec_IntFreeP( &vDrf );
return vStr;
}
......
src/base/acb/acbUtil.c
......@@ -21,6 +21,7 @@
#include "acb.h"
#include "base/abc/abc.h"
#include "base/io/ioAbc.h"
#include "base/main/main.h"
ABC_NAMESPACE_IMPL_START
......@@ -166,67 +167,65 @@ int Acb_NtkCountPoDrivers( Acb_Ntk_t * p, Vec_Int_t * vObjs )
SeeAlso []
***********************************************************************/
int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
int Acb_NtkNodeDeref_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
{
int i, Fanin, * pFanins, Counter = 1;
if ( Acb_ObjIsCi(p, iObj) )
return 0;
if ( nGates )
{
int Type = Acb_ObjType( p, iObj );
if ( Type == ABC_OPER_CONST_F )
nGates[0]++;
if ( Type == ABC_OPER_CONST_T )
nGates[1]++;
if ( Type == ABC_OPER_BIT_BUF )
nGates[2]++;
if ( Type == ABC_OPER_BIT_INV )
nGates[3]++;
else
nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
}
Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
{
assert( Vec_IntEntry(vRefs, Fanin) > 0 );
Vec_IntAddToEntry( vRefs, Fanin, -1 );
if ( Vec_IntEntry(vRefs, Fanin) == 0 )
Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin, nGates );
Counter += Acb_NtkNodeDeref_rec( vRefs, p, Fanin );
}
return Counter;
}
int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj )
int Acb_NtkNodeRef_rec( Vec_Int_t * vRefs, Acb_Ntk_t * p, int iObj, int nGates[5] )
{
int i, Fanin, * pFanins, Counter = 1;
if ( Acb_ObjIsCi(p, iObj) )
return 0;
if ( nGates )
{
int nFan = Acb_ObjFaninNum(p, iObj);
int Type = Acb_ObjType( p, iObj );
if ( Type == ABC_OPER_CONST_F )
nGates[0]++;
else if ( Type == ABC_OPER_CONST_T )
nGates[1]++;
else if ( Type == ABC_OPER_BIT_BUF || Type == ABC_OPER_CO )
nGates[2]++;
else if ( Type == ABC_OPER_BIT_INV )
nGates[3]++;
else
{
assert( nFan >= 2 );
nGates[4] += Acb_ObjFaninNum(p, iObj)-1;
}
}
Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
{
if ( Vec_IntEntry(vRefs, Fanin) == 0 )
Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin );
Counter += Acb_NtkNodeRef_rec( vRefs, p, Fanin, nGates );
Vec_IntAddToEntry( vRefs, Fanin, 1 );
}
return Counter;
}
int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjs, int nGates[5] )
int Acb_NtkFindMffcSize( Acb_Ntk_t * p, Vec_Int_t * vObjsRefed, Vec_Int_t * vObjsDerefed, int nGates[5] )
{
Vec_Int_t * vRefs = Vec_IntStart( Acb_NtkObjNumMax(p) );
int i, iObj, Fanin, * pFanins, Count1 = 0, Count2 = 0;
int i, iObj, Fanin, * pFanins, Count2 = 0;
Acb_NtkForEachObj( p, iObj )
Acb_ObjForEachFaninFast( p, iObj, pFanins, Fanin, i )
Vec_IntAddToEntry( vRefs, Fanin, 1 );
//Vec_IntForEachEntry( vObjs, iObj, i )
// assert( Vec_IntEntry(vRefs, iObj) > 0 );
Vec_IntForEachEntry( vObjs, iObj, i )
Vec_IntAddToEntry( vRefs, iObj, 1 );
Vec_IntForEachEntry( vObjs, iObj, i )
Count1 += Acb_NtkNodeDeref_rec( vRefs, p, iObj, nGates );
Vec_IntForEachEntry( vObjs, iObj, i )
Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj );
Vec_IntForEachEntry( vObjs, iObj, i )
Vec_IntAddToEntry( vRefs, iObj, -1 );
assert( Count1 == Count2 );
Vec_IntForEachEntry( vObjsRefed, iObj, i )
Acb_NtkNodeRef_rec( vRefs, p, iObj, NULL );
Vec_IntForEachEntry( vObjsDerefed, iObj, i )
if ( Vec_IntEntry(vRefs, iObj) == 0 )
Count2 += Acb_NtkNodeRef_rec( vRefs, p, iObj, nGates );
Vec_IntFree( vRefs );
return Count1;
return Count2;
}
/**Function*************************************************************
......@@ -942,6 +941,63 @@ int Abc_NtkExtract( char * pFileName0, char * pFileName1, int fUseXors, int fVer
SeeAlso []
***********************************************************************/
void Acb_NtkFindNamesInPlaces( char * pBuffer, Vec_Int_t * vPlaces, Vec_Ptr_t * vPivots )
{
int * pCounts = Abc_FrameReadGateCounts();
Vec_Ptr_t * vNames = Vec_PtrAlloc( 100 );
int i, k, iObj, Pos;
for ( i = 0; i < 5; i++ )
pCounts[i] = 0;
Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
{
int nFanins = 0;
char pLocal[1000], * pTemp, * pName, * pSpot;
char * pPivot = (char *)Vec_PtrEntry(vPivots, iObj);
for ( k = 0; k < 1000; k++ )
{
if ( pBuffer[Pos+k] == '\n' )
{
pLocal[k] = 0;
break;
}
else
pLocal[k] = pBuffer[Pos+k];
}
assert( k < 1000 );
pSpot = strstr( pLocal, pPivot );
if ( pSpot == NULL )
{
printf( "Cannot find location of signal \"%s\" in this line.\n", pPivot );
continue;
}
pTemp = strtok( pLocal, " \r\n\t,;()" );
while ( pTemp )
{
if ( !strcmp(pTemp, "1\'b0") )
pCounts[0]++;
else if ( !strcmp(pTemp, "1\'b1") )
pCounts[1]++;
else if ( !strcmp(pTemp, "buf") || !strcmp(pTemp, "assign") )
pCounts[2]++;
else if ( !strcmp(pTemp, "not") )
pCounts[3]++;
else if ( strcmp(pTemp, pPivot) && pTemp > pSpot )
{
nFanins++;
Vec_PtrForEachEntry( char *, vNames, pName, k )
if ( !strcmp(pName, pTemp) )
break;
if ( k == Vec_PtrSize(vNames) )
Vec_PtrPush( vNames, Abc_UtilStrsav(pTemp) );
}
pTemp = strtok( NULL, " \r\n\t,;()" );
}
if ( nFanins > 1 )
pCounts[4] += nFanins-1;
}
//printf( "Found %d names\n", Vec_PtrSize(vNames) );
Abc_FrameSetSignalNames( vNames );
}
Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
{
Vec_Int_t * vPlaces; int First = 1, Pos = -1, fComment = 0;
......@@ -1002,6 +1058,7 @@ void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames,
return;
}
vPlaces = Acb_NtkPlaces( pFileNameIn, vNames );
Acb_NtkFindNamesInPlaces( pBuffer, vPlaces, vNames );
Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
{
for ( k = Prev; k < Pos; k++ )
......
src/base/main/main.h
......@@ -105,6 +105,8 @@ extern ABC_DLL void * Abc_FrameReadManDd();
extern ABC_DLL void * Abc_FrameReadManDec();
extern ABC_DLL void * Abc_FrameReadManDsd();
extern ABC_DLL void * Abc_FrameReadManDsd2();
extern ABC_DLL Vec_Ptr_t * Abc_FrameReadSignalNames();
extern ABC_DLL int * Abc_FrameReadGateCounts();
extern ABC_DLL char * Abc_FrameReadFlag( char * pFlag );
extern ABC_DLL int Abc_FrameIsFlagEnabled( char * pFlag );
......@@ -147,6 +149,7 @@ extern ABC_DLL void Abc_FrameSetCnf( Vec_Int_t * vInv );
extern ABC_DLL void Abc_FrameSetStr( Vec_Str_t * vInv );
extern ABC_DLL void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs );
extern ABC_DLL void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs );
extern ABC_DLL void Abc_FrameSetSignalNames( Vec_Ptr_t * vNames );
extern ABC_DLL int Abc_FrameCheckPoConst( Abc_Frame_t * p, int iPoNum );
......
src/base/main/mainFrame.c
......@@ -67,6 +67,8 @@ void * Abc_FrameReadManDec() { if ( s_GlobalFram
void * Abc_FrameReadManDsd() { return s_GlobalFrame->pManDsd; }
void * Abc_FrameReadManDsd2() { return s_GlobalFrame->pManDsd2; }
char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); }
Vec_Ptr_t * Abc_FrameReadSignalNames() { return s_GlobalFrame->vSignalNames; }
int * Abc_FrameReadGateCounts() { return s_GlobalFrame->pGateCounts; }
int Abc_FrameReadBmcFrames( Abc_Frame_t * p ) { return s_GlobalFrame->nFrames; }
int Abc_FrameReadProbStatus( Abc_Frame_t * p ) { return s_GlobalFrame->Status; }
......@@ -102,6 +104,7 @@ void Abc_FrameSetManDsd2( void * pMan ) { if (s_GlobalFrame
void Abc_FrameSetInv( Vec_Int_t * vInv ) { Vec_IntFreeP(&s_GlobalFrame->pAbcWlcInv); s_GlobalFrame->pAbcWlcInv = vInv; }
void Abc_FrameSetJsonStrs( Abc_Nam_t * pStrs ) { Abc_NamDeref( s_GlobalFrame->pJsonStrs ); s_GlobalFrame->pJsonStrs = pStrs; }
void Abc_FrameSetJsonObjs( Vec_Wec_t * vObjs ) { Vec_WecFreeP(&s_GlobalFrame->vJsonObjs ); s_GlobalFrame->vJsonObjs = vObjs; }
void Abc_FrameSetSignalNames( Vec_Ptr_t * vNames ) { if ( s_GlobalFrame->vSignalNames ) Vec_PtrFreeFree( s_GlobalFrame->vSignalNames ); s_GlobalFrame->vSignalNames = vNames; }
int Abc_FrameIsBatchMode() { return s_GlobalFrame ? s_GlobalFrame->fBatchMode : 0; }
......@@ -231,6 +234,8 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
}
Vec_IntFreeP( &p->vIndFlops );
Vec_PtrFreeP( &p->vLTLProperties_global );
if ( p->vSignalNames )
Vec_PtrFreeFree( p->vSignalNames );
Abc_FrameDeleteAllNetworks( p );
ABC_FREE( p->pDrivingCell );
ABC_FREE( p->pCex2 );
......
src/base/main/mainInt.h
......@@ -133,6 +133,8 @@ struct Abc_Frame_t_
int nFrames; // the number of time frames completed by BMC
Vec_Ptr_t * vPlugInComBinPairs; // pairs of command and its binary name
Vec_Ptr_t * vLTLProperties_global; // related to LTL
Vec_Ptr_t * vSignalNames; // temporary storage for signal names
int pGateCounts[5];// temporary gate counts
void * pSave1;
void * pSave2;
void * pSave3;
......
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