Skip to content

A
abc
Commit a13c64a5 by Alan Mishchenko
Options

Version abc70206

parent 8da52b6f
Showing with 935 additions and 274 deletions
abc.dsp
......@@ -1706,8 +1706,20 @@ SOURCE=.\src\opt\bdc\bdc.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\bdc\bdcCore.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\bdc\bdcDec.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\bdc\bdcInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\bdc\bdcTable.c
# End Source File
# End Group
# End Group
# Begin Group "map"
......
abc.plg 0 → 100644
<html>
<body>
<pre>
<h1>Build Log</h1>
<h3>
--------------------Configuration: abc - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83C.tmp" with contents
[
/nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /I "src\base\seq" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\bsat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\sim" /I "src\opt\rwr" /I "src\opt\kit" /I "src\opt\res" /I "src\map\fpga" /I "src\map\if" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /I "src\misc\espresso" /I "src\misc\nm" /I "src\misc\hash" /I "src\aig\ivy" /I "src\aig\hop" /I "src\aig\rwt" /I "src\aig\deco" /I "src\aig\mem" /I "src\temp\esop" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
"C:\_projects\abc\src\base\abc\abcObj.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP83C.tmp"
<h3>Output Window</h3>
Compiling...
abcObj.c
<h3>Results</h3>
abcObj.obj - 0 error(s), 0 warning(s)
</pre>
</body>
</html>
abclib.plg 0 → 100644
This diff is collapsed. Click to expand it.
abctestlib.plg 0 → 100644
<html>
<body>
<pre>
<h1>Build Log</h1>
<h3>
--------------------Configuration: abctestlib - Win32 Debug--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1389.tmp" with contents
[
/nologo /MLd /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /FR"Debug/" /Fp"Debug/abctestlib.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c
"C:\_projects\abc\demo.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1389.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP138A.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_debug.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abctestlib.pdb" /debug /machine:I386 /out:"_TEST/abctestlib.exe" /pdbtype:sept
.\Debug\demo.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP138A.tmp"
<h3>Output Window</h3>
Compiling...
demo.c
Linking...
Creating command line "bscmake.exe /nologo /o"Debug/abctestlib.bsc" .\Debug\demo.sbr"
Creating browse info file...
<h3>Output Window</h3>
<h3>Results</h3>
abctestlib.exe - 0 error(s), 0 warning(s)
</pre>
</body>
</html>
src/base/abc/abc.h
......@@ -197,6 +197,7 @@ struct Abc_Ntk_t_
Extra_MmFixed_t * pMmObj; // memory manager for objects
Extra_MmStep_t * pMmStep; // memory manager for arrays
void * pManFunc; // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
Abc_Lib_t * pDesign;
// Abc_Lib_t * pVerLib; // for structural verilog designs
Abc_ManTime_t * pManTime; // the timing manager (for mapped networks) stores arrival/required times for all nodes
void * pManCut; // the cut manager (for AIGs) stores information about the cuts computed for the nodes
......@@ -244,10 +245,11 @@ static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p
static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; }
static inline int Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1; }
static inline int Abc_InfoIsOne( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~p[i] ) return 0; return 1; }
static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; }
static inline void Abc_InfoCopy( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i]; }
static inline void Abc_InfoAnd( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i]; }
static inline void Abc_InfoOr( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i]; }
static inline void Abc_InfoXor( unsigned * p, unsigned * q, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i]; }
static inline int Abc_InfoIsOrOne( unsigned * p, unsigned * q, int nWords ){ int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~(p[i] | q[i]) ) return 0; return 1; }
// checking the network type
static inline bool Abc_NtkIsNetlist( Abc_Ntk_t * pNtk ) { return pNtk->ntkType == ABC_NTK_NETLIST; }
......
src/base/abc/abcNetlist.c
......@@ -25,8 +25,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk );
static void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter );
static void Abc_NtkAddPoBuffers( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
......@@ -51,8 +49,9 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
int i, k;
assert( Abc_NtkIsNetlist(pNtk) );
// consider simple case when there is hierarchy
if ( pNtk->tName2Model )
return Abc_NtkNetlistToLogicHie( pNtk );
assert( pNtk->tName2Model == NULL );
// if ( pNtk->tName2Model )
// return Abc_NtkNetlistToLogicHie( pNtk );
// start the network
if ( Abc_NtkHasMapping(pNtk) )
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_MAP );
......@@ -79,159 +78,6 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
/**Function*************************************************************
Synopsis [Transform the netlist into a logic network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pObj;
int i, Counter = 0;
assert( Abc_NtkIsNetlist(pNtk) );
// start the network
// pNtkNew = Abc_NtkAlloc( Type, Func, 1 );
if ( !Abc_NtkHasMapping(pNtk) )
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 );
else
pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_MAP, 1 );
// duplicate the name and the spec
pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec);
// clean the node copy fields
Abc_NtkForEachNode( pNtk, pObj, i )
pObj->pCopy = NULL;
// clone PIs/POs/latches and make old nets point to new terminals; create names
Abc_NtkForEachCi( pNtk, pObj, i )
{
Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj, 0);
Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)), NULL );
}
Abc_NtkForEachPo( pNtk, pObj, i )
{
Abc_NtkDupObj(pNtkNew, pObj, 0);
Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)), NULL );
}
// recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtk, &Counter );
if ( Counter )
printf( "Warning: The total of %d block boxes are transformed into PI/PO pairs.\n", Counter );
// connect the CO nodes
Abc_NtkForEachCo( pNtk, pObj, i )
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
// copy the timing information
Abc_ManTimeDup( pNtk, pNtkNew );
// fix the problem with CO pointing directly to CIs
Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
// duplicate EXDC
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkNetlistToLogic( pNtk->pExdc );
if ( !Abc_NtkCheck( pNtkNew ) )
fprintf( stdout, "Abc_NtkNetlistToLogic(): Network check has failed.\n" );
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Transform the netlist into a logic network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int * pCounter )
{
char Prefix[1000];
Vec_Ptr_t * vNodes;
Abc_Ntk_t * pNtkModel;
Abc_Obj_t * pNode, * pObj, * pFanin;
int i, k;
// collect nodes and boxes in topological order
vNodes = Abc_NtkDfs( pNtkOld, 0 );
// duplicate nodes, create PIs/POs corresponding to blackboxes
// have to do it first if blackboxes break combinational loops
// (current we do not allow whiteboxes to break combinational loops)
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_ObjIsNode(pNode) )
{
// duplicate the node and save it in the fanout net
Abc_NtkDupObj( pNtkNew, pNode, 0 );
Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
continue;
}
assert( Abc_ObjIsBox(pNode) );
pNtkModel = pNode->pData;
if ( !Abc_NtkHasBlackbox(pNtkModel) )
continue;
// consider this blockbox
if ( pNtkNew->pBlackBoxes == NULL )
{
pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
}
sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
// create new PIs from the POs of the box
Abc_NtkForEachPo( pNtkModel, pObj, k )
{
pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) );
}
// create new POs from the PIs of the box
Abc_NtkForEachPi( pNtkModel, pObj, k )
{
pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
// Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
Abc_ObjAssignName( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) );
}
(*pCounter)++;
Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
}
// connect nodes and boxes
Vec_PtrForEachEntry( vNodes, pNode, i )
{
if ( Abc_ObjIsNode(pNode) )
{
// printf( "adding node %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
Abc_ObjForEachFanin( pNode, pFanin, k )
Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
continue;
}
assert( Abc_ObjIsBox(pNode) );
pNtkModel = pNode->pData;
// printf( "adding model %s\n", Abc_NtkName(pNtkModel) );
// consider the case of the black box
if ( Abc_NtkHasBlackbox(pNtkModel) )
{
// create new POs from the PIs of the box
Abc_NtkForEachPi( pNtkModel, pObj, k )
Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
continue;
}
// transfer the nodes to the box inputs
Abc_NtkForEachPi( pNtkModel, pObj, k )
Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
// construct recursively
Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
// transfer the results back
Abc_NtkForEachPo( pNtkModel, pObj, k )
Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;
}
Vec_PtrFree( vNodes );
}
/**Function*************************************************************
Synopsis [Transform the logic network into a netlist.]
Description []
......
src/base/abc/abcObj.c
......@@ -327,7 +327,7 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanout0Ntk(pObj)), NULL );
else if ( Abc_ObjIsCo(pObj) )
Abc_ObjAssignName( pObjNew, Abc_ObjName(Abc_ObjFanin0Ntk(pObj)), NULL );
else if ( Abc_ObjIsBox(pObj) )
else if ( Abc_ObjIsBox(pObj) || Abc_ObjIsNet(pObj) )
Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL );
}
// copy functionality/names
......@@ -350,8 +350,6 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName
}
else if ( Abc_ObjIsNet(pObj) ) // copy the name
{
assert( 0 );
// pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
}
else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value
pObjNew->pData = pObj->pData;
......
src/base/abci/abc.c
......@@ -2577,13 +2577,14 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pPars->nWindow = 33;
pPars->nCands = 3;
pPars->nSimWords = 8;
pPars->fVerbose = 1;
pPars->nWindow = 62;
pPars->nCands = 5;
pPars->nSimWords = 4;
pPars->fArea = 0;
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "WSavwh" ) ) != EOF )
{
switch ( c )
{
......@@ -2609,6 +2610,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 )
goto usage;
break;
case 'a':
pPars->fArea ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
......@@ -2627,9 +2631,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkHasAig(pNtk) )
if ( !Abc_NtkIsLogic(pNtk) )
{
fprintf( pErr, "This command can only be applied to AIG logic network (run \"aig\").\n" );
fprintf( pErr, "This command can only be applied to a logic network.\n" );
return 1;
}
......@@ -2642,10 +2646,11 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with don't-cares\n" );
fprintf( pErr, "\t-W <NM> : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
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-h : print the command usage\n");
......
src/base/io/ioReadBlifMv.c
......@@ -176,6 +176,8 @@ Abc_Lib_t * Io_ReadBlifMv( char * pFileName, int fBlifMv, int fCheck )
}
}
}
// pDesign should be linked to all models of the design
Io_WriteBlifMvDesign( pDesign, "_temp_.mv" );
Abc_LibPrint( pDesign );
Abc_LibFree( pDesign );
......@@ -637,7 +639,7 @@ static void Io_MvReadInterfaces( Io_MvMan_t * p )
/**Function*************************************************************
Synopsis [Reads the AIG in the binary AIGER format.]
Synopsis []
Description []
......
src/misc/extra/extra.h
......@@ -112,6 +112,10 @@ typedef unsigned long long uint64;
#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
#endif
#ifndef PRTP
#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), 100.0*(t)/(T))
#endif
/*===========================================================================*/
/* Various Utilities */
/*===========================================================================*/
......
src/opt/bdc/bdc.h
......@@ -20,7 +20,7 @@
#ifndef __BDC_H__
#define __BDC_H__
#ifdef __cplusplus
extern "C" {
#endif
......@@ -57,8 +57,8 @@ struct Bdc_Par_t_
/*=== bdcCore.c ==========================================================*/
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
extern void Bdc_ManAlloc( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit );
extern void Bdc_ManFree( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit );
#ifdef __cplusplus
......
src/opt/bdc/bdcCore.c
......@@ -18,7 +18,6 @@
***********************************************************************/
#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
......@@ -43,32 +42,50 @@
Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
{
Bdc_Man_t * p;
int i;
unsigned * pData;
int i, k, nBits;
p = ALLOC( Bdc_Man_t, 1 );
memset( p, 0, sizeof(Bdc_Man_t) );
assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
p->nNodesLimit = 0; // will be set later
// memory
p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
p->nNodesAlloc = 256;
p->nNodesAlloc = 512;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
p->vSpots = Vec_IntAlloc( 256 );
// set up constant 1 and elementary variables
for ( i = 0; i < pPars->nVarsMax; i++ )
// truth tables
p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
// set elementary truth tables
nBits = (1 << pPars->nVarsMax);
Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
for ( k = 0; k < pPars->nVarsMax; k++ )
{
pData = Vec_PtrEntry( p->vTruths, k+1 );
Kit_TruthClear( pData, p->nVars );
for ( i = 0; i < nBits; i++ )
if ( i & (1 << k) )
pData[i>>5] |= (1 << (i&31));
}
p->nNodes = pPars->nVarsMax + 1;
// remember the current place in memory
p->nMemStart = Vec_IntSize( p->vMemory );
p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
// start the internal ISFs
p->pIsfOL = &p->IsfOL; Bdc_IsfStart( p, p->pIsfOL );
p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL );
p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR );
return p;
}
/**Function*************************************************************
Synopsis [Deallocate resynthesis manager.]
......@@ -80,15 +97,21 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
SeeAlso []
***********************************************************************/
void Bdc_ManAlloc( Bdc_Man_t * p )
void Bdc_ManFree( Bdc_Man_t * p )
{
Vec_IntFree( p->vMemory );
Vec_IntFree( p->vSpots );
Vec_PtrFree( p->vTruths );
free( p->pNodes );
free( p->pTable );
free( p );
}
/**Function*************************************************************
Synopsis [Sets up the divisors.]
Synopsis [Clears the manager.]
Description [The first n+1 entries are const1 and elem variables.]
Description []
SideEffects []
......@@ -97,23 +120,31 @@ void Bdc_ManAlloc( Bdc_Man_t * p )
***********************************************************************/
void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
{
Bdc_Fun_t ** pSpot, * pFunc;
unsigned * puTruth;
Bdc_Fun_t * pNode;
int i;
// clean hash table
Vec_PtrForEachEntry( p->vSpots, pSpot, i )
*pSpot = NULL;
// reset nodes
p->nNodes = p->pPars->nVarsMax + 1;
// reset memory
Vec_IntShrink( p->vMemory, p->nMemStart );
// add new nodes to the hash table
Bdc_TableClear( p );
Vec_IntClear( p->vMemory );
// add constant 1 and elementary vars
p->nNodes = p->nNodesNew = 0;
for ( i = 0; i <= p->pPars->nVarsMax; i++ )
{
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_PI;
pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
pNode->uSupp = i? (1 << (i-1)) : 0;
Bdc_TableAdd( p, pNode );
}
// add the divisors
Vec_PtrForEachEntry( vDivs, puTruth, i )
{
pFunc = Bdc_ManNewNode( p );
pFunc->Type = BDC_TYPE_PI;
pFunc->puFunc = puTruth;
pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars );
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_PI;
pNode->puFunc = puTruth;
pNode->uSupp = Kit_TruthSupport( puTruth, p->nVars );
Bdc_TableAdd( p, pNode );
if ( i == p->nDivsLimit )
break;
}
}
......@@ -128,25 +159,26 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
SeeAlso []
***********************************************************************/
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit )
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
// set current manager parameters
p->nVars = nVars;
p->nWords = Kit_TruthWordNum( nVars );
p->nNodeLimit = nNodeLimit;
Bdc_ManPrepare( p, vDivs );
p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
// copy the function
Bdc_IsfStart( p, pIsf );
Bdc_IsfClean( pIsf );
pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords );
pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords );
Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
// call decomposition
Bdc_SuppMinimize( p, pIsf );
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
if ( p->pRoot == NULL )
return -1;
return p->nNodes - (p->pPars->nVarsMax + 1);
return p->nNodesNew;
}
......
src/opt/bdc/bdcInt.h
......@@ -29,13 +29,15 @@ extern "C" {
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "dec.h"
#include "kit.h"
#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
#define BDC_SCALE 100 // value used to compute the cost
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
......@@ -46,18 +48,19 @@ typedef enum {
BDC_TYPE_CONST1, // 1: constant 1
BDC_TYPE_PI, // 2: primary input
BDC_TYPE_AND, // 4: AND-gate
BDC_TYPE_XOR, // 5: XOR-gate
BDC_TYPE_MUX, // 6: MUX-gate
BDC_TYPE_OTHER // 7: unused
BDC_TYPE_OR, // 5: OR-gate (temporary)
BDC_TYPE_XOR, // 6: XOR-gate
BDC_TYPE_MUX, // 7: MUX-gate
BDC_TYPE_OTHER // 8: unused
} Bdc_Type_t;
typedef struct Bdc_Fun_t_ Bdc_Fun_t;
struct Bdc_Fun_t_
{
int Type; // Const1, PI, AND, XOR, MUX
Bdc_Fun_t * pFan0; // next function with same support
Bdc_Fun_t * pFan1; // next function with same support
Bdc_Fun_t * pFan2; // next function with same support
Bdc_Fun_t * pFan0; // fanin of the given node
Bdc_Fun_t * pFan1; // fanin of the given node
Bdc_Fun_t * pFan2; // fanin of the given node
unsigned uSupp; // bit mask of current support
unsigned * puFunc; // the function of the node
Bdc_Fun_t * pNext; // next function with same support
......@@ -67,11 +70,10 @@ struct Bdc_Fun_t_
typedef struct Bdc_Isf_t_ Bdc_Isf_t;
struct Bdc_Isf_t_
{
unsigned uSupp; // bit mask of current support
unsigned uUnique; // bit mask of unique support
int Var; // the first variable assigned
unsigned uSupp; // the current support
unsigned * puOn; // on-set
unsigned * puOff; // off-set
int Cost; // cost of this component
};
typedef struct Bdc_Man_t_ Bdc_Man_t;
......@@ -81,25 +83,44 @@ struct Bdc_Man_t_
Bdc_Par_t * pPars; // parameter set
int nVars; // the number of variables
int nWords; // the number of words
int nNodeLimit; // the limit on the number of new nodes
int nNodesLimit; // the limit on the number of new nodes
int nDivsLimit; // the limit on the number of divisors
// internal nodes
Bdc_Fun_t * pNodes; // storage for decomposition nodes
int nNodes; // the number of nodes used
int nNodesNew; // the number of nodes used
int nNodesAlloc; // the number of nodes allocated
Bdc_Fun_t * pRoot; // the root node
// resub candidates
Bdc_Fun_t ** pTable; // hash table of candidates
int nTableSize; // hash table size (1 << nVarsMax)
Vec_Int_t * vSpots; // the occupied spots in the table
// elementary truth tables
Vec_Ptr_t * vTruths; // for const 1 and elementary variables
unsigned * puTemp1; // temporary truth table
unsigned * puTemp2; // temporary truth table
unsigned * puTemp3; // temporary truth table
unsigned * puTemp4; // temporary truth table
// temporary ISFs
Bdc_Isf_t * pIsfOL, IsfOL;
Bdc_Isf_t * pIsfOR, IsfOR;
Bdc_Isf_t * pIsfAL, IsfAL;
Bdc_Isf_t * pIsfAR, IsfAR;
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
int nMemStart; // the starting memory size
};
// working with complemented attributes of objects
static inline bool Bdc_IsComplement( Bdc_Fun_t * p ) { return (bool)((unsigned long)p & (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
static inline int Bdc_IsComplement( Bdc_Fun_t * p ) { return (int)((unsigned long)p & (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01); }
static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)01); }
static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_Fun_t *)((unsigned long)p ^ (unsigned long)(c!=0)); }
static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p ) { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
static inline void Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
static inline void Bdc_IsfClean( Bdc_Isf_t * p ) { p->uSupp = 0; p->Var = 0; }
static inline void Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q ) { Bdc_Isf_t T = *p; *p = *q; *q = T; }
static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT; }
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
......@@ -109,11 +130,14 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== bdcSupp.c ==========================================================*/
extern int Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
/*=== bdcDec.c ==========================================================*/
extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
extern void Bdc_TableClear( Bdc_Man_t * p );
extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
#ifdef __cplusplus
}
......
src/opt/bdc/bdcTable.c 0 → 100644
/**CFile****************************************************************
FileName [bdcTable.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Truth-table-based bi-decomposition engine.]
Synopsis [Hash table for intermediate nodes.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - January 30, 2007.]
Revision [$Id: bdcTable.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Minimizes the support of the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
int v;
// go through the support variables
for ( v = 0; v < p->nVars; v++ )
{
if ( (pIsf->uSupp & (1 << v)) == 0 )
continue;
Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
continue;
// remove the variable
Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
pIsf->uSupp &= ~(1 << v);
}
}
/**Function*************************************************************
Synopsis [Checks containment of the function in the ISF.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
{
return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars );
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
{
Bdc_Fun_t * pFunc;
for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
return pFunc;
return NULL;
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc )
{
if ( p->pTable[pFunc->uSupp] == NULL )
Vec_IntPush( p->vSpots, pFunc->uSupp );
pFunc->pNext = p->pTable[pFunc->uSupp];
p->pTable[pFunc->uSupp] = pFunc;
}
/**Function*************************************************************
Synopsis [Adds the new entry to the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Bdc_TableClear( Bdc_Man_t * p )
{
int Spot, i;
Vec_IntForEachEntry( p->vSpots, Spot, i )
p->pTable[Spot] = NULL;
Vec_IntClear( p->vSpots );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/bdc/bdc_.c
......@@ -18,7 +18,6 @@
***********************************************************************/
#include "abc.h"
#include "bdcInt.h"
////////////////////////////////////////////////////////////////////////
......
src/opt/kit/kit.h
......@@ -207,6 +207,22 @@ static inline int Kit_TruthIsImply( unsigned * pIn1, unsigned * pIn2, int nVars
return 0;
return 1;
}
static inline int Kit_TruthIsDisjoint( unsigned * pIn1, unsigned * pIn2, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn1[w] & pIn2[w] )
return 0;
return 1;
}
static inline int Kit_TruthIsDisjoint3( unsigned * pIn1, unsigned * pIn2, unsigned * pIn3, int nVars )
{
int w;
for ( w = Kit_TruthWordNum(nVars)-1; w >= 0; w-- )
if ( pIn1[w] & pIn2[w] & pIn3[w] )
return 0;
return 1;
}
static inline void Kit_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
{
int w;
......@@ -320,7 +336,11 @@ extern int Kit_TruthSupport( unsigned * pTruth, int nVars );
extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
extern void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar );
extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar );
extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin );
......
src/opt/kit/kitTruth.c
......@@ -490,6 +490,81 @@ void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar )
SeeAlso []
***********************************************************************/
void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] | ((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1);
return;
case 1:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] | ((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2);
return;
case 2:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] | ((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4);
return;
case 3:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] | ((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8);
return;
case 4:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] | ((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16);
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pRes[i] = pTruth[i] | pTruth[Step+i];
pRes[Step+i] = pRes[i];
}
pRes += 2*Step;
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Existantially quantifies the set of variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
{
int v;
Kit_TruthCopy( pRes, pTruth, nVars );
for ( v = 0; v < nVars; v++ )
if ( uMask & (1 << v) )
Kit_TruthExist( pRes, nVars, v );
}
/**Function*************************************************************
Synopsis [Unversally quantifies the variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
......@@ -533,6 +608,81 @@ void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar )
}
}
/**Function*************************************************************
Synopsis [Universally quantifies the variable.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar )
{
int nWords = Kit_TruthWordNum( nVars );
int i, k, Step;
assert( iVar < nVars );
switch ( iVar )
{
case 0:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] & (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1));
return;
case 1:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] & (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2));
return;
case 2:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] & (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4));
return;
case 3:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] & (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8));
return;
case 4:
for ( i = 0; i < nWords; i++ )
pRes[i] = pTruth[i] & (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16));
return;
default:
Step = (1 << (iVar - 5));
for ( k = 0; k < nWords; k += 2*Step )
{
for ( i = 0; i < Step; i++ )
{
pRes[i] = pTruth[i] & pTruth[Step+i];
pRes[Step+i] = pRes[i];
}
pRes += 2*Step;
pTruth += 2*Step;
}
return;
}
}
/**Function*************************************************************
Synopsis [Universally quantifies the set of variables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask )
{
int v;
Kit_TruthCopy( pRes, pTruth, nVars );
for ( v = 0; v < nVars; v++ )
if ( uMask & (1 << v) )
Kit_TruthForall( pRes, nVars, v );
}
/**Function*************************************************************
......
src/opt/res/res.h
......@@ -44,6 +44,8 @@ struct Res_Par_t_
int nWindow; // window size
int nSimWords; // the number of simulation words
int nCands; // the number of candidates to try
int fArea; // performs optimization for area
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
......
src/opt/res/resCore.c
......@@ -48,17 +48,24 @@ struct Res_Man_t_
int nDivNodes; // the total number of divisors
int nWinsTriv; // the total number of trivial windows
int nWinsUsed; // the total number of useful windows (with at least one candidate)
int nConstsUsed; // the total number of constant nodes under ODC
int nCandSets; // the total number of candidates
int nProvedSets; // the total number of proved groups
int nSimEmpty; // the empty simulation info
int nTotalNets; // the total number of nets
int nTotalNodes; // the total number of nodess
int nTotalNets2; // the total number of nets
int nTotalNodes2; // the total number of nodess
// runtime
int timeWin; // windowing
int timeDiv; // divisors
int timeAig; // strashing
int timeSim; // simulation
int timeCand; // resubstitution candidates
int timeSat; // SAT solving
int timeSatTotal; // SAT solving total
int timeSatSat; // SAT solving (sat calls)
int timeSatUnsat; // SAT solving (unsat calls)
int timeSatSim; // SAT solving (simulation)
int timeInt; // interpolation
int timeUpd; // updating
int timeTotal; // total runtime
......@@ -120,19 +127,30 @@ void Res_ManFree( Res_Man_t * p )
printf( "\n" );
printf( "WinsTriv = %d. ", p->nWinsTriv );
printf( "SimsEmpt = %d. ", p->nSimEmpty );
printf( "Const = %d. ", p->nConstsUsed );
printf( "WindUsed = %d. ", p->nWinsUsed );
printf( "Cands = %d. ", p->nCandSets );
printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
printf( "Proved = %d.", p->nProvedSets );
printf( "\n" );
printf( "Reduction in nodes = %d. (%.2f %%) ",
p->nTotalNodes-p->nTotalNodes2,
100.0*(p->nTotalNodes-p->nTotalNodes2)/p->nTotalNodes );
printf( "Reduction in nets = %d. (%.2f %%) ",
p->nTotalNets-p->nTotalNets2,
100.0*(p->nTotalNets-p->nTotalNets2)/p->nTotalNets );
printf( "\n" );
PRT( "Windowing ", p->timeWin );
PRT( "Divisors ", p->timeDiv );
PRT( "Strashing ", p->timeAig );
PRT( "Simulation ", p->timeSim );
PRT( "Candidates ", p->timeCand );
PRT( "SAT solver ", p->timeSat );
PRT( "Interpol ", p->timeInt );
PRT( "Undating ", p->timeUpd );
PRTP( "Windowing ", p->timeWin, p->timeTotal );
PRTP( "Divisors ", p->timeDiv, p->timeTotal );
PRTP( "Strashing ", p->timeAig, p->timeTotal );
PRTP( "Simulation ", p->timeSim, p->timeTotal );
PRTP( "Candidates ", p->timeCand, p->timeTotal );
PRTP( "SAT solver ", p->timeSatTotal, p->timeTotal );
PRTP( " sat ", p->timeSatSat, p->timeTotal );
PRTP( " unsat ", p->timeSatUnsat, p->timeTotal );
PRTP( " simul ", p->timeSatSim, p->timeTotal );
PRTP( "Interpol ", p->timeInt, p->timeTotal );
PRTP( "Undating ", p->timeUpd, p->timeTotal );
PRT( "TOTAL ", p->timeTotal );
}
Res_WinFree( p->pWin );
......@@ -160,6 +178,7 @@ void Res_ManFree( Res_Man_t * p )
***********************************************************************/
int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
{
ProgressBar * pProgress;
Res_Man_t * p;
Abc_Obj_t * pObj;
Hop_Obj_t * pFunc;
......@@ -168,18 +187,33 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
unsigned * puTruth;
int i, k, RetValue, nNodesOld, nFanins;
int clk, clkTotal = clock();
assert( Abc_NtkHasAig(pNtk) );
// start the manager
p = Res_ManAlloc( pPars );
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
p->nTotalNodes = Abc_NtkNodeNum(pNtk);
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
// convert into the AIG
if ( !Abc_NtkLogicToAig(pNtk) )
{
fprintf( stdout, "Converting to BDD has failed.\n" );
Res_ManFree( p );
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
// set the number of levels
Abc_NtkLevel( pNtk );
// try resynthesizing nodes in the topological order
nNodesOld = Abc_NtkObjNumMax(pNtk);
pProgress = Extra_ProgressBarStart( stdout, nNodesOld );
Abc_NtkForEachObj( pNtk, pObj, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( !Abc_ObjIsNode(pObj) )
continue;
if ( pObj->Id > nNodesOld )
......@@ -205,7 +239,7 @@ p->timeWin += clock() - clk;
// collect the divisors
clk = clock();
Res_WinDivisors( p->pWin, pObj->Level - 1 );
Res_WinDivisors( p->pWin, pObj->Level + 2 ); //- 1 );
p->timeDiv += clock() - clk;
p->nWins++;
......@@ -232,7 +266,7 @@ p->timeAig += clock() - clk;
// prepare simulation info
clk = clock();
RetValue = Res_SimPrepare( p->pSim, p->pAig );
RetValue = Res_SimPrepare( p->pSim, p->pAig, Vec_PtrSize(p->pWin->vLeaves), 0 ); //p->pPars->fVerbose );
p->timeSim += clock() - clk;
if ( !RetValue )
{
......@@ -240,14 +274,33 @@ p->timeSim += clock() - clk;
continue;
}
// consider the case of constant node
if ( p->pSim->fConst0 || p->pSim->fConst1 )
{
p->nConstsUsed++;
pFunc = p->pSim->fConst1? Hop_ManConst1(pNtk->pManFunc) : Hop_ManConst0(pNtk->pManFunc);
vFanins = Vec_VecEntry( p->vResubsW, 0 );
Vec_PtrClear( vFanins );
Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
continue;
}
// printf( " " );
// find resub candidates for the node
clk = clock();
RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
if ( p->pPars->fArea )
RetValue = Res_FilterCandidatesArea( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
else
RetValue = Res_FilterCandidatesNets( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
p->timeCand += clock() - clk;
p->nCandSets += RetValue;
if ( RetValue == 0 )
continue;
// printf( "%d(%d) ", Vec_PtrSize(p->pWin->vDivs), RetValue );
p->nWinsUsed++;
// iterate through candidate resubstitutions
......@@ -260,15 +313,20 @@ p->timeCand += clock() - clk;
clk = clock();
if ( p->pCnf ) Sto_ManFree( p->pCnf );
p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
p->timeSat += clock() - clk;
if ( p->pCnf == NULL )
{
p->timeSatSat += clock() - clk;
// printf( " Sat\n" );
// printf( "-" );
continue;
}
p->timeSatUnsat += clock() - clk;
// printf( "+" );
p->nProvedSets++;
// printf( " Unsat\n" );
// continue;
// printf( "Proved %d.\n", k );
// write it into a file
// Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
......@@ -277,10 +335,11 @@ p->timeSat += clock() - clk;
clk = clock();
nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
p->timeInt += clock() - clk;
assert( nFanins == Vec_PtrSize(vFanins) - 2 );
if ( nFanins != Vec_PtrSize(vFanins) - 2 )
continue;
assert( puTruth );
// Extra_PrintBinary( stdout, puTruth, 1 << nFanins ); printf( "\n" );
// transform interpolant into the AIG
pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
......@@ -294,8 +353,15 @@ clk = clock();
p->timeUpd += clock() - clk;
break;
}
// printf( "\n" );
}
Extra_ProgressBarStop( pProgress );
p->timeSatSim += p->pSim->timeSat;
p->timeSatTotal = p->timeSatSat + p->timeSatUnsat + p->timeSatSim;
p->nTotalNets2 = Abc_NtkGetTotalFanins(pNtk);
p->nTotalNodes2 = Abc_NtkNodeNum(pNtk);
// quit resubstitution manager
p->timeTotal = clock() - clkTotal;
......
src/opt/res/resDivs.c
......@@ -26,7 +26,6 @@
////////////////////////////////////////////////////////////////////////
static void Res_WinMarkTfi( Res_Win_t * p );
static int Res_WinVisitMffc( Res_Win_t * p );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -61,7 +60,7 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( p->pNode->pNtk );
Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
Res_WinVisitMffc( p );
Res_WinVisitMffc( p->pNode );
Abc_ObjForEachFanin( p->pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
......@@ -260,13 +259,14 @@ int Res_NodeRef_rec( Abc_Obj_t * pNode )
SeeAlso []
***********************************************************************/
int Res_WinVisitMffc( Res_Win_t * p )
int Res_WinVisitMffc( Abc_Obj_t * pNode )
{
int Count1, Count2;
assert( Abc_ObjIsNode(pNode) );
// dereference the node (mark with the current trav ID)
Count1 = Res_NodeDeref_rec( p->pNode );
Count1 = Res_NodeDeref_rec( pNode );
// reference it back
Count2 = Res_NodeRef_rec( p->pNode );
Count2 = Res_NodeRef_rec( pNode );
assert( Count1 == Count2 );
return Count1;
}
......
src/opt/res/resFilter.c
......@@ -26,6 +26,7 @@
////////////////////////////////////////////////////////////////////////
static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
static int Res_FilterCriticalFanin( Abc_Obj_t * pNode );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
......@@ -42,7 +43,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
SeeAlso []
***********************************************************************/
int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin, * pFanin2;
unsigned * pInfo;
......@@ -52,13 +53,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
printf( "Failed 1!\n" );
{
// printf( "Failed 1!\n" );
return 0;
}
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
printf( "Failed 2!\n" );
{
// printf( "Failed 2!\n" );
return 0;
}
// try removing fanins
// printf( "Fanins: " );
......@@ -71,7 +78,7 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue )
{
// printf( "Node %4d. Removing fanin %4d.\n", pWin->pNode->Id, Abc_ObjFaninId(pWin->pNode, i) );
// printf( "Node %4d. Candidate fanin %4d.\n", pWin->pNode->Id, pFanin->Id );
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
......@@ -94,6 +101,104 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
return Counter;
}
/**Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
{
Abc_Obj_t * pFanin;
unsigned * pInfo, * pInfo2;
int Counter, RetValue, i, k, iBest;
// check that the info the node is one
pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
{
// printf( "Failed 1!\n" );
return 0;
}
// collect the fanin info
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue == 0 )
{
// printf( "Failed 2!\n" );
return 0;
}
// try removing fanins
// printf( "Fanins: " );
Counter = 0;
Vec_VecClear( vResubs );
Vec_VecClear( vResubsW );
// get the best fanins
iBest = Res_FilterCriticalFanin( pWin->pNode );
if ( iBest == -1 )
return 0;
// get the info without the critical fanin
pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << iBest) );
RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
if ( RetValue )
{
// printf( "Can be done without one!\n" );
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
{
if ( k != iBest )
{
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
Vec_VecPush( vResubsW, Counter, pFanin );
}
}
Counter++;
// printf( "*" );
return Counter;
}
// go through the divisors
for ( i = Abc_ObjFaninNum(pWin->pNode) + 2; i < Abc_NtkPoNum(pAig); i++ )
{
pInfo2 = Vec_PtrEntry( pSim->vOuts, i );
if ( !Abc_InfoIsOrOne( pInfo, pInfo2, pSim->nWordsOut ) )
continue;
// collect the nodes
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
// collect the remaning fanins and the divisor
Abc_ObjForEachFanin( pWin->pNode, pFanin, k )
{
if ( k != iBest )
{
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
Vec_VecPush( vResubsW, Counter, pFanin );
}
}
// collect the divisor
Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,i) );
Vec_VecPush( vResubsW, Counter, Vec_PtrEntry(pWin->vDivs, i-2-Abc_ObjFaninNum(pWin->pNode)) );
Counter++;
if ( Counter == Vec_VecSize(vResubs) )
break;
}
return Counter;
}
/**Function*************************************************************
Synopsis [Finds sets of feasible candidates.]
......@@ -121,6 +226,40 @@ unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsig
}
/**Function*************************************************************
Synopsis [Returns the index of the most critical fanin.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Res_FilterCriticalFanin( Abc_Obj_t * pNode )
{
Abc_Obj_t * pFanin;
int i, iBest = -1, CostMax = 0, CostCur;
Abc_ObjForEachFanin( pNode, pFanin, i )
{
if ( !Abc_ObjIsNode(pFanin) )
continue;
if ( Abc_ObjFanoutNum(pFanin) > 1 )
continue;
CostCur = Res_WinVisitMffc( pFanin );
if ( CostMax < CostCur )
{
CostMax = CostCur;
iBest = i;
}
}
// if ( CostMax > 0 )
// printf( "<%d>", CostMax );
return iBest;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/opt/res/resInt.h
......@@ -68,9 +68,15 @@ typedef struct Res_Sim_t_ Res_Sim_t;
struct Res_Sim_t_
{
Abc_Ntk_t * pAig; // AIG for simulation
int nTruePis; // the number of true PIs of the window
int fConst0; // the node can be replaced by constant 0
int fConst1; // the node can be replaced by constant 0
// simulation parameters
int nWords; // the number of simulation words
int nPats; // the number of patterns
int nWordsIn; // the number of simulation words in the input patterns
int nPatsIn; // the number of patterns in the input patterns
int nBytesIn; // the number of bytes in the input patterns
int nWordsOut; // the number of simulation words in the output patterns
int nPatsOut; // the number of patterns in the output patterns
// simulation info
......@@ -82,6 +88,8 @@ struct Res_Sim_t_
int nPats1; // the number of 1-patterns accumulated
// resub candidates
Vec_Vec_t * vCands; // resubstitution candidates
// statistics
int timeSat;
};
////////////////////////////////////////////////////////////////////////
......@@ -95,15 +103,17 @@ struct Res_Sim_t_
/*=== resDivs.c ==========================================================*/
extern void Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
extern void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
extern int Res_WinVisitMffc( Abc_Obj_t * pNode );
/*=== resFilter.c ==========================================================*/
extern int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
extern int Res_FilterCandidatesNets( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
extern int Res_FilterCandidatesArea( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
/*=== resSat.c ==========================================================*/
extern void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
extern void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
extern int Res_SatSimulate( Res_Sim_t * p, int nPats, int fOnSet );
/*=== resSim.c ==========================================================*/
extern Res_Sim_t * Res_SimAlloc( int nWords );
extern void Res_SimFree( Res_Sim_t * p );
extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
extern int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig, int nTruePis, int fVerbose );
/*=== resStrash.c ==========================================================*/
extern Abc_Ntk_t * Res_WndStrash( Res_Win_t * p );
/*=== resWnd.c ==========================================================*/
......
src/opt/res/resSat.c
......@@ -128,25 +128,27 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
Description [The array of fanins contains exactly two entries: the
care set and the functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, int fOnSet )
{
sat_solver * pSat;
Vec_Ptr_t * vFanins;
Vec_Ptr_t * vNodes;
Abc_Obj_t * pObj;
int i, nNodes;
// make sure fanins contain POs of the AIG
pObj = Vec_PtrEntry( vFanins, 0 );
assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
assert( Vec_PtrSize(vFanins) == 2 );
// start the array
vFanins = Vec_PtrAlloc( 2 );
pObj = Abc_NtkPo( pAig, 0 );
Vec_PtrPush( vFanins, pObj );
pObj = Abc_NtkPo( pAig, 1 );
Vec_PtrPush( vFanins, pObj );
// collect reachable nodes
vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
......@@ -171,21 +173,154 @@ void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
Res_SatAddAnd( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
Vec_PtrFree( vNodes );
// add clauses for POs
Vec_PtrForEachEntry( vFanins, pObj, i )
Res_SatAddEqual( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add clauses for the first PO
pObj = Abc_NtkPo( pAig, 0 );
Res_SatAddEqual( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add clauses for the second PO
pObj = Abc_NtkPo( pAig, 1 );
Res_SatAddEqual( pSat, (int)pObj->pCopy,
(int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
// add trivial clauses
pObj = Vec_PtrEntry(vFanins, 0);
pObj = Abc_NtkPo( pAig, 0 );
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
pObj = Vec_PtrEntry(vFanins, 1);
Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
pObj = Abc_NtkPo( pAig, 1 );
Res_SatAddConst1( pSat, (int)pObj->pCopy, !fOnSet ); // on-set
Vec_PtrFree( vFanins );
return pSat;
}
/**Function*************************************************************
Synopsis [Loads AIG into the SAT solver for constrained simulation.]
Description [Returns 1 if the required number of patterns are found.
Returns 0 if the solver ran out of time or proved a constant.
In the latter, case one of the flags, fConst0 or fConst1, are set to 1.]
SideEffects []
SeeAlso []
***********************************************************************/
int Res_SatSimulate( Res_Sim_t * p, int nPatsLimit, int fOnSet )
{
Vec_Int_t * vLits;
Vec_Ptr_t * vPats;
sat_solver * pSat;
int RetValue, i, k, value, status, Lit, Var, iPat;
int clk = clock();
//printf( "Looking for %s: ", fOnSet? "onset " : "offset" );
// decide what problem should be solved
Lit = toLitCond( (int)Abc_NtkPo(p->pAig,1)->pCopy, !fOnSet );
if ( fOnSet )
{
iPat = p->nPats1;
vPats = p->vPats1;
}
else
{
iPat = p->nPats0;
vPats = p->vPats0;
}
assert( iPat < nPatsLimit );
// derive the SAT solver
pSat = Res_SatSimulateConstr( p->pAig, fOnSet );
pSat->fSkipSimplify = 1;
status = sat_solver_simplify( pSat );
if ( status == 0 )
{
if ( iPat == 0 )
{
// if ( fOnSet )
// p->fConst0 = 1;
// else
// p->fConst1 = 1;
RetValue = 0;
}
goto finish;
}
// enumerate through the SAT assignments
RetValue = 1;
vLits = Vec_IntAlloc( 32 );
for ( k = iPat; k < nPatsLimit; k++ )
{
// solve with the assumption
// status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
if ( status == l_False )
{
//printf( "Const %d\n", !fOnSet );
if ( k == 0 )
{
if ( fOnSet )
p->fConst0 = 1;
else
p->fConst1 = 1;
RetValue = 0;
}
break;
}
else if ( status == l_True )
{
// save the pattern
Vec_IntClear( vLits );
for ( i = 0; i < p->nTruePis; i++ )
{
Var = (int)Abc_NtkPi(p->pAig,i)->pCopy;
value = (int)(pSat->model.ptr[Var] == l_True);
if ( value )
Abc_InfoSetBit( Vec_PtrEntry(vPats, i), k );
Lit = toLitCond( Var, value );
Vec_IntPush( vLits, Lit );
// printf( "%d", value );
}
// printf( "\n" );
status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
if ( status == 0 )
{
k++;
RetValue = 1;
break;
}
}
else
{
//printf( "Undecided\n" );
if ( k == 0 )
RetValue = 0;
else
RetValue = 1;
break;
}
}
Vec_IntFree( vLits );
//printf( "Found %d patterns\n", k - iPat );
// set the new number of patterns
if ( fOnSet )
p->nPats1 = k;
else
p->nPats0 = k;
finish:
sat_solver_delete( pSat );
p->timeSat += clock() - clk;
return RetValue;
}
/**Function*************************************************************
Synopsis [Asserts equality of the variable to a constant.]
Description []
......
src/opt/res/resWin.c
......@@ -94,7 +94,7 @@ void Res_WinFree( Res_Win_t * p )
SeeAlso []
***********************************************************************/
void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
int Res_WinCollectLeavesAndNodes( Res_Win_t * p )
{
Vec_Ptr_t * vFront;
Abc_Obj_t * pObj, * pTemp;
......@@ -127,7 +127,8 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
}
}
}
assert( Vec_PtrSize(p->vLeaves) > 0 );
if ( Vec_PtrSize(p->vLeaves) == 0 )
return 0;
// collect the nodes in the reverse order
Vec_PtrClear( p->vNodes );
......@@ -146,6 +147,7 @@ void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
// set minimum traversal level
p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
assert( p->nLevTravMin >= 0 );
return 1;
}
......@@ -371,6 +373,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
// if this is not an internal node - make it a new branch
if ( !Abc_NodeIsTravIdPrevious(pObj) )
{
assert( Vec_PtrFind(p->vLeaves, pObj) == -1 );
Abc_NodeSetTravIdCurrent( pObj );
Vec_PtrPush( p->vBranches, pObj );
return;
......@@ -452,11 +455,15 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
p->pNode = pNode;
p->nWinTfiMax = nWinTfiMax;
p->nWinTfoMax = nWinTfoMax;
Vec_PtrClear( p->vBranches );
Vec_PtrClear( p->vDivs );
Vec_PtrClear( p->vRoots );
Vec_PtrPush( p->vRoots, pNode );
// compute the leaves
Res_WinCollectLeavesAndNodes( p );
if ( !Res_WinCollectLeavesAndNodes( p ) )
return 0;
// compute the candidate roots
if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
......
src/sat/bsat/satSolver.c
......@@ -457,6 +457,12 @@ static inline void sat_solver_canceluntil(sat_solver* s, int level) {
reasons = s->reasons;
bound = (veci_begin(&s->trail_lim))[level];
////////////////////////////////////////
// added to cancel all assignments
// if ( level == -1 )
// bound = 0;
////////////////////////////////////////
for (c = s->qtail-1; c >= bound; c--) {
int x = lit_var(trail[c]);
values [x] = l_Undef;
......@@ -881,7 +887,7 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
return l_Undef;
}
if (sat_solver_dlevel(s) == 0)
if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify)
// Simplify the set of problem clauses:
sat_solver_simplify(s);
......
src/sat/bsat/satSolver.h
......@@ -170,6 +170,8 @@ struct sat_solver_t
Sat_MmStep_t * pMem;
int fSkipSimplify; // set to one to skip simplification of the clause database
// clause store
void * pStore;
......
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