luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changes to several APIs.

This commit is contained in:
Alan Mishchenko 2019-11-03 22:04:14 +02:00
parent 6b2fe00cd8
commit ec1dc44287
8 changed files with 483 additions and 80 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -1255,6 +1255,7 @@ extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVe
extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
extern void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes );
extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves );
extern Vec_Int_t * Gia_ManCollectAndsAll( Gia_Man_t * p );
extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes );
extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
@ -1697,6 +1698,7 @@ extern Vec_Int_t * Gia_ManFirstFanouts( Gia_Man_t * p );
extern int Gia_ManCheckSuppOverlap( Gia_Man_t * p, int iNode1, int iNode2 );
extern int Gia_ManCountPisWithFanout( Gia_Man_t * p );
extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p );
extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p );
/*=== giaCTas.c ===========================================================*/
typedef struct Tas_Man_t_ Tas_Man_t;

20
src/aig/gia/giaDfs.c
View File

@ -141,6 +141,26 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN
}
}
/**Function*************************************************************
Synopsis [Collects support nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManCollectAndsAll( Gia_Man_t * p )
{
Gia_Obj_t * pObj; int i;
Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManAndNum(p) );
Gia_ManForEachAnd( p, pObj, i )
Vec_IntPush( vNodes, i );
return vNodes;
}
/**Function*************************************************************
Synopsis [Counts the support size of the node.]

3
src/aig/gia/giaSim4.c
View File

@ -41,8 +41,9 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
void Gia_Sim4Try( char * pFileName0, char * pFileName1, int fVerbose )
int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose )
{
return 0;
}
////////////////////////////////////////////////////////////////////////

28
src/aig/gia/giaUtil.c
View File

@ -2194,6 +2194,34 @@ int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p )
return Count;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, iLit;
Vec_IntForEachEntry( vCopy, iLit, i )
{
if ( iLit == -1 )
continue;
pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) );
if ( !~pObj->Value )
Vec_IntWriteEntry( vCopy, i, -1 );
else
Vec_IntWriteEntry( vCopy, i, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(iLit)) );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

70
src/base/abci/abc.c
View File

@ -4333,8 +4333,8 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( Abc_NtkNodeNum(pNtk) == 0 || Abc_NtkPiNum(pNtk) == 0 )
{
Abc_Print( -1, "The network does not have internal nodes.\n" );
return 1;
Abc_Print( 0, "The network does not have internal nodes.\n" );
return 0;
}
if ( !Abc_NtkIsLogic(pNtk) )
{
@ -6933,13 +6933,17 @@ usage:
***********************************************************************/
int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Acb_NtkRunEco( char * pFileNames[3], int fVerbose );
int c, fVerbose = 0;
extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
char * pFileNames[4] = {NULL};
int c, fCheck = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -6951,16 +6955,18 @@ int Abc_CommandRunEco( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// pArgvNew = argv + globalUtilOptind;
// nArgcNew = argc - globalUtilOptind;
if ( argc - globalUtilOptind != 3 )
if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 3 )
{
Abc_Print( 1, "Expecting three file names on the command line.\n" );
goto usage;
}
Acb_NtkRunEco( argv + globalUtilOptind, fVerbose );
for ( c = 0; c < argc - globalUtilOptind; c++ )
pFileNames[c] = argv[globalUtilOptind+c];
Acb_NtkRunEco( pFileNames, fCheck, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: runeco <implementation> <specification> <weights> [-vh]\n" );
Abc_Print( -2, "usage: runeco [-cvh] <implementation> <specification> <weights>\n" );
Abc_Print( -2, "\t performs computation of patch functions during ECO,\n" );
Abc_Print( -2, "\t as described in the following paper: A. Q. Dao et al\n" );
Abc_Print( -2, "\t \"Efficient computation of ECO patch functions\", Proc. DAC\'18\n" );
@ -6968,6 +6974,7 @@ usage:
Abc_Print( -2, "\t (currently only applicable to benchmarks from 2017 ICCAD CAD competition\n" );
Abc_Print( -2, "\t http://cad-contest-2017.el.cycu.edu.tw/Problem_A/default.html as follows:\n" );
Abc_Print( -2, "\t \"runeco unit1/F.v unit1/G.v unit1/weight.txt; cec -n out.v unit1/G.v\")\n" );
Abc_Print( -2, "\t-c : toggle checking that the problem has a solution [default = %s]\n", fCheck? "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;
@ -6988,6 +6995,7 @@ usage:
int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Acb_NtkRunGen( char * pFileNames[2], int fVerbose );
char * pFileNames[4] = {NULL};
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
@ -7008,11 +7016,13 @@ int Abc_CommandRunGen( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Expecting two file names on the command line.\n" );
goto usage;
}
Acb_NtkRunGen( argv + globalUtilOptind, fVerbose );
for ( c = 0; c < 2; c++ )
pFileNames[c] = argv[globalUtilOptind+c];
Acb_NtkRunGen( pFileNames, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: rungen <file1> <file2> [-vh]\n" );
Abc_Print( -2, "usage: rungen [-vh] <file1> <file2>\n" );
Abc_Print( -2, "\t experimental command\n" );
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");
@ -7032,13 +7042,28 @@ usage:
***********************************************************************/
int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_Sim4Try( char * pFileName0, char * pFileName1, int fVerbose );
int c, fVerbose = 1;
extern void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose );
char * pFileNames[4] = {NULL, NULL, "out.v", NULL};
int c, fOrder = 0, nWords = 1, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Wovh" ) ) != EOF )
{
switch ( c )
{
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nWords < 0 )
goto usage;
break;
case 'o':
fOrder ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -7048,19 +7073,24 @@ int Abc_CommandRunSim( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( argc - globalUtilOptind != 2 )
if ( argc - globalUtilOptind < 2 || argc - globalUtilOptind > 4 )
{
Abc_Print( 1, "Expecting two file names on the command line.\n" );
Abc_Print( 1, "Expecting two or three file names on the command line.\n" );
goto usage;
}
Gia_Sim4Try( argv[globalUtilOptind+0], argv[globalUtilOptind+1], fVerbose );
Gia_ManRandom(1);
for ( c = 0; c < argc - globalUtilOptind; c++ )
pFileNames[c] = argv[globalUtilOptind+c];
Acb_NtkRunSim( pFileNames, nWords, fOrder, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: runsim <file1> <file2> [-vh]\n" );
Abc_Print( -2, "\t experimental command\n" );
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");
Abc_Print( -2, "usage: runsim [-W] [-ovh] [-N <num>] <file1> <file2> <file3>\n" );
Abc_Print( -2, "\t experimental simulation command\n" );
Abc_Print( -2, "\t-W <num> : the number of words of simulation info [default = %d]\n", nWords );
Abc_Print( -2, "\t-o : toggle using a different node ordering [default = %s]\n", fOrder? "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;
}

6
src/base/acb/acbAbc.c
View File

@ -177,7 +177,7 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
ObjId = Acb_ObjAlloc( pNtk, ABC_OPER_CI, 0, 0 );
Vec_IntWriteEntry( vMap, NameId, ObjId );
Acb_ObjSetName( pNtk, ObjId, NameId );
Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 );
Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 );
}
Ndr_ModForEachTarget( p, Mod, Obj )
{
@ -198,12 +198,14 @@ Acb_Ntk_t * Acb_NtkFromNdr( char * pFileName, void * pModule, Abc_Nam_t * pNames
}
Ndr_ModForEachNode( p, Mod, Obj )
{
//char * pName;
NameId = Ndr_ObjReadBody( p, Obj, NDR_OUTPUT );
//pName = Abc_NamStr( pMan->pStrs, NameId );
ObjId = Vec_IntEntry( vMap, NameId );
nArray = Ndr_ObjReadArray( p, Obj, NDR_INPUT, &pArray );
for ( k = 0; k < nArray; k++ )
Acb_ObjAddFanin( pNtk, ObjId, Vec_IntEntry(vMap, pArray[k]) );
Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 0 );
Acb_ObjSetWeight( pNtk, ObjId, vWeights ? Vec_IntEntry(vWeights, NameId) : 1 );
}
Ndr_ModForEachPo( p, Mod, Obj )
{

136
src/base/acb/acbFunc.c
View File

@ -175,6 +175,14 @@ Abc_Nam_t * Acb_VerilogStartNames()
}
return pNames;
}
void Acb_VerilogRemoveComments ( char * pBuffer )
{
char * pTemp;
for ( pTemp = pBuffer; *pTemp; pTemp++ )
if ( pTemp[0] == '/' && pTemp[1] == '/' )
while ( *pTemp && *pTemp != '\n' )
*pTemp++ = ' ';
}
Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
{
Vec_Int_t * vBuffer = Vec_IntAlloc( 1000 );
@ -182,11 +190,12 @@ Vec_Int_t * Acb_VerilogSimpleLex( char * pFileName, Abc_Nam_t * pNames )
char * pToken;
if ( pBuffer == NULL )
return NULL;
pToken = strtok( pBuffer, " \n\r()," );
Acb_VerilogRemoveComments( pBuffer );
pToken = strtok( pBuffer, " \n\r\t()," );
while ( pToken )
{
Vec_IntPush( vBuffer, Abc_NamStrFindOrAdd(pNames, pToken, NULL) );
pToken = strtok( NULL, " \n\r(),;" );
pToken = strtok( NULL, " \n\r\t(),;" );
}
ABC_FREE( pBuffer );
return vBuffer;
@ -204,7 +213,7 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
Vec_Int_t * vWires = Vec_IntAlloc(100);
Vec_Int_t * vTypes = Vec_IntAlloc(100);
Vec_Int_t * vFanins = Vec_IntAlloc(100);
Vec_Int_t * vCur = NULL;
Vec_Int_t * vCur = NULL;
int i, ModuleID, Token, Size, Count = 0;
assert( Vec_IntEntry(vBuffer, 0) == ACB_MODULE );
Vec_IntForEachEntryStart( vBuffer, Token, i, 2 )
@ -221,9 +230,12 @@ void * Acb_VerilogSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames )
vCur = vWires;
else if ( Token >= ACB_BUF && Token <= ACB_XNOR )
{
char * pToken = Abc_NamStr(pNames, Vec_IntEntry(vBuffer, i+1));
Vec_IntPush( vTypes, Token );
Vec_IntPush( vTypes, Vec_IntSize(vFanins) );
vCur = vFanins;
if ( pToken[1] == 'z' && pToken[2] == '_' && pToken[3] == 'g' && pToken[4] == '_' )
i++;
}
else
Vec_IntPush( vCur, Token );
@ -412,7 +424,7 @@ void Acb_VerilogSimpleWrite( Acb_Ntk_t * p, char * pFileName )
assert( Acb_ObjType(p, iObj) == ABC_OPER_CONST_F || Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
fprintf( pFile, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
fprintf( pFile, " 1\'b%d", Acb_ObjType(p, iObj) == ABC_OPER_CONST_T );
fprintf( pFile, " );" );
fprintf( pFile, " );\n" );
}
fprintf( pFile, "\nendmodule\n\n" );
@ -547,7 +559,7 @@ Vec_Int_t * Acb_NtkFindDivsCis( Acb_Ntk_t * p, Vec_Int_t * vSupp )
printf( "Divisors are %d support variables (CIs in the TFO of the targets).\n", Vec_IntSize(vSupp) );
return vDivs;
}
Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock )
Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBlock, int fVerbose )
{
int fPrintWeights = 0;
int nDivLimit = 3000;
@ -589,8 +601,10 @@ Vec_Int_t * Acb_NtkFindDivs( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Bit_t * vBloc
printf( "%d", (Vec_IntEntry(&p->vObjWeight, iObj) / 1) % 10 );
printf( "\n" );
}
if ( fVerbose )
printf( "Reducing divisor set from %d to ", Vec_IntSize(vDivs) );
Vec_IntShrink( vDivs, nDivLimit );
if ( fVerbose )
printf( "%d.\n", Vec_IntSize(vDivs) );
return vDivs;
}
@ -644,11 +658,15 @@ Vec_Int_t * Acb_NtkFindNodes( Acb_Ntk_t * p, Vec_Int_t * vRoots, Vec_Int_t * vDi
***********************************************************************/
int Acb_ObjToGia( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
{
//char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
int * pFanin, iFanin, k, Type, Res;
assert( !Acb_ObjIsCio(p, iObj) );
Vec_IntClear( vTemp );
Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
{
assert( Acb_ObjCopy(p, iFanin) >= 0 );
Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
}
Type = Acb_ObjType( p, iObj );
if ( Type == ABC_OPER_CONST_F )
return 0;
@ -688,6 +706,7 @@ Gia_Man_t * Acb_NtkToGia( Acb_Ntk_t * p, Vec_Int_t * vSupp, Vec_Int_t * vNodes,
Vec_Int_t * vFanins;
int i, iObj;
pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
Gia_ManHashAlloc( pNew );
Acb_NtkCleanObjCopies( p );
// create primary inputs
@ -1202,7 +1221,14 @@ Vec_Int_t * Acb_DerivePatchSupport( Cnf_Dat_t * pCnf, int iTar, int nTargets, in
if ( TimeOut ) sat_solver_set_runtime_limit( pSat, TimeOut * CLOCKS_PER_SEC + Abc_Clock() );
status = sat_solver_solve( pSat, Vec_IntArray(vSupp), Vec_IntLimit(vSupp), 0, 0, 0, 0 );
if ( TimeOut ) sat_solver_set_runtime_limit( pSat, 0 );
if ( status != l_False )
if ( status == l_True )
{
printf( "ECO does not exist.\n" );
sat_solver_delete( pSat );
Vec_IntFree( vSupp );
return NULL;
}
if ( status == l_Undef )
{
printf( "Support computation timed out after %d sec.\n", TimeOut );
sat_solver_delete( pSat );
@ -1789,12 +1815,12 @@ Vec_Str_t * Acb_GenerateInstance( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t *
{
int i, iObj;
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
Vec_StrAppend( vStr, "patch p0 (" );
Vec_StrAppend( vStr, " patch p0 (" );
Vec_IntForEachEntry( vTars, iObj, i )
Vec_StrPrintF( vStr, "%s .%s(%s)", i ? ",":"", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
Vec_IntForEachEntryInVec( vDivs, vUsed, iObj, i )
Vec_StrPrintF( vStr, ", .%s(%s)", Acb_ObjNameStr(p, iObj), Acb_ObjNameStr(p, iObj) );
Vec_StrAppend( vStr, " );\n" );
Vec_StrAppend( vStr, " );\n\n" );
Vec_StrPush( vStr, '\0' );
return vStr;
}
@ -1880,7 +1906,7 @@ Vec_Str_t * Acb_GeneratePatch( Acb_Ntk_t * p, Vec_Int_t * vDivs, Vec_Int_t * vUs
Vec_StrPrintF( vStr, " %s (", Acb_Oper2Name( ABC_OPER_BIT_BUF ) );
Vec_StrPrintF( vStr, " %s, ", (char *)Vec_PtrEntry(vNames, Vec_IntEntry(vGate, 1)) );
Vec_StrPrintF( vStr, " 1\'b%d", Vec_IntEntry(vGate, 0) == ABC_OPER_CONST_T );
Vec_StrPrintF( vStr, " );" );
Vec_StrPrintF( vStr, " );\n" );
}
}
Vec_StrAppend( vStr, "\nendmodule\n\n" );
@ -1913,28 +1939,23 @@ void Acb_GenerateFilePatch( Vec_Str_t * p, char * pFileNamePatch )
}
void Acb_GenerateFileOut( Vec_Str_t * vPatchLine, char * pFileNameF, char * pFileNameOut, Vec_Str_t * vPatch )
{
char * pBuffer = ABC_ALLOC( char, 10000 );
FILE * pFileIn, * pFileOut;
// input file
pFileIn = fopen( pFileNameF, "rb" );
if ( !pFileIn )
FILE * pFileOut;
char * pBuffer = Extra_FileReadContents( pFileNameF );
if ( pBuffer == NULL )
return;
// output file
pFileOut = fopen( pFileNameOut, "wb" );
if ( !pFileOut )
return;
// copy line by line
while ( fgets(pBuffer, 10000, pFileIn) )
if ( pFileOut )
{
if ( strstr(pBuffer, "endmodule") )
fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
fputs( pBuffer, pFileOut );
char * pTemp = strstr( pBuffer, "endmodule" );
int nFirst = pTemp-pBuffer, nSecond = strlen(pBuffer) - nFirst;
int Value = fwrite( pBuffer, nFirst, 1, pFileOut );
fprintf( pFileOut, "\n%s", Vec_StrArray(vPatchLine) );
Value = fwrite( pBuffer+nFirst, nSecond, 1, pFileOut );
if ( vPatch )
fprintf( pFileOut, "\n%s\n", Vec_StrArray(vPatch) );
}
if ( vPatch )
fprintf( pFileOut, "\n\n%s\n", Vec_StrArray(vPatch) );
fclose( pFileIn );
fclose( pFileOut );
ABC_FREE( pBuffer );
fclose( pFileOut );
}
/**Function*************************************************************
@ -2012,10 +2033,10 @@ Gia_Man_t * Acb_NtkEcoSynthesize( Gia_Man_t * p )
}
return pNew;
}
Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
Cnf_Dat_t * Acb_NtkDeriveMiterCnf( Gia_Man_t * p, int iTar, int nTars, int fVerbose )
{
Gia_Man_t * pCof = Gia_ManDup( p );
Cnf_Dat_t * pCnf; int v, fVerbose = 1;
Cnf_Dat_t * pCnf; int v;
for ( v = 0; v < iTar; v++ )
{
pCof = Gia_ManDupUniv( p = pCof, Gia_ManCiNum(pCof) - nTars + v );
@ -2024,8 +2045,8 @@ Cnf_Dat_t * Acb_NtkEcoCompute( Gia_Man_t * p, int iTar, int nTars )
}
if ( fVerbose ) printf( "M_quo: " );
if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
pCof = Acb_NtkEcoSynthesize( p = pCof );
Gia_ManStop( p );
//pCof = Acb_NtkEcoSynthesize( p = pCof );
//Gia_ManStop( p );
if ( fVerbose ) printf( "M_syn: " );
if ( fVerbose ) Gia_ManPrintStats( pCof, NULL );
if ( 0 && iTar < nTars )
@ -2113,7 +2134,7 @@ Gia_Man_t * Gia_ManInterOneInt( Gia_Man_t * pCof1, Gia_Man_t * pCof0, int Depth
Gia_ManStop( pInter[m] );
return pFinal;
}
Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars )
Gia_Man_t * Acb_NtkDeriveMiterCnfInter2( Gia_Man_t * p, int iTar, int nTars )
{
// extern Gia_Man_t * Gia_ManInterOne( Gia_Man_t * pNtkOn, Gia_Man_t * pNtkOff, int fVerbose );
extern Gia_Man_t * Abc_GiaSynthesizeInter( Gia_Man_t * p );
@ -2154,7 +2175,7 @@ Gia_Man_t * Acb_NtkEcoComputeInter2( Gia_Man_t * p, int iTar, int nTars )
//Gia_ManPrintStats( pInter, NULL );
return pInter;
}
Gia_Man_t * Acb_NtkEcoComputeInter( Gia_Man_t * p, int iTar, int nTars )
Gia_Man_t * Acb_NtkDeriveMiterCnfInter( Gia_Man_t * p, int iTar, int nTars )
{
Gia_Man_t * pCof1, * pCof = Gia_ManDup( p ); int v;
for ( v = 0; v < iTar; v++ )
@ -2271,7 +2292,7 @@ Vec_Ptr_t * Acb_TransformPatchFunctions( Vec_Ptr_t * vSops, Vec_Wec_t * vSupps,
SeeAlso []
***********************************************************************/
int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF, int fCisOnly )
int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileName[4], int fCisOnly, int fCheck, int fVerbose )
{
extern Gia_Man_t * Abc_SopSynthesizeOne( char * pSop, int fClp );
@ -2286,7 +2307,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
Vec_Int_t * vSuppF = Acb_NtkFindSupp( pNtkF, vRoots );
Vec_Int_t * vSuppG = Acb_NtkFindSupp( pNtkG, vRoots );
Vec_Int_t * vSupp = Vec_IntTwoMerge( vSuppF, vSuppG );
Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock );
Vec_Int_t * vDivs = fCisOnly ? Acb_NtkFindDivsCis( pNtkF, vSupp ) : Acb_NtkFindDivs( pNtkF, vSupp, vBlock, fVerbose );
Vec_Int_t * vNodesF = Acb_NtkFindNodes( pNtkF, vRoots, vDivs );
Vec_Int_t * vNodesG = Acb_NtkFindNodes( pNtkG, vRoots, NULL );
@ -2309,21 +2330,24 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
char * pSop = NULL;
int i, Res;
printf( "The number of targets = %d.\n", nTargets );
if ( fVerbose )
{
printf( "The number of targets = %d.\n", nTargets );
printf( "NtkF: " );
Gia_ManPrintStats( pGiaF, NULL );
printf( "NtkG: " );
Gia_ManPrintStats( pGiaG, NULL );
printf( "Miter: " );
Gia_ManPrintStats( pGiaM, NULL );
printf( "NtkF: " );
Gia_ManPrintStats( pGiaF, NULL );
printf( "NtkG: " );
Gia_ManPrintStats( pGiaG, NULL );
printf( "Miter: " );
Gia_ManPrintStats( pGiaM, NULL );
}
// check that the problem has a solution
if ( 0 )//fCisOnly )
if ( fCheck )//fCisOnly )
{
int Lit, status;
sat_solver * pSat;
pCnf = Acb_NtkEcoCompute( pGiaM, nTargets, nTargets );
pCnf = Acb_NtkDeriveMiterCnf( pGiaM, nTargets, nTargets, fVerbose );
pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Cnf_DataFree( pCnf );
// add output clause
@ -2350,7 +2374,7 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
vSupp = Vec_IntStartNatural( Vec_IntSize(vDivs) );
printf( "Target %d has support with %d variables.\n", i, Vec_IntSize(vSupp) );
pOne = Acb_NtkEcoComputeInter( pGiaM, i, nTargets );
pOne = Acb_NtkDeriveMiterCnfInter( pGiaM, i, nTargets );
printf( "Tar%02d: ", i );
Gia_ManPrintStats( pOne, NULL );
@ -2363,12 +2387,11 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
}
else
{
pCnf = Acb_NtkEcoCompute( pGiaM, i, nTargets );
pCnf = Acb_NtkDeriveMiterCnf( pGiaM, i, nTargets, fVerbose );
// vSupp = Acb_DerivePatchSupportS( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, NULL, TimeOut );
vSupp = Acb_DerivePatchSupport( pCnf, i, nTargets, Vec_IntSize(vDivs), vDivs, pNtkF, vSuppOld, TimeOut );
if ( vSupp == NULL )
{
Vec_IntFree( vSuppOld );
Cnf_DataFree( pCnf );
RetValue = 0;
goto cleanup;
@ -2383,7 +2406,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
Cnf_DataFree( pCnf );
if ( pSop == NULL )
{
Vec_IntFree( vSuppOld );
RetValue = 0;
goto cleanup;
}
@ -2405,7 +2427,6 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
Vec_IntAppend( Vec_WecPushLevel(vSupps), vSupp );
Vec_IntFree( vSupp );
}
Vec_IntFree( vSuppOld );
// make sure the function is UNSAT
printf( "\n" );
@ -2443,8 +2464,9 @@ int Acb_NtkEcoPerform( Acb_Ntk_t * pNtkF, Acb_Ntk_t * pNtkG, char * pFileNameF,
Acb_PrintPatch( pNtkF, vDivs, vUsed, clk );
// generate output files
Acb_GenerateFilePatch( vPatch, "patch.v" );
Acb_GenerateFileOut( vInst, pFileNameF, "out.v", vPatch );
if ( pFileName[3] == NULL ) Acb_GenerateFilePatch( vPatch, "patch.v" );
Acb_GenerateFileOut( vInst, pFileName[0], pFileName[3] ? pFileName[3] : "out.v", vPatch );
printf( "Finished dumping resulting file \"%s\".\n\n", pFileName[3] ? pFileName[3] : "out.v" );
//Gia_AigerWrite( pGiaG, "test.aig", 0, 0, 0 );
cleanup:
// cleanup
@ -2460,9 +2482,9 @@ cleanup:
Vec_PtrFreeFree( vSops );
Vec_WecFree( vSupps );
if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
Vec_IntFree( vSuppOld );
Vec_IntFreeP( &vUsed );
if ( vFuncs ) Vec_PtrFreeFree( vFuncs );
Gia_ManStop( pGiaF );
Gia_ManStop( pGiaG );
@ -2511,7 +2533,7 @@ void Acb_NtkTestRun2( char * pFileNames[3], int fVerbose )
SeeAlso []
***********************************************************************/
void Acb_NtkRunEco( char * pFileNames[3], int fVerbose )
void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose )
{
Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileNames[0], pFileNames[2] );
Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileNames[1], NULL );
@ -2528,11 +2550,11 @@ void Acb_NtkRunEco( char * pFileNames[3], int fVerbose )
Acb_IntallLibrary();
if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 0 ) )
if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 0, fCheck, fVerbose ) )
{
printf( "General ECO computation timed out. Trying inputs only.\n\n" );
if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames[0], 1 ) )
printf( "Input-only ECO computation also timed out.\n\n" );
printf( "General computation timed out. Trying inputs only.\n\n" );
if ( !Acb_NtkEcoPerform( pNtkF, pNtkG, pFileNames, 1, fCheck, fVerbose ) )
printf( "Input-only computation also timed out.\n\n" );
}
Acb_ManFree( pNtkF->pDesign );

298
src/base/acb/acbUtil.c
View File

@ -470,6 +470,304 @@ void Acb_NtkUpdateNode( Acb_Ntk_t * p, int Pivot, word uTruth, Vec_Int_t * vSupp
Vec_IntClear( &p->vSuppOld );
}
/**Function*************************************************************
Synopsis [Derive AIG for one network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkFindNodes2_rec( Acb_Ntk_t * p, int iObj, Vec_Int_t * vNodes )
{
int * pFanin, iFanin, i;
if ( Acb_ObjSetTravIdCur(p, iObj) )
return;
if ( Acb_ObjIsCi(p, iObj) )
return;
Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, i )
Acb_NtkFindNodes2_rec( p, iFanin, vNodes );
assert( !Acb_ObjIsCo(p, iObj) );
Vec_IntPush( vNodes, iObj );
}
Vec_Int_t * Acb_NtkFindNodes2( Acb_Ntk_t * p )
{
int i, iObj;
Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
Acb_NtkIncTravId( p );
Acb_NtkForEachCo( p, iObj, i )
Acb_NtkFindNodes2_rec( p, Acb_ObjFanin(p, iObj, 0), vNodes );
return vNodes;
}
int Acb_ObjToGia2( Gia_Man_t * pNew, Acb_Ntk_t * p, int iObj, Vec_Int_t * vTemp )
{
//char * pName = Abc_NamStr( p->pDesign->pStrs, Acb_ObjName(p, iObj) );
int * pFanin, iFanin, k, Type, Res;
assert( !Acb_ObjIsCio(p, iObj) );
Vec_IntClear( vTemp );
Acb_ObjForEachFaninFast( p, iObj, pFanin, iFanin, k )
{
assert( Acb_ObjCopy(p, iFanin) >= 0 );
Vec_IntPush( vTemp, Acb_ObjCopy(p, iFanin) );
}
Type = Acb_ObjType( p, iObj );
if ( Type == ABC_OPER_CONST_F )
return 0;
if ( Type == ABC_OPER_CONST_T )
return 1;
if ( Type == ABC_OPER_BIT_BUF )
return Vec_IntEntry(vTemp, 0);
if ( Type == ABC_OPER_BIT_INV )
return Abc_LitNot( Vec_IntEntry(vTemp, 0) );
if ( Type == ABC_OPER_BIT_AND || Type == ABC_OPER_BIT_NAND )
{
Res = 1;
Vec_IntForEachEntry( vTemp, iFanin, k )
Res = Gia_ManAppendAnd2( pNew, Res, iFanin );
return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NAND );
}
if ( Type == ABC_OPER_BIT_OR || Type == ABC_OPER_BIT_NOR )
{
Res = 0;
Vec_IntForEachEntry( vTemp, iFanin, k )
Res = Gia_ManAppendOr2( pNew, Res, iFanin );
return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NOR );
}
if ( Type == ABC_OPER_BIT_XOR || Type == ABC_OPER_BIT_NXOR )
{
Res = 0;
Vec_IntForEachEntry( vTemp, iFanin, k )
Res = Gia_ManAppendXor2( pNew, Res, iFanin );
return Abc_LitNotCond( Res, Type == ABC_OPER_BIT_NXOR );
}
assert( 0 );
return -1;
}
Gia_Man_t * Acb_NtkToGia2( Acb_Ntk_t * p )
{
Gia_Man_t * pNew, * pOne;
Vec_Int_t * vFanins, * vNodes;
int i, iObj;
pNew = Gia_ManStart( 2 * Acb_NtkObjNum(p) + 1000 );
pNew->pName = Abc_UtilStrsav(Acb_NtkName(p));
Acb_NtkCleanObjCopies( p );
Acb_NtkForEachCi( p, iObj, i )
Acb_ObjSetCopy( p, iObj, Gia_ManAppendCi(pNew) );
vFanins = Vec_IntAlloc( 4 );
vNodes = Acb_NtkFindNodes2( p );
Vec_IntForEachEntry( vNodes, iObj, i )
Acb_ObjSetCopy( p, iObj, Acb_ObjToGia2(pNew, p, iObj, vFanins) );
Vec_IntFree( vNodes );
Vec_IntFree( vFanins );
Acb_NtkForEachCo( p, iObj, i )
Gia_ManAppendCo( pNew, Acb_ObjCopy(p, Acb_ObjFanin(p, iObj, 0)) );
pNew = Gia_ManCleanup( pOne = pNew );
Gia_ManUpdateCopy( &p->vObjCopy, pOne );
Gia_ManStop( pOne );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkCollectCopies( Acb_Ntk_t * p, Gia_Man_t * pGia, Vec_Ptr_t ** pvNodesR )
{
int i, iObj, iLit;
Vec_Int_t * vObjs = Acb_NtkFindNodes2( p );
Vec_Int_t * vNodes = Vec_IntAlloc( Acb_NtkObjNum(p) );
Vec_Ptr_t * vNodesR = Vec_PtrStart( Gia_ManObjNum(pGia) );
Vec_IntForEachEntry( vObjs, iObj, i )
if ( (iLit = Acb_ObjCopy(p, iObj)) >= 0 && Gia_ObjIsAnd(Gia_ManObj(pGia, Abc_Lit2Var(iLit))) )
{
if ( Vec_PtrEntry(vNodesR, Abc_Lit2Var(iLit)) == NULL )
{
Vec_PtrWriteEntry( vNodesR, Abc_Lit2Var(iLit), Abc_UtilStrsav(Acb_ObjNameStr(p, iObj)) );
Vec_IntPush( vNodes, Abc_Lit2Var(iLit) );
}
}
Vec_IntFree( vObjs );
Vec_IntSort( vNodes, 0 );
*pvNodesR = vNodesR;
return vNodes;
}
Vec_Int_t * Acb_NtkCollectUser( Acb_Ntk_t * p, Vec_Ptr_t * vUser )
{
char * pTemp; int i;
Vec_Int_t * vRes = Vec_IntAlloc( Vec_PtrSize(vUser) );
Vec_Int_t * vMap = Vec_IntStart( Abc_NamObjNumMax(Acb_NtkNam(p)) );
Acb_NtkForEachNode( p, i )
if ( Acb_ObjName(p, i) > 0 )
Vec_IntWriteEntry( vMap, Acb_ObjName(p, i), Acb_ObjCopy(p, i) );
Vec_PtrForEachEntry( char *, vUser, pTemp, i )
if ( Acb_NtkStrId(p, pTemp) < Vec_IntSize(vMap) )
{
int iLit = Vec_IntEntry( vMap, Acb_NtkStrId(p, pTemp) );
assert( iLit > 0 );
//printf( "Obj = %3d Name = %3d Copy = %3d\n", i, Acb_NtkStrId(p, pTemp), iLit );
Vec_IntPush( vRes, Abc_Lit2Var(iLit) );
}
assert( Vec_IntSize(vRes) == Vec_PtrSize(vUser) );
Vec_IntFree( vMap );
Vec_IntUniqify( vRes );
return vRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acb_NtkExtract( char * pFileName0, char * pFileName1, int fVerbose,
Gia_Man_t ** ppGiaF, Gia_Man_t ** ppGiaG, Vec_Int_t ** pvNodes, Vec_Ptr_t ** pvNodesR )
{
extern Acb_Ntk_t * Acb_VerilogSimpleRead( char * pFileName, char * pFileNameW );
Acb_Ntk_t * pNtkF = Acb_VerilogSimpleRead( pFileName0, NULL );
Acb_Ntk_t * pNtkG = Acb_VerilogSimpleRead( pFileName1, NULL );
int RetValue = 0;
if ( pNtkF && pNtkG )
{
Gia_Man_t * pGiaF = Acb_NtkToGia2( pNtkF );
Gia_Man_t * pGiaG = Acb_NtkToGia2( pNtkG );
assert( Acb_NtkCiNum(pNtkF) == Acb_NtkCiNum(pNtkG) );
assert( Acb_NtkCoNum(pNtkF) == Acb_NtkCoNum(pNtkG) );
*ppGiaF = pGiaF;
*ppGiaG = pGiaG;
*pvNodes = Acb_NtkCollectCopies( pNtkF, pGiaF, pvNodesR );
RetValue = 1;
}
if ( pNtkF->pDesign ) Acb_ManFree( pNtkF->pDesign );
if ( pNtkG->pDesign ) Acb_ManFree( pNtkG->pDesign );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Acb_NtkPlaces( char * pFileName, Vec_Ptr_t * vNames )
{
Vec_Int_t * vPlaces; int First = 1, Pos = -1;
char * pTemp, * pBuffer = Extra_FileReadContents( pFileName );
char * pLimit = pBuffer + strlen(pBuffer);
if ( pBuffer == NULL )
return NULL;
vPlaces = Vec_IntAlloc( Vec_PtrSize(vNames) );
for ( pTemp = pBuffer; *pTemp; pTemp++ )
{
if ( *pTemp == '\n' )
Pos = pTemp - pBuffer + 1;
else if ( *pTemp == '(' )
{
if ( First )
First = 0;
else
{
char * pToken = strtok( pTemp+1, " \n\r\t" );
char * pName; int i;
Vec_PtrForEachEntry( char *, vNames, pName, i )
if ( !strcmp(pName, pToken) )
Vec_IntPushTwo( vPlaces, Pos, i );
pTemp = pToken + strlen(pToken);
while ( *pTemp == 0 )
pTemp++;
assert( pTemp < pLimit );
}
}
}
assert( Vec_IntSize(vPlaces) == 2*Vec_PtrSize(vNames) );
ABC_FREE( pBuffer );
return vPlaces;
}
void Acb_NtkInsert( char * pFileNameIn, char * pFileNameOut, Vec_Ptr_t * vNames )
{
int i, k, Prev = 0, Pos, Pos2, iObj;
Vec_Int_t * vPlaces;
char * pName, * pBuffer;
FILE * pFile = fopen( pFileNameOut, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open output file \"%s\".\n", pFileNameOut );
return;
}
pBuffer = Extra_FileReadContents( pFileNameIn );
if ( pBuffer == NULL )
{
fclose( pFile );
printf( "Cannot open input file \"%s\".\n", pFileNameIn );
return;
}
vPlaces = Acb_NtkPlaces( pFileNameIn, vNames );
Vec_IntForEachEntryDouble( vPlaces, Pos, iObj, i )
{
for ( k = Prev; k < Pos; k++ )
fputc( pBuffer[k], pFile );
fprintf( pFile, "// [t_%d = %s] //", iObj, (char *)Vec_PtrEntry(vNames, iObj) );
Prev = Pos;
}
Vec_IntFree( vPlaces );
pName = strstr(pBuffer, "endmodule");
Pos2 = pName - pBuffer;
for ( k = Prev; k < Pos2; k++ )
fputc( pBuffer[k], pFile );
fprintf( pFile, "\n\n" );
fprintf( pFile, " wire " );
Vec_PtrForEachEntry( char *, vNames, pName, i )
fprintf( pFile, " t_%d%s", i, i==Vec_PtrSize(vNames)-1 ? ";" : "," );
fprintf( pFile, "\n\n" );
Vec_PtrForEachEntry( char *, vNames, pName, i )
fprintf( pFile, " buf( %s, t_%d );\n", pName, i );
fprintf( pFile, "\n" );
for ( k = Pos2; pBuffer[k]; k++ )
fputc( pBuffer[k], pFile );
ABC_FREE( pBuffer );
fclose( pFile );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acb_NtkRunSim( char * pFileName[4], int nWords, int fOrder, int fVerbose )
{
extern int Gia_Sim4Try( char * pFileName0, char * pFileName1, char * pFileName2, int nWords, int fOrder, int fVerbose );
extern void Acb_NtkRunEco( char * pFileNames[4], int fCheck, int fVerbose );
char * pFileNames[4] = { pFileName[2], pFileName[1], NULL, pFileName[2] };
if ( Gia_Sim4Try( pFileName[0], pFileName[1], pFileName[2], nWords, fOrder, fVerbose ) )
Acb_NtkRunEco( pFileNames, 0, fVerbose );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////