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

Version abc80205

This commit is contained in:
Alan Mishchenko 2008-02-05 08:01:00 -08:00
parent 3b790eb17e
commit 7174787aba
29 changed files with 4800 additions and 91 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
abc.dsp
View File

@ -1626,14 +1626,26 @@ SOURCE=.\src\opt\mfs\mfsCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsDiv.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsInter.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsResub.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\mfs\mfsSat.c
# End Source File
# Begin Source File

1201
abc.plg Normal file
View File

File diff suppressed because it is too large Load Diff

2208
abclib.plg Normal file
View File

File diff suppressed because it is too large Load Diff

32
abctestlib.plg Normal file
View File

@ -0,0 +1,32 @@
<html>
<body>
<pre>
<h1>Build Log</h1>
<h3>
--------------------Configuration: abctestlib - Win32 Release--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B8.tmp" with contents
[
/nologo /ML /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /Fp"Release/abctestlib.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c
"C:\_projects\abc\demo.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B8.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B9.tmp" with contents
[
kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib C:\_projects\abc\abclib\abclib_release.lib /nologo /subsystem:console /incremental:no /pdb:"Release/abctestlib.pdb" /machine:I386 /out:"_TEST/abctestlib.exe"
.\Release\demo.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP20B9.tmp"
<h3>Output Window</h3>
Compiling...
demo.c
Linking...
<h3>Results</h3>
abctestlib.exe - 0 error(s), 0 warning(s)
</pre>
</body>
</html>

1
src/aig/aig/aig.h
View File

@ -471,6 +471,7 @@ extern Aig_Man_t * Aig_ManStart( int nNodesMax );
extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p );
extern Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj );
extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered );
extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p );
extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
extern void Aig_ManStop( Aig_Man_t * p );
extern int Aig_ManCleanup( Aig_Man_t * p );

34
src/aig/aig/aigMan.c
View File

@ -215,6 +215,40 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates the AIG manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj;
int i;
// create the new manager
pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
pNew->pName = Aig_UtilStrsav( p->pName );
// create the PIs
Aig_ManCleanData( p );
Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
Aig_ManForEachPi( p, pObj, i )
pObj->pData = Aig_ObjCreatePi( pNew );
// duplicate internal nodes
Aig_ManForEachObj( p, pObj, i )
{
assert( !Aig_ObjIsBuf(pObj) );
if ( Aig_ObjIsNode(pObj) )
pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
}
return pNew;
}
/**Function*************************************************************
Synopsis [Extracts the miter composed of XOR of the two nodes.]

78
src/aig/fra/fraClaus.c
View File

@ -1494,6 +1494,79 @@ void Fra_ClausPrintIndClauses( Clu_Man_t * p )
printf( "\n" );
}
/**Function*************************************************************
Synopsis [Writes the clauses into an AIGER file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
{
Aig_Obj_t * pLiteral;
int NodeId = pVar2Id[ lit_var(Lit) ];
assert( NodeId >= 0 );
pLiteral = Aig_ManObj( p->pAig, NodeId )->pData;
return Aig_NotCond( pLiteral, lit_sign(Lit) );
}
/**Function*************************************************************
Synopsis [Writes the clauses into an AIGER file.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_ClausWriteIndClauses( Clu_Man_t * p )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
Aig_Man_t * pNew;
Aig_Obj_t * pClause, * pLiteral;
char Buffer[500];
int * pStart, * pVar2Id;
int Beg, End, i, k;
// create mapping from SAT vars to node IDs
pVar2Id = ALLOC( int, p->pCnf->nVars );
memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
if ( p->pCnf->pVarNums[i] >= 0 )
{
assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
pVar2Id[ p->pCnf->pVarNums[i] ] = i;
}
// start the manager
pNew = Aig_ManDupWithoutPos( p->pAig );
// add the clauses
Beg = 0;
pStart = Vec_IntArray( p->vLitsProven );
Vec_IntForEachEntry( p->vClausesProven, End, i )
{
pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
for ( k = Beg + 1; k < End; k++ )
{
pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
pClause = Aig_Or( pNew, pClause, pLiteral );
}
Aig_ObjCreatePo( pNew, pClause );
Beg = End;
}
free( pVar2Id );
Aig_ManCleanup( pNew );
// write the manager into a file
sprintf( Buffer, "%s_care.aig", p->pAig->pName );
printf( "Care clauses are written into file \"%s\".\n", Buffer );
Ioa_WriteAiger( pNew, Buffer, 0, 1 );
Aig_ManStop( pNew );
}
/**Function*************************************************************
Synopsis [Checks if the clause holds using the given simulation info.]
@ -1751,6 +1824,11 @@ clk = clock();
Fra_ClausPrintIndClauses( p );
Fra_ClausEstimateCoverage( p );
}
if ( !p->fTarget )
{
Fra_ClausWriteIndClauses( p );
}
/*
// print the statistic into a file
{

13
src/aig/fra/fraHot.c
View File

@ -395,25 +395,28 @@ Aig_Man_t * Fra_OneHotCreateExdc( Fra_Man_t * p, Vec_Int_t * vOneHots )
{
Aig_Man_t * pNew;
Aig_Obj_t * pObj1, * pObj2, * pObj;
int i, Out1, Out2;
int i, Out1, Out2, nTruePis;
pNew = Aig_ManStart( Vec_IntSize(vOneHots)/2 );
for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
// for ( i = 0; i < Aig_ManRegNum(p->pManAig); i++ )
// Aig_ObjCreatePi(pNew);
Aig_ManForEachPi( p->pManAig, pObj, i )
Aig_ObjCreatePi(pNew);
nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
for ( i = 0; i < Vec_IntSize(vOneHots); i += 2 )
{
Out1 = Vec_IntEntry( vOneHots, i );
Out2 = Vec_IntEntry( vOneHots, i+1 );
if ( Out1 == 0 && Out2 == 0 )
continue;
pObj1 = Aig_ManPi( pNew, Fra_LitReg(Out1) );
pObj2 = Aig_ManPi( pNew, Fra_LitReg(Out2) );
pObj1 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out1) );
pObj2 = Aig_ManPi( pNew, nTruePis + Fra_LitReg(Out2) );
pObj1 = Aig_NotCond( pObj1, Fra_LitSign(Out1) );
pObj2 = Aig_NotCond( pObj2, Fra_LitSign(Out2) );
pObj = Aig_Or( pNew, pObj1, pObj2 );
Aig_ObjCreatePo( pNew, pObj );
}
Aig_ManCleanup(pNew);
printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
// printf( "Created AIG with %d nodes and %d outputs.\n", Aig_ManNodeNum(pNew), Aig_ManPoNum(pNew) );
return pNew;
}

10
src/aig/fra/fraInd.c
View File

@ -470,8 +470,16 @@ clk2 = clock();
clk2 = clock();
if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
{
extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
char Buffer[500];
Aig_Man_t * pNew;
pManAigNew = Aig_ManDup( pManAig, 1 );
pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
// pManAigNew->pManExdc = Fra_OneHotCreateExdc( p, p->vOneHots );
pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
sprintf( Buffer, "%s_care.aig", p->pManAig->pName );
printf( "Care one-hotness clauses are written into file \"%s\".\n", Buffer );
Ioa_WriteAiger( pNew, Buffer, 0, 1 );
Aig_ManStop( pNew );
}
else
{

2
src/base/abc/abc.h
View File

@ -199,7 +199,7 @@ struct Abc_Ntk_t_
int * pModel; // counter-example (for miters)
void * pSeqModel; // counter-example (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pManExdc; // the EXDC network (if given)
void * pExcare; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy;
Hop_Man_t * pHaig; // history AIG

2
src/base/abc/abcDfs.c
View File

@ -677,7 +677,7 @@ void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
// mark the node as visited
Abc_NodeSetTravIdCurrent( pNode );
// collect the CI
if ( Abc_ObjIsCi(pNode) || Abc_ObjFaninNum(pNode) == 0 )
if ( Abc_ObjIsCi(pNode) )//|| Abc_ObjFaninNum(pNode) == 0 )
{
Vec_PtrPush( vNodes, pNode );
return;

13
src/base/abc/abcNtk.c
View File

@ -23,8 +23,6 @@
#include "main.h"
#include "mio.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@ -348,8 +346,8 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
// duplicate the EXDC Ntk
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
if ( pNtk->pManExdc )
pNtkNew->pManExdc = Aig_ManDup( pNtk->pManExdc, 0 );
if ( pNtk->pExcare )
pNtkNew->pExcare = Abc_NtkDup( pNtk->pExcare );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" );
pNtk->pCopy = pNtkNew;
@ -941,11 +939,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
// free EXDC Ntk
if ( pNtk->pExdc )
Abc_NtkDelete( pNtk->pExdc );
if ( pNtk->pManExdc )
{
Aig_ManStop( pNtk->pManExdc );
pNtk->pManExdc = NULL;
}
if ( pNtk->pExcare )
Abc_NtkDelete( pNtk->pExcare );
// dereference the BDDs
if ( Abc_NtkHasBdd(pNtk) )
{

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

@ -101,6 +101,7 @@ static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCareSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -280,6 +281,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 );
Cmd_CommandAdd( pAbc, "Various", "care_set", Abc_CommandCareSet, 1 );
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 );
Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 );
@ -3257,14 +3259,18 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nGrowthLevel = 0;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nDepthMax = 20;
pPars->nDivMax = 200;
pPars->nWinSizeMax = 300;
pPars->nGrowthLevel = 0;
pPars->fResub = 1;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WFLavwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLravwh" ) ) != EOF )
{
switch ( c )
{
@ -3276,7 +3282,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->nWinTfoLevs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinTfoLevs < 1 || pPars->nWinTfoLevs > 99 )
if ( pPars->nWinTfoLevs < 0 )
goto usage;
break;
case 'F':
@ -3290,6 +3296,28 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nFanoutsMax < 1 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
pPars->nDepthMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nDepthMax < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nWinSizeMax < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
@ -3301,6 +3329,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nGrowthLevel < 0 || pPars->nGrowthLevel > ABC_INFINITY )
goto usage;
break;
case 'r':
pPars->fResub ^= 1;
break;
case 'a':
pPars->fArea ^= 1;
break;
@ -3337,14 +3368,17 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: mfs [-W <num>] [-F <num>] [-L <num>] [-vh]\n" );
fprintf( pErr, "usage: mfs [-WFDML <num>] [-arvh]\n" );
fprintf( pErr, "\t performs don't-care-based optimization of logic networks\n" );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= NM <= 100) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= n) [default = %d]\n", pPars->nFanoutsMax );
fprintf( pErr, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs );
fprintf( pErr, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax );
fprintf( pErr, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
fprintf( pErr, "\t-M <num> : the max size of window to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
fprintf( pErr, "\t-L <num> : the largest increase in node level after resynthesis (0 <= num) [default = %d]\n", pPars->nGrowthLevel );
// fprintf( pErr, "\t-a : toggle optimization for area only [default = %s]\n", pPars->fArea? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
// fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-a : toggle minimizing area or edges [default = %s]\n", pPars->fArea? "area": "edges" );
fprintf( pErr, "\t-r : toggle resubstitution and dc-minimization [default = %s]\n", pPars->fResub? "resub": "dc-min" );
fprintf( pErr, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
fprintf( pErr, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@ -5739,6 +5773,93 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandCareSet( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr, * pFile;
Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
char * FileName;
int c;
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( argc != globalUtilOptind + 1 )
{
goto usage;
}
// get the input file name
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
fprintf( pAbc->Err, "\n" );
return 1;
}
fclose( pFile );
// set the new network
pNtkNew = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
if ( pNtkNew == NULL )
{
fprintf( pAbc->Err, "Reading network from file has failed.\n" );
return 1;
}
// replace the EXDC
if ( pNtk->pExcare )
{
Abc_NtkDelete( pNtk->pExcare );
pNtk->pExcare = NULL;
}
pNtkRes = Abc_NtkDup( pNtk );
pNtkRes->pExcare = pNtkNew;
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
fprintf( pErr, "usage: care_set [-h] <file>\n" );
fprintf( pErr, "\t sets the network from file as a care for the current network\n" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t<file> : file with the new care network\n");
return 1;
}
/**Function*************************************************************
Synopsis []

5
src/base/abci/abcDar.c
View File

@ -184,11 +184,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
}
if ( pMan->pManExdc )
{
pNtkNew->pManExdc = pMan->pManExdc;
pMan->pManExdc = NULL;
}
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
return pNtkNew;

2
src/base/abci/abcIf.c
View File

@ -21,6 +21,7 @@
#include "abc.h"
#include "if.h"
#include "kit.h"
#include "aig.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@ -87,7 +88,6 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
// duplicate EXDC
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{

0
src/map/pcm/module.make
View File

0
src/map/ply/module.make
View File

6
src/opt/mfs/mfs.h
View File

@ -43,7 +43,11 @@ struct Mfs_Par_t_
// general parameters
int nWinTfoLevs; // the maximum fanout levels
int nFanoutsMax; // the maximum number of fanouts
int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis
int nDepthMax; // the maximum number of logic levels
int nDivMax; // the maximum number of divisors
int nWinSizeMax; // the maximum size of the window
int nGrowthLevel; // the maximum allowed growth in level
int fResub; // performs resubstitution
int fArea; // performs optimization for area
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats

116
src/opt/mfs/mfsCore.c
View File

@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Synopsis [Core procedures of this package.]
Author [Alan Mishchenko]
@ -28,6 +28,60 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
int clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
clk = clock();
p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
p->timeWin += clock() - clk;
if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
return 1;
// compute the divisors of the window
clk = clock();
p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
p->timeDiv += clock() - clk;
// construct AIG for the window
clk = clock();
p->pAigWin = Abc_NtkConstructAig( p, pNode );
p->timeAig += clock() - clk;
// translate it into CNF
clk = clock();
p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
p->timeCnf += clock() - clk;
// create the SAT problem
clk = clock();
p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
if ( p->pSat == NULL )
{
p->nNodesBad++;
return 1;
}
// solve the SAT problem
if ( p->pPars->fArea )
Abc_NtkMfsResubArea( p, pNode );
else
Abc_NtkMfsResubEdge( p, pNode );
p->timeSat += clock() - clk;
return 1;
}
/**Function*************************************************************
Synopsis []
@ -42,6 +96,7 @@
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
int clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
@ -80,9 +135,14 @@ p->timeSat += clock() - clk;
***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
int i, Counter;
int i, clk = clock();
int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
assert( Abc_NtkIsLogic(pNtk) );
if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
if ( pNtk->pManExdc != NULL )
printf( "Performing don't-care computation with don't-cares.\n" );
// start the manager
p = Mfs_ManAlloc();
p->pPars = pPars;
p = Mfs_ManAlloc( pPars );
p->pNtk = pNtk;
p->pCare = pNtk->pManExdc;
if ( pNtk->pExcare )
{
Abc_Ntk_t * pTemp;
pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
p->pCare = Abc_NtkToDar( pTemp, 0 );
Abc_NtkDelete( pTemp );
}
if ( pPars->fVerbose )
{
if ( p->pCare != NULL )
printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
else
printf( "Performing optimization without constraints.\n" );
}
if ( !pPars->fResub )
printf( "Currently don't-cares are not used but the stats are printed.\n" );
// label the register outputs
if ( p->pCare )
{
Counter = 1;
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjFaninNum(pObj) == 0 )
pObj->pData = NULL;
else
pObj->pData = (void *)Counter++;
assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
pObj->pData = (void *)i;
}
// compute levels
Abc_NtkLevel( pNtk );
Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// compute don't-cares for each node
p->nTotalNodesBeg = nTotalNodesBeg;
p->nTotalEdgesBeg = nTotalEdgesBeg;
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
Abc_NtkMfsNode( p, pObj );
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
else
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
// undo labesl
if ( p->pCare )
@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
}
// free the manager
p->timeTotal = clock() - clk;
Mfs_ManStop( p );
return 1;
}

303
src/opt/mfs/mfsDiv.c Normal file
View File

@ -0,0 +1,303 @@
/**CFile****************************************************************
FileName [mfsDiv.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Procedures to compute candidate divisors.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Marks and collects the TFI cone of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MfsWinMarkTfi_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vCone )
{
Abc_Obj_t * pFanin;
int i;
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
Abc_NodeSetTravIdCurrent( pObj );
if ( Abc_ObjIsCi(pObj) )
{
Vec_PtrPush( vCone, pObj );
return;
}
assert( Abc_ObjIsNode(pObj) );
// visit the fanins of the node
Abc_ObjForEachFanin( pObj, pFanin, i )
Abc_MfsWinMarkTfi_rec( pFanin, vCone );
Vec_PtrPush( vCone, pObj );
}
/**Function*************************************************************
Synopsis [Marks and collects the TFI cone of the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_MfsWinMarkTfi( Abc_Obj_t * pNode )
{
Vec_Ptr_t * vCone;
vCone = Vec_PtrAlloc( 100 );
Abc_MfsWinMarkTfi_rec( pNode, vCone );
return vCone;
}
/**Function*************************************************************
Synopsis [Marks the TFO of the collected nodes up to the given level.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_MfsWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
{
Abc_Obj_t * pFanout;
int i;
if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
return;
if ( Abc_NodeIsTravIdCurrent(pObj) )
return;
Abc_NodeSetTravIdCurrent( pObj );
Abc_ObjForEachFanout( pObj, pFanout, i )
Abc_MfsWinSweepLeafTfo_rec( pFanout, nLevelLimit );
}
/**Function*************************************************************
Synopsis [Dereferences the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_MfsNodeDeref_rec( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanin;
int i, Counter = 1;
if ( Abc_ObjIsCi(pNode) )
return 0;
Abc_NodeSetTravIdCurrent( pNode );
Abc_ObjForEachFanin( pNode, pFanin, i )
{
assert( pFanin->vFanouts.nSize > 0 );
if ( --pFanin->vFanouts.nSize == 0 )
Counter += Abc_MfsNodeDeref_rec( pFanin );
}
return Counter;
}
/**Function*************************************************************
Synopsis [References the node's MFFC.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_MfsNodeRef_rec( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanin;
int i, Counter = 1;
if ( Abc_ObjIsCi(pNode) )
return 0;
Abc_ObjForEachFanin( pNode, pFanin, i )
{
if ( pFanin->vFanouts.nSize++ == 0 )
Counter += Abc_MfsNodeRef_rec( pFanin );
}
return Counter;
}
/**Function*************************************************************
Synopsis [Labels MFFC of the node with the current trav ID.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_MfsWinVisitMffc( Abc_Obj_t * pNode )
{
int Count1, Count2;
assert( Abc_ObjIsNode(pNode) );
// dereference the node (mark with the current trav ID)
Count1 = Abc_MfsNodeDeref_rec( pNode );
// reference it back
Count2 = Abc_MfsNodeRef_rec( pNode );
assert( Count1 == Count2 );
return Count1;
}
/**Function*************************************************************
Synopsis [Computes divisors and add them to nodes in the window.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax )
{
Vec_Ptr_t * vCone, * vDivs;
Abc_Obj_t * pObj, * pFanout, * pFanin;
int k, f, m;
int nDivsPlus = 0, nTrueSupp;
assert( p->vDivs == NULL );
// mark the TFI with the current trav ID
Abc_NtkIncrementTravId( pNode->pNtk );
vCone = Abc_MfsWinMarkTfi( pNode );
// count the number of PIs
nTrueSupp = 0;
Vec_PtrForEachEntry( vCone, pObj, k )
nTrueSupp += Abc_ObjIsCi(pObj);
// printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
// mark with the current trav ID those nodes that should not be divisors:
// (1) the node and its TFO
// (2) the MFFC of the node
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( pNode->pNtk );
Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
Abc_MfsWinVisitMffc( pNode );
Abc_ObjForEachFanin( pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
// at this point the nodes are marked with two trav IDs:
// nodes to be collected as divisors are marked with previous trav ID
// nodes to be avoided as divisors are marked with current trav ID
// start collecting the divisors
vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
Vec_PtrForEachEntry( vCone, pObj, k )
{
if ( !Abc_NodeIsTravIdPrevious(pObj) )
continue;
if ( (int)pObj->Level > nLevDivMax )
continue;
Vec_PtrPush( vDivs, pObj );
if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
break;
}
Vec_PtrFree( vCone );
// explore the fanouts of already collected divisors
if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
Vec_PtrForEachEntry( vDivs, pObj, k )
{
// consider fanouts of this node
Abc_ObjForEachFanout( pObj, pFanout, f )
{
// stop if there are too many fanouts
if ( f > 20 )
break;
// skip nodes that are already added
if ( Abc_NodeIsTravIdPrevious(pFanout) )
continue;
// skip nodes in the TFO or in the MFFC of node
if ( Abc_NodeIsTravIdCurrent(pFanout) )
continue;
// skip COs
if ( !Abc_ObjIsNode(pFanout) )
continue;
// skip nodes with large level
if ( (int)pFanout->Level >= nLevDivMax )
continue;
// skip nodes whose fanins are not divisors
Abc_ObjForEachFanin( pFanout, pFanin, m )
if ( !Abc_NodeIsTravIdPrevious(pFanin) )
break;
if ( m < Abc_ObjFaninNum(pFanout) )
continue;
// make sure this divisor in not among the nodes
// Vec_PtrForEachEntry( p->vNodes, pFanin, m )
// assert( pFanout != pFanin );
// add the node to the divisors
Vec_PtrPush( vDivs, pFanout );
// Vec_PtrPush( p->vNodes, pFanout );
Vec_PtrPushUnique( p->vNodes, pFanout );
Abc_NodeSetTravIdPrevious( pFanout );
nDivsPlus++;
if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
break;
}
if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
break;
}
// sort the divisors by level in the increasing order
Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease );
// add the fanins of the node
Abc_ObjForEachFanin( pNode, pFanin, k )
Vec_PtrPush( vDivs, pFanin );
/*
printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) );
Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
printf( "%d ", Abc_ObjLevel(pObj) );
printf( "\n" );
*/
//printf( "%d ", p->nDivsPlus );
// printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes),
// nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
return vDivs;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

35
src/opt/mfs/mfsInt.h
View File

@ -34,6 +34,7 @@ extern "C" {
#include "aig.h"
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@ -52,11 +53,23 @@ struct Mfs_Man_t_
Vec_Ptr_t * vRoots; // the roots of the window
Vec_Ptr_t * vSupp; // the support of the window
Vec_Ptr_t * vNodes; // the internal nodes of the window
Vec_Ptr_t * vDivs; // the divisors of the node
Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVars; // the projection variables
// intermediate simulation data
Vec_Ptr_t * vDivCexes; // the counter-example for dividors
int nDivWords; // the number of words
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
sat_solver * pSat; // the SAT solver used
Int_Man_t * pMan; // interpolation manager;
Vec_Int_t * vMem; // memory for intermediate SOPs
Vec_Vec_t * vLevels; // levelized structure for updating
Vec_Ptr_t * vFanins; // the new set of fanins
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
@ -64,14 +77,24 @@ struct Mfs_Man_t_
unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set
// performance statistics
int nNodesTried;
int nNodesBad;
int nNodesResub;
int nNodesGained;
int nMintsCare;
int nMintsTotal;
int nNodesBad;
// node/edge stats
int nTotalNodesBeg;
int nTotalNodesEnd;
int nTotalEdgesBeg;
int nTotalEdgesEnd;
// statistics
int timeWin;
int timeDiv;
int timeAig;
int timeCnf;
int timeSat;
int timeInt;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
@ -86,10 +109,18 @@ struct Mfs_Man_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== mfsDiv.c ==========================================================*/
extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
/*=== mfsInter.c ==========================================================*/
extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
/*=== mfsMan.c ==========================================================*/
extern Mfs_Man_t * Mfs_ManAlloc();
extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars );
extern void Mfs_ManStop( Mfs_Man_t * p );
extern void Mfs_ManClean( Mfs_Man_t * p );
/*=== mfsResub.c ==========================================================*/
extern int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
extern int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsStrash.c ==========================================================*/

254
src/opt/mfs/mfsInter.c Normal file
View File

@ -0,0 +1,254 @@
/**CFile****************************************************************
FileName [mfsInter.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Procedures for computing resub function by interpolation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
#include "kit.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Adds constraints for the two-input AND-gate.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
{
lit Lits[3];
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
return 0;
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
return 0;
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, 1 );
Lits[2] = toLitCond( iVarC, 0 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
return 0;
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, 0 );
Lits[2] = toLitCond( iVarC, 1 );
if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
return 0;
return 1;
}
/**Function*************************************************************
Synopsis [Creates miter for checking resubsitution.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
{
sat_solver * pSat;
Aig_Obj_t * pObjPo;
int Lits[2], status, iVar, i, c;
// get the literal for the output of F
pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
// collect the outputs of the divisors
Vec_IntClear( p->vProjVars );
Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
{
assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
}
assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
// start the solver
pSat = sat_solver_new();
sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
if ( pCands )
sat_solver_store_alloc( pSat );
// load the first copy of the clauses
for ( i = 0; i < p->pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
// add the clause for the first output of F
if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
{
sat_solver_delete( pSat );
return NULL;
}
// bookmark the clauses of A
if ( pCands )
sat_solver_store_mark_clauses_a( pSat );
// transform the literals
for ( i = 0; i < p->pCnf->nLiterals; i++ )
p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
// load the second copy of the clauses
for ( i = 0; i < p->pCnf->nClauses; i++ )
{
if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
// transform the literals
for ( i = 0; i < p->pCnf->nLiterals; i++ )
p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
// add the clause for the second output of F
Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
{
sat_solver_delete( pSat );
return NULL;
}
if ( pCands )
{
// add relevant clauses for EXOR gates
for ( c = 0; c < nCands; c++ )
{
// get the variable number of this divisor
i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
// get the corresponding SAT variable
iVar = Vec_IntEntry( p->vProjVars, i );
// add the corresponding EXOR gate
if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{
sat_solver_delete( pSat );
return NULL;
}
// add the corresponding clause
if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
{
sat_solver_delete( pSat );
return NULL;
}
}
// bookmark the roots
sat_solver_store_mark_roots( pSat );
}
else
{
// add the clauses for the EXOR gates - and remember their outputs
Vec_IntForEachEntry( p->vProjVars, iVar, i )
{
if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
{
sat_solver_delete( pSat );
return NULL;
}
Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
}
// simplify the solver
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
// printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
sat_solver_delete( pSat );
return NULL;
}
}
return pSat;
}
/**Function*************************************************************
Synopsis [Performs interpolation.]
Description [Derives the new function of the node.]
SideEffects []
SeeAlso []
***********************************************************************/
Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
{
extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
sat_solver * pSat;
Sto_Man_t * pCnf = NULL;
unsigned * puTruth;
Kit_Graph_t * pGraph;
Hop_Obj_t * pFunc;
int nFanins, status;
// derive the SAT solver for interpolation
pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
// solve the problem
status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
if ( status != l_False )
{
printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
return NULL;
}
// get the learned clauses
pCnf = sat_solver_store_release( pSat );
sat_solver_delete( pSat );
// derive the interpolant
nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
Sto_ManFree( pCnf );
assert( nFanins == nCands );
// transform interpolant into AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph );
Kit_GraphFree( pGraph );
return pFunc;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

66
src/opt/mfs/mfsMan.c
View File

@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Procedure to manipulation the manager.]
Synopsis [Procedures working with the manager.]
Author [Alan Mishchenko]
@ -28,7 +28,6 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
@ -40,13 +39,21 @@
SeeAlso []
***********************************************************************/
Mfs_Man_t * Mfs_ManAlloc()
Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
{
Mfs_Man_t * p;
// start the manager
p = ALLOC( Mfs_Man_t, 1 );
memset( p, 0, sizeof(Mfs_Man_t) );
p->pPars = pPars;
p->vProjVars = Vec_IntAlloc( 100 );
p->vDivLits = Vec_IntAlloc( 100 );
p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
p->pMan = Int_ManAlloc();
p->vMem = Vec_IntAlloc( 0 );
p->vLevels = Vec_VecStart( 32 );
p->vFanins = Vec_PtrAlloc( 32 );
return p;
}
@ -75,12 +82,15 @@ void Mfs_ManClean( Mfs_Man_t * p )
Vec_PtrFree( p->vSupp );
if ( p->vNodes )
Vec_PtrFree( p->vNodes );
if ( p->vDivs )
Vec_PtrFree( p->vDivs );
p->pAigWin = NULL;
p->pCnf = NULL;
p->pSat = NULL;
p->pCnf = NULL;
p->pSat = NULL;
p->vRoots = NULL;
p->vSupp = NULL;
p->vSupp = NULL;
p->vNodes = NULL;
p->vDivs = NULL;
}
/**Function*************************************************************
@ -96,14 +106,31 @@ void Mfs_ManClean( Mfs_Man_t * p )
***********************************************************************/
void Mfs_ManPrint( Mfs_Man_t * p )
{
printf( "Nodes tried = %d. Bad nodes = %d.\n",
p->nNodesTried, p->nNodesBad );
printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n",
p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal );
PRT( "Win", p->timeWin );
PRT( "Aig", p->timeAig );
PRT( "Cnf", p->timeCnf );
PRT( "Sat", p->timeSat );
if ( p->pPars->fResub )
{
printf( "Reduction in nodes = %5d. (%.2f %%) ",
p->nTotalNodesBeg-p->nTotalNodesEnd,
100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
printf( "Reduction in edges = %5d. (%.2f %%) ",
p->nTotalEdgesBeg-p->nTotalEdgesEnd,
100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
printf( "\n" );
printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
}
else
{
printf( "Nodes = %d. Care mints = %d. Total mints = %d. Ratio = %5.2f.\n",
p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal );
}
PRTP( "Win", p->timeWin , p->timeTotal );
PRTP( "Div", p->timeDiv , p->timeTotal );
PRTP( "Aig", p->timeAig , p->timeTotal );
PRTP( "Cnf", p->timeCnf , p->timeTotal );
PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal );
PRTP( "Int", p->timeInt , p->timeTotal );
PRTP( "ALL", p->timeTotal , p->timeTotal );
}
/**Function*************************************************************
@ -119,9 +146,18 @@ void Mfs_ManPrint( Mfs_Man_t * p )
***********************************************************************/
void Mfs_ManStop( Mfs_Man_t * p )
{
Mfs_ManPrint( p );
if ( p->pPars->fVerbose )
Mfs_ManPrint( p );
if ( p->pCare )
Aig_ManStop( p->pCare );
Mfs_ManClean( p );
Int_ManFree( p->pMan );
Vec_IntFree( p->vMem );
Vec_VecFree( p->vLevels );
Vec_PtrFree( p->vFanins );
Vec_IntFree( p->vProjVars );
Vec_IntFree( p->vDivLits );
Vec_PtrFree( p->vDivCexes );
free( p );
}

276
src/opt/mfs/mfsResub.c Normal file
View File

@ -0,0 +1,276 @@
/**CFile****************************************************************
FileName [mfsResub.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [The good old minimization with complete don't-cares.]
Synopsis [Procedures to perform resubstitution.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "mfsInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Updates the network after resubstitution.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
{
Abc_Obj_t * pObjNew, * pFanin;
int k;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
// update the level of the node
Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
}
/**Function*************************************************************
Synopsis [Tries resubstitution.]
Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
{
unsigned * pData, * pDataTot;
int RetValue, iVar, i;
p->nSatCalls++;
RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue == l_False || RetValue == l_True );
if ( RetValue == l_False )
return 1;
p->nSatCexes++;
// store the counter-example
pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
assert( pData[0] == 0 );
Vec_IntForEachEntry( p->vProjVars, iVar, i )
{
if ( sat_solver_var_value( p->pSat, iVar ) )
Aig_InfoSetBit( pData, i );
}
// AND the result with the previous ones
pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
for ( i = 0; i < p->nDivWords; i++ )
pDataTot[i] &= pData[i];
return 0;
}
/**Function*************************************************************
Synopsis [Performs resubstitution for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
{
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
unsigned * pData;
int pCands[MFS_FANIN_MAX];
int iVar, i, nCands, clk;
Abc_Obj_t * pFanin;
Hop_Obj_t * pFunc;
assert( iFanin >= 0 );
// clean simulation info
Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords );
pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
p->nCexes = 0;
if ( fVeryVerbose )
{
printf( "\n" );
printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
iFanin, Abc_ObjFaninNum(pNode),
Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
}
// try fanins without the critical fanin
nCands = 0;
Vec_PtrClear( p->vFanins );
Abc_ObjForEachFanin( pNode, pFanin, i )
{
if ( i == iFanin )
continue;
Vec_PtrPush( p->vFanins, pFanin );
iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
}
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
p->nNodesResub++;
// p->nNodesGained += Abc_NodeMffcLabel(pNode);
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
// update the network
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
p->timeInt += clock() - clk;
return 1;
}
if ( fOnlyRemove )
return 0;
// shift variables by 1
for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
p->vFanins->nSize++;
if ( fVeryVerbose )
{
for ( i = 0; i < 8; i++ )
printf( " " );
for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
printf( "%d", i % 10 );
for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
if ( i == iFanin )
printf( "*" );
else
printf( "%c", 'a' + i );
printf( "\n" );
}
iVar = -1;
while ( 1 )
{
if ( fVeryVerbose )
{
printf( "%3d: %2d ", p->nCexes, iVar );
pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
printf( "%d", Aig_InfoHasBit(pData, i) );
printf( "\n" );
}
// find the next divisor to try
pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
if ( Aig_InfoHasBit( pData, iVar ) )
break;
if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
return 0;
pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
{
if ( fVeryVerbose )
printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
p->nNodesResub++;
// p->nNodesGained += Abc_NodeMffcLabel(pNode);
clk = clock();
// derive the function
pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
// update the network
// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
p->timeInt += clock() - clk;
return 1;
}
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs resubstitution for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanin;
int i;
Abc_ObjForEachFanin( pNode, pFanin, i )
if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
{
if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis [Performs resubstitution for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanin;
int i;
Abc_ObjForEachFanin( pNode, pFanin, i )
if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
{
if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
return 1;
}
Abc_ObjForEachFanin( pNode, pFanin, i )
if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
{
if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
return 1;
}
return 0;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

24
src/opt/mfs/mfsSat.c
View File

@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Synopsis [Procedures to compute don't-cares using SAT.]
Author [Alan Mishchenko]
@ -43,9 +43,11 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
{
int Lits[MFS_FANIN_MAX];
int RetValue, iVar, b, Mint;
RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
if ( RetValue != l_True )
RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
assert( RetValue == l_False || RetValue == l_True );
if ( RetValue == l_False )
return 0;
p->nCares++;
// add SAT assignment to the solver
Mint = 0;
Vec_IntForEachEntry( p->vProjVars, iVar, b )
@ -95,15 +97,19 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
// iterate through the SAT assignments
while ( Abc_NtkMfsSolveSat_iter( p ) );
p->nCares = 0;
while ( Abc_NtkMfsSolveSat_iter(p) );
// write statistics
p->nCares = 0;
for ( i = 0; i < p->nWords; i++ )
p->nCares += Aig_WordCountOnes( p->uCare[i] );
p->nMintsCare += p->nCares;
p->nMintsTotal += 32 * p->nWords;
p->nMintsTotal += (1<<p->nFanins);
if ( p->pPars->fVeryVerbose )
{
printf( "Node %4d : Care = %2d. Total = %2d. ", pNode->Id, p->nCares, (1<<p->nFanins) );
Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
printf( "\n" );
}
}
////////////////////////////////////////////////////////////////////////

41
src/opt/mfs/mfsStrash.c
View File

@ -144,18 +144,18 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
SeeAlso []
***********************************************************************/
Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan )
{
Aig_Obj_t * pObj0, * pObj1;
if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
return pObj->pData;
Aig_ObjSetTravIdCurrent( pMan, pObj );
Aig_ObjSetTravIdCurrent( pCare, pObj );
if ( Aig_ObjIsPi(pObj) )
return pObj->pData = NULL;
pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
if ( pObj0 == NULL )
return pObj->pData = NULL;
pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
if ( pObj1 == NULL )
return pObj->pData = NULL;
pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
@ -184,6 +184,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
pMan = Aig_ManStart( 1000 );
// construct the root node's AIG cone
pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
// assert( Aig_ManConst1(pMan) == pObjAig );
Aig_ObjCreatePo( pMan, pObjAig );
if ( p->pCare )
{
@ -191,27 +192,43 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
Aig_ManIncrementTravId( p->pCare );
Vec_PtrForEachEntry( p->vSupp, pFanin, i )
{
if ( pFanin->pData == NULL )
continue;
pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
pPi = Aig_ManPi( p->pCare, (int)pFanin->pData );
Aig_ObjSetTravIdCurrent( p->pCare, pPi );
pPi->pData = pFanin->pCopy;
}
// construct the constraints
Aig_ManForEachPo( p->pCare, pPo, i )
{
pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan );
// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
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 );
}
}
// construct the fanins
Abc_ObjForEachFanin( pNode, pFanin, i )
if ( p->pPars->fResub )
{
pObjAig = (Aig_Obj_t *)pFanin->pCopy;
// construct the node
pObjAig = (Aig_Obj_t *)pNode->pCopy;
Aig_ObjCreatePo( pMan, pObjAig );
// construct the divisors
Vec_PtrForEachEntry( p->vDivs, pFanin, i )
{
pObjAig = (Aig_Obj_t *)pFanin->pCopy;
Aig_ObjCreatePo( pMan, pObjAig );
}
}
else
{
// construct the fanins
Abc_ObjForEachFanin( pNode, pFanin, i )
{
pObjAig = (Aig_Obj_t *)pFanin->pCopy;
Aig_ObjCreatePo( pMan, pObjAig );
}
}
Aig_ManCleanup( pMan );
return pMan;

2
src/opt/mfs/mfsWin.c
View File

@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
Synopsis []
Synopsis [Procedures to compute windows stretching to the PIs.]
Author [Alan Mishchenko]

3
src/opt/mfs/module.make
View File

@ -1,5 +1,8 @@
SRC += src/opt/mfs/mfsCore.c \
src/opt/mfs/mfsDiv.c \
src/opt/mfs/mfsInter.c \
src/opt/mfs/mfsMan.c \
src/opt/mfs/mfsResub.c \
src/opt/mfs/mfsSat.c \
src/opt/mfs/mfsStrash.c \
src/opt/mfs/mfsWin.c

3
src/opt/res/resCore.c
View File

@ -183,12 +183,15 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
{
Abc_Obj_t * pObjNew, * pFanin;
int k;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
// update the level of the node
Abc_NtkUpdate( pObj, pObjNew, vLevels );
}