summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abci/abc.c231
-rw-r--r--src/base/abci/abcDec.c22
-rw-r--r--src/base/abci/abcDetect.c1067
-rw-r--r--src/base/cba/cba.h111
-rw-r--r--src/base/cba/cbaTypes.h169
-rw-r--r--src/base/io/io.c3
-rw-r--r--src/base/io/ioWriteDot.c2
-rw-r--r--src/base/wlc/module.make1
-rw-r--r--src/base/wlc/wlc.h6
-rw-r--r--src/base/wlc/wlcBlast.c11
-rw-r--r--src/base/wlc/wlcCom.c48
-rw-r--r--src/base/wlc/wlcNtk.c73
-rw-r--r--src/base/wlc/wlcWin.c166
13 files changed, 1748 insertions, 162 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 953a6c6a..7da88d3c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -55,6 +55,7 @@
#include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h"
#include "opt/sfm/sfm.h"
+#include "opt/sbd/sbd.h"
#include "bool/rpo/rpo.h"
#include "map/mpm/mpm.h"
#include "opt/fret/fretime.h"
@@ -134,7 +135,7 @@ static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandCascade ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandVarMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandDetect ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFaultClasses ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBmsStop ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -481,6 +482,7 @@ static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Mfsd ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -778,7 +780,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "cascade", Abc_CommandCascade, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "extract", Abc_CommandExtract, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 );
- Cmd_CommandAdd( pAbc, "Synthesis", "detect", Abc_CommandDetect, 0 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 );
@@ -1122,6 +1124,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&mfsd", Abc_CommandAbc9Mfsd, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
@@ -6212,6 +6215,9 @@ usage:
Abc_Print( -2, "\t 3: disjoint-support decomposition with cofactoring\n" );
Abc_Print( -2, "\t 4: updated disjoint-support decomposition with cofactoring\n" );
Abc_Print( -2, "\t 5: enumerating decomposable variable sets\n" );
+ Abc_Print( -2, "\t 6: disjoint-support decomposition with cofactoring and boolean difference analysis\n" );
+ Abc_Print( -2, "\t from V. Callegaro, F. S. Marranghello, M. G. A. Martins, R. P. Ribas and A. I. Reis,\n");
+ Abc_Print( -2, "\t \"Bottom-up disjoint-support decomposition based on cofactor and boolean difference analysis,\" ICCD'15.\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables (binary files only) [default = unused]\n" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -7235,23 +7241,33 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFaultClasses( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose );
+ extern void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose );
+ extern void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt );
Abc_Ntk_t * pNtk;
- int c, fSeq = 0, fVerbose = 0;
+ int c, fGen = 0, fStuckAt = 0, fSeq = 0, fVerbose = 0, fVeryVerbose = 0;
pNtk = Abc_FrameReadNtk(pAbc);
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "gcsvwh" ) ) != EOF )
{
switch ( c )
{
+ case 'g':
+ fGen ^= 1;
+ break;
+ case 'c':
+ fStuckAt ^= 1;
+ break;
case 's':
fSeq ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -7268,14 +7284,25 @@ int Abc_CommandDetect( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Only applicable to a logic network.\n" );
return 1;
}
- Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose );
+ if ( fGen )
+ {
+ char * pFileName = Extra_FileNameGenericAppend(Abc_NtkSpec(pNtk), "_faults.txt");
+ Abc_NtkGenFaultList( pNtk, pFileName, fStuckAt );
+ }
+ else
+ Abc_NtkDetectClassesTest( pNtk, fSeq, fVerbose, fVeryVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: detect [-svh]\n" );
- Abc_Print( -2, "\t detects properties of internal nodes\n" );
- Abc_Print( -2, "\t-s : toggle using sequential circuit information [default = %s]\n", fSeq? "yes": "no" );
- Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "usage: faultclasses [-gcsvwh]\n" );
+ Abc_Print( -2, "\t computes equivalence classes of faults in the given mapped netlist;\n" );
+ Abc_Print( -2, "\t the fault list with faults in the format: <fault_id> <node_name> <fault_name>\n" );
+ Abc_Print( -2, "\t should be read by command \"read_fins\" before calling this command\n" );
+ Abc_Print( -2, "\t-g : toggle generating a fault list for the current mapped network [default = %s]\n", fGen? "yes": "no" );
+ Abc_Print( -2, "\t-c : toggle using only stuck-at faults in the generated fault list [default = %s]\n", fStuckAt? "yes": "no" );
+ Abc_Print( -2, "\t-s : toggle detecting sequential equivalence classes [default = %s]\n", fSeq? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle verbose printout during computation [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing of resulting fault equivalence classes [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
@@ -7443,7 +7470,7 @@ usage:
Abc_Print( -2, "\t finds optimum networks using SAT-based exact synthesis for hex truth tables <truth1> <truth2> ...\n" );
Abc_Print( -2, "\t-D <num> : constrain maximum depth (if too low, algorithm may not terminate)\n" );
Abc_Print( -2, "\t-A <list> : input arrival times (comma separated list)\n" );
- Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %s]\n", nStartGates );
+ Abc_Print( -2, "\t-S <num> : number of start gates in search [default = %d]\n", nStartGates );
Abc_Print( -2, "\t-C <num> : the limit on the number of conflicts; turn off with 0 [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-a : toggle create AIG [default = %s]\n", fMakeAIG ? "yes" : "no" );
Abc_Print( -2, "\t-t : run test suite\n" );
@@ -11840,7 +11867,7 @@ int Abc_CommandTestColor( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ //Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int nCutMax = 1;
int nLeafMax = 4;
int nDivMax = 2;
@@ -12047,8 +12074,6 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
// extern void Cba_PrsReadBlifTest();
// Cba_PrsReadBlifTest();
- extern void Sfm_TimTest( Abc_Ntk_t * pNtk );
- Sfm_TimTest( pNtk );
}
return 0;
usage:
@@ -26971,12 +26996,13 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
char ** pArgvNew;
char * FileName, * pTemp;
int c, nArgcNew;
- int fUseMini = 0;
+ int fMiniAig = 0;
+ int fMiniLut = 0;
int fVerbose = 0;
int fGiaSimple = 0;
int fSkipStrash = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "csmvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "csmlvh" ) ) != EOF )
{
switch ( c )
{
@@ -26987,7 +27013,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
fSkipStrash ^= 1;
break;
case 'm':
- fUseMini ^= 1;
+ fMiniAig ^= 1;
+ break;
+ case 'l':
+ fMiniLut ^= 1;
break;
case 'v':
fVerbose ^= 1;
@@ -27020,8 +27049,10 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
}
fclose( pFile );
- if ( fUseMini )
+ if ( fMiniAig )
pAig = Gia_ManReadMiniAig( FileName );
+ else if ( fMiniLut )
+ pAig = Gia_ManReadMiniLut( FileName );
// else if ( Extra_FileIsType( FileName, ".v", NULL, NULL ) )
// Abc3_ReadShowHie( FileName, fSkipStrash );
else
@@ -27031,11 +27062,12 @@ int Abc_CommandAbc9Read( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- Abc_Print( -2, "usage: &r [-csmvh] <file>\n" );
+ Abc_Print( -2, "usage: &r [-csmlvh] <file>\n" );
Abc_Print( -2, "\t reads the current AIG from the AIGER file\n" );
Abc_Print( -2, "\t-c : toggles reading simple AIG [default = %s]\n", fGiaSimple? "yes": "no" );
Abc_Print( -2, "\t-s : toggles structural hashing while reading [default = %s]\n", !fSkipStrash? "yes": "no" );
- Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fUseMini? "yes": "no" );
+ Abc_Print( -2, "\t-m : toggles reading MiniAIG rather than AIGER file [default = %s]\n", fMiniAig? "yes": "no" );
+ Abc_Print( -2, "\t-l : toggles reading MiniLUT rather than AIGER file [default = %s]\n", fMiniLut? "yes": "no" );
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n");
@@ -27616,6 +27648,7 @@ static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int
*pnBestLuts = nCurLuts;
*pnBestEdges = nCurEdges;
*pnBestLevels = nCurLevels;
+ //printf( "\nUpdating best (%d %d %d).\n\n", nCurLuts, nCurEdges, nCurLevels );
return 1;
}
return 0;
@@ -27815,9 +27848,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, nArgcNew;
int fUnique = 0;
int fMiniAig = 0;
+ int fMiniLut = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "umvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "umlvh" ) ) != EOF )
{
switch ( c )
{
@@ -27827,6 +27861,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMiniAig ^= 1;
break;
+ case 'l':
+ fMiniLut ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -27857,15 +27894,18 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else if ( fMiniAig )
Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
+ else if ( fMiniLut )
+ Gia_ManWriteMiniLut( pAbc->pGia, pFileName );
else
Gia_AigerWrite( pAbc->pGia, pFileName, 0, 0 );
return 0;
usage:
- Abc_Print( -2, "usage: &w [-umvh] <file>\n" );
+ Abc_Print( -2, "usage: &w [-umlvh] <file>\n" );
Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" );
Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
+ Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<file> : the file name\n");
@@ -28193,9 +28233,10 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Gia_ManMuxProfiling( Gia_Man_t * p );
extern void Gia_ManProfileStructures( Gia_Man_t * p, int nLimit, int fVerbose );
extern void Acec_StatsCollect( Gia_Man_t * p, int fVerbose );
- int c, fNpn = 0, fMuxes = 0, nLimit = 0, fVerbose = 0;
+ extern void Acec_ManProfile( Gia_Man_t * p, int fVerbose );
+ int c, fNpn = 0, fMuxes = 0, fAdders = 0, nLimit = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Nnmavh" ) ) != EOF )
{
switch ( c )
{
@@ -28216,6 +28257,9 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fMuxes ^= 1;
break;
+ case 'a':
+ fAdders ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -28241,16 +28285,19 @@ int Abc_CommandAbc9MuxProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else if ( fMuxes )
Gia_ManMuxProfiling( pAbc->pGia );
+ else if ( fAdders )
+ Acec_ManProfile( pAbc->pGia, fVerbose );
else
Gia_ManProfileStructures( pAbc->pGia, nLimit, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &profile [-N num] [-nmvh]\n" );
+ Abc_Print( -2, "usage: &profile [-N num] [-nmavh]\n" );
Abc_Print( -2, "\t profile gate structures appearing in the AIG\n" );
Abc_Print( -2, "\t-N num : limit on class size to show [default = %d]\n", nLimit );
Abc_Print( -2, "\t-n : toggle profiling NPN-classes (for 3-LUT mapped AIGs) [default = %s]\n", fNpn? "yes": "no" );
Abc_Print( -2, "\t-m : toggle profiling MUX structures [default = %s]\n", fMuxes? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle profiling adder structures [default = %s]\n", fAdders? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
@@ -30989,7 +31036,7 @@ usage:
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
Abc_Print( -2, "\t-K num : the target LUT size for downstream mapping [default = %d]\n", nLutSize );
- Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
+ Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
@@ -40805,6 +40852,136 @@ usage:
Synopsis []
Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandAbc9Mfsd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars );
+ Gia_Man_t * pTemp; int c;
+ Sbd_Par_t Pars, * pPars = &Pars;
+ Sbd_ParSetDefault( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KWFMCacvwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'K':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nLutSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nLutSize < 0 )
+ goto usage;
+ break;
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nTfoLevels = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nTfoLevels < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nTfoFanMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nTfoFanMax < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "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 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'a':
+ pPars->fArea ^= 1;
+ break;
+ case 'c':
+ pPars->fCover ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pAbc->pGia == NULL )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Mfs(): There is no AIG.\n" );
+ return 0;
+ }
+ if ( Gia_ManBufNum(pAbc->pGia) )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Mfs(): This command does not work with barrier buffers.\n" );
+ return 1;
+ }
+ if ( Gia_ManHasMapping(pAbc->pGia) )
+ {
+ Abc_Print( -1, "Abc_CommandAbc9Mfs(): The current AIG has mapping (run &st to unmap).\n" );
+ return 0;
+ }
+ pTemp = Sbd_NtkPerform( pAbc->pGia, pPars );
+ Abc_FrameUpdateGia( pAbc, pTemp );
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: &mfsd [-KWFMC <num>] [-acvwh]\n" );
+ Abc_Print( -2, "\t performs SAT-based delay-oriented AIG optimization\n" );
+ Abc_Print( -2, "\t-K <num> : the LUT size for delay minimization (2 <= num <= 6) [default = %d]\n", pPars->nLutSize );
+ Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevels );
+ Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nTfoFanMax );
+ Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+ Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
+ Abc_Print( -2, "\t-c : toggle using complete slow covering procedure [default = %s]\n", pPars->fCover? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
SideEffects []
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 919a46de..8bb04f16 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -26,6 +26,7 @@
#include "bool/kit/kit.h"
#include "opt/dau/dau.h"
#include "misc/util/utilTruth.h"
+#include "opt/dsc/dsc.h"
ABC_NAMESPACE_IMPL_START
@@ -484,6 +485,8 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
pAlgoName = "fast DSD";
else if ( DecType == 5 )
pAlgoName = "analysis";
+ else if ( DecType == 6 )
+ pAlgoName = "DSD ICCD'15";
if ( pAlgoName )
printf( "Applying %-10s to %8d func%s of %2d vars... ",
@@ -577,6 +580,23 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
if ( fVerbose )
printf( "\n" );
}
+ } else if ( DecType == 6 )
+ {
+ char pDsd[DSC_MAX_STR];
+ /* memory pool with a capacity of storing 3*nVars
+ truth-tables for negative and positive cofactors and
+ the boolean difference for each input variable */
+ word *mem_pool = Dsc_alloc_pool(p->nVars);
+ for ( i = 0; i < p->nFuncs; i++ )
+ {
+ if ( fVerbose )
+ printf( "%7d : ", i );
+ Dsc_Decompose(p->pFuncs[i], p->nVars, pDsd, mem_pool);
+ if ( fVerbose )
+ printf( "%s\n", pDsd[0] ? pDsd : "NULL");
+ nNodes += Dsc_CountAnds( pDsd );
+ }
+ Dsc_free_pool(mem_pool);
}
else assert( 0 );
@@ -629,7 +649,7 @@ int Abc_DecTest( char * pFileName, int DecType, int nVarNum, int fVerbose )
printf( "Using truth tables from file \"%s\"...\n", pFileName );
if ( DecType == 0 )
{ if ( nVarNum < 0 ) Abc_TtStoreTest( pFileName ); }
- else if ( DecType >= 1 && DecType <= 5 )
+ else if ( DecType >= 1 && DecType <= 6 )
Abc_TruthDecTest( pFileName, DecType, nVarNum, fVerbose );
else
printf( "Unknown decomposition type value (%d).\n", DecType );
diff --git a/src/base/abci/abcDetect.c b/src/base/abci/abcDetect.c
index c87169b5..8b8bba64 100644
--- a/src/base/abci/abcDetect.c
+++ b/src/base/abci/abcDetect.c
@@ -23,6 +23,8 @@
#include "misc/util/utilNam.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
+#include "map/mio/mio.h"
+#include "map/mio/exp.h"
ABC_NAMESPACE_IMPL_START
@@ -31,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
typedef enum {
- ABC_FIN_NONE = 0, // 0: unknown
+ ABC_FIN_NONE = -100, // 0: unknown
ABC_FIN_SA0, // 1:
ABC_FIN_SA1, // 2:
ABC_FIN_NEG, // 3:
@@ -52,6 +54,51 @@ typedef enum {
/**Function*************************************************************
+ Synopsis [Generates fault list for the given mapped network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkGenFaultList( Abc_Ntk_t * pNtk, char * pFileName, int fStuckAt )
+{
+ Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
+ Mio_Gate_t * pGate;
+ Abc_Obj_t * pObj;
+ int i, Count = 1;
+ FILE * pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file \"%s\" for writing.\n", pFileName );
+ return;
+ }
+ assert( Abc_NtkIsMappedLogic(pNtk) );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ Mio_Gate_t * pGateObj = (Mio_Gate_t *)pObj->pData;
+ int nInputs = Mio_GateReadPinNum(pGateObj);
+ // add basic faults (SA0, SA1, NEG)
+ fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA0" ), Count++;
+ fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "SA1" ), Count++;
+ fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), "NEG" ), Count++;
+ if ( fStuckAt )
+ continue;
+ // add other faults, which correspond to changing the given gate
+ // by another gate with the same support-size from the same library
+ Mio_LibraryForEachGate( pLib, pGate )
+ if ( pGate != pGateObj && Mio_GateReadPinNum(pGate) == nInputs )
+ fprintf( pFile, "%d %s %s\n", Count, Abc_ObjName(pObj), Mio_GateReadName(pGate) ), Count++;
+ }
+ printf( "Generated fault list \"%s\" for network \"%s\" with %d nodes and %d %sfaults.\n",
+ pFileName, Abc_NtkName(pNtk), Abc_NtkNodeNum(pNtk), Count-1, fStuckAt ? "stuck-at ":"" );
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
Synopsis [Recognize type.]
Description []
@@ -61,6 +108,16 @@ typedef enum {
SeeAlso []
***********************************************************************/
+int Io_ReadFinTypeMapped( Mio_Library_t * pLib, char * pThis )
+{
+ Mio_Gate_t * pGate = Mio_LibraryReadGateByName( pLib, pThis, NULL );
+ if ( pGate == NULL )
+ {
+ printf( "Cannot find gate \"%s\" in the current library.\n", pThis );
+ return ABC_FIN_NONE;
+ }
+ return Mio_GateReadCell( pGate );
+}
int Io_ReadFinType( char * pThis )
{
if ( !strcmp(pThis, "SA0") ) return ABC_FIN_SA0;
@@ -106,6 +163,7 @@ char * Io_WriteFinType( int Type )
***********************************************************************/
Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
{
+ Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
char Buffer[1000];
Abc_Obj_t * pObj;
Abc_Nam_t * pNam;
@@ -142,6 +200,8 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
{
// read line number
char * pToken = strtok( Buffer, " \n\r\t" );
+ if ( pToken == NULL )
+ break;
if ( nLines++ != atoi(pToken) )
{
printf( "Line numbers are not consecutive. Quitting.\n" );
@@ -158,7 +218,15 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
}
// read type
pToken = strtok( NULL, " \n\r\t" );
- Type = Io_ReadFinType( pToken );
+ if ( Abc_NtkIsMappedLogic(pNtk) )
+ {
+ if ( !strcmp(pToken, "SA0") || !strcmp(pToken, "SA1") || !strcmp(pToken, "NEG") )
+ Type = Io_ReadFinType( pToken );
+ else
+ Type = Io_ReadFinTypeMapped( pLib, pToken );
+ }
+ else
+ Type = Io_ReadFinType( pToken );
if ( Type == ABC_FIN_NONE )
{
printf( "Cannot read type \"%s\" of object \"%s\".\n", pToken, Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
@@ -167,7 +235,7 @@ Vec_Int_t * Io_ReadFins( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose )
Vec_IntPushTwo( vPairs, Vec_IntEntry(vMap, iObj), Type );
}
assert( Vec_IntSize(vPairs) == 2 * nLines );
- printf( "Finished reading %d lines.\n", nLines - 1 );
+ printf( "Finished reading %d lines from the fault list file \"%s\".\n", nLines - 1, pFileName );
// verify the reader by printing the results
if ( fVerbose )
@@ -184,6 +252,984 @@ finish:
/**Function*************************************************************
+ Synopsis [Extend the network by adding second timeframe.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFrameExtend( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vFanins, * vNodes;
+ Abc_Obj_t * pObj, * pFanin, * pReset, * pEnable, * pSignal;
+ Abc_Obj_t * pResetN, * pEnableN, * pAnd0, * pAnd1, * pMux;
+ int i, k, iStartPo, nPisOld = Abc_NtkPiNum(pNtk), nPosOld = Abc_NtkPoNum(pNtk);
+ // skip if there are no flops
+ if ( pNtk->nConstrs == 0 )
+ return;
+ assert( Abc_NtkPiNum(pNtk) >= pNtk->nConstrs );
+ assert( Abc_NtkPoNum(pNtk) >= pNtk->nConstrs * 4 );
+ // collect nodes
+ vNodes = Vec_PtrAlloc( Abc_NtkNodeNum(pNtk) );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ Vec_PtrPush( vNodes, pObj );
+ // duplicate PIs
+ vFanins = Vec_PtrAlloc( 2 );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ {
+ if ( i == nPisOld )
+ break;
+ if ( i < nPisOld - pNtk->nConstrs )
+ {
+ Abc_NtkDupObj( pNtk, pObj, 0 );
+ Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" );
+ continue;
+ }
+ // create flop input
+ iStartPo = nPosOld + 4 * (i - nPisOld);
+ pReset = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 1 ) );
+ pEnable = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 2 ) );
+ pSignal = Abc_ObjFanin0( Abc_NtkPo( pNtk, iStartPo + 3 ) );
+ pResetN = Abc_NtkCreateNodeInv( pNtk, pReset );
+ pEnableN = Abc_NtkCreateNodeInv( pNtk, pEnable );
+ Vec_PtrFillTwo( vFanins, 2, pEnableN, pObj );
+ pAnd0 = Abc_NtkCreateNodeAnd( pNtk, vFanins );
+ Vec_PtrFillTwo( vFanins, 2, pEnable, pSignal );
+ pAnd1 = Abc_NtkCreateNodeAnd( pNtk, vFanins );
+ Vec_PtrFillTwo( vFanins, 2, pAnd0, pAnd1 );
+ pMux = Abc_NtkCreateNodeOr( pNtk, vFanins );
+ Vec_PtrFillTwo( vFanins, 2, pResetN, pMux );
+ pObj->pCopy = Abc_NtkCreateNodeAnd( pNtk, vFanins );
+ }
+ // duplicate internal nodes
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ Abc_NtkDupObj( pNtk, pObj, 0 );
+ // connect objects
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy );
+ // create new POs and reconnect flop inputs
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ if ( i == nPosOld )
+ break;
+ if ( i < nPosOld - 4 * pNtk->nConstrs )
+ {
+ Abc_NtkDupObj( pNtk, pObj, 0 );
+ Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj), "_frame1" );
+ Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
+ continue;
+ }
+ Abc_ObjPatchFanin( pObj, Abc_ObjFanin0(pObj), Abc_ObjFanin0(pObj)->pCopy );
+ }
+ Vec_PtrFree( vFanins );
+ Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detect equivalence classes of nodes in terms of their TFO.]
+
+ Description [Given is the logic network (pNtk) and the set of objects
+ (primary inputs or internal nodes) to be considered (vObjs), this function
+ returns a set of equivalence classes of these objects in terms of their
+ transitive fanout (TFO). Two objects belong to the same class if the set
+ of COs they feed into are the same.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDetectObjClasses_rec( Abc_Obj_t * pObj, Vec_Int_t * vMap, Hsh_VecMan_t * pHash, Vec_Int_t * vTemp )
+{
+ Vec_Int_t * vArray, * vSet;
+ Abc_Obj_t * pNext; int i;
+ // get the CO set for this object
+ int Entry = Vec_IntEntry(vMap, Abc_ObjId(pObj));
+ if ( Entry != -1 ) // the set is already computed
+ return Entry;
+ // compute a new CO set
+ assert( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) );
+ // if there is no fanouts, the set of COs is empty
+ if ( Abc_ObjFanoutNum(pObj) == 0 )
+ {
+ Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), 0 );
+ return 0;
+ }
+ // compute the set for the first fanout
+ Entry = Abc_NtkDetectObjClasses_rec( Abc_ObjFanout0(pObj), vMap, pHash, vTemp );
+ if ( Abc_ObjFanoutNum(pObj) == 1 )
+ {
+ Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry );
+ return Entry;
+ }
+ vSet = Vec_IntAlloc( 16 );
+ // initialize the set with that of first fanout
+ vArray = Hsh_VecReadEntry( pHash, Entry );
+ Vec_IntClear( vSet );
+ Vec_IntAppend( vSet, vArray );
+ // iteratively add sets of other fanouts
+ Abc_ObjForEachFanout( pObj, pNext, i )
+ {
+ if ( i == 0 )
+ continue;
+ Entry = Abc_NtkDetectObjClasses_rec( pNext, vMap, pHash, vTemp );
+ vArray = Hsh_VecReadEntry( pHash, Entry );
+ Vec_IntTwoMerge2( vSet, vArray, vTemp );
+ ABC_SWAP( Vec_Int_t, *vSet, *vTemp );
+ }
+ // create or find new set and map the object into it
+ Entry = Hsh_VecManAdd( pHash, vSet );
+ Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), Entry );
+ Vec_IntFree( vSet );
+ return Entry;
+}
+Vec_Wec_t * Abc_NtkDetectObjClasses( Abc_Ntk_t * pNtk, Vec_Int_t * vObjs, Vec_Wec_t ** pvCos )
+{
+ Vec_Wec_t * vClasses; // classes of equivalence objects from vObjs
+ Vec_Int_t * vClassMap; // mapping of each CO set into its class in vClasses
+ Vec_Int_t * vClass; // one equivalence class
+ Abc_Obj_t * pObj;
+ int i, iObj, SetId, ClassId;
+ // create hash table to hash sets of CO indexes
+ Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000 );
+ // create elementary sets (each composed of one CO) and map COs into them
+ Vec_Int_t * vMap = Vec_IntStartFull( Abc_NtkObjNumMax(pNtk) );
+ Vec_Int_t * vSet = Vec_IntAlloc( 16 );
+ assert( Abc_NtkIsLogic(pNtk) );
+ // compute empty set
+ SetId = Hsh_VecManAdd( pHash, vSet );
+ assert( SetId == 0 );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ Vec_IntFill( vSet, 1, Abc_ObjId(pObj) );
+ SetId = Hsh_VecManAdd( pHash, vSet );
+ Vec_IntWriteEntry( vMap, Abc_ObjId(pObj), SetId );
+ }
+ // make sure the array of objects is sorted
+ Vec_IntSort( vObjs, 0 );
+ // begin from the objects and map their IDs into sets of COs
+ Abc_NtkForEachObjVec( vObjs, pNtk, pObj, i )
+ Abc_NtkDetectObjClasses_rec( pObj, vMap, pHash, vSet );
+ Vec_IntFree( vSet );
+ // create map for mapping CO set its their classes
+ vClassMap = Vec_IntStartFull( Hsh_VecSize(pHash) + 1 );
+ // collect classes of objects
+ vClasses = Vec_WecAlloc( 1000 );
+ Vec_IntForEachEntry( vObjs, iObj, i )
+ {
+ //char * pName = Abc_ObjName( Abc_NtkObj(pNtk, iObj) );
+ // for a given object (iObj), find the ID of its COs set
+ SetId = Vec_IntEntry( vMap, iObj );
+ assert( SetId >= 0 );
+ // for the given CO set, finds its equivalence class
+ ClassId = Vec_IntEntry( vClassMap, SetId );
+ if ( ClassId == -1 ) // there is no equivalence class
+ {
+ // map this CO set into a new equivalence class
+ Vec_IntWriteEntry( vClassMap, SetId, Vec_WecSize(vClasses) );
+ vClass = Vec_WecPushLevel( vClasses );
+ }
+ else // get hold of the equivalence class
+ vClass = Vec_WecEntry( vClasses, ClassId );
+ // add objects to the class
+ Vec_IntPush( vClass, iObj );
+ // print the set for this object
+ //printf( "Object %5d : ", iObj );
+ //Vec_IntPrint( Hsh_VecReadEntry(pHash, SetId) );
+ }
+ // collect arrays of COs for each class
+ *pvCos = Vec_WecStart( Vec_WecSize(vClasses) );
+ Vec_WecForEachLevel( vClasses, vClass, i )
+ {
+ iObj = Vec_IntEntry( vClass, 0 );
+ // for a given object (iObj), find the ID of its COs set
+ SetId = Vec_IntEntry( vMap, iObj );
+ assert( SetId >= 0 );
+ // for the given CO set ID, find the set
+ vSet = Hsh_VecReadEntry( pHash, SetId );
+ Vec_IntAppend( Vec_WecEntry(*pvCos, i), vSet );
+ }
+ Hsh_VecManStop( pHash );
+ Vec_IntFree( vClassMap );
+ Vec_IntFree( vMap );
+ return vClasses;
+}
+void Abc_NtkDetectClassesTest2( Abc_Ntk_t * pNtk, int fVerbose, int fVeryVerbose )
+{
+ Vec_Int_t * vObjs;
+ Vec_Wec_t * vRes, * vCos;
+ // for testing, create the set of object IDs for all combinational inputs (CIs)
+ Abc_Obj_t * pObj; int i;
+ vObjs = Vec_IntAlloc( Abc_NtkCiNum(pNtk) );
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ Vec_IntPush( vObjs, Abc_ObjId(pObj) );
+ // compute equivalence classes of CIs and print them
+ vRes = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCos );
+ Vec_WecPrint( vRes, 0 );
+ Vec_WecPrint( vCos, 0 );
+ // clean up
+ Vec_IntFree( vObjs );
+ Vec_WecFree( vRes );
+ Vec_WecFree( vCos );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Collecting objects.]
+
+ Description [Collects combinational inputs (vCIs) and internal nodes (vNodes)
+ reachable from the given set of combinational outputs (vCOs).]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFinMiterCollect_rec( Abc_Obj_t * pObj, Vec_Int_t * vCis, Vec_Int_t * vNodes )
+{
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ return;
+ Abc_NodeSetTravIdCurrent(pObj);
+ if ( Abc_ObjIsCi(pObj) )
+ Vec_IntPush( vCis, Abc_ObjId(pObj) );
+ else
+ {
+ Abc_Obj_t * pFanin; int i;
+ assert( Abc_ObjIsNode( pObj ) );
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ Abc_NtkFinMiterCollect_rec( pFanin, vCis, vNodes );
+ Vec_IntPush( vNodes, Abc_ObjId(pObj) );
+ }
+}
+void Abc_NtkFinMiterCollect( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes )
+{
+ Abc_Obj_t * pObj; int i;
+ Vec_IntClear( vCis );
+ Vec_IntClear( vNodes );
+ Abc_NtkIncrementTravId( pNtk );
+ Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
+ Abc_NtkFinMiterCollect_rec( Abc_ObjFanin0(pObj), vCis, vNodes );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates expression using given simulation info.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim )
+{
+ int i, w, nVars = Mio_GateReadPinNum(pGate);
+ Vec_Int_t * vExpr = Mio_GateReadExpr( pGate );
+ assert( nVars <= 6 );
+ for ( w = 0; w < nWords; w++ )
+ {
+ word uFanins[6];
+ for ( i = 0; i < nVars; i++ )
+ uFanins[i] = ppFaninSims[i][w];
+ pObjSim[w] = Exp_Truth6( nVars, vExpr, uFanins );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulates expression for one simulation pattern.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] )
+{
+ int nVars = Mio_GateReadPinNum(pGate);
+ int i, iMint = 0;
+ for ( i = 0; i < nVars; i++ )
+ if ( iBits[i] )
+ iMint |= (1 << i);
+ return Abc_InfoHasBit( (unsigned *)Mio_GateReadTruthP(pGate), iMint );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Simulated expression with one bit.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits )
+{
+ int i, nVars = Mio_GateReadPinNum(pGate);
+ Vec_Int_t * vExpr = Mio_GateReadExpr( pGate );
+ if ( Exp_IsConst0(vExpr) )
+ return 0;
+ if ( Exp_IsConst1(vExpr) )
+ return 1;
+ if ( Exp_IsLit(vExpr) )
+ {
+ int Index0 = Vec_IntEntry(vExpr,0) >> 1;
+ int fCompl0 = Vec_IntEntry(vExpr,0) & 1;
+ assert( Index0 < nVars );
+ return Abc_LitNotCond( iLits[Index0], fCompl0 );
+ }
+ Vec_IntClear( vLits );
+ for ( i = 0; i < nVars; i++ )
+ Vec_IntPush( vLits, iLits[i] );
+ for ( i = 0; i < Exp_NodeNum(vExpr); i++ )
+ {
+ int Index0 = Vec_IntEntry( vExpr, 2*i+0 ) >> 1;
+ int Index1 = Vec_IntEntry( vExpr, 2*i+1 ) >> 1;
+ int fCompl0 = Vec_IntEntry( vExpr, 2*i+0 ) & 1;
+ int fCompl1 = Vec_IntEntry( vExpr, 2*i+1 ) & 1;
+ Vec_IntPush( vLits, Gia_ManHashAnd( pGia, Abc_LitNotCond(Vec_IntEntry(vLits, Index0), fCompl0), Abc_LitNotCond(Vec_IntEntry(vLits, Index1), fCompl1) ) );
+ }
+ return Abc_LitNotCond( Vec_IntEntryLast(vLits), Vec_IntEntryLast(vExpr) & 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis [AIG construction and simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_NtkFinSimOneLit( Gia_Man_t * pNew, Abc_Obj_t * pObj, int Type, Vec_Int_t * vMap, int n, Vec_Int_t * vTemp )
+{
+ if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 )
+ {
+ extern int Mio_LibGateSimulateGia( Gia_Man_t * pGia, Mio_Gate_t * pGate, int iLits[6], Vec_Int_t * vLits );
+ Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc;
+ int i, Lits[6];
+ for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
+ Lits[i] = Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId(pObj, i), n) );
+ return Mio_LibGateSimulateGia( pNew, Mio_LibraryReadGateById(pLib, Type), Lits, vTemp );
+ }
+ else
+ {
+ int iLit0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId0(pObj), n) ) : -1;
+ int iLit1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_IntEntry( vMap, Abc_Var2Lit(Abc_ObjFaninId1(pObj), n) ) : -1;
+ assert( Type != ABC_FIN_NEG );
+ if ( Type == ABC_FIN_SA0 ) return 0;
+ if ( Type == ABC_FIN_SA1 ) return 1;
+ if ( Type == ABC_FIN_RDOB_BUFF ) return iLit0;
+ if ( Type == ABC_FIN_RDOB_NOT ) return Abc_LitNot( iLit0 );
+ if ( Type == ABC_FIN_RDOB_AND ) return Gia_ManHashAnd( pNew, iLit0, iLit1 );
+ if ( Type == ABC_FIN_RDOB_OR ) return Gia_ManHashOr( pNew, iLit0, iLit1 );
+ if ( Type == ABC_FIN_RDOB_XOR ) return Gia_ManHashXor( pNew, iLit0, iLit1 );
+ if ( Type == ABC_FIN_RDOB_NAND ) return Abc_LitNot(Gia_ManHashAnd( pNew, iLit0, iLit1 ));
+ if ( Type == ABC_FIN_RDOB_NOR ) return Abc_LitNot(Gia_ManHashOr( pNew, iLit0, iLit1 ));
+ if ( Type == ABC_FIN_RDOB_NXOR ) return Abc_LitNot(Gia_ManHashXor( pNew, iLit0, iLit1 ));
+ assert( 0 );
+ return -1;
+ }
+}
+static inline int Abc_NtkFinSimOneBit( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords, int iBit )
+{
+ if ( Abc_NtkIsMappedLogic(pObj->pNtk) && Type >= 0 )
+ {
+ extern int Mio_LibGateSimulateOne( Mio_Gate_t * pGate, int iBits[6] );
+ Mio_Library_t * pLib = (Mio_Library_t *)pObj->pNtk->pManFunc;
+ int i, iBits[6];
+ for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
+ {
+ word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) );
+ iBits[i] = Abc_InfoHasBit( (unsigned*)pSim0, iBit );
+ }
+ return Mio_LibGateSimulateOne( Mio_LibraryReadGateById(pLib, Type), iBits );
+ }
+ else
+ {
+ word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL;
+ word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL;
+ int iBit0 = Abc_ObjFaninNum(pObj) > 0 ? Abc_InfoHasBit( (unsigned*)pSim0, iBit ) : -1;
+ int iBit1 = Abc_ObjFaninNum(pObj) > 1 ? Abc_InfoHasBit( (unsigned*)pSim1, iBit ) : -1;
+ assert( Type != ABC_FIN_NEG );
+ if ( Type == ABC_FIN_SA0 ) return 0;
+ if ( Type == ABC_FIN_SA1 ) return 1;
+ if ( Type == ABC_FIN_RDOB_BUFF ) return iBit0;
+ if ( Type == ABC_FIN_RDOB_NOT ) return !iBit0;
+ if ( Type == ABC_FIN_RDOB_AND ) return iBit0 & iBit1;
+ if ( Type == ABC_FIN_RDOB_OR ) return iBit0 | iBit1;
+ if ( Type == ABC_FIN_RDOB_XOR ) return iBit0 ^ iBit1;
+ if ( Type == ABC_FIN_RDOB_NAND ) return !(iBit0 & iBit1);
+ if ( Type == ABC_FIN_RDOB_NOR ) return !(iBit0 | iBit1);
+ if ( Type == ABC_FIN_RDOB_NXOR ) return !(iBit0 ^ iBit1);
+ assert( 0 );
+ return -1;
+ }
+}
+static inline void Abc_NtkFinSimOneWord( Abc_Obj_t * pObj, int Type, Vec_Wrd_t * vSims, int nWords )
+{
+ if ( Abc_NtkIsMappedLogic(pObj->pNtk) )
+ {
+ extern void Mio_LibGateSimulate( Mio_Gate_t * pGate, word * ppFaninSims[6], int nWords, word * pObjSim );
+ word * ppSims[6]; int i;
+ word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
+ assert( Type == -1 );
+ for ( i = 0; i < Abc_ObjFaninNum(pObj); i++ )
+ ppSims[i] = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId(pObj, i) );
+ Mio_LibGateSimulate( (Mio_Gate_t *)pObj->pData, ppSims, nWords, pSim );
+ }
+ else
+ {
+ word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) ); int w;
+ word * pSim0 = Abc_ObjFaninNum(pObj) > 0 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) ) : NULL;
+ word * pSim1 = Abc_ObjFaninNum(pObj) > 1 ? Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId1(pObj) ) : NULL;
+ assert( Type != ABC_FIN_NEG );
+ if ( Type == ABC_FIN_SA0 ) for ( w = 0; w < nWords; w++ ) pSim[w] = 0;
+ else if ( Type == ABC_FIN_SA1 ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~((word)0);
+ else if ( Type == ABC_FIN_RDOB_BUFF ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w];
+ else if ( Type == ABC_FIN_RDOB_NOT ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~pSim0[w];
+ else if ( Type == ABC_FIN_RDOB_AND ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] & pSim1[w];
+ else if ( Type == ABC_FIN_RDOB_OR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] | pSim1[w];
+ else if ( Type == ABC_FIN_RDOB_XOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = pSim0[w] ^ pSim1[w];
+ else if ( Type == ABC_FIN_RDOB_NAND ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] & pSim1[w]);
+ else if ( Type == ABC_FIN_RDOB_NOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] | pSim1[w]);
+ else if ( Type == ABC_FIN_RDOB_NXOR ) for ( w = 0; w < nWords; w++ ) pSim[w] = ~(pSim0[w] ^ pSim1[w]);
+ else assert( 0 );
+ }
+}
+
+
+// returns 1 if the functionality with indexes i1 and i2 is the same
+static inline int Abc_NtkFinCompareSimTwo( Abc_Ntk_t * pNtk, Vec_Int_t * vCos, Vec_Wrd_t * vSims, int nWords, int i1, int i2 )
+{
+ Abc_Obj_t * pObj; int i;
+ assert( i1 != i2 );
+ Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
+ {
+ word * pSim0 = Vec_WrdEntryP( vSims, nWords * Abc_ObjFaninId0(pObj) );
+ if ( Abc_InfoHasBit((unsigned*)pSim0, i1) != Abc_InfoHasBit((unsigned*)pSim0, i2) )
+ return 0;
+ }
+ return 1;
+}
+
+Gia_Man_t * Abc_NtkFinMiterToGia( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes,
+ int iObjs[2], int Types[2], Vec_Int_t * vLits )
+{
+ Gia_Man_t * pNew = NULL, * pTemp;
+ Abc_Obj_t * pObj;
+ Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+ int n, i, Type, iMiter, iLit, * pLits;
+ // create AIG manager
+ pNew = Gia_ManStart( 1000 );
+ pNew->pName = Abc_UtilStrsav( pNtk->pName );
+ pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
+ Gia_ManHashStart( pNew );
+ // create inputs
+ Abc_NtkForEachObjVec( vCis, pNtk, pObj, i )
+ {
+ iLit = Gia_ManAppendCi(pNew);
+ for ( n = 0; n < 2; n++ )
+ {
+ if ( iObjs[n] != (int)Abc_ObjId(pObj) )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), iLit );
+ else if ( Types[n] != ABC_FIN_NEG )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) );
+ else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(iLit) );
+ }
+ }
+ // create internal nodes
+ Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
+ {
+ Type = Abc_NtkIsMappedLogic(pNtk) ? Mio_GateReadCell((Mio_Gate_t *)pObj->pData) : Vec_IntEntry(vTypes, Abc_ObjId(pObj));
+ for ( n = 0; n < 2; n++ )
+ {
+ if ( iObjs[n] != (int)Abc_ObjId(pObj) )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp) );
+ else if ( Types[n] != ABC_FIN_NEG )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_NtkFinSimOneLit(pNew, pObj, Types[n], vLits, n, vTemp) );
+ else // if ( iObjs[n] == (int)Abc_ObjId(pObj) && Types[n] == ABC_FIN_NEG )
+ Vec_IntWriteEntry( vLits, Abc_Var2Lit(Abc_ObjId(pObj), n), Abc_LitNot(Abc_NtkFinSimOneLit(pNew, pObj, Type, vLits, n, vTemp)) );
+ }
+ }
+ // create comparator
+ iMiter = 0;
+ Abc_NtkForEachObjVec( vCos, pNtk, pObj, i )
+ {
+ pLits = Vec_IntEntryP( vLits, Abc_Var2Lit(Abc_ObjFaninId0(pObj), 0) );
+ iLit = Gia_ManHashXor( pNew, pLits[0], pLits[1] );
+ iMiter = Gia_ManHashOr( pNew, iMiter, iLit );
+ }
+ Gia_ManAppendCo( pNew, iMiter );
+ // perform cleanup
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ Vec_IntFree( vTemp );
+ return pNew;
+}
+void Abc_NtkFinSimulateOne( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes,
+ Vec_Wec_t * vMap2, Vec_Int_t * vPat, Vec_Wrd_t * vSims, int nWords, Vec_Int_t * vPairs, Vec_Wec_t * vRes, int iLevel, int iItem )
+{
+ Abc_Obj_t * pObj;
+ Vec_Int_t * vClass, * vArray;
+ int i, Counter = 0;
+ int nItems = Vec_WecSizeSize(vRes);
+ assert( nItems == Vec_WecSizeSize(vMap2) );
+ assert( nItems <= 128 * nWords );
+ // assign inputs
+ assert( Vec_IntSize(vPat) == Vec_IntSize(vCis) );
+ Abc_NtkForEachObjVec( vCis, pNtk, pObj, i )
+ {
+ int w, iObj = Abc_ObjId( pObj );
+ word Init = Vec_IntEntry(vPat, i) ? ~((word)0) : 0;
+ word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
+ for ( w = 0; w < nWords; w++ )
+ pSim[w] = Init;
+ vArray = Vec_WecEntry(vMap2, iObj);
+ if ( Vec_IntSize(vArray) > 0 )
+ {
+ int k, iFin, Index, iObj, Type;
+ Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
+ {
+ assert( Index < 64 );
+ iObj = Vec_IntEntry( vPairs, 2*iFin );
+ assert( iObj == (int)Abc_ObjId(pObj) );
+ Type = Vec_IntEntry( vPairs, 2*iFin+1 );
+ assert( Type == ABC_FIN_NEG || Type == ABC_FIN_SA0 || Type == ABC_FIN_SA1 );
+ if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) )
+ Abc_InfoXorBit( (unsigned *)pSim, Index );
+ Counter++;
+ }
+ }
+ }
+ // simulate internal nodes
+ Abc_NtkForEachObjVec( vNodes, pNtk, pObj, i )
+ {
+ int iObj = Abc_ObjId( pObj );
+ int Type = Abc_NtkIsMappedLogic(pNtk) ? -1 : Vec_IntEntry( vTypes, iObj );
+ word * pSim = Vec_WrdEntryP( vSims, nWords * Abc_ObjId(pObj) );
+ Abc_NtkFinSimOneWord( pObj, Type, vSims, nWords );
+ vArray = Vec_WecEntry(vMap2, iObj);
+ if ( Vec_IntSize(vArray) > 0 )
+ {
+ int k, iFin, Index, iObj, Type;
+ Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
+ {
+ assert( Index < 64 * nWords );
+ iObj = Vec_IntEntry( vPairs, 2*iFin );
+ assert( iObj == (int)Abc_ObjId(pObj) );
+ Type = Vec_IntEntry( vPairs, 2*iFin+1 );
+ if ( Type == ABC_FIN_NEG || Abc_InfoHasBit((unsigned *)pSim, Index) != Abc_NtkFinSimOneBit(pObj, Type, vSims, nWords, Index) )
+ Abc_InfoXorBit( (unsigned *)pSim, Index );
+ Counter++;
+ }
+ }
+ }
+ assert( nItems == 2*Counter );
+
+ // confirm no refinement
+ Vec_WecForEachLevelStop( vRes, vClass, i, iLevel+1 )
+ {
+ int k, iFin, Index, Value;
+ int Index0 = Vec_IntEntry( vClass, 1 );
+ Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 )
+ {
+ if ( i == iLevel && k/2 >= iItem )
+ break;
+ //printf( "Double-checking pair %d and %d\n", iFin0, iFin );
+ Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index );
+ assert( Value ); // the same value
+ }
+ }
+
+ // check refinement
+ Vec_WecForEachLevelStart( vRes, vClass, i, iLevel )
+ {
+ int k, iFin, Index, Value, Index0 = Vec_IntEntry(vClass, 1);
+ int j = (i == iLevel) ? 2*iItem : 2;
+ Vec_Int_t * vNewClass = NULL;
+ Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, j )
+ {
+ Value = Abc_NtkFinCompareSimTwo( pNtk, vCos, vSims, nWords, Index0, Index );
+ if ( Value ) // the same value
+ {
+ Vec_IntWriteEntry( vClass, j++, iFin );
+ Vec_IntWriteEntry( vClass, j++, Index );
+ continue;
+ }
+ // create new class
+ vNewClass = vNewClass ? vNewClass : Vec_WecPushLevel( vRes );
+ Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry
+ vClass = Vec_WecEntry( vRes, i );
+ }
+ Vec_IntShrink( vClass, j );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Check equivalence using SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Abc_NtkFinCheckPair( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes, int iObjs[2], int Types[2], Vec_Int_t * vLits )
+{
+ Gia_Man_t * pGia = Abc_NtkFinMiterToGia( pNtk, vTypes, vCos, vCis, vNodes, iObjs, Types, vLits );
+ if ( Gia_ManAndNum(pGia) == 0 && Gia_ObjIsConst0(Gia_ObjFanin0(Gia_ManCo(pGia, 0))) )
+ {
+ Vec_Int_t * vPat = Gia_ObjFaninC0(Gia_ManCo(pGia, 0)) ? Vec_IntStart(Vec_IntSize(vCis)) : NULL;
+ Gia_ManStop( pGia );
+ return vPat;
+ }
+ else
+ {
+ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose );
+ Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 );
+ sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( pSat == NULL )
+ {
+ Gia_ManStop( pGia );
+ Cnf_DataFree( pCnf );
+ return NULL;
+ }
+ else
+ {
+ int i, nConfLimit = 10000;
+ Vec_Int_t * vPat = NULL;
+ int status, iVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1;
+ //Gia_AigerWrite( pGia, "temp_detect.aig", 0, 0 );
+ Gia_ManStop( pGia );
+ Cnf_DataFree( pCnf );
+ status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ vPat = Vec_IntAlloc(0);
+ else if ( status == l_True )
+ {
+ vPat = Vec_IntAlloc( Vec_IntSize(vCis) );
+ for ( i = 0; i < Vec_IntSize(vCis); i++ )
+ Vec_IntPush( vPat, sat_solver_var_value(pSat, iVarBeg+i) );
+ }
+ //printf( "%d ", sat_solver_nconflicts(pSat) );
+ sat_solver_delete( pSat );
+ return vPat;
+ }
+ }
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Refinement of equivalence classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkFinLocalSetup( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Int_t * vResArray )
+{
+ int i, iFin;
+ Vec_IntClear( vResArray );
+ Vec_IntForEachEntry( vList, iFin, i )
+ {
+ int iObj = Vec_IntEntry( vPairs, 2*iFin );
+ Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj );
+ Vec_IntPushTwo( vArray, iFin, i );
+ Vec_IntPushTwo( vResArray, iFin, i );
+ }
+}
+void Abc_NtkFinLocalSetdown( Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2 )
+{
+ int i, iFin;
+ Vec_IntForEachEntry( vList, iFin, i )
+ {
+ int iObj = Vec_IntEntry( vPairs, 2*iFin );
+ Vec_Int_t * vArray = Vec_WecEntry( vMap2, iObj );
+ Vec_IntClear( vArray );
+ }
+}
+int Abc_NtkFinRefinement( Abc_Ntk_t * pNtk, Vec_Int_t * vTypes, Vec_Int_t * vCos, Vec_Int_t * vCis, Vec_Int_t * vNodes,
+ Vec_Int_t * vPairs, Vec_Int_t * vList, Vec_Wec_t * vMap2, Vec_Wec_t * vResult )
+{
+ Vec_Wec_t * vRes = Vec_WecAlloc( 100 );
+ int nWords = Abc_Bit6WordNum( Vec_IntSize(vList) );
+ Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Abc_NtkObjNumMax(pNtk) ); // simulation info for each object
+ Vec_Int_t * vLits = Vec_IntStart( 2*Abc_NtkObjNumMax(pNtk) ); // two literals for each object
+ Vec_Int_t * vPat, * vClass, * vArray;
+ int i, k, iFin, Index, nCalls = 0;
+ // prepare
+ vArray = Vec_WecPushLevel( vRes );
+ Abc_NtkFinLocalSetup( vPairs, vList, vMap2, vArray );
+ // try all-0/all-1 pattern
+ for ( i = 0; i < 2; i++ )
+ {
+ vPat = Vec_IntAlloc( Vec_IntSize(vCis) );
+ Vec_IntFill( vPat, Vec_IntSize(vCis), i );
+ Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, 0, 1 );
+ Vec_IntFree( vPat );
+ }
+ // explore the classes
+ //Vec_WecPrint( vRes, 0 );
+ Vec_WecForEachLevel( vRes, vClass, i )
+ {
+ int iFin0 = Vec_IntEntry( vClass, 0 );
+ Vec_IntForEachEntryDoubleStart( vClass, iFin, Index, k, 2 )
+ {
+ int Objs[2] = { Vec_IntEntry(vPairs, 2*iFin0), Vec_IntEntry(vPairs, 2*iFin) };
+ int Types[2] = { Vec_IntEntry(vPairs, 2*iFin0+1), Vec_IntEntry(vPairs, 2*iFin+1) };
+ nCalls++;
+ //printf( "Checking pair %d and %d.\n", iFin0, iFin );
+ vPat = Abc_NtkFinCheckPair( pNtk, vTypes, vCos, vCis, vNodes, Objs, Types, vLits );
+ if ( vPat == NULL ) // proved
+ continue;
+ assert( Vec_IntEntry(vClass, k) == iFin );
+ if ( Vec_IntSize(vPat) == 0 )
+ {
+ Vec_Int_t * vNewClass = Vec_WecPushLevel( vRes );
+ Vec_IntPushTwo( vNewClass, iFin, Index ); // index and first entry
+ vClass = Vec_WecEntry( vRes, i );
+ Vec_IntDrop( vClass, k+1 );
+ Vec_IntDrop( vClass, k );
+ }
+ else // resimulate and refine
+ Abc_NtkFinSimulateOne( pNtk, vTypes, vCos, vCis, vNodes, vMap2, vPat, vSims, nWords, vPairs, vRes, i, k/2 );
+ Vec_IntFree( vPat );
+ // make sure refinement happened (k'th entry is now absent or different)
+ vClass = Vec_WecEntry( vRes, i );
+ assert( Vec_IntSize(vClass) <= k || Vec_IntEntry(vClass, k) != iFin );
+ k -= 2;
+ //Vec_WecPrint( vRes, 0 );
+ }
+ }
+ // unprepare
+ Abc_NtkFinLocalSetdown( vPairs, vList, vMap2 );
+ // reload proved equivs into the final array
+ Vec_WecForEachLevel( vRes, vArray, i )
+ {
+ assert( Vec_IntSize(vArray) % 2 == 0 );
+ if ( Vec_IntSize(vArray) <= 2 )
+ continue;
+ vClass = Vec_WecPushLevel( vResult );
+ Vec_IntForEachEntryDouble( vArray, iFin, Index, k )
+ Vec_IntPush( vClass, iFin );
+ }
+ Vec_WecFree( vRes );
+ Vec_WrdFree( vSims );
+ Vec_IntFree( vLits );
+ return nCalls;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Detecting classes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Abc_ObjFinGateType( Abc_Obj_t * pNode )
+{
+ char * pSop = (char *)pNode->pData;
+ if ( !strcmp(pSop, "1 1\n") ) return ABC_FIN_RDOB_BUFF;
+ if ( !strcmp(pSop, "0 1\n") ) return ABC_FIN_RDOB_NOT;
+ if ( !strcmp(pSop, "11 1\n") ) return ABC_FIN_RDOB_AND;
+ if ( !strcmp(pSop, "11 0\n") ) return ABC_FIN_RDOB_NAND;
+ if ( !strcmp(pSop, "00 0\n") ) return ABC_FIN_RDOB_OR;
+ if ( !strcmp(pSop, "00 1\n") ) return ABC_FIN_RDOB_NOR;
+ if ( !strcmp(pSop, "01 1\n10 1\n") ) return ABC_FIN_RDOB_XOR;
+ if ( !strcmp(pSop, "11 1\n00 1\n") ) return ABC_FIN_RDOB_NXOR;
+ return ABC_FIN_NONE;
+}
+int Abc_NtkFinCheckTypesOk( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj; int i;
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ if ( Abc_ObjFinGateType(pObj) == ABC_FIN_NONE )
+ return i;
+ return 0;
+}
+int Abc_NtkFinCheckTypesOk2( Abc_Ntk_t * pNtk )
+{
+ Mio_Library_t * pLib = (Mio_Library_t *)pNtk->pManFunc;
+ int i, iObj, Type;
+ Vec_IntForEachEntryDoubleStart( pNtk->vFins, iObj, Type, i, 2 )
+ {
+ Abc_Obj_t * pObj = Abc_NtkObj( pNtk, iObj );
+ Mio_Gate_t * pGateFlt, * pGateObj = (Mio_Gate_t *)pObj->pData;
+ if ( Type < 0 ) // SA0, SA1, NEG
+ continue;
+ pGateFlt = Mio_LibraryReadGateById( pLib, Type );
+ if ( Mio_GateReadPinNum(pGateFlt) < 1 )
+ continue;
+ if ( Mio_GateReadPinNum(pGateObj) != Mio_GateReadPinNum(pGateFlt) )
+ return iObj;
+ }
+ return 0;
+}
+Vec_Int_t * Abc_NtkFinComputeTypes( Abc_Ntk_t * pNtk )
+{
+ Abc_Obj_t * pObj; int i;
+ Vec_Int_t * vObjs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ Vec_IntWriteEntry( vObjs, Abc_ObjId(pObj), Abc_ObjFinGateType(pObj) );
+ return vObjs;
+}
+Vec_Int_t * Abc_NtkFinComputeObjects( Vec_Int_t * vPairs, Vec_Wec_t ** pvMap, int nObjs )
+{
+ int i, iObj, Type;
+ Vec_Int_t * vObjs = Vec_IntAlloc( 100 );
+ *pvMap = Vec_WecStart( nObjs );
+ Vec_IntForEachEntryDoubleStart( vPairs, iObj, Type, i, 2 )
+ {
+ Vec_IntPush( vObjs, iObj );
+ Vec_WecPush( *pvMap, iObj, i/2 );
+ }
+ Vec_IntUniqify( vObjs );
+ return vObjs;
+}
+Vec_Int_t * Abc_NtkFinCreateList( Vec_Wec_t * vMap, Vec_Int_t * vClass )
+{
+ int i, iObj;
+ Vec_Int_t * vList = Vec_IntAlloc( 100 );
+ Vec_IntForEachEntry( vClass, iObj, i )
+ Vec_IntAppend( vList, Vec_WecEntry(vMap, iObj) );
+ return vList;
+}
+int Abc_NtkFinCountPairs( Vec_Wec_t * vClasses )
+{
+ int i, Counter = 0;
+ Vec_Int_t * vLevel;
+ Vec_WecForEachLevel( vClasses, vLevel, i )
+ Counter += Vec_IntSize(vLevel) - 1;
+ return Counter;
+}
+Vec_Wec_t * Abc_NtkDetectFinClasses( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Vec_Int_t * vTypes = NULL; // gate types
+ Vec_Int_t * vPairs; // original info as a set of pairs (ObjId, TypeId)
+ Vec_Int_t * vObjs; // all those objects that have some fin
+ Vec_Wec_t * vMap; // for each object, the set of fins
+ Vec_Wec_t * vMap2; // for each local object, the set of pairs (Info, Index)
+ Vec_Wec_t * vClasses; // classes of objects
+ Vec_Wec_t * vCoSets; // corresponding CO sets
+ Vec_Int_t * vClass; // one class
+ Vec_Int_t * vCoSet; // one set of COs
+ Vec_Int_t * vCiSet; // one set of CIs
+ Vec_Int_t * vNodeSet; // one set of nodes
+ Vec_Int_t * vList; // one info list
+ Vec_Wec_t * vResult; // resulting equivalences
+ int i, iObj, nCalls;
+ if ( pNtk->vFins == NULL )
+ {
+ printf( "Current network does not have the required info.\n" );
+ return NULL;
+ }
+ assert( Abc_NtkIsSopLogic(pNtk) || Abc_NtkIsMappedLogic(pNtk) );
+ if ( Abc_NtkIsSopLogic(pNtk) )
+ {
+ iObj = Abc_NtkFinCheckTypesOk(pNtk);
+ if ( iObj )
+ {
+ printf( "Current network contains unsupported gate types (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
+ return NULL;
+ }
+ vTypes = Abc_NtkFinComputeTypes( pNtk );
+ }
+ else if ( Abc_NtkIsMappedLogic(pNtk) )
+ {
+ iObj = Abc_NtkFinCheckTypesOk2(pNtk);
+ if ( iObj )
+ {
+ printf( "Current network has mismatch between mapped gate size and fault gate size (for example, see node \"%s\").\n", Abc_ObjName(Abc_NtkObj(pNtk, iObj)) );
+ return NULL;
+ }
+ }
+ else assert( 0 );
+ //Abc_NtkFrameExtend( pNtk );
+ // collect data
+ vPairs = pNtk->vFins;
+ vObjs = Abc_NtkFinComputeObjects( vPairs, &vMap, Abc_NtkObjNumMax(pNtk) );
+ vClasses = Abc_NtkDetectObjClasses( pNtk, vObjs, &vCoSets );
+ // refine classes
+ vCiSet = Vec_IntAlloc( 1000 );
+ vNodeSet = Vec_IntAlloc( 1000 );
+ vMap2 = Vec_WecStart( Abc_NtkObjNumMax(pNtk) );
+ vResult = Vec_WecAlloc( 1000 );
+ Vec_WecForEachLevel( vClasses, vClass, i )
+ {
+ // extract one window
+ vCoSet = Vec_WecEntry( vCoSets, i );
+ Abc_NtkFinMiterCollect( pNtk, vCoSet, vCiSet, vNodeSet );
+ // refine one class
+ vList = Abc_NtkFinCreateList( vMap, vClass );
+ nCalls = Abc_NtkFinRefinement( pNtk, vTypes, vCoSet, vCiSet, vNodeSet, vPairs, vList, vMap2, vResult );
+ if ( fVerbose )
+ printf( "Group %4d : Obj =%4d. Fins =%4d. CI =%5d. CO =%5d. Node =%6d. SAT calls =%5d.\n",
+ i, Vec_IntSize(vClass), Vec_IntSize(vList), Vec_IntSize(vCiSet), Vec_IntSize(vCoSet), Vec_IntSize(vNodeSet), nCalls );
+ Vec_IntFree( vList );
+ }
+ // sort entries in each array
+ Vec_WecForEachLevel( vResult, vClass, i )
+ Vec_IntSort( vClass, 0 );
+ // sort by the index of the first entry
+ Vec_WecSortByFirstInt( vResult, 0 );
+ // cleanup
+ Vec_IntFreeP( & vTypes );
+ Vec_IntFree( vObjs );
+ Vec_WecFree( vClasses );
+ Vec_WecFree( vMap );
+ Vec_WecFree( vMap2 );
+ Vec_WecFree( vCoSets );
+ Vec_IntFree( vCiSet );
+ Vec_IntFree( vNodeSet );
+ return vResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Print results.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintFinResults( Vec_Wec_t * vClasses )
+{
+ Vec_Int_t * vClass;
+ int i, k, Entry;
+ Vec_WecForEachLevel( vClasses, vClass, i )
+ Vec_IntForEachEntryStart( vClass, Entry, k, 1 )
+ printf( "%d %d\n", Vec_IntEntry(vClass, 0), Entry );
+}
+
+/**Function*************************************************************
+
Synopsis [Top-level procedure.]
Description []
@@ -193,9 +1239,20 @@ finish:
SeeAlso []
***********************************************************************/
-void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose )
+void Abc_NtkDetectClassesTest( Abc_Ntk_t * pNtk, int fSeq, int fVerbose, int fVeryVerbose )
{
- printf( "This procedure is currently not used.\n" );
+ Vec_Wec_t * vResult;
+ abctime clk = Abc_Clock();
+ if ( fSeq )
+ Abc_NtkFrameExtend( pNtk );
+ vResult = Abc_NtkDetectFinClasses( pNtk, fVerbose );
+ printf( "Computed %d equivalence classes with %d item pairs. ", Vec_WecSize(vResult), Abc_NtkFinCountPairs(vResult) );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ if ( fVeryVerbose )
+ Vec_WecPrint( vResult, 1 );
+// if ( fVerbose )
+// Abc_NtkPrintFinResults( vResult );
+ Vec_WecFree( vResult );
}
diff --git a/src/base/cba/cba.h b/src/base/cba/cba.h
index 36a93f32..adf12a45 100644
--- a/src/base/cba/cba.h
+++ b/src/base/cba/cba.h
@@ -29,6 +29,7 @@
#include "misc/extra/extra.h"
#include "misc/util/utilNam.h"
#include "misc/vec/vecHash.h"
+#include "cbaTypes.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -40,116 +41,6 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
-// network objects
-typedef enum {
- CBA_OBJ_NONE = 0, // 00: unused
- CBA_OBJ_PI, // 01: input
- CBA_OBJ_PO, // 02: output
- CBA_OBJ_BOX, // 03: box
-
- CBA_BOX_CF, // 04:
- CBA_BOX_CT, // 05:
- CBA_BOX_CX, // 06:
- CBA_BOX_CZ, // 07:
-
- CBA_BOX_BUF, // 08:
- CBA_BOX_INV, // 09:
- CBA_BOX_AND, // 10:
- CBA_BOX_NAND, // 11:
- CBA_BOX_OR, // 12:
- CBA_BOX_NOR, // 13:
- CBA_BOX_XOR, // 14:
- CBA_BOX_XNOR, // 15:
- CBA_BOX_SHARP, // 16:
- CBA_BOX_SHARPL, // 17:
- CBA_BOX_MUX, // 18:
- CBA_BOX_MAJ, // 19:
-
- CBA_BOX_ABC, // 20:
- CBA_BOX_BA, // 21:
- CBA_BOX_BO, // 22:
- CBA_BOX_BX, // 23:
- CBA_BOX_BN, // 24:
- CBA_BOX_BAO, // 25:
- CBA_BOX_BOA, // 26:
-
- CBA_BOX_RAND, // 27:
- CBA_BOX_RNAND, // 28:
- CBA_BOX_ROR, // 29:
- CBA_BOX_RNOR, // 30:
- CBA_BOX_RXOR, // 31:
- CBA_BOX_RXNOR, // 32:
-
- CBA_BOX_LNOT, // 33
- CBA_BOX_LAND, // 34:
- CBA_BOX_LNAND, // 35:
- CBA_BOX_LOR, // 36:
- CBA_BOX_LNOR, // 37:
- CBA_BOX_LXOR, // 38:
- CBA_BOX_LXNOR, // 39:
-
- CBA_BOX_NMUX, // 40:
- CBA_BOX_SEL, // 41:
- CBA_BOX_PSEL, // 42:
- CBA_BOX_ENC, // 43:
- CBA_BOX_PENC, // 44:
- CBA_BOX_DEC, // 45:
- CBA_BOX_EDEC, // 46:
-
- CBA_BOX_ADD, // 47:
- CBA_BOX_SUB, // 48:
- CBA_BOX_MUL, // 49:
- CBA_BOX_SMUL, // 50:
- CBA_BOX_DIV, // 51:
- CBA_BOX_MOD, // 52:
- CBA_BOX_REM, // 53:
- CBA_BOX_POW, // 54:
- CBA_BOX_MIN, // 55:
- CBA_BOX_SQRT, // 56:
- CBA_BOX_ABS, // 57:
-
- CBA_BOX_SLTHAN, // 58:
- CBA_BOX_LTHAN, // 59:
- CBA_BOX_LETHAN, // 60:
- CBA_BOX_METHAN, // 61:
- CBA_BOX_MTHAN, // 62:
- CBA_BOX_EQU, // 63:
- CBA_BOX_NEQU, // 64:
-
- CBA_BOX_SHIL, // 65:
- CBA_BOX_SHIR, // 66:
- CBA_BOX_SHILA, // 67:
- CBA_BOX_SHIRA, // 68:
- CBA_BOX_ROTL, // 69:
- CBA_BOX_ROTR, // 70:
-
- CBA_BOX_NODE, // 71:
- CBA_BOX_LUT, // 72:
- CBA_BOX_GATE, // 73:
- CBA_BOX_TABLE, // 74:
-
- CBA_BOX_TRI, // 75:
- CBA_BOX_RAM, // 76:
- CBA_BOX_RAMR, // 77:
- CBA_BOX_RAMW, // 78:
- CBA_BOX_RAMWC, // 79:
- CBA_BOX_RAML, // 80:
- CBA_BOX_RAMS, // 81:
- CBA_BOX_RAMBOX, // 82:
-
- CBA_BOX_LATCH, // 83:
- CBA_BOX_LATCHRS, // 84:
- CBA_BOX_DFF, // 85:
- CBA_BOX_DFFCPL, // 86:
- CBA_BOX_DFFRS, // 87:
-
- CBA_BOX_SLICE, // 88:
- CBA_BOX_CONCAT, // 89:
-
- CBA_BOX_LAST // 90
-} Cba_ObjType_t;
-
-
typedef struct Cba_Ntk_t_ Cba_Ntk_t;
typedef struct Cba_Man_t_ Cba_Man_t;
diff --git a/src/base/cba/cbaTypes.h b/src/base/cba/cbaTypes.h
new file mode 100644
index 00000000..6fad9985
--- /dev/null
+++ b/src/base/cba/cbaTypes.h
@@ -0,0 +1,169 @@
+/**CFile****************************************************************
+
+ FileName [cbaTypes.h]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Hierarchical word-level netlist.]
+
+ Synopsis [External declarations.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - July 21, 2015.]
+
+ Revision [$Id: cbaTypes.h,v 1.00 2014/11/29 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifndef ABC__base__cba__cba__types_h
+#define ABC__base__cba__cba__types_h
+
+////////////////////////////////////////////////////////////////////////
+/// INCLUDES ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// PARAMETERS ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+/// BASIC TYPES ///
+////////////////////////////////////////////////////////////////////////
+
+// network objects
+typedef enum {
+ CBA_OBJ_NONE = 0, // 00: unused
+ CBA_OBJ_PI, // 01: input
+ CBA_OBJ_PO, // 02: output
+ CBA_OBJ_BOX, // 03: box
+
+ CBA_BOX_CF, // 04:
+ CBA_BOX_CT, // 05:
+ CBA_BOX_CX, // 06:
+ CBA_BOX_CZ, // 07:
+
+ CBA_BOX_BUF, // 08:
+ CBA_BOX_INV, // 09:
+ CBA_BOX_AND, // 10:
+ CBA_BOX_NAND, // 11:
+ CBA_BOX_OR, // 12:
+ CBA_BOX_NOR, // 13:
+ CBA_BOX_XOR, // 14:
+ CBA_BOX_XNOR, // 15:
+ CBA_BOX_SHARP, // 16:
+ CBA_BOX_SHARPL, // 17:
+ CBA_BOX_MUX, // 18:
+ CBA_BOX_MAJ, // 19:
+
+ CBA_BOX_ABC, // 20:
+ CBA_BOX_BA, // 21:
+ CBA_BOX_BO, // 22:
+ CBA_BOX_BX, // 23:
+ CBA_BOX_BN, // 24:
+ CBA_BOX_BAO, // 25:
+ CBA_BOX_BOA, // 26:
+
+ CBA_BOX_RAND, // 27:
+ CBA_BOX_RNAND, // 28:
+ CBA_BOX_ROR, // 29:
+ CBA_BOX_RNOR, // 30:
+ CBA_BOX_RXOR, // 31:
+ CBA_BOX_RXNOR, // 32:
+
+ CBA_BOX_LNOT, // 33
+ CBA_BOX_LAND, // 34:
+ CBA_BOX_LNAND, // 35:
+ CBA_BOX_LOR, // 36:
+ CBA_BOX_LNOR, // 37:
+ CBA_BOX_LXOR, // 38:
+ CBA_BOX_LXNOR, // 39:
+
+ CBA_BOX_NMUX, // 40:
+ CBA_BOX_SEL, // 41:
+ CBA_BOX_PSEL, // 42:
+ CBA_BOX_ENC, // 43:
+ CBA_BOX_PENC, // 44:
+ CBA_BOX_DEC, // 45:
+ CBA_BOX_EDEC, // 46:
+
+ CBA_BOX_ADD, // 47:
+ CBA_BOX_SUB, // 48:
+ CBA_BOX_MUL, // 49:
+ CBA_BOX_SMUL, // 50:
+ CBA_BOX_DIV, // 51:
+ CBA_BOX_MOD, // 52:
+ CBA_BOX_REM, // 53:
+ CBA_BOX_POW, // 54:
+ CBA_BOX_MIN, // 55:
+ CBA_BOX_SQRT, // 56:
+ CBA_BOX_ABS, // 57:
+
+ CBA_BOX_SLTHAN, // 58:
+ CBA_BOX_LTHAN, // 59:
+ CBA_BOX_LETHAN, // 60:
+ CBA_BOX_METHAN, // 61:
+ CBA_BOX_MTHAN, // 62:
+ CBA_BOX_EQU, // 63:
+ CBA_BOX_NEQU, // 64:
+
+ CBA_BOX_SHIL, // 65:
+ CBA_BOX_SHIR, // 66:
+ CBA_BOX_SHILA, // 67:
+ CBA_BOX_SHIRA, // 68:
+ CBA_BOX_ROTL, // 69:
+ CBA_BOX_ROTR, // 70:
+
+ CBA_BOX_NODE, // 71:
+ CBA_BOX_LUT, // 72:
+ CBA_BOX_GATE, // 73:
+ CBA_BOX_TABLE, // 74:
+
+ CBA_BOX_TRI, // 75:
+ CBA_BOX_RAM, // 76:
+ CBA_BOX_RAMR, // 77:
+ CBA_BOX_RAMW, // 78:
+ CBA_BOX_RAMWC, // 79:
+ CBA_BOX_RAML, // 80:
+ CBA_BOX_RAMS, // 81:
+ CBA_BOX_RAMBOX, // 82:
+
+ CBA_BOX_LATCH, // 83:
+ CBA_BOX_LATCHRS, // 84:
+ CBA_BOX_DFF, // 85:
+ CBA_BOX_DFFCPL, // 86:
+ CBA_BOX_DFFRS, // 87:
+
+ CBA_BOX_SLICE, // 88:
+ CBA_BOX_CONCAT, // 89:
+
+ CBA_BOX_LAST // 90
+} Cba_ObjType_t;
+
+
+////////////////////////////////////////////////////////////////////////
+/// MACRO DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// ITERATORS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/base/io/io.c b/src/base/io/io.c
index b181bc1d..093eccca 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2378,6 +2378,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
Abc_Obj_t * pObj;
FILE * pFile;
int i, f;
+ /*
Abc_NtkForEachLatch( pNtk, pObj, i )
if ( !Abc_LatchIsInit0(pObj) )
{
@@ -2385,7 +2386,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
return 1;
}
-
+ */
pFile = fopen( pFileName, "w" );
if ( pFile == NULL )
{
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 7de6bd81..3431c761 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -74,7 +74,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
Abc_Obj_t * pNode, * pFanin;
char * pSopString;
int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds, fCompl, Prev;
- int Limit = 300;
+ int Limit = 500;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
diff --git a/src/base/wlc/module.make b/src/base/wlc/module.make
index 081be200..5a95a63f 100644
--- a/src/base/wlc/module.make
+++ b/src/base/wlc/module.make
@@ -8,4 +8,5 @@ SRC += src/base/wlc/wlcAbs.c \
src/base/wlc/wlcReadVer.c \
src/base/wlc/wlcSim.c \
src/base/wlc/wlcStdin.c \
+ src/base/wlc/wlcWin.c \
src/base/wlc/wlcWriteVer.c
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 90596093..1df3e5e9 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -244,6 +244,8 @@ static inline Wlc_Obj_t * Wlc_ObjFoToFi( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
#define Wlc_ObjForEachFanin( pObj, iFanin, i ) \
for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i++ )
+#define Wlc_ObjForEachFaninObj( p, pObj, pFanin, i ) \
+ for ( i = 0; (i < Wlc_ObjFaninNum(pObj)) && (((pFanin) = Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, i))), 1); i++ )
#define Wlc_ObjForEachFaninReverse( pObj, iFanin, i ) \
for ( i = Wlc_ObjFaninNum(pObj) - 1; (i >= 0) && (((iFanin) = Wlc_ObjFaninId(pObj, i)), 1); i-- )
@@ -272,6 +274,8 @@ extern char * Wlc_ObjName( Wlc_Ntk_t * p, int iObj );
extern void Wlc_ObjUpdateType( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, int Type );
extern void Wlc_ObjAddFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFanins );
extern void Wlc_NtkFree( Wlc_Ntk_t * p );
+extern void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj );
+extern void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray );
extern void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type );
extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose );
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p );
@@ -287,6 +291,8 @@ extern void Wlc_NtkDeleteSim( Vec_Ptr_t * p );
extern int Wlc_StdinProcessSmt( Abc_Frame_t * pAbc, char * pCmd );
/*=== wlcReadVer.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName, char * pStr );
+/*=== wlcWin.c =============================================================*/
+extern void Wlc_WinProfileArith( Wlc_Ntk_t * p );
/*=== wlcWriteVer.c ========================================================*/
extern void Wlc_WriteVer( Wlc_Ntk_t * p, char * pFileName, int fAddCos, int fNoFlops );
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index c86c7cf0..ec3b040d 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -292,6 +292,10 @@ int Wlc_BlastLessSigned( Gia_Man_t * pNew, int * pArg0, int * pArg1, int nBits )
void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps )
{
int fUseXor = 0;
+ int fCompl = (a == 1 || b == 1 || c == 1);
+ // propagate complement through the FA - helps generate less redundant logic
+ if ( fCompl )
+ a = Abc_LitNot(a), b = Abc_LitNot(b), c = Abc_LitNot(c);
if ( fUseXor )
{
int Xor = Gia_ManHashXor(pNew, a, b);
@@ -310,6 +314,8 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int *
*ps = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_));
*pc = Gia_ManHashOr (pNew, And1, And2);
}
+ if ( fCompl )
+ *ps = Abc_LitNot(*ps), *pc = Abc_LitNot(*pc);
}
void Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits ) // result is in pAdd0
{
@@ -412,6 +418,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
assert( fSigned == 0 || fSigned == 1 );
// prepare result
Vec_IntFill( vRes, nArgA + nArgB, 0 );
+ //Vec_IntFill( vRes, nArgA + nArgB + 1, 0 );
pRes = Vec_IntArray( vRes );
// prepare intermediate storage
Vec_IntFill( vTemp, 2 * nArgA, 0 );
@@ -426,6 +433,7 @@ void Wlc_BlastMultiplier( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA,
pArgS[nArgA-1] = fSigned;
for ( a = 0; a < nArgA; a++ )
Wlc_BlastFullAdderCtrl( pNew, 1, pArgC[a], pArgS[a], Carry, &Carry, &pRes[nArgB+a], 0 );
+ //Vec_IntWriteEntry( vRes, nArgA + nArgB, Carry );
}
void Wlc_BlastDivider( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes )
{
@@ -804,7 +812,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
Vec_WecPush( vLevels, k, 0 );
}
//Vec_WecPrint( vProds, 0 );
-
+ //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
Wlc_BlastReduceMatrix( pNew, vProds, vLevels, vRes );
Vec_WecFree( vProds );
@@ -1360,6 +1368,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in
{
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManDupRemapLiterals( vBits, pTemp );
+ //printf( "Cutoff ID %d became %d.\n", 75, Abc_Lit2Var(Gia_ManObj(pTemp, 73)->Value) );
Gia_ManStop( pTemp );
}
// transform AIG with init state
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 7856fae8..f3eb6dd7 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -34,6 +34,7 @@ static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
@@ -67,6 +68,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 );
+ Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
}
@@ -554,6 +556,50 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv )
SeeAlso []
******************************************************************************/
+int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
+ int c, fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
+ return 0;
+ }
+ Wlc_WinProfileArith( pNtk );
+ return 0;
+usage:
+ Abc_Print( -2, "usage: %%profile [-vh]\n" );
+ Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
+ Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
@@ -575,7 +621,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pNtk == NULL )
{
- Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
+ Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
return 0;
}
// transform
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 5a08cd99..6f396771 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -44,8 +44,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
">>>", // 10: shift right (arithmetic)
"<<", // 11: shift left
"<<<", // 12: shift left (arithmetic)
- "rotateR", // 13: rotate right
- "rotateL", // 14: rotate left
+ "rotR", // 13: rotate right
+ "rotL", // 14: rotate left
"~", // 15: bitwise NOT
"&", // 16: bitwise AND
"|", // 17: bitwise OR
@@ -55,8 +55,8 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"~^", // 21: bitwise NXOR
"[:]", // 22: bit selection
"{,}", // 23: bit concatenation
- "zeroPad", // 24: zero padding
- "signExt", // 25: sign extension
+ "zPad", // 24: zero padding
+ "sExt", // 25: sign extension
"!", // 26: logic NOT
"=>", // 27: logic implication
"&&", // 28: logic AND
@@ -83,7 +83,7 @@ static char * Wlc_Names[WLC_OBJ_NUMBER+1] = {
"**", // 49: arithmetic power
"-", // 50: arithmetic minus
"sqrt", // 51: integer square root
- "square", // 52: integer square
+ "squar", // 52: integer square
"table", // 53: bit table
NULL // 54: unused
};
@@ -471,6 +471,57 @@ void Wlc_NtkPrintDistrib( Wlc_Ntk_t * p, int fVerbose )
Vec_VecFree( (Vec_Vec_t *)vOccurs );
Vec_IntFree( vAnds );
}
+void Wlc_NtkPrintNode( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+ printf( "%8d : ", Wlc_ObjId(p, pObj) );
+ printf( "%3d%s", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
+ if ( pObj->Type == WLC_OBJ_CONST )
+ printf( " " );
+ else
+ {
+ printf( " = %3d%s %5s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[(int)pObj->Type] );
+ if ( Wlc_ObjFaninNum(pObj) > 1 )
+ printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
+ else
+ printf( " " );
+ if ( Wlc_ObjFaninNum(pObj) > 2 )
+ printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin2(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin2(p, pObj)) ? "s" : " " );
+ else
+ printf( " " );
+ }
+ printf( " : " );
+ printf( "%-12s", Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+ if ( pObj->Type == WLC_OBJ_CONST )
+ {
+ printf( " = %d\'%sh", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s":"" );
+ if ( pObj->fXConst )
+ {
+ int k;
+ for ( k = 0; k < (Wlc_ObjRange(pObj) + 3) / 4; k++ )
+ printf( "x" );
+ }
+ else
+ Abc_TtPrintHexArrayRev( stdout, (word *)Wlc_ObjConstValue(pObj), (Wlc_ObjRange(pObj) + 3) / 4 );
+ }
+ else
+ {
+ printf( " = %-12s %5s ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[(int)pObj->Type] );
+ if ( Wlc_ObjFaninNum(pObj) > 1 )
+ printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
+ else
+ printf( " " );
+ if ( Wlc_ObjFaninNum(pObj) > 2 )
+ printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId2(pObj)) );
+ }
+ printf( "\n" );
+}
+void Wlc_NtkPrintNodeArray( Wlc_Ntk_t * p, Vec_Int_t * vArray )
+{
+ Wlc_Obj_t * pObj;
+ int i;
+ Wlc_NtkForEachObjVec( vArray, p, pObj, i )
+ Wlc_NtkPrintNode( p, pObj );
+}
void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
{
Wlc_Obj_t * pObj;
@@ -480,16 +531,8 @@ void Wlc_NtkPrintNodes( Wlc_Ntk_t * p, int Type )
{
if ( (int)pObj->Type != Type )
continue;
- printf( "%8d :", Counter++ );
- printf( "%8d : ", i );
- printf( "%3d%s = ", Wlc_ObjRange(pObj), Wlc_ObjIsSigned(pObj) ? "s" : " " );
- printf( "%3d%s %s ", Wlc_ObjRange(Wlc_ObjFanin0(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin0(p, pObj)) ? "s" : " ", Wlc_Names[Type] );
- printf( "%3d%s ", Wlc_ObjRange(Wlc_ObjFanin1(p, pObj)), Wlc_ObjIsSigned(Wlc_ObjFanin1(p, pObj)) ? "s" : " " );
- printf( " : " );
- printf( "%-12s = ", Wlc_ObjName(p, i) );
- printf( "%-12s %s ", Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)), Wlc_Names[Type] );
- printf( "%-12s ", Wlc_ObjName(p, Wlc_ObjFaninId1(pObj)) );
- printf( "\n" );
+ printf( "%8d :", Counter++ );
+ Wlc_NtkPrintNode( p, pObj );
}
}
void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbose )
diff --git a/src/base/wlc/wlcWin.c b/src/base/wlc/wlcWin.c
new file mode 100644
index 00000000..4dc748f4
--- /dev/null
+++ b/src/base/wlc/wlcWin.c
@@ -0,0 +1,166 @@
+/**CFile****************************************************************
+
+ FileName [wlcWin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Verilog parser.]
+
+ Synopsis [Parses several flavors of word-level Verilog.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - August 22, 2014.]
+
+ Revision [$Id: wlcWin.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "wlc.h"
+#include "base/abc/abc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Collect arithmetic nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Wlc_ObjIsArithm( Wlc_Obj_t * pObj )
+{
+ return pObj->Type == WLC_OBJ_CONST ||
+ pObj->Type == WLC_OBJ_BUF || pObj->Type == WLC_OBJ_BIT_NOT ||
+ pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT ||
+// pObj->Type == WLC_OBJ_BIT_SELECT || pObj->Type == WLC_OBJ_BIT_CONCAT ||
+ pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
+ pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
+}
+int Wlc_ObjIsArithmReal( Wlc_Obj_t * pObj )
+{
+ return pObj->Type == WLC_OBJ_BIT_NOT ||
+ pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
+ pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
+}
+int Wlc_ManCountArithmReal( Wlc_Ntk_t * p, Vec_Int_t * vNodes )
+{
+ Wlc_Obj_t * pObj;
+ int i, Counter = 0;
+ Wlc_NtkForEachObjVec( vNodes, p, pObj, i )
+ Counter += Wlc_ObjIsArithmReal( pObj );
+ return Counter;
+}
+int Wlc_ObjHasArithm_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+ if ( pObj->Type == WLC_OBJ_CONST )
+ return 0;
+ if ( pObj->Type == WLC_OBJ_BUF || pObj->Type == WLC_OBJ_BIT_NOT ||
+ pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT )
+ return Wlc_ObjHasArithm_rec( p, Wlc_ObjFanin0(p, pObj) );
+ return pObj->Type == WLC_OBJ_ARI_ADD || pObj->Type == WLC_OBJ_ARI_SUB ||
+ pObj->Type == WLC_OBJ_ARI_MULTI || pObj->Type == WLC_OBJ_ARI_MINUS;
+}
+int Wlc_ObjHasArithmFanins( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+ Wlc_Obj_t * pFanin; int i;
+ assert( !Wlc_ObjHasArithm_rec(p, pObj) );
+ Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
+ if ( Wlc_ObjHasArithm_rec(p, pFanin) )
+ return 1;
+ return 0;
+}
+void Wlc_WinCompute_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+{
+ Wlc_Obj_t * pFanin; int i;
+ if ( pObj->Mark )
+ return;
+ pObj->Mark = 1;
+ if ( !Wlc_ObjIsArithm(pObj) )
+ {
+ Vec_IntPush( vLeaves, Wlc_ObjId(p, pObj) );
+ return;
+ }
+ Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
+ Wlc_WinCompute_rec( p, pFanin, vLeaves, vNodes );
+ Vec_IntPush( vNodes, Wlc_ObjId(p, pObj) );
+}
+void Wlc_WinCleanMark_rec( Wlc_Ntk_t * p, Wlc_Obj_t * pObj )
+{
+ Wlc_Obj_t * pFanin; int i;
+ if ( !pObj->Mark )
+ return;
+ pObj->Mark = 0;
+ Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
+ Wlc_WinCleanMark_rec( p, pFanin );
+}
+void Wlc_WinCompute( Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
+{
+ Vec_IntClear( vLeaves );
+ Vec_IntClear( vNodes );
+ if ( Wlc_ObjHasArithm_rec(p, pObj) )
+ {
+ Wlc_WinCompute_rec( p, pObj, vLeaves, vNodes );
+ Wlc_WinCleanMark_rec( p, pObj );
+ }
+ else if ( Wlc_ObjHasArithmFanins(p, pObj) )
+ {
+ Wlc_Obj_t * pFanin; int i;
+ Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
+ if ( Wlc_ObjHasArithm_rec(p, pFanin) )
+ Wlc_WinCompute_rec( p, pFanin, vLeaves, vNodes );
+ Wlc_ObjForEachFaninObj( p, pObj, pFanin, i )
+ if ( Wlc_ObjHasArithm_rec(p, pFanin) )
+ Wlc_WinCleanMark_rec( p, pFanin );
+ }
+ else assert( 0 );
+}
+void Wlc_WinProfileArith( Wlc_Ntk_t * p )
+{
+ Vec_Int_t * vLeaves = Vec_IntAlloc( 1000 );
+ Vec_Int_t * vNodes = Vec_IntAlloc( 1000 );
+ Wlc_Obj_t * pObj; int i, Count = 0;
+ Wlc_NtkForEachObj( p, pObj, i )
+ pObj->Mark = 0;
+ Wlc_NtkForEachObj( p, pObj, i )
+ if ( Wlc_ObjHasArithm_rec(p, pObj) ? Wlc_ObjIsCo(pObj) : Wlc_ObjHasArithmFanins(p, pObj) )
+ {
+ Wlc_WinCompute( p, pObj, vLeaves, vNodes );
+ if ( Wlc_ManCountArithmReal(p, vNodes) < 2 )
+ continue;
+
+ printf( "Arithmetic cone of node %d (%s):\n", Wlc_ObjId(p, pObj), Wlc_ObjName(p, Wlc_ObjId(p, pObj)) );
+ Wlc_NtkPrintNode( p, pObj );
+ Vec_IntReverseOrder( vNodes );
+ Wlc_NtkPrintNodeArray( p, vNodes );
+ printf( "\n" );
+ Count++;
+ }
+ Wlc_NtkForEachObj( p, pObj, i )
+ assert( pObj->Mark == 0 );
+ printf( "Finished printing %d arithmetic cones.\n", Count );
+ Vec_IntFree( vLeaves );
+ Vec_IntFree( vNodes );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-22 20:50:47 +0000