Skip to content

A
abc
Commit d01b1a0e by Alan Mishchenko
Options

Version abc50822

parent 0e4de190
Showing with 3998 additions and 154 deletions
abc.dsp
......@@ -42,7 +42,7 @@ RSC=rc.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
# ADD CPP /nologo /W3 /GX /O2 /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /c
# ADD BASE RSC /l 0x409 /d "NDEBUG"
# ADD RSC /l 0x409 /d "NDEBUG"
BSC32=bscmake.exe
......@@ -66,7 +66,7 @@ LINK32=link.exe
# PROP Ignore_Export_Lib 0
# PROP Target_Dir ""
# ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR /YX /FD /GZ /c
# ADD BASE RSC /l 0x409 /d "_DEBUG"
# ADD RSC /l 0x409 /d "_DEBUG"
BSC32=bscmake.exe
......@@ -121,6 +121,10 @@ SOURCE=.\src\base\abc\abcCreate.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcCut.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abc\abcDfs.c
# End Source File
# Begin Source File
......@@ -1132,6 +1136,46 @@ SOURCE=.\src\opt\rwr\rwrPrint.c
SOURCE=.\src\opt\rwr\rwrUtil.c
# End Source File
# End Group
# Begin Group "cut"
# PROP Default_Filter ""
# Begin Source File
SOURCE=.\src\opt\cut\cut.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutInt.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutList.h
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutMan.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutMerge.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutNode.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutSeq.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutTable.c
# End Source File
# Begin Source File
SOURCE=.\src\opt\cut\cutTruth.c
# End Source File
# End Group
# End Group
# Begin Group "map"
......@@ -1361,6 +1405,10 @@ SOURCE=.\src\misc\extra\extraUtilBitMatrix.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraUtilCanon.c
# End Source File
# Begin Source File
SOURCE=.\src\misc\extra\extraUtilFile.c
# End Source File
# Begin Source File
......
abc.opt
No preview for this file type
abc.plg
......@@ -6,14 +6,14 @@
--------------------Configuration: abc - Win32 Release--------------------
</h3>
<h3>Command Lines</h3>
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1976.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F6.tmp" with contents
[
/nologo /ML /W3 /GX /O2 /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c
"C:\_projects\abc\src\map\mapper\mapperCore.c"
"C:\_projects\abc\src\map\mapper\mapperCut.c"
/nologo /ML /W3 /GX /O2 /I "src\base\abc" /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\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\opt\cut" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c
"C:\_projects\abc\src\opt\cut\cutMan.c"
"C:\_projects\abc\src\misc\extra\extraUtilMisc.c"
]
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1976.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1977.tmp" with contents
Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F6.tmp"
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F7.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 /nologo /subsystem:console /incremental:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe"
.\Release\abc.obj
......@@ -22,6 +22,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Release\abcCheck.obj
.\Release\abcCollapse.obj
.\Release\abcCreate.obj
.\Release\abcCut.obj
.\Release\abcDfs.obj
.\Release\abcDsd.obj
.\Release\abcFanio.obj
......@@ -222,7 +223,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Release\rwrExp.obj
.\Release\rwrLib.obj
.\Release\rwrMan.obj
.\Release\rwrPrint.obj
.\Release\rwrUtil.obj
.\Release\cutMan.obj
.\Release\cutNode.obj
.\Release\cutSeq.obj
.\Release\cutTable.obj
.\Release\cutTruth.obj
.\Release\fpga.obj
.\Release\fpgaCore.obj
.\Release\fpgaCreate.obj
......@@ -278,15 +285,16 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
.\Release\safe_mem.obj
.\Release\strsav.obj
.\Release\texpand.obj
.\Release\rwrPrint.obj
.\Release\cutMerge.obj
.\Release\extraUtilCanon.obj
]
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1977.tmp"
Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F7.tmp"
<h3>Output Window</h3>
Compiling...
mapperCore.c
mapperCut.c
cutMan.c
extraUtilMisc.c
Linking...
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1979.tmp" with contents
Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F9.tmp" with contents
[
/nologo /o"Release/abc.bsc"
.\Release\abc.sbr
......@@ -295,6 +303,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1979.tmp" with cont
.\Release\abcCheck.sbr
.\Release\abcCollapse.sbr
.\Release\abcCreate.sbr
.\Release\abcCut.sbr
.\Release\abcDfs.sbr
.\Release\abcDsd.sbr
.\Release\abcFanio.sbr
......@@ -495,7 +504,13 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1979.tmp" with cont
.\Release\rwrExp.sbr
.\Release\rwrLib.sbr
.\Release\rwrMan.sbr
.\Release\rwrPrint.sbr
.\Release\rwrUtil.sbr
.\Release\cutMan.sbr
.\Release\cutNode.sbr
.\Release\cutSeq.sbr
.\Release\cutTable.sbr
.\Release\cutTruth.sbr
.\Release\fpga.sbr
.\Release\fpgaCore.sbr
.\Release\fpgaCreate.sbr
......@@ -551,8 +566,9 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1979.tmp" with cont
.\Release\safe_mem.sbr
.\Release\strsav.sbr
.\Release\texpand.sbr
.\Release\rwrPrint.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1979.tmp"
.\Release\cutMerge.sbr
.\Release\extraUtilCanon.sbr]
Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP22F9.tmp"
Creating browse info file...
<h3>Output Window</h3>
......
src/base/abc/abc.c
......@@ -23,6 +23,7 @@
#include "ft.h"
#include "fraig.h"
#include "fxu.h"
#include "cut.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
......@@ -58,6 +59,7 @@ static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSplit ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigTrust ( Abc_Frame_t * pAbc, int argc, char ** argv );
......@@ -126,6 +128,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
Cmd_CommandAdd( pAbc, "Various", "split", Abc_CommandSplit, 1 );
Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 );
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_trust", Abc_CommandFraigTrust, 1 );
......@@ -149,6 +152,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Ft_FactorStartMan();
// Rwt_Man4ExploreStart();
// Map_Var3Print();
// Map_Var4Test();
}
/**Function*************************************************************
......@@ -929,14 +934,14 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
fMulti = 0;
fSimple = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "tfmcsh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "TFmcsh" ) ) != EOF )
{
switch ( c )
{
case 't':
case 'T':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nThresh = atoi(argv[util_optind]);
......@@ -944,10 +949,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nThresh < 0 )
goto usage;
break;
case 'f':
case 'F':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-f\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFaninMax = atoi(argv[util_optind]);
......@@ -994,10 +999,10 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: renode [-t num] [-f num] [-cmsh]\n" );
fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" );
fprintf( pErr, "\t transforms an AIG into a logic network by creating larger nodes\n" );
fprintf( pErr, "\t-t num : the threshold for AIG node duplication [default = %d]\n", nThresh );
fprintf( pErr, "\t-f num : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
fprintf( pErr, "\t-T num : the threshold for AIG node duplication [default = %d]\n", nThresh );
fprintf( pErr, "\t-F num : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
fprintf( pErr, "\t-c : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
fprintf( pErr, "\t-m : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" );
fprintf( pErr, "\t-s : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" );
......@@ -1099,14 +1104,14 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
p->fUseCompl = 1;
p->fVerbose = 0;
util_getopt_reset();
while ( (c = util_getopt(argc, argv, "lnsdzcvh")) != EOF )
while ( (c = util_getopt(argc, argv, "LNsdzcvh")) != EOF )
{
switch (c)
{
case 'l':
case 'L':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-l\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
p->nPairsMax = atoi(argv[util_optind]);
......@@ -1114,10 +1119,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( p->nPairsMax < 0 )
goto usage;
break;
case 'n':
case 'N':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
p->nNodesExt = atoi(argv[util_optind]);
......@@ -1168,10 +1173,10 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: fx [-n num] [-l num] [-sdzcvh]\n");
fprintf( pErr, "usage: fx [-N num] [-L num] [-sdzcvh]\n");
fprintf( pErr, "\t performs unate fast extract on the current network\n");
fprintf( pErr, "\t-n num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );
fprintf( pErr, "\t-l num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-N num : the maximum number of divisors to extract [default = %d]\n", p->nNodesExt );
fprintf( pErr, "\t-L num : the maximum number of cube pairs to consider [default = %d]\n", p->nPairsMax );
fprintf( pErr, "\t-s : use only single-cube divisors [default = %s]\n", p->fOnlyS? "yes": "no" );
fprintf( pErr, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
fprintf( pErr, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
......@@ -1423,14 +1428,14 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseDcs = 0;
fVerbose = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "ncdvh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "NCdvh" ) ) != EOF )
{
switch ( c )
{
case 'n':
case 'N':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nNodeSizeMax = atoi(argv[util_optind]);
......@@ -1438,10 +1443,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nNodeSizeMax < 0 )
goto usage;
break;
case 'c':
case 'C':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nConeSizeMax = atoi(argv[util_optind]);
......@@ -1487,10 +1492,10 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: refactor [-n num] [-c num] [-dvh]\n" );
fprintf( pErr, "usage: refactor [-N num] [-C num] [-dvh]\n" );
fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" );
fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );
fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", nConeSizeMax );
fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax );
fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax );
fprintf( pErr, "\t-d : toggle use of don't-cares [default = %s]\n", fUseDcs? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
......@@ -1663,14 +1668,14 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
fInitial = 0;
nFrames = 5;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "fih" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Fih" ) ) != EOF )
{
switch ( c )
{
case 'f':
case 'F':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[util_optind]);
......@@ -1713,9 +1718,9 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: frames [-f num] [-ih]\n" );
fprintf( pErr, "usage: frames [-F num] [-ih]\n" );
fprintf( pErr, "\t unrolls the network for a number of time frames\n" );
fprintf( pErr, "\t-f num : the number of frames to unroll [default = %d]\n", nFrames );
fprintf( pErr, "\t-F num : the number of frames to unroll [default = %d]\n", nFrames );
fprintf( pErr, "\t-i : toggles initializing the first frame [default = %s]\n", fInitial? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -2015,14 +2020,14 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
fUseAllCis = 0;
Output = -1;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "oah" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Oah" ) ) != EOF )
{
switch ( c )
{
case 'o':
case 'O':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-o\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" );
goto usage;
}
Output = atoi(argv[util_optind]);
......@@ -2092,11 +2097,11 @@ int Abc_CommandSplit( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: split [-o num] [-ah] <name>\n" );
fprintf( pErr, "usage: split [-O num] [-ah] <name>\n" );
fprintf( pErr, "\t replaces the current network by the logic cone of one output\n" );
fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-o num : (optional) the 0-based number of the output\n");
fprintf( pErr, "\t-O num : (optional) the 0-based number of the output\n");
fprintf( pErr, "\tname : (optional) the name of the output\n");
return 1;
}
......@@ -2151,6 +2156,121 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Cut_Params_t Params, * pParams = &Params;
Cut_Man_t * pCutMan;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
extern Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
// set defaults
pParams->nVarsMax = 5; // the max cut size ("k" of the k-feasible cuts)
pParams->nKeepMax = 250; // the max number of cuts kept at a node
pParams->fTruth = 1; // compute truth tables
pParams->fHash = 0; // hash cuts to detect unique
pParams->fFilter = 0; // filter dominated cuts
pParams->fSeq = 0; // compute sequential cuts
pParams->fDrop = 0; // drop cuts on the fly
pParams->fVerbose = 0; // the verbosiness flag
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "KMtrfsdvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
pParams->nVarsMax = atoi(argv[util_optind]);
util_optind++;
if ( pParams->nVarsMax < 0 )
goto usage;
break;
case 'M':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
pParams->nKeepMax = atoi(argv[util_optind]);
util_optind++;
if ( pParams->nKeepMax < 0 )
goto usage;
break;
case 't':
pParams->fTruth ^= 1;
break;
case 'r':
pParams->fHash ^= 1;
break;
case 'f':
pParams->fFilter ^= 1;
break;
case 's':
pParams->fSeq ^= 1;
break;
case 'd':
pParams->fDrop ^= 1;
break;
case 'v':
pParams->fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
fprintf( pErr, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsAig(pNtk) )
{
fprintf( pErr, "Cut computation is available only for AIGs.\n" );
return 1;
}
pCutMan = Abc_NtkCuts( pNtk, pParams );
Cut_ManPrintStats( pCutMan );
Cut_ManStop( pCutMan );
return 0;
usage:
fprintf( pErr, "usage: cut [-K num] [-M num] [-trfsdvh]\n" );
fprintf( pErr, "\t computes k-feasible cuts for the AIG\n" );
fprintf( pErr, "\t-K num : max number of leaves (4 <= num <= 6) [default = %d]\n", pParams->nVarsMax );
fprintf( pErr, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax );
fprintf( pErr, "\t-t : toggle truth table computation [default = %s]\n", pParams->fTruth? "yes": "no" );
fprintf( pErr, "\t-r : toggle reduction by hashing [default = %s]\n", pParams->fHash? "yes": "no" );
fprintf( pErr, "\t-f : toggle filtering by dominance [default = %s]\n", pParams->fFilter? "yes": "no" );
fprintf( pErr, "\t-s : toggle sequential cut computation [default = %s]\n", pParams->fSeq? "yes": "no" );
fprintf( pErr, "\t-d : toggle dropping when fanouts are done [default = %s]\n", pParams->fDrop? "yes": "no" );
fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
......@@ -2168,7 +2288,7 @@ usage:
int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
{
char Buffer[100];
Fraig_Params_t Params;
Fraig_Params_t Params, * pParams = &Params;
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int fAllNodes;
......@@ -2180,17 +2300,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
// set defaults
fAllNodes = 0;
Params.nPatsRand = 2048; // the number of words of random simulation info
Params.nPatsDyna = 2048; // the number of words of dynamic simulation info
Params.nBTLimit = 99; // the max number of backtracks to perform
Params.fFuncRed = 1; // performs only one level hashing
Params.fFeedBack = 1; // enables solver feedback
Params.fDist1Pats = 1; // enables distance-1 patterns
Params.fDoSparse = 0; // performs equiv tests for sparse functions
Params.fChoicing = 0; // enables recording structural choices
Params.fTryProve = 0; // tries to solve the final miter
Params.fVerbose = 0; // the verbosiness flag
Params.fVerboseP = 0; // the verbosiness flag
pParams->nPatsRand = 2048; // the number of words of random simulation info
pParams->nPatsDyna = 2048; // the number of words of dynamic simulation info
pParams->nBTLimit = 99; // the max number of backtracks to perform
pParams->fFuncRed = 1; // performs only one level hashing
pParams->fFeedBack = 1; // enables solver feedback
pParams->fDist1Pats = 1; // enables distance-1 patterns
pParams->fDoSparse = 0; // performs equiv tests for sparse functions
pParams->fChoicing = 0; // enables recording structural choices
pParams->fTryProve = 0; // tries to solve the final miter
pParams->fVerbose = 0; // the verbosiness flag
pParams->fVerboseP = 0; // the verbosiness flag
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF )
{
......@@ -2200,51 +2320,51 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'R':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-r\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
Params.nPatsRand = atoi(argv[util_optind]);
pParams->nPatsRand = atoi(argv[util_optind]);
util_optind++;
if ( Params.nPatsRand < 0 )
if ( pParams->nPatsRand < 0 )
goto usage;
break;
case 'D':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-d\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
Params.nPatsDyna = atoi(argv[util_optind]);
pParams->nPatsDyna = atoi(argv[util_optind]);
util_optind++;
if ( Params.nPatsDyna < 0 )
if ( pParams->nPatsDyna < 0 )
goto usage;
break;
case 'B':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-b\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
goto usage;
}
Params.nBTLimit = atoi(argv[util_optind]);
pParams->nBTLimit = atoi(argv[util_optind]);
util_optind++;
if ( Params.nBTLimit < 0 )
if ( pParams->nBTLimit < 0 )
goto usage;
break;
case 'r':
Params.fFuncRed ^= 1;
pParams->fFuncRed ^= 1;
break;
case 's':
Params.fDoSparse ^= 1;
pParams->fDoSparse ^= 1;
break;
case 'c':
Params.fChoicing ^= 1;
pParams->fChoicing ^= 1;
break;
case 'p':
Params.fTryProve ^= 1;
pParams->fTryProve ^= 1;
break;
case 'v':
Params.fVerbose ^= 1;
pParams->fVerbose ^= 1;
break;
case 'a':
fAllNodes ^= 1;
......@@ -2268,7 +2388,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// report the proof
Params.fVerboseP = Params.fTryProve;
pParams->fVerboseP = pParams->fTryProve;
// get the new network
if ( Abc_NtkIsAig(pNtk) )
......@@ -2285,7 +2405,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( Params.fTryProve ) // report the result
if ( pParams->fTryProve ) // report the result
Abc_NtkMiterReport( pNtkRes );
// replace the current network
......@@ -2293,17 +2413,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
sprintf( Buffer, "%d", Params.nBTLimit );
sprintf( Buffer, "%d", pParams->nBTLimit );
fprintf( pErr, "usage: fraig [-R num] [-D num] [-B num] [-rscpvah]\n" );
fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" );
fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", Params.nPatsRand );
fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", Params.nPatsDyna );
fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n", Params.nBTLimit==-1? "infinity" : Buffer );
fprintf( pErr, "\t-r : toggle functional reduction [default = %s]\n", Params.fFuncRed? "yes": "no" );
fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", Params.fDoSparse? "yes": "no" );
fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", Params.fChoicing? "yes": "no" );
fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", Params.fTryProve? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", Params.fVerbose? "yes": "no" );
fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand );
fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna );
fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n", pParams->nBTLimit==-1? "infinity" : Buffer );
fprintf( pErr, "\t-r : toggle functional reduction [default = %s]\n", pParams->fFuncRed? "yes": "no" );
fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", pParams->fDoSparse? "yes": "no" );
fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", pParams->fChoicing? "yes": "no" );
fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", pParams->fTryProve? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" );
fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
......@@ -2657,14 +2777,14 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
fSweep = 1;
fVerbose = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "dasvh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Dasvh" ) ) != EOF )
{
switch ( c )
{
case 'd':
case 'D':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-d\" should be followed by a floating point number.\n" );
fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" );
goto usage;
}
DelayTarget = (float)atof(argv[util_optind]);
......@@ -2743,9 +2863,9 @@ usage:
sprintf( Buffer, "not used" );
else
sprintf( Buffer, "%.3f", DelayTarget );
fprintf( pErr, "usage: map [-d num] [-asvh]\n" );
fprintf( pErr, "usage: map [-D num] [-asvh]\n" );
fprintf( pErr, "\t performs standard cell mapping of the current network\n" );
fprintf( pErr, "\t-d num : sets the global required times [default = %s]\n", Buffer );
fprintf( pErr, "\t-D num : sets the global required times [default = %s]\n", Buffer );
fprintf( pErr, "\t-a : toggles area recovery [default = %s]\n", fRecovery? "yes": "no" );
fprintf( pErr, "\t-s : toggles sweep after mapping [default = %s]\n", fSweep? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
......@@ -3299,14 +3419,14 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
nFrames = 3;
fSat = 0;
util_getopt_reset();
while ( ( c = util_getopt( argc, argv, "fsh" ) ) != EOF )
while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF )
{
switch ( c )
{
case 'f':
case 'F':
if ( util_optind >= argc )
{
fprintf( pErr, "Command line switch \"-t\" should be followed by an integer.\n" );
fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[util_optind]);
......@@ -3338,11 +3458,11 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pErr, "usage: sec [-sh] [-f num] <file1> <file2>\n" );
fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\n" );
fprintf( pErr, "\t performs bounded sequential equivalence checking\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\t-f num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
fprintf( pErr, "\tfile1 : (optional) the file with the first network\n");
fprintf( pErr, "\tfile2 : (optional) the file with the second network\n");
fprintf( pErr, "\t if no files are given, uses the current network and its spec\n");
......
src/base/abc/abc.h
......@@ -426,7 +426,7 @@ extern Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode );
extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes );
extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk );
extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll );
extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos );
extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi );
extern int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk );
extern bool Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
......
src/base/abc/abcAig.c
......@@ -156,7 +156,7 @@ Abc_Aig_t * Abc_AigDup( Abc_Aig_t * pMan, Abc_Aig_t * pManNew )
Abc_NtkForEachLatch( pMan->pNtkAig, pObj, i )
pObj->pCopy = Abc_NtkLatch( pManNew->pNtkAig, i );
// copy internal nodes
vNodes = Abc_AigDfs( pMan->pNtkAig, 1 );
vNodes = Abc_AigDfs( pMan->pNtkAig, 1, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
if ( !Abc_NodeIsAigAnd(pObj) )
......
src/base/abc/abcCut.c 0 → 100644
/**CFile****************************************************************
FileName [abcCut.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Interface to cut computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "abc.h"
#include "cut.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the cuts for the network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
{
Cut_Man_t * p;
Abc_Obj_t * pObj, * pDriver, * pNode;
Vec_Ptr_t * vNodes;
Vec_Int_t * vChoices;
int i;
int clk = clock();
assert( Abc_NtkIsAig(pNtk) );
// start the manager
pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
p = Cut_ManStart( pParams );
if ( pParams->fDrop )
Cut_ManSetFanoutCounts( p, Abc_NtkFanoutCounts(pNtk) );
// set cuts for PIs
Abc_NtkForEachCi( pNtk, pObj, i )
if ( Abc_ObjFanoutNum(pObj) > 0 )
Cut_NodeSetTriv( p, pObj->Id );
// compute cuts for internal nodes
vNodes = Abc_AigDfs( pNtk, 0, 1 );
vChoices = Vec_IntAlloc( 100 );
Vec_PtrForEachEntry( vNodes, pObj, i )
{
// when we reached a CO, it is time to deallocate the cuts
if ( Abc_ObjIsCo(pObj) )
{
if ( pParams->fDrop )
Cut_NodeTryDroppingCuts( p, Abc_ObjFaninId0(pObj) );
continue;
}
// skip constant node, it has no cuts
if ( Abc_NodeIsConst(pObj) )
continue;
// compute the cuts to the internal node
Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj),
Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
// add cuts due to choices
if ( Abc_NodeIsAigChoice(pObj) )
{
Vec_IntClear( vChoices );
for ( pNode = pObj; pNode; pNode = pNode->pData )
Vec_IntPush( vChoices, pNode->Id );
Cut_NodeUnionCuts( p, vChoices );
}
}
if ( !pParams->fSeq )
{
Vec_PtrFree( vNodes );
Vec_IntFree( vChoices );
PRT( "Total", clock() - clk );
return p;
}
assert( 0 );
// compute sequential cuts
Abc_NtkIncrementTravId( pNtk );
Abc_NtkForEachLatch( pNtk, pObj, i )
{
pDriver = Abc_ObjFanin0(pObj);
if ( !Abc_ObjIsNode(pDriver) )
continue;
if ( Abc_NodeIsTravIdCurrent(pDriver) )
continue;
Abc_NodeSetTravIdCurrent(pDriver);
Cut_NodeSetComputedAsNew( p, pDriver->Id );
}
// compute as long as new cuts appear
return p;
}
/**Function*************************************************************
Synopsis [Creates the array of fanout counters.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk )
{
Vec_Int_t * vFanNums;
Abc_Obj_t * pObj;//, * pFanout;
int i;//, k, nFanouts;
vFanNums = Vec_IntAlloc( 0 );
Vec_IntFill( vFanNums, Abc_NtkObjNumMax(pNtk), -1 );
Abc_NtkForEachObj( pNtk, pObj, i )
if ( Abc_ObjIsCi(pObj) || Abc_ObjIsNode(pObj) )
{
Vec_IntWriteEntry( vFanNums, i, Abc_ObjFanoutNum(pObj) );
/*
// get the number of non-CO fanouts
nFanouts = 0;
Abc_ObjForEachFanout( pObj, pFanout, k )
if ( !Abc_ObjIsCo(pFanout) )
nFanouts++;
Vec_IntWriteEntry( vFanNums, i, nFanouts );
*/
}
return vFanNums;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/base/abc/abcDfs.c
......@@ -141,8 +141,8 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
Synopsis [Returns the reverse DFS ordered array of logic nodes.]
Description [Collects only the internal nodes, leaving CIs and CO.
However it marks with the current TravId both CIs and COs.]
Description [Collects only the internal nodes, leaving out CIs/COs.
However it marks both CIs and COs with the current TravId.]
SideEffects []
......@@ -210,15 +210,15 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
Synopsis [Returns the DFS ordered array of logic nodes.]
Description [Collects only the internal nodes, leaving CIs and CO.
However it marks with the current TravId both CIs and COs.]
Description [Collects only the internal nodes, leaving out CIs/COs.
However it marks both CIs and COs with the current TravId.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll )
Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos )
{
Vec_Ptr_t * vNodes;
Abc_Obj_t * pNode;
......@@ -231,8 +231,10 @@ Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll )
// go through the PO nodes and call for each of them
Abc_NtkForEachCo( pNtk, pNode, i )
{
Abc_NodeSetTravIdCurrent( pNode );
Abc_AigDfs_rec( Abc_ObjFanin0(pNode), vNodes );
Abc_NodeSetTravIdCurrent( pNode );
if ( fCollectCos )
Vec_PtrPush( vNodes, pNode );
}
// collect dangling nodes if asked to
if ( fCollectAll )
......
src/base/abc/abcFpga.c
......@@ -121,7 +121,7 @@ Fpga_Man_t * Abc_NtkToFpga( Abc_Ntk_t * pNtk, int fRecovery, int fVerbose )
pNode->pCopy = (Abc_Obj_t *)Fpga_ManReadInputs(pMan)[i];
// load the AIG into the mapper
vNodes = Abc_AigDfs( pNtk, 0 );
vNodes = Abc_AigDfs( pNtk, 0, 0 );
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
......
src/base/abc/abcFraig.c
......@@ -104,7 +104,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA
pConst1 = Abc_AigConst1( pNtk->pManFunc );
// perform strashing
vNodes = Abc_AigDfs( pNtk, fAllNodes );
vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
......
src/base/abc/abcMap.c
......@@ -147,7 +147,7 @@ Map_Man_t * Abc_NtkToMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, i
pNode->pCopy = (Abc_Obj_t *)Map_ManReadInputs(pMan)[i];
// load the AIG into the mapper
vNodes = Abc_AigDfs( pNtk, 0 );
vNodes = Abc_AigDfs( pNtk, 0, 0 );
pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
Vec_PtrForEachEntry( vNodes, pNode, i )
{
......
src/base/abc/abcSeq.c
......@@ -87,7 +87,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
}
// copy internal nodes
vNodes = Abc_AigDfs( pNtk, 1 );
vNodes = Abc_AigDfs( pNtk, 1, 0 );
Vec_PtrForEachEntry( vNodes, pObj, i )
if ( Abc_ObjFaninNum(pObj) == 2 )
pObj->pCopy = Abc_AigAnd( pManNew, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
......
src/base/abc/module.make
......@@ -4,6 +4,7 @@ SRC += src/base/abc/abc.c \
src/base/abc/abcCheck.c \
src/base/abc/abcCollapse.c \
src/base/abc/abcCreate.c \
src/base/abc/abcCut.c \
src/base/abc/abcDfs.c \
src/base/abc/abcDsd.c \
src/base/abc/abcFanio.c \
......
src/map/mapper/mapperCanon.c
......@@ -170,13 +170,26 @@ void Map_CanonComputePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[]
int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned uTruth[], unsigned char * puPhases, unsigned uTruthRes[] )
{
unsigned uTruth0, uTruth1;
unsigned uCanon0, uCanon1, uCanonBest;
unsigned uCanon0, uCanon1, uCanonBest, uPhaseBest;
int i, Limit;
if ( nVarsMax != 5 || nVarsReal < 5 )
if ( nVarsMax == 6 )
return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
if ( nVarsReal < 5 )
{
// return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
uTruth0 = uTruth[0] & 0xFFFF;
assert( p->pCounters[uTruth0] > 0 );
uTruthRes[0] = (p->uCanons[uTruth0] << 16) | p->uCanons[uTruth0];
uTruthRes[1] = uTruthRes[0];
puPhases[0] = p->uPhases[uTruth0][0];
return 1;
}
assert( nVarsMax == 5 );
assert( nVarsReal == 5 );
uTruth0 = uTruth[0] & 0xFFFF;
uTruth1 = (uTruth[0] >> 16);
if ( uTruth1 == 0 )
......@@ -202,7 +215,7 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
}
uCanon0 = p->uCanons[uTruth0];
uCanon1 = p->uCanons[uTruth1];
if ( uCanon0 && uCanon1 && uCanon0 > uCanon1 ) // using nCanon1 as the main one
if ( uCanon0 >= uCanon1 ) // using nCanon1 as the main one
{
assert( p->pCounters[uTruth1] > 0 );
uCanonBest = 0xFFFF;
......@@ -210,16 +223,17 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
{
uCanon0 = Extra_TruthPolarize( uTruth0, p->uPhases[uTruth1][i], 4 );
if ( uCanonBest > uCanon0 )
{
uCanonBest = uCanon0;
uPhaseBest = p->uPhases[uTruth1][i];
}
}
uTruthRes[0] = (uCanon1 << 16) | uCanonBest;
uTruthRes[1] = uTruthRes[0];
Limit = (p->pCounters[uTruth1] > 4)? 4 : p->pCounters[uTruth1];
for ( i = 0; i < Limit; i++ )
puPhases[i] = p->uPhases[uTruth1][i];
return Limit;
puPhases[0] = uPhaseBest;
return 1;
}
else if ( uCanon0 && uCanon1 && uCanon0 < uCanon1 )
else if ( uCanon0 < uCanon1 )
{
assert( p->pCounters[uTruth0] > 0 );
uCanonBest = 0xFFFF;
......@@ -227,22 +241,27 @@ int Map_CanonComputeFast( Map_Man_t * p, int nVarsMax, int nVarsReal, unsigned u
{
uCanon1 = Extra_TruthPolarize( uTruth1, p->uPhases[uTruth0][i], 4 );
if ( uCanonBest > uCanon1 )
{
uCanonBest = uCanon1;
uPhaseBest = p->uPhases[uTruth0][i];
}
}
uTruthRes[0] = (uCanon0 << 16) | uCanonBest;
uTruthRes[1] = uTruthRes[0];
Limit = (p->pCounters[uTruth0] > 4)? 4 : p->pCounters[uTruth0];
for ( i = 0; i < Limit; i++ )
{
puPhases[i] = p->uPhases[uTruth0][i];
puPhases[i] |= (1 << 4);
}
return Limit;
puPhases[0] = uPhaseBest | (1 << 4);
return 1;
}
else
{
assert( 0 );
return Map_CanonComputeSlow( p->uTruths, nVarsMax, nVarsReal, uTruth, puPhases, uTruthRes );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/mapper/mapperCore.c
......@@ -69,7 +69,7 @@ int Map_Mapping( Map_Man_t * p )
Map_MappingTruths( p );
p->timeTruth = clock() - clk;
//////////////////////////////////////////////////////////////////////
//PRT( "Truths", clock() - clk );
PRT( "Truths", clock() - clk );
//////////////////////////////////////////////////////////////////////
// compute the minimum-delay mapping
......
src/map/mapper/mapperCreate.c
......@@ -197,7 +197,7 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
assert( p->nVarsMax > 0 );
if ( p->nVarsMax == 5 )
Extra_Truth4VarN( &p->uCanons, &p->uPhases, &p->pCounters, 16 );
Extra_Truth4VarN( &p->uCanons, &p->uPhases, &p->pCounters, 8 );
// start various data structures
Map_TableCreate( p );
......
src/map/mapper/mapperCut.c
......@@ -692,6 +692,7 @@ int Map_MappingCountAllCuts( Map_Man_t * pMan )
Map_Cut_t * pCut;
int i, nCuts;
// int nCuts55 = 0, nCuts5x = 0, nCuts4x = 0, nCuts3x = 0;
// int pCounts[7] = {0};
nCuts = 0;
for ( i = 0; i < pMan->nBins; i++ )
for ( pNode = pMan->pBins[i]; pNode; pNode = pNode->pNext )
......@@ -708,9 +709,14 @@ int Map_MappingCountAllCuts( Map_Man_t * pMan )
nCuts4x++;
else if ( Map_CutRegular(pCut->pOne)->nLeaves == 3 || Map_CutRegular(pCut->pTwo)->nLeaves == 3 )
nCuts3x++;
*/
*/
// pCounts[ Map_CutRegular(pCut->pOne)->nLeaves ]++;
// pCounts[ Map_CutRegular(pCut->pTwo)->nLeaves ]++;
}
// printf( "Total cuts = %6d. 55 = %6d. 5x = %6d. 4x = %6d. 3x = %6d.\n", nCuts, nCuts55, nCuts5x, nCuts4x, nCuts3x );
// printf( "Total cuts = %6d. 6= %6d. 5= %6d. 4= %6d. 3= %6d. 2= %6d. 1= %6d.\n",
// nCuts, pCounts[6], pCounts[5], pCounts[4], pCounts[3], pCounts[2], pCounts[1] );
return nCuts;
}
......
src/map/mapper/mapperTruth.c
......@@ -93,8 +93,13 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
// unsigned uCanon1, uCanon2;
unsigned uTruth[2], uCanon[2];
unsigned char uPhases[16];
int fUseFast = 1;
unsigned * uCanon2;
char * pPhases2;
int fUseFast = 0;
int fUseRec = 1;
extern int Map_CanonCompute( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
// generally speaking, 1-input cut can be matched into a wire!
if ( pCut->nLeaves == 1 )
return;
......@@ -112,6 +117,21 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
// compute the canonical form for the positive phase
if ( fUseFast )
Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
else if ( fUseRec )
{
// Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
Extra_TruthCanonFastN( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
/*
if ( uCanon[0] != uCanon2[0] || uPhases[0] != pPhases2[0] )
{
int k = 0;
Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
}
*/
uCanon[0] = uCanon2[0];
uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
uPhases[0] = pPhases2[0];
}
else
Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
pCut->M[1].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
......@@ -125,6 +145,21 @@ void Map_TruthsCut( Map_Man_t * p, Map_Cut_t * pCut )
uTruth[1] = ~uTruth[1];
if ( fUseFast )
Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
else if ( fUseRec )
{
// Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
Extra_TruthCanonFastN( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
/*
if ( uCanon[0] != uCanon2[0] || uPhases[0] != pPhases2[0] )
{
int k = 0;
Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
}
*/
uCanon[0] = uCanon2[0];
uCanon[1] = (p->nVarsMax == 6)? uCanon2[1] : uCanon2[0];
uPhases[0] = pPhases2[0];
}
else
Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
pCut->M[0].pSupers = Map_SuperTableLookupC( p->pSuperLib, uCanon );
......@@ -243,6 +278,25 @@ void Map_CutsCollect_rec( Map_Cut_t * pCut, Map_NodeVec_t * vVisited )
Map_NodeVecPush( vVisited, (Map_Node_t *)pCut );
}
/*
{
unsigned * uCanon2;
char * pPhases2;
Map_CanonComputeSlow( p->uTruths, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
if ( uCanon2[0] != uCanon[0] )
{
int v = 0;
Map_CanonCompute( p->nVarsMax, pCut->nLeaves, uTruth, &uCanon2, &pPhases2 );
Map_CanonComputeFast( p, p->nVarsMax, pCut->nLeaves, uTruth, uPhases, uCanon );
}
// else
// {
// printf( "Correct.\n" );
// }
}
*/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
src/misc/extra/extra.h
......@@ -216,6 +216,10 @@ extern unsigned Extra_TruthCanonNPN( unsigned uTruth, int nVars );
extern void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap );
extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax );
/* permutation mapping */
extern unsigned short Extra_TruthPerm4One( unsigned uTruth, int Phase );
extern unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase );
extern void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes );
/* precomputing tables for permutation mapping */
extern void ** Extra_ArrayAlloc( int nCols, int nRows, int Size );
extern unsigned short ** Extra_TruthPerm43();
extern unsigned ** Extra_TruthPerm53();
......@@ -223,6 +227,11 @@ extern unsigned ** Extra_TruthPerm54();
/* for independence from CUDD */
extern unsigned int Cudd_PrimeCopy( unsigned int p );
/*=== extraUtilCanon.c ========================================================*/
/* fast computation of N-canoninical form up to 6 inputs */
extern int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes );
/*=== extraUtilProgress.c ================================================================*/
typedef struct ProgressBarStruct ProgressBar;
......
src/misc/extra/extraUtilCanon.c 0 → 100644
/**CFile****************************************************************
FileName [extraUtilMisc.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [extra]
Synopsis [Computing canonical forms of Boolean functions using truth tables.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: extraUtilMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "extra.h"
/*---------------------------------------------------------------------------*/
/* Constant declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Stucture declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Type declarations */
/*---------------------------------------------------------------------------*/
/*---------------------------------------------------------------------------*/
/* Variable declarations */
/*---------------------------------------------------------------------------*/
static unsigned s_Truths3[256];
static char s_Phases3[256][9];
/*---------------------------------------------------------------------------*/
/* Macro declarations */
/*---------------------------------------------------------------------------*/
/**AutomaticStart*************************************************************/
/*---------------------------------------------------------------------------*/
/* Static function prototypes */
/*---------------------------------------------------------------------------*/
static int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag );
/**AutomaticEnd***************************************************************/
/*---------------------------------------------------------------------------*/
/* Definition of exported functions */
/*---------------------------------------------------------------------------*/
/**Function********************************************************************
Synopsis [Computes the N-canonical form of the Boolean function up to 6 inputs.]
Description [The N-canonical form is defined as the truth table with
the minimum integer value. This function exhaustively enumerates
through the complete set of 2^N phase assignments.
Returns pointers to the static storage to the truth table and phases.
This data should be used before the function is called again.]
SideEffects []
SeeAlso []
******************************************************************************/
int Extra_TruthCanonFastN( int nVarsMax, int nVarsReal, unsigned * pt, unsigned ** pptRes, char ** ppfRes )
{
static unsigned uTruthStore6[2];
int RetValue;
assert( nVarsMax <= 6 );
assert( nVarsReal <= nVarsMax );
RetValue = Extra_TruthCanonN_rec( nVarsReal <= 3? 3: nVarsReal, (unsigned char *)pt, pptRes, ppfRes, 0 );
if ( nVarsMax == 6 && nVarsReal < nVarsMax )
{
uTruthStore6[0] = **pptRes;
uTruthStore6[1] = **pptRes;
*pptRes = uTruthStore6;
}
return RetValue;
}
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
/**Function*************************************************************
Synopsis [Recursive implementation of the above.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Extra_TruthCanonN_rec( int nVars, unsigned char * pt, unsigned ** pptRes, char ** ppfRes, int Flag )
{
static unsigned uTruthStore[7][2][2];
static char uPhaseStore[7][2][64];
unsigned char * pt0, * pt1;
unsigned * ptRes0, * ptRes1, * ptRes;
unsigned uInit0, uInit1, uTruth0, uTruth1, uTemp;
char * pfRes0, * pfRes1, * pfRes;
int nf0, nf1, nfRes, i, nVarsN;
// table lookup for three vars
if ( nVars == 3 )
{
*pptRes = &s_Truths3[*pt];
*ppfRes = s_Phases3[*pt]+1;
return s_Phases3[*pt][0];
}
// number of vars for the next call
nVarsN = nVars-1;
// truth table for the next call
pt0 = pt;
pt1 = pt + (1 << nVarsN) / 8;
// 5-var truth tables for this call
uInit0 = *((unsigned *)pt0);
uInit1 = *((unsigned *)pt1);
if ( nVarsN == 3 )
{
uInit0 &= 0xFF;
uInit1 &= 0xFF;
uInit0 = (uInit0 << 24) | (uInit0 << 16) | (uInit0 << 8) | uInit0;
uInit1 = (uInit1 << 24) | (uInit1 << 16) | (uInit1 << 8) | uInit1;
}
else if ( nVarsN == 4 )
{
uInit0 &= 0xFFFF;
uInit1 &= 0xFFFF;
uInit0 = (uInit0 << 16) | uInit0;
uInit1 = (uInit1 << 16) | uInit1;
}
// storage for truth tables and phases
ptRes = uTruthStore[nVars][Flag];
pfRes = uPhaseStore[nVars][Flag];
// solve trivial cases
if ( uInit1 == 0 )
{
nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
uTruth1 = uInit1;
uTruth0 = *ptRes0;
nfRes = 0;
for ( i = 0; i < nf0; i++ )
pfRes[nfRes++] = pfRes0[i];
goto finish;
}
if ( uInit0 == 0 )
{
nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
uTruth1 = uInit0;
uTruth0 = *ptRes1;
nfRes = 0;
for ( i = 0; i < nf1; i++ )
pfRes[nfRes++] = pfRes1[i] | (1<<nVarsN);
goto finish;
}
if ( uInit1 == 0xFFFFFFFF )
{
nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
uTruth1 = *ptRes0;
uTruth0 = uInit1;
nfRes = 0;
for ( i = 0; i < nf0; i++ )
pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
goto finish;
}
if ( uInit0 == 0xFFFFFFFF )
{
nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
uTruth1 = *ptRes1;
uTruth0 = uInit0;
nfRes = 0;
for ( i = 0; i < nf1; i++ )
pfRes[nfRes++] = pfRes1[i];
goto finish;
}
// solve the problem for cofactors
nf0 = Extra_TruthCanonN_rec( nVarsN, pt0, &ptRes0, &pfRes0, 0 );
nf1 = Extra_TruthCanonN_rec( nVarsN, pt1, &ptRes1, &pfRes1, 1 );
// combine the result
if ( *ptRes1 < *ptRes0 )
{
uTruth0 = 0xFFFFFFFF;
nfRes = 0;
for ( i = 0; i < nf1; i++ )
{
uTemp = Extra_TruthPolarize( uInit0, pfRes1[i], nVarsN );
if ( uTruth0 > uTemp )
{
nfRes = 0;
uTruth0 = uTemp;
pfRes[nfRes++] = pfRes1[i];
}
else if ( uTruth0 == uTemp )
pfRes[nfRes++] = pfRes1[i];
}
uTruth1 = *ptRes1;
}
else if ( *ptRes1 > *ptRes0 )
{
uTruth0 = 0xFFFFFFFF;
nfRes = 0;
for ( i = 0; i < nf0; i++ )
{
uTemp = Extra_TruthPolarize( uInit1, pfRes0[i], nVarsN );
if ( uTruth0 > uTemp )
{
nfRes = 0;
uTruth0 = uTemp;
pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
}
else if ( uTruth0 == uTemp )
pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
}
uTruth1 = *ptRes0;
}
else
{
assert( nf0 == nf1 );
nfRes = 0;
for ( i = 0; i < nf1; i++ )
pfRes[nfRes++] = pfRes1[i];
for ( i = 0; i < nf0; i++ )
pfRes[nfRes++] = pfRes0[i] | (1<<nVarsN);
uTruth0 = Extra_TruthPolarize( uInit0, pfRes1[0], nVarsN );
uTruth1 = *ptRes0;
}
finish :
if ( nVarsN == 3 )
{
uTruth0 &= 0xFF;
uTruth1 &= 0xFF;
uTemp = (uTruth1 << 8) | uTruth0;
*ptRes = (uTemp << 16) | uTemp;
}
else if ( nVarsN == 4 )
{
uTruth0 &= 0xFFFF;
uTruth1 &= 0xFFFF;
*ptRes = (uTruth1 << 16) | uTruth0;
}
else if ( nVarsN == 5 )
{
*(ptRes+0) = uTruth0;
*(ptRes+1) = uTruth1;
}
*pptRes = ptRes;
*ppfRes = pfRes;
return nfRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Map_Var3Print()
{
extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
unsigned * uCanons;
char ** uPhases;
char * pCounters;
int i, k;
Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
for ( i = 0; i < 256; i++ )
{
if ( i % 8 == 0 )
printf( "\n" );
Extra_PrintHex( stdout, uCanons[i], 5 );
printf( ", " );
}
printf( "\n" );
for ( i = 0; i < 256; i++ )
{
printf( "%3d */ { %2d, ", i, pCounters[i] );
for ( k = 0; k < pCounters[i]; k++ )
printf( "%s%d", k? ", ":"", uPhases[i][k] );
printf( " }\n" );
}
printf( "\n" );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Map_Var3Test()
{
extern void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters );
unsigned * uCanons;
char ** uPhases;
char * pCounters;
int i;
unsigned * ptRes;
char * pfRes;
unsigned uTruth;
int Count;
Extra_Truth3VarN( &uCanons, &uPhases, &pCounters );
for ( i = 0; i < 256; i++ )
{
uTruth = i;
Count = Extra_TruthCanonFastN( 5, 3, &uTruth, &ptRes, &pfRes );
if ( *ptRes != uCanons[i] || Count != pCounters[i] )
{
int k = 0;
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Map_Var4Test()
{
extern void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int PhaseMax );
unsigned short * uCanons;
char ** uPhases;
char * pCounters;
int i, k;
unsigned * ptRes;
char * pfRes;
unsigned uTruth;
int Count;
Extra_Truth4VarN( &uCanons, &uPhases, &pCounters, 16 );
for ( i = 0; i < 256*256; i++ )
{
uTruth = i;
Count = Extra_TruthCanonFastN( 5, 4, &uTruth, &ptRes, &pfRes );
if ( (*ptRes & 0xFFFF) != uCanons[i] || Count != pCounters[i] )
{
int k = 0;
}
for ( k = 0; k < Count; k++ )
if ( uPhases[i][k] != pfRes[k] )
{
int v = 0;
}
}
}
/*---------------------------------------------------------------------------*/
/* Definition of static Functions */
/*---------------------------------------------------------------------------*/
static unsigned s_Truths3[256] =
{
0x00000000, 0x01010101, 0x01010101, 0x03030303, 0x01010101, 0x05050505, 0x06060606, 0x07070707,
0x01010101, 0x06060606, 0x05050505, 0x07070707, 0x03030303, 0x07070707, 0x07070707, 0x0f0f0f0f,
0x01010101, 0x11111111, 0x12121212, 0x13131313, 0x14141414, 0x15151515, 0x16161616, 0x17171717,
0x18181818, 0x19191919, 0x1a1a1a1a, 0x1b1b1b1b, 0x1c1c1c1c, 0x1d1d1d1d, 0x1e1e1e1e, 0x1f1f1f1f,
0x01010101, 0x12121212, 0x11111111, 0x13131313, 0x18181818, 0x1a1a1a1a, 0x19191919, 0x1b1b1b1b,
0x14141414, 0x16161616, 0x15151515, 0x17171717, 0x1c1c1c1c, 0x1e1e1e1e, 0x1d1d1d1d, 0x1f1f1f1f,
0x03030303, 0x13131313, 0x13131313, 0x33333333, 0x1c1c1c1c, 0x35353535, 0x36363636, 0x37373737,
0x1c1c1c1c, 0x36363636, 0x35353535, 0x37373737, 0x3c3c3c3c, 0x3d3d3d3d, 0x3d3d3d3d, 0x3f3f3f3f,
0x01010101, 0x14141414, 0x18181818, 0x1c1c1c1c, 0x11111111, 0x15151515, 0x19191919, 0x1d1d1d1d,
0x12121212, 0x16161616, 0x1a1a1a1a, 0x1e1e1e1e, 0x13131313, 0x17171717, 0x1b1b1b1b, 0x1f1f1f1f,
0x05050505, 0x15151515, 0x1a1a1a1a, 0x35353535, 0x15151515, 0x55555555, 0x56565656, 0x57575757,
0x1a1a1a1a, 0x56565656, 0x5a5a5a5a, 0x5b5b5b5b, 0x35353535, 0x57575757, 0x5b5b5b5b, 0x5f5f5f5f,
0x06060606, 0x16161616, 0x19191919, 0x36363636, 0x19191919, 0x56565656, 0x66666666, 0x67676767,
0x16161616, 0x69696969, 0x56565656, 0x6b6b6b6b, 0x36363636, 0x6b6b6b6b, 0x67676767, 0x6f6f6f6f,
0x07070707, 0x17171717, 0x1b1b1b1b, 0x37373737, 0x1d1d1d1d, 0x57575757, 0x67676767, 0x77777777,
0x1e1e1e1e, 0x6b6b6b6b, 0x5b5b5b5b, 0x7b7b7b7b, 0x3d3d3d3d, 0x7d7d7d7d, 0x7e7e7e7e, 0x7f7f7f7f,
0x01010101, 0x18181818, 0x14141414, 0x1c1c1c1c, 0x12121212, 0x1a1a1a1a, 0x16161616, 0x1e1e1e1e,
0x11111111, 0x19191919, 0x15151515, 0x1d1d1d1d, 0x13131313, 0x1b1b1b1b, 0x17171717, 0x1f1f1f1f,
0x06060606, 0x19191919, 0x16161616, 0x36363636, 0x16161616, 0x56565656, 0x69696969, 0x6b6b6b6b,
0x19191919, 0x66666666, 0x56565656, 0x67676767, 0x36363636, 0x67676767, 0x6b6b6b6b, 0x6f6f6f6f,
0x05050505, 0x1a1a1a1a, 0x15151515, 0x35353535, 0x1a1a1a1a, 0x5a5a5a5a, 0x56565656, 0x5b5b5b5b,
0x15151515, 0x56565656, 0x55555555, 0x57575757, 0x35353535, 0x5b5b5b5b, 0x57575757, 0x5f5f5f5f,
0x07070707, 0x1b1b1b1b, 0x17171717, 0x37373737, 0x1e1e1e1e, 0x5b5b5b5b, 0x6b6b6b6b, 0x7b7b7b7b,
0x1d1d1d1d, 0x67676767, 0x57575757, 0x77777777, 0x3d3d3d3d, 0x7e7e7e7e, 0x7d7d7d7d, 0x7f7f7f7f,
0x03030303, 0x1c1c1c1c, 0x1c1c1c1c, 0x3c3c3c3c, 0x13131313, 0x35353535, 0x36363636, 0x3d3d3d3d,
0x13131313, 0x36363636, 0x35353535, 0x3d3d3d3d, 0x33333333, 0x37373737, 0x37373737, 0x3f3f3f3f,
0x07070707, 0x1d1d1d1d, 0x1e1e1e1e, 0x3d3d3d3d, 0x17171717, 0x57575757, 0x6b6b6b6b, 0x7d7d7d7d,
0x1b1b1b1b, 0x67676767, 0x5b5b5b5b, 0x7e7e7e7e, 0x37373737, 0x77777777, 0x7b7b7b7b, 0x7f7f7f7f,
0x07070707, 0x1e1e1e1e, 0x1d1d1d1d, 0x3d3d3d3d, 0x1b1b1b1b, 0x5b5b5b5b, 0x67676767, 0x7e7e7e7e,
0x17171717, 0x6b6b6b6b, 0x57575757, 0x7d7d7d7d, 0x37373737, 0x7b7b7b7b, 0x77777777, 0x7f7f7f7f,
0x0f0f0f0f, 0x1f1f1f1f, 0x1f1f1f1f, 0x3f3f3f3f, 0x1f1f1f1f, 0x5f5f5f5f, 0x6f6f6f6f, 0x7f7f7f7f,
0x1f1f1f1f, 0x6f6f6f6f, 0x5f5f5f5f, 0x7f7f7f7f, 0x3f3f3f3f, 0x7f7f7f7f, 0x7f7f7f7f, 0xffffffff
};
static char s_Phases3[256][9] =
{
/* 0 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 },
/* 1 */ { 1, 0 },
/* 2 */ { 1, 1 },
/* 3 */ { 2, 0, 1 },
/* 4 */ { 1, 2 },
/* 5 */ { 2, 0, 2 },
/* 6 */ { 2, 0, 3 },
/* 7 */ { 1, 0 },
/* 8 */ { 1, 3 },
/* 9 */ { 2, 1, 2 },
/* 10 */ { 2, 1, 3 },
/* 11 */ { 1, 1 },
/* 12 */ { 2, 2, 3 },
/* 13 */ { 1, 2 },
/* 14 */ { 1, 3 },
/* 15 */ { 4, 0, 1, 2, 3 },
/* 16 */ { 1, 4 },
/* 17 */ { 2, 0, 4 },
/* 18 */ { 2, 0, 5 },
/* 19 */ { 1, 0 },
/* 20 */ { 2, 0, 6 },
/* 21 */ { 1, 0 },
/* 22 */ { 1, 0 },
/* 23 */ { 1, 0 },
/* 24 */ { 2, 0, 7 },
/* 25 */ { 1, 0 },
/* 26 */ { 1, 0 },
/* 27 */ { 1, 0 },
/* 28 */ { 1, 0 },
/* 29 */ { 1, 0 },
/* 30 */ { 1, 0 },
/* 31 */ { 1, 0 },
/* 32 */ { 1, 5 },
/* 33 */ { 2, 1, 4 },
/* 34 */ { 2, 1, 5 },
/* 35 */ { 1, 1 },
/* 36 */ { 2, 1, 6 },
/* 37 */ { 1, 1 },
/* 38 */ { 1, 1 },
/* 39 */ { 1, 1 },
/* 40 */ { 2, 1, 7 },
/* 41 */ { 1, 1 },
/* 42 */ { 1, 1 },
/* 43 */ { 1, 1 },
/* 44 */ { 1, 1 },
/* 45 */ { 1, 1 },
/* 46 */ { 1, 1 },
/* 47 */ { 1, 1 },
/* 48 */ { 2, 4, 5 },
/* 49 */ { 1, 4 },
/* 50 */ { 1, 5 },
/* 51 */ { 4, 0, 1, 4, 5 },
/* 52 */ { 1, 6 },
/* 53 */ { 1, 0 },
/* 54 */ { 1, 0 },
/* 55 */ { 1, 0 },
/* 56 */ { 1, 7 },
/* 57 */ { 1, 1 },
/* 58 */ { 1, 1 },
/* 59 */ { 1, 1 },
/* 60 */ { 4, 0, 1, 6, 7 },
/* 61 */ { 1, 0 },
/* 62 */ { 1, 1 },
/* 63 */ { 2, 0, 1 },
/* 64 */ { 1, 6 },
/* 65 */ { 2, 2, 4 },
/* 66 */ { 2, 2, 5 },
/* 67 */ { 1, 2 },
/* 68 */ { 2, 2, 6 },
/* 69 */ { 1, 2 },
/* 70 */ { 1, 2 },
/* 71 */ { 1, 2 },
/* 72 */ { 2, 2, 7 },
/* 73 */ { 1, 2 },
/* 74 */ { 1, 2 },
/* 75 */ { 1, 2 },
/* 76 */ { 1, 2 },
/* 77 */ { 1, 2 },
/* 78 */ { 1, 2 },
/* 79 */ { 1, 2 },
/* 80 */ { 2, 4, 6 },
/* 81 */ { 1, 4 },
/* 82 */ { 1, 5 },
/* 83 */ { 1, 4 },
/* 84 */ { 1, 6 },
/* 85 */ { 4, 0, 2, 4, 6 },
/* 86 */ { 1, 0 },
/* 87 */ { 1, 0 },
/* 88 */ { 1, 7 },
/* 89 */ { 1, 2 },
/* 90 */ { 4, 0, 2, 5, 7 },
/* 91 */ { 1, 0 },
/* 92 */ { 1, 6 },
/* 93 */ { 1, 2 },
/* 94 */ { 1, 2 },
/* 95 */ { 2, 0, 2 },
/* 96 */ { 2, 4, 7 },
/* 97 */ { 1, 4 },
/* 98 */ { 1, 5 },
/* 99 */ { 1, 4 },
/* 100 */ { 1, 6 },
/* 101 */ { 1, 4 },
/* 102 */ { 4, 0, 3, 4, 7 },
/* 103 */ { 1, 0 },
/* 104 */ { 1, 7 },
/* 105 */ { 4, 0, 3, 5, 6 },
/* 106 */ { 1, 7 },
/* 107 */ { 1, 0 },
/* 108 */ { 1, 7 },
/* 109 */ { 1, 3 },
/* 110 */ { 1, 3 },
/* 111 */ { 2, 0, 3 },
/* 112 */ { 1, 4 },
/* 113 */ { 1, 4 },
/* 114 */ { 1, 5 },
/* 115 */ { 1, 4 },
/* 116 */ { 1, 6 },
/* 117 */ { 1, 4 },
/* 118 */ { 1, 4 },
/* 119 */ { 2, 0, 4 },
/* 120 */ { 1, 7 },
/* 121 */ { 1, 5 },
/* 122 */ { 1, 5 },
/* 123 */ { 2, 0, 5 },
/* 124 */ { 1, 6 },
/* 125 */ { 2, 0, 6 },
/* 126 */ { 2, 0, 7 },
/* 127 */ { 1, 0 },
/* 128 */ { 1, 7 },
/* 129 */ { 2, 3, 4 },
/* 130 */ { 2, 3, 5 },
/* 131 */ { 1, 3 },
/* 132 */ { 2, 3, 6 },
/* 133 */ { 1, 3 },
/* 134 */ { 1, 3 },
/* 135 */ { 1, 3 },
/* 136 */ { 2, 3, 7 },
/* 137 */ { 1, 3 },
/* 138 */ { 1, 3 },
/* 139 */ { 1, 3 },
/* 140 */ { 1, 3 },
/* 141 */ { 1, 3 },
/* 142 */ { 1, 3 },
/* 143 */ { 1, 3 },
/* 144 */ { 2, 5, 6 },
/* 145 */ { 1, 4 },
/* 146 */ { 1, 5 },
/* 147 */ { 1, 5 },
/* 148 */ { 1, 6 },
/* 149 */ { 1, 6 },
/* 150 */ { 4, 1, 2, 4, 7 },
/* 151 */ { 1, 1 },
/* 152 */ { 1, 7 },
/* 153 */ { 4, 1, 2, 5, 6 },
/* 154 */ { 1, 5 },
/* 155 */ { 1, 1 },
/* 156 */ { 1, 6 },
/* 157 */ { 1, 2 },
/* 158 */ { 1, 2 },
/* 159 */ { 2, 1, 2 },
/* 160 */ { 2, 5, 7 },
/* 161 */ { 1, 4 },
/* 162 */ { 1, 5 },
/* 163 */ { 1, 5 },
/* 164 */ { 1, 6 },
/* 165 */ { 4, 1, 3, 4, 6 },
/* 166 */ { 1, 3 },
/* 167 */ { 1, 1 },
/* 168 */ { 1, 7 },
/* 169 */ { 1, 1 },
/* 170 */ { 4, 1, 3, 5, 7 },
/* 171 */ { 1, 1 },
/* 172 */ { 1, 7 },
/* 173 */ { 1, 3 },
/* 174 */ { 1, 3 },
/* 175 */ { 2, 1, 3 },
/* 176 */ { 1, 5 },
/* 177 */ { 1, 4 },
/* 178 */ { 1, 5 },
/* 179 */ { 1, 5 },
/* 180 */ { 1, 6 },
/* 181 */ { 1, 4 },
/* 182 */ { 1, 4 },
/* 183 */ { 2, 1, 4 },
/* 184 */ { 1, 7 },
/* 185 */ { 1, 5 },
/* 186 */ { 1, 5 },
/* 187 */ { 2, 1, 5 },
/* 188 */ { 1, 7 },
/* 189 */ { 2, 1, 6 },
/* 190 */ { 2, 1, 7 },
/* 191 */ { 1, 1 },
/* 192 */ { 2, 6, 7 },
/* 193 */ { 1, 4 },
/* 194 */ { 1, 5 },
/* 195 */ { 4, 2, 3, 4, 5 },
/* 196 */ { 1, 6 },
/* 197 */ { 1, 2 },
/* 198 */ { 1, 3 },
/* 199 */ { 1, 2 },
/* 200 */ { 1, 7 },
/* 201 */ { 1, 2 },
/* 202 */ { 1, 3 },
/* 203 */ { 1, 3 },
/* 204 */ { 4, 2, 3, 6, 7 },
/* 205 */ { 1, 2 },
/* 206 */ { 1, 3 },
/* 207 */ { 2, 2, 3 },
/* 208 */ { 1, 6 },
/* 209 */ { 1, 4 },
/* 210 */ { 1, 5 },
/* 211 */ { 1, 4 },
/* 212 */ { 1, 6 },
/* 213 */ { 1, 6 },
/* 214 */ { 1, 7 },
/* 215 */ { 2, 2, 4 },
/* 216 */ { 1, 7 },
/* 217 */ { 1, 6 },
/* 218 */ { 1, 7 },
/* 219 */ { 2, 2, 5 },
/* 220 */ { 1, 6 },
/* 221 */ { 2, 2, 6 },
/* 222 */ { 2, 2, 7 },
/* 223 */ { 1, 2 },
/* 224 */ { 1, 7 },
/* 225 */ { 1, 4 },
/* 226 */ { 1, 5 },
/* 227 */ { 1, 5 },
/* 228 */ { 1, 6 },
/* 229 */ { 1, 6 },
/* 230 */ { 1, 7 },
/* 231 */ { 2, 3, 4 },
/* 232 */ { 1, 7 },
/* 233 */ { 1, 6 },
/* 234 */ { 1, 7 },
/* 235 */ { 2, 3, 5 },
/* 236 */ { 1, 7 },
/* 237 */ { 2, 3, 6 },
/* 238 */ { 2, 3, 7 },
/* 239 */ { 1, 3 },
/* 240 */ { 4, 4, 5, 6, 7 },
/* 241 */ { 1, 4 },
/* 242 */ { 1, 5 },
/* 243 */ { 2, 4, 5 },
/* 244 */ { 1, 6 },
/* 245 */ { 2, 4, 6 },
/* 246 */ { 2, 4, 7 },
/* 247 */ { 1, 4 },
/* 248 */ { 1, 7 },
/* 249 */ { 2, 5, 6 },
/* 250 */ { 2, 5, 7 },
/* 251 */ { 1, 5 },
/* 252 */ { 2, 6, 7 },
/* 253 */ { 1, 6 },
/* 254 */ { 1, 7 },
/* 255 */ { 8, 0, 1, 2, 3, 4, 5, 6, 7 }
};
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/misc/extra/extraUtilMisc.c
......@@ -429,8 +429,6 @@ unsigned Extra_TruthPolarize( unsigned uTruth, int Polarity, int nVars )
uCof1 >>= Shift;
uTruth = uCof0 | uCof1;
}
if ( nVars < 5 )
uTruth &= ((~0) >> (32-nMints));
return uTruth;
}
......@@ -752,6 +750,74 @@ void Extra_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** p
SeeAlso []
***********************************************************************/
void Extra_Truth3VarN( unsigned ** puCanons, char *** puPhases, char ** ppCounters )
{
int nPhasesMax = 8;
unsigned * uCanons;
unsigned uTruth, uPhase, uTruth32;
char ** uPhases, * pCounters;
int nFuncs, nClasses, i;
nFuncs = (1 << 8);
uCanons = ALLOC( unsigned, nFuncs );
memset( uCanons, 0, sizeof(unsigned) * nFuncs );
pCounters = ALLOC( char, nFuncs );
memset( pCounters, 0, sizeof(char) * nFuncs );
uPhases = (char **)Extra_ArrayAlloc( nFuncs, nPhasesMax, sizeof(char) );
nClasses = 0;
for ( uTruth = 0; uTruth < (unsigned)nFuncs; uTruth++ )
{
// skip already assigned
uTruth32 = ((uTruth << 24) | (uTruth << 16) | (uTruth << 8) | uTruth);
if ( uCanons[uTruth] )
{
assert( uTruth32 > uCanons[uTruth] );
continue;
}
nClasses++;
for ( i = 0; i < 8; i++ )
{
uPhase = Extra_TruthPolarize( uTruth, i, 3 );
if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
{
uCanons[uPhase] = uTruth32;
uPhases[uPhase][0] = i;
pCounters[uPhase] = 1;
}
else
{
assert( uCanons[uPhase] == uTruth32 );
if ( pCounters[uPhase] < nPhasesMax )
uPhases[uPhase][ pCounters[uPhase]++ ] = i;
}
}
}
if ( puCanons )
*puCanons = uCanons;
else
free( uCanons );
if ( puPhases )
*puPhases = uPhases;
else
free( uPhases );
if ( ppCounters )
*ppCounters = pCounters;
else
free( pCounters );
printf( "The number of 3N-classes = %d.\n", nClasses );
}
/**Function*************************************************************
Synopsis [Computes NPN canonical forms for 4-variable functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** ppCounters, int nPhasesMax )
{
unsigned short * uCanons;
......@@ -778,7 +844,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
for ( i = 0; i < 16; i++ )
{
uPhase = Extra_TruthPolarize( uTruth, i, 4 );
if ( uCanons[uPhase] == 0 )
if ( uCanons[uPhase] == 0 && (uTruth || i==0) )
{
uCanons[uPhase] = uTruth;
uPhases[uPhase][0] = i;
......@@ -804,6 +870,7 @@ void Extra_Truth4VarN( unsigned short ** puCanons, char *** puPhases, char ** pp
*ppCounters = pCounters;
else
free( pCounters );
printf( "The number of 4N-classes = %d.\n", nClasses );
}
/**Function*************************************************************
......@@ -1005,6 +1072,208 @@ unsigned Extra_TruthPerm5One( unsigned uTruth, int Phase )
/**Function*************************************************************
Synopsis [Computes a phase of the 3-var function.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Extra_TruthPerm6One( unsigned * uTruth, int Phase, unsigned * uTruthRes )
{
// cases
static unsigned Cases[64] = {
0, // 000000 - skip
0, // 000001 - skip
0xCCCCCCCC, // 000010 - single var
0, // 000011 - skip
0xF0F0F0F0, // 000100 - single var
1, // 000101
1, // 000110
0, // 000111 - skip
0xFF00FF00, // 001000 - single var
1, // 001001
1, // 001010
1, // 001011
1, // 001100
1, // 001101
1, // 001110
0, // 001111 - skip
0xFFFF0000, // 010000 - skip
1, // 010001
1, // 010010
1, // 010011
1, // 010100
1, // 010101
1, // 010110
1, // 010111 - four var
1, // 011000
1, // 011001
1, // 011010
1, // 011011 - four var
1, // 011100
1, // 011101 - four var
1, // 011110 - four var
0, // 011111 - skip
0xFFFFFFFF, // 100000 - single var
1, // 100001
1, // 100010
1, // 100011
1, // 100100
1, // 100101
1, // 100110
1, // 100111
1, // 101000
1, // 101001
1, // 101010
1, // 101011
1, // 101100
1, // 101101
1, // 101110
1, // 101111
1, // 110000
1, // 110001
1, // 110010
1, // 110011
1, // 110100
1, // 110101
1, // 110110
1, // 110111
1, // 111000
1, // 111001
1, // 111010
1, // 111011
1, // 111100
1, // 111101
1, // 111110
0 // 111111 - skip
};
// permutations
static int Perms[64][6] = {
{ 0, 0, 0, 0, 0, 0 }, // 000000 - skip
{ 0, 0, 0, 0, 0, 0 }, // 000001 - skip
{ 0, 0, 0, 0, 0, 0 }, // 000010 - single var
{ 0, 0, 0, 0, 0, 0 }, // 000011 - skip
{ 0, 0, 0, 0, 0, 0 }, // 000100 - single var
{ 0, 2, 1, 3, 4, 5 }, // 000101
{ 2, 0, 1, 3, 4, 5 }, // 000110
{ 0, 0, 0, 0, 0, 0 }, // 000111 - skip
{ 0, 0, 0, 0, 0, 0 }, // 001000 - single var
{ 0, 2, 3, 1, 4, 5 }, // 001001
{ 2, 0, 3, 1, 4, 5 }, // 001010
{ 0, 1, 3, 2, 4, 5 }, // 001011
{ 2, 3, 0, 1, 4, 5 }, // 001100
{ 0, 3, 1, 2, 4, 5 }, // 001101
{ 3, 0, 1, 2, 4, 5 }, // 001110
{ 0, 0, 0, 0, 0, 0 }, // 001111 - skip
{ 0, 0, 0, 0, 0, 0 }, // 010000 - skip
{ 0, 4, 2, 3, 1, 5 }, // 010001
{ 4, 0, 2, 3, 1, 5 }, // 010010
{ 0, 1, 3, 4, 2, 5 }, // 010011
{ 2, 3, 0, 4, 1, 5 }, // 010100
{ 0, 3, 1, 4, 2, 5 }, // 010101
{ 3, 0, 1, 4, 2, 5 }, // 010110
{ 0, 1, 2, 4, 3, 5 }, // 010111 - four var
{ 2, 3, 4, 0, 1, 5 }, // 011000
{ 0, 3, 4, 1, 2, 5 }, // 011001
{ 3, 0, 4, 1, 2, 5 }, // 011010
{ 0, 1, 4, 2, 3, 5 }, // 011011 - four var
{ 3, 4, 0, 1, 2, 5 }, // 011100
{ 0, 4, 1, 2, 3, 5 }, // 011101 - four var
{ 4, 0, 1, 2, 3, 5 }, // 011110 - four var
{ 0, 0, 0, 0, 0, 0 }, // 011111 - skip
{ 0, 0, 0, 0, 0, 0 }, // 100000 - single var
{ 0, 2, 3, 4, 5, 1 }, // 100001
{ 2, 0, 3, 4, 5, 1 }, // 100010
{ 0, 1, 3, 4, 5, 2 }, // 100011
{ 2, 3, 0, 4, 5, 1 }, // 100100
{ 0, 3, 1, 4, 5, 2 }, // 100101
{ 3, 0, 1, 4, 5, 2 }, // 100110
{ 0, 1, 2, 4, 5, 3 }, // 100111
{ 2, 3, 4, 0, 5, 1 }, // 101000
{ 0, 3, 4, 1, 5, 2 }, // 101001
{ 3, 0, 4, 1, 5, 2 }, // 101010
{ 0, 1, 4, 2, 5, 3 }, // 101011
{ 3, 4, 0, 1, 5, 2 }, // 101100
{ 0, 4, 1, 2, 5, 3 }, // 101101
{ 4, 0, 1, 2, 5, 3 }, // 101110
{ 0, 1, 2, 3, 5, 4 }, // 101111
{ 2, 3, 4, 5, 0, 1 }, // 110000
{ 0, 3, 4, 5, 1, 2 }, // 110001
{ 3, 0, 4, 5, 1, 2 }, // 110010
{ 0, 1, 4, 5, 2, 3 }, // 110011
{ 3, 4, 0, 5, 1, 2 }, // 110100
{ 0, 4, 1, 5, 2, 3 }, // 110101
{ 4, 0, 1, 5, 2, 3 }, // 110110
{ 0, 1, 2, 5, 3, 4 }, // 110111
{ 3, 4, 5, 0, 1, 2 }, // 111000
{ 0, 4, 5, 1, 2, 3 }, // 111001
{ 4, 0, 5, 1, 2, 3 }, // 111010
{ 0, 1, 5, 2, 3, 4 }, // 111011
{ 4, 5, 0, 1, 2, 3 }, // 111100
{ 0, 5, 1, 2, 3, 4 }, // 111101
{ 5, 0, 1, 2, 3, 4 }, // 111110
{ 0, 0, 0, 0, 0, 0 } // 111111 - skip
};
int i, k, iRes;
assert( Phase >= 0 && Phase < 64 );
if ( Cases[Phase] == 0 )
{
uTruthRes[0] = uTruth[0];
uTruthRes[1] = uTruth[1];
return;
}
if ( Cases[Phase] > 1 )
{
if ( Phase == 32 )
{
uTruthRes[0] = 0x00000000;
uTruthRes[1] = 0xFFFFFFFF;
}
else
{
uTruthRes[0] = Cases[Phase];
uTruthRes[1] = Cases[Phase];
}
return;
}
uTruthRes[0] = 0;
uTruthRes[1] = 0;
for ( i = 0; i < 64; i++ )
{
if ( i < 32 )
{
if ( uTruth[0] & (1 << i) )
{
for ( iRes = 0, k = 0; k < 6; k++ )
if ( i & (1 << Perms[Phase][k]) )
iRes |= (1 << k);
if ( iRes < 32 )
uTruthRes[0] |= (1 << iRes);
else
uTruthRes[1] |= (1 << (iRes-32));
}
}
else
{
if ( uTruth[1] & (1 << (i-32)) )
{
for ( iRes = 0, k = 0; k < 6; k++ )
if ( i & (1 << Perms[Phase][k]) )
iRes |= (1 << k);
if ( iRes < 32 )
uTruthRes[0] |= (1 << iRes);
else
uTruthRes[1] |= (1 << (iRes-32));
}
}
}
}
/**Function*************************************************************
Synopsis [Allocated lookup table for truth table permutation.]
Description []
......@@ -1085,6 +1354,33 @@ unsigned ** Extra_TruthPerm54()
/**Function*************************************************************
Synopsis [Allocated lookup table for truth table permutation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
unsigned ** Extra_TruthPerm63()
{
unsigned ** pTable;
unsigned uTruth[2];
int i, k;
pTable = (unsigned **)Extra_ArrayAlloc( 256, 64, 8 );
for ( i = 0; i < 256; i++ )
{
uTruth[0] = (i << 24) | (i << 16) | (i << 8) | i;
uTruth[1] = uTruth[0];
for ( k = 0; k < 64; k++ )
Extra_TruthPerm6One( uTruth, k, &pTable[i][k] );
}
return pTable;
}
/**Function*************************************************************
Synopsis [Returns the smallest prime larger than the number.]
Description []
......
src/misc/extra/module.make
SRC += src/misc/extra/extraUtilBdd.c \
src/misc/extra/extraUtilBitMatrix.c \
src/misc/extra/extraUtilCanon.c \
src/misc/extra/extraUtilFile.c \
src/misc/extra/extraUtilMemory.c \
src/misc/extra/extraUtilMisc.c \
......
src/misc/vec/vecInt.h
......@@ -50,6 +50,8 @@ struct Vec_Int_t_
#define Vec_IntForEachEntry( vVec, Entry, i ) \
for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
#define Vec_IntForEachEntryStart( vVec, Entry, i, Start ) \
for ( i = Start; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
......
src/opt/cut/cut.h 0 → 100644
/**CFile****************************************************************
FileName [cut.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: .h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CUT_H__
#define __CUT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Cut_ManStruct_t_ Cut_Man_t;
typedef struct Cut_CutStruct_t_ Cut_Cut_t;
typedef struct Cut_ParamsStruct_t_ Cut_Params_t;
struct Cut_ParamsStruct_t_
{
int nVarsMax; // the max cut size ("k" of the k-feasible cuts)
int nKeepMax; // the max number of cuts kept at a node
int nIdsMax; // the max number of IDs of cut objects
int fTruth; // compute truth tables
int fHash; // hash cuts to detect unique
int fFilter; // filter dominated cuts
int fSeq; // compute sequential cuts
int fDrop; // drop cuts on the fly
int fVerbose; // the verbosiness flag
};
struct Cut_CutStruct_t_
{
unsigned uTruth : 16; // truth table for 4-input cuts
unsigned uPhase : 7; // the phase when mapping into a canonical form
unsigned fSimul : 1; // the value of cut's output at 000.. pattern
unsigned fCompl : 1; // the cut is complemented
unsigned fSeq : 1; // the cut is sequential
unsigned nVarsMax : 3; // the max number of vars [4-6]
unsigned nLeaves : 3; // the number of leaves [4-6]
Cut_Cut_t * pNext; // the next cut in the list
void * pData; // the user data
int pLeaves[0]; // the array of leaves
};
static inline unsigned * Cut_CutReadTruth( Cut_Cut_t * p ) { if ( p->nVarsMax == 4 ) return (unsigned *)p; return (unsigned *)(p->pLeaves + p->nVarsMax + p->fSeq); }
static inline unsigned Cut_CutReadPhase( Cut_Cut_t * p ) { return p->uPhase; }
static inline int Cut_CutReadLeaveNum( Cut_Cut_t * p ) { return p->nLeaves; }
static inline int * Cut_CutReadLeaves( Cut_Cut_t * p ) { return p->pLeaves; }
static inline void * Cut_CutReadData( Cut_Cut_t * p ) { return p->pData; }
static inline void * Cut_CutWriteData( Cut_Cut_t * p, void * pData ) { p->pData = pData; }
static inline void Cut_CutWriteTruth( Cut_Cut_t * p, unsigned * puTruth ) {
if ( p->nVarsMax == 4 ) { p->uTruth = *puTruth; return; }
p->pLeaves[p->nVarsMax + p->fSeq] = (int)puTruth[0];
if ( p->nVarsMax == 6 ) p->pLeaves[p->nVarsMax + p->fSeq + 1] = (int)puTruth[1];
}
////////////////////////////////////////////////////////////////////////
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cutMan.c ==========================================================*/
extern Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams );
extern void Cut_ManStop( Cut_Man_t * p );
extern void Cut_ManPrintStats( Cut_Man_t * p );
extern void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts );
/*=== cutNode.c ==========================================================*/
extern void Cut_NodeSetTriv( Cut_Man_t * p, int Node );
extern Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 );
extern Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes );
extern Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node );
extern void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList );
extern void Cut_NodeFreeCuts( Cut_Man_t * p, int Node );
extern void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node );
extern void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
src/opt/cut/cutInt.h 0 → 100644
/**CFile****************************************************************
FileName [cutInt.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CUT_INT_H__
#define __CUT_INT_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include <stdio.h>
#include "extra.h"
#include "vec.h"
#include "cut.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Cut_HashTableStruct_t_ Cut_HashTable_t;
struct Cut_ManStruct_t_
{
// user preferences
Cut_Params_t * pParams; // computation parameters
Vec_Int_t * vFanCounts; // the array of fanout counters
// storage for cuts
Vec_Ptr_t * vCuts; // cuts by ID
Vec_Ptr_t * vCutsNew; // cuts by ID
Cut_HashTable_t * tTable; // cuts by their leaves (and root)
// memory management
Extra_MmFixed_t * pMmCuts;
int EntrySize;
// temporary variables
Cut_Cut_t * pReady;
Vec_Ptr_t * vTemp;
int fCompl0;
int fCompl1;
int fSimul;
// precomputations
unsigned uTruthVars[6][2];
unsigned short ** pPerms43;
unsigned ** pPerms53;
unsigned ** pPerms54;
// statistics
int nCutsCur;
int nCutsAlloc;
int nCutsDealloc;
int nCutsPeak;
int nCutsTriv;
int nCutsNode;
// runtime
int timeMerge;
int timeUnion;
int timeTruth;
int timeFilter;
int timeHash;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== cutMerge.c ==========================================================*/
extern Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
/*=== cutNode.c ==========================================================*/
extern Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p );
/*=== cutTable.c ==========================================================*/
extern Cut_HashTable_t * Cut_TableStart( int Size );
extern void Cut_TableStop( Cut_HashTable_t * pTable );
extern int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore );
extern void Cut_TableClear( Cut_HashTable_t * pTable );
extern int Cut_TableReadTime( Cut_HashTable_t * pTable );
/*=== cutTruth.c ==========================================================*/
extern void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
src/opt/cut/cutList.h 0 → 100644
/**CFile****************************************************************
FileName [cutList.h]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Implementation of layered listed list of cuts.]
Synopsis [External declarations.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutList.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef __CUT_LIST_H__
#define __CUT_LIST_H__
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
typedef struct Cut_ListStruct_t_ Cut_List_t;
struct Cut_ListStruct_t_
{
Cut_Cut_t * pHead[7];
Cut_Cut_t ** ppTail[7];
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cut_ListStart( Cut_List_t * p )
{
int i;
for ( i = 1; i <= 6; i++ )
{
p->pHead[i] = 0;
p->ppTail[i] = &p->pHead[i];
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Cut_ListAdd( Cut_List_t * p, Cut_Cut_t * pCut )
{
assert( pCut->nLeaves > 0 && pCut->nLeaves < 7 );
*p->ppTail[pCut->nLeaves] = pCut;
p->ppTail[pCut->nLeaves] = &pCut->pNext;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
{
int i;
for ( i = 1; i < 6; i++ )
*p->ppTail[i] = p->pHead[i+1];
*p->ppTail[6] = NULL;
return p->pHead[1];
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
#endif
src/opt/cut/cutMan.c 0 → 100644
/**CFile****************************************************************
FileName [cutMan.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Cut manager.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the cut manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Man_t * Cut_ManStart( Cut_Params_t * pParams )
{
Cut_Man_t * p;
int clk = clock();
assert( pParams->nVarsMax >= 4 && pParams->nVarsMax <= 6 );
p = ALLOC( Cut_Man_t, 1 );
memset( p, 0, sizeof(Cut_Man_t) );
// set and correct parameters
p->pParams = pParams;
if ( p->pParams->fSeq )
p->pParams->fHash = 1;
// space for cuts
p->vCuts = Vec_PtrAlloc( pParams->nIdsMax );
Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
if ( pParams->fSeq )
{
p->vCutsNew = Vec_PtrAlloc( pParams->nIdsMax );
Vec_PtrFill( p->vCuts, pParams->nIdsMax, NULL );
}
// hash tables
if ( pParams->fHash )
p->tTable = Cut_TableStart( p->pParams->nKeepMax );
// entry size
p->EntrySize = sizeof(Cut_Cut_t) + (pParams->nVarsMax + pParams->fSeq) * sizeof(int);
if ( pParams->nVarsMax == 5 )
p->EntrySize += sizeof(unsigned);
else if ( pParams->nVarsMax == 6 )
p->EntrySize += 2 * sizeof(unsigned);
// memory for cuts
p->pMmCuts = Extra_MmFixedStart( p->EntrySize );
// precomputations
// if ( pParams->fTruth && pParams->nVarsMax == 4 )
// p->pPerms43 = Extra_TruthPerm43();
// else if ( pParams->fTruth )
// {
// p->pPerms53 = Extra_TruthPerm53();
// p->pPerms54 = Extra_TruthPerm54();
// }
p->uTruthVars[0][1] = p->uTruthVars[0][0] = 0xAAAAAAAA; // 1010 1010 1010 1010 1010 1010 1010 1010
p->uTruthVars[1][1] = p->uTruthVars[1][0] = 0xCCCCCCCC; // 1010 1010 1010 1010 1010 1010 1010 1010
p->uTruthVars[2][1] = p->uTruthVars[2][0] = 0xF0F0F0F0; // 1111 0000 1111 0000 1111 0000 1111 0000
p->uTruthVars[3][1] = p->uTruthVars[3][0] = 0xFF00FF00; // 1111 1111 0000 0000 1111 1111 0000 0000
p->uTruthVars[4][1] = p->uTruthVars[4][0] = 0xFFFF0000; // 1111 1111 1111 1111 0000 0000 0000 0000
p->uTruthVars[5][0] = 0x00000000;
p->uTruthVars[5][1] = 0xFFFFFFFF;
p->vTemp = Vec_PtrAlloc( 100 );
return p;
}
/**Function*************************************************************
Synopsis [Stops the cut manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_ManStop( Cut_Man_t * p )
{
Cut_Cut_t * pCut;
int i;
Vec_PtrForEachEntry( p->vCuts, pCut, i )
{
if ( pCut != NULL )
{
int k = 0;
}
}
if ( p->vCutsNew ) Vec_PtrFree( p->vCutsNew );
if ( p->vCuts ) Vec_PtrFree( p->vCuts );
if ( p->vFanCounts ) Vec_IntFree( p->vFanCounts );
if ( p->pPerms43 ) free( p->pPerms43 );
if ( p->pPerms53 ) free( p->pPerms53 );
if ( p->pPerms54 ) free( p->pPerms54 );
if ( p->vTemp ) Vec_PtrFree( p->vTemp );
if ( p->tTable ) Cut_TableStop( p->tTable );
Extra_MmFixedStop( p->pMmCuts, 0 );
free( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_ManPrintStats( Cut_Man_t * p )
{
printf( "Cut computation statistics:\n" );
printf( "Current cuts = %8d. (Trivial = %d.)\n", p->nCutsCur-p->nCutsTriv, p->nCutsTriv );
printf( "Peak cuts = %8d.\n", p->nCutsPeak );
printf( "Total allocated = %8d.\n", p->nCutsAlloc );
printf( "Total deallocated = %8d.\n", p->nCutsDealloc );
printf( "The cut size = %3d bytes.\n", p->EntrySize );
printf( "Peak memory = %.2f Mb.\n", (float)p->nCutsPeak * p->EntrySize / (1<<20) );
PRT( "Merge ", p->timeMerge );
PRT( "Union ", p->timeUnion );
PRT( "Hash ", Cut_TableReadTime(p->tTable) );
PRT( "Filter", p->timeFilter );
PRT( "Truth ", p->timeTruth );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_ManSetFanoutCounts( Cut_Man_t * p, Vec_Int_t * vFanCounts )
{
p->vFanCounts = vFanCounts;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/cutMerge.c 0 → 100644
/**CFile****************************************************************
FileName [cutMerge.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Procedure to merge two cuts.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutMerge.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description [This procedure works.]
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutMergeTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
Cut_Cut_t * pRes;
int * pRow;
int nLeaves0, nLeaves1, Limit;
int i, k, Count, nNodes;
assert( pCut0->nLeaves >= pCut1->nLeaves );
// the case of the largest cut sizes
Limit = p->pParams->nVarsMax;
nLeaves0 = pCut0->nLeaves;
nLeaves1 = pCut1->nLeaves;
if ( nLeaves0 == Limit && nLeaves1 == Limit )
{
for ( i = 0; i < nLeaves0; i++ )
if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
return NULL;
pRes = Cut_CutAlloc( p );
for ( i = 0; i < nLeaves0; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = nLeaves0;
return pRes;
}
// the case when one of the cuts is the largest
if ( nLeaves0 == Limit )
{
for ( i = 0; i < nLeaves1; i++ )
{
for ( k = nLeaves0 - 1; k >= 0; k-- )
if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
break;
if ( k == -1 ) // did not find
return NULL;
}
pRes = Cut_CutAlloc( p );
for ( i = 0; i < nLeaves0; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = nLeaves0;
return pRes;
}
// other cases
nNodes = nLeaves0;
for ( i = 0; i < nLeaves1; i++ )
{
for ( k = nLeaves0 - 1; k >= 0; k-- )
{
if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
continue;
if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
{
pRow = M[k+1];
if ( pRow[0] == 0 )
pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
else if ( pRow[1] == 0 )
pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
else if ( pRow[2] == 0 )
pRow[2] = pCut1->pLeaves[i];
else
assert( 0 );
if ( ++nNodes > Limit )
{
for ( i = 0; i <= nLeaves0; i++ )
M[i][0] = 0;
return NULL;
}
}
break;
}
if ( k == -1 )
{
pRow = M[0];
if ( pRow[0] == 0 )
pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
else if ( pRow[1] == 0 )
pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
else if ( pRow[2] == 0 )
pRow[2] = pCut1->pLeaves[i];
else
assert( 0 );
if ( ++nNodes > Limit )
{
for ( i = 0; i <= nLeaves0; i++ )
M[i][0] = 0;
return NULL;
}
continue;
}
}
pRes = Cut_CutAlloc( p );
for ( Count = 0, i = 0; i <= nLeaves0; i++ )
{
if ( i > 0 )
pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
pRow = M[i];
if ( pRow[0] )
{
pRes->pLeaves[Count++] = pRow[0];
if ( pRow[1] )
{
pRes->pLeaves[Count++] = pRow[1];
if ( pRow[2] )
pRes->pLeaves[Count++] = pRow[2];
}
pRow[0] = 0;
}
}
assert( Count == nNodes );
pRes->nLeaves = nNodes;
return pRes;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutMergeTwo2( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
Cut_Cut_t * pRes;
int * pLeaves;
int Limit, nLeaves0, nLeaves1;
int i, k, c;
assert( pCut0->nLeaves >= pCut1->nLeaves );
// consider two cuts
nLeaves0 = pCut0->nLeaves;
nLeaves1 = pCut1->nLeaves;
// the case of the largest cut sizes
Limit = p->pParams->nVarsMax;
if ( nLeaves0 == Limit && nLeaves1 == Limit )
{
for ( i = 0; i < nLeaves0; i++ )
if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
return NULL;
pRes = Cut_CutAlloc( p );
for ( i = 0; i < nLeaves0; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = pCut0->nLeaves;
return pRes;
}
// the case when one of the cuts is the largest
if ( nLeaves0 == Limit )
{
for ( i = 0; i < nLeaves1; i++ )
{
for ( k = nLeaves0 - 1; k >= 0; k-- )
if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
break;
if ( k == -1 ) // did not find
return NULL;
}
pRes = Cut_CutAlloc( p );
for ( i = 0; i < nLeaves0; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = pCut0->nLeaves;
return pRes;
}
// prepare the cut
if ( p->pReady == NULL )
p->pReady = Cut_CutAlloc( p );
pLeaves = p->pReady->pLeaves;
// compare two cuts with different numbers
i = k = 0;
for ( c = 0; c < Limit; c++ )
{
if ( k == nLeaves1 )
{
if ( i == nLeaves0 )
{
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
pLeaves[c] = pCut0->pLeaves[i++];
continue;
}
if ( i == nLeaves0 )
{
if ( k == nLeaves1 )
{
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
pLeaves[c] = pCut1->pLeaves[k++];
continue;
}
if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
{
pLeaves[c] = pCut0->pLeaves[i++];
continue;
}
if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
{
pLeaves[c] = pCut1->pLeaves[k++];
continue;
}
pLeaves[c] = pCut0->pLeaves[i++];
k++;
}
if ( i < nLeaves0 || k < nLeaves1 )
return NULL;
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutMergeTwo3( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
Cut_Cut_t * pRes;
int * pLeaves;
int Limit, nLeaves0, nLeaves1;
int i, k, c;
assert( pCut0->nLeaves >= pCut1->nLeaves );
// prepare the cut
if ( p->pReady == NULL )
p->pReady = Cut_CutAlloc( p );
pLeaves = p->pReady->pLeaves;
// consider two cuts
Limit = p->pParams->nVarsMax;
nLeaves0 = pCut0->nLeaves;
nLeaves1 = pCut1->nLeaves;
if ( nLeaves0 == Limit )
{ // the case when one of the cuts is the largest
if ( nLeaves1 == Limit )
{ // the case when both cuts are the largest
for ( i = 0; i < nLeaves0; i++ )
{
pLeaves[i] = pCut0->pLeaves[i];
if ( pLeaves[i] != pCut1->pLeaves[i] )
return NULL;
}
}
else
{
for ( i = k = 0; i < nLeaves0; i++ )
{
pLeaves[i] = pCut0->pLeaves[i];
if ( k == (int)nLeaves1 )
continue;
if ( pLeaves[i] < pCut1->pLeaves[k] )
continue;
if ( pLeaves[i] == pCut1->pLeaves[k++] )
continue;
return NULL;
}
if ( k < nLeaves1 )
return NULL;
}
p->pReady->nLeaves = nLeaves0;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
// compare two cuts with different numbers
i = k = 0;
for ( c = 0; c < Limit; c++ )
{
if ( k == nLeaves1 )
{
if ( i == nLeaves0 )
{
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
pLeaves[c] = pCut0->pLeaves[i++];
continue;
}
if ( i == nLeaves0 )
{
if ( k == nLeaves1 )
{
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
pLeaves[c] = pCut1->pLeaves[k++];
continue;
}
if ( pCut0->pLeaves[i] < pCut1->pLeaves[k] )
{
pLeaves[c] = pCut0->pLeaves[i++];
continue;
}
if ( pCut0->pLeaves[i] > pCut1->pLeaves[k] )
{
pLeaves[c] = pCut1->pLeaves[k++];
continue;
}
pLeaves[c] = pCut0->pLeaves[i++];
k++;
}
if ( i < nLeaves0 || k < nLeaves1 )
return NULL;
p->pReady->nLeaves = c;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutMergeTwo4( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
Cut_Cut_t * pRes;
int * pLeaves;
int i, k, min, NodeTemp, Limit, nTotal;
assert( pCut0->nLeaves >= pCut1->nLeaves );
// prepare the cut
if ( p->pReady == NULL )
p->pReady = Cut_CutAlloc( p );
pLeaves = p->pReady->pLeaves;
// consider two cuts
Limit = p->pParams->nVarsMax;
if ( pCut0->nLeaves == (unsigned)Limit )
{ // the case when one of the cuts is the largest
if ( pCut1->nLeaves == (unsigned)Limit )
{ // the case when both cuts are the largest
for ( i = 0; i < (int)pCut0->nLeaves; i++ )
{
pLeaves[i] = pCut0->pLeaves[i];
if ( pLeaves[i] != pCut1->pLeaves[i] )
return NULL;
}
}
else
{
for ( i = k = 0; i < (int)pCut0->nLeaves; i++ )
{
pLeaves[i] = pCut0->pLeaves[i];
if ( k == (int)pCut1->nLeaves )
continue;
if ( pLeaves[i] < pCut1->pLeaves[k] )
continue;
if ( pLeaves[i] == pCut1->pLeaves[k++] )
continue;
return NULL;
}
if ( k < (int)pCut1->nLeaves )
return NULL;
}
p->pReady->nLeaves = pCut0->nLeaves;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
// count the number of unique entries in pCut1
nTotal = pCut0->nLeaves;
for ( i = 0; i < (int)pCut1->nLeaves; i++ )
{
// try to find this entry among the leaves of pCut0
for ( k = 0; k < (int)pCut0->nLeaves; k++ )
if ( pCut1->pLeaves[i] == pCut0->pLeaves[k] )
break;
if ( k < (int)pCut0->nLeaves ) // found
continue;
// we found a new entry to add
if ( nTotal == Limit )
return NULL;
pLeaves[nTotal++] = pCut1->pLeaves[i];
}
// we know that the feasible cut exists
// add the starting entries
for ( k = 0; k < (int)pCut0->nLeaves; k++ )
pLeaves[k] = pCut0->pLeaves[k];
// selection-sort the entries
for ( i = 0; i < nTotal - 1; i++ )
{
min = i;
for ( k = i+1; k < nTotal; k++ )
if ( pLeaves[k] < pLeaves[min] )
min = k;
NodeTemp = pLeaves[i];
pLeaves[i] = pLeaves[min];
pLeaves[min] = NodeTemp;
}
p->pReady->nLeaves = nTotal;
pRes = p->pReady; p->pReady = NULL;
return pRes;
}
/**Function*************************************************************
Synopsis [Merges two cuts.]
Description [This procedure works.]
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutMergeTwo5( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
static int M[7][3] = {{0},{0},{0},{0},{0},{0},{0}};
Cut_Cut_t * pRes;
int * pRow;
unsigned uSign0, uSign1;
int i, k, nNodes, Count;
unsigned Limit = p->pParams->nVarsMax;
assert( pCut0->nLeaves >= pCut1->nLeaves );
// the case of the largest cut sizes
if ( pCut0->nLeaves == Limit && pCut1->nLeaves == Limit )
{
for ( i = 0; i < (int)pCut0->nLeaves; i++ )
if ( pCut0->pLeaves[i] != pCut1->pLeaves[i] )
return NULL;
pRes = Cut_CutAlloc( p );
for ( i = 0; i < (int)pCut0->nLeaves; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = pCut0->nLeaves;
return pRes;
}
// the case when one of the cuts is the largest
if ( pCut0->nLeaves == Limit )
{
if ( !p->pParams->fTruth )
{
for ( i = 0; i < (int)pCut1->nLeaves; i++ )
{
for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
break;
if ( k == -1 ) // did not find
return NULL;
}
pRes = Cut_CutAlloc( p );
}
else
{
uSign1 = 0;
for ( i = 0; i < (int)pCut1->nLeaves; i++ )
{
for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
if ( pCut0->pLeaves[k] == pCut1->pLeaves[i] )
{
uSign1 |= (1 << i);
break;
}
if ( k == -1 ) // did not find
return NULL;
}
pRes = Cut_CutAlloc( p );
pRes->uTruth = (uSign1 << 8);
}
for ( i = 0; i < (int)pCut0->nLeaves; i++ )
pRes->pLeaves[i] = pCut0->pLeaves[i];
pRes->nLeaves = pCut0->nLeaves;
return pRes;
}
// other cases
nNodes = pCut0->nLeaves;
for ( i = 0; i < (int)pCut1->nLeaves; i++ )
{
for ( k = pCut0->nLeaves - 1; k >= 0; k-- )
{
if ( pCut0->pLeaves[k] > pCut1->pLeaves[i] )
continue;
if ( pCut0->pLeaves[k] < pCut1->pLeaves[i] )
{
pRow = M[k+1];
if ( pRow[0] == 0 )
pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
else if ( pRow[1] == 0 )
pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
else if ( pRow[2] == 0 )
pRow[2] = pCut1->pLeaves[i];
else
assert( 0 );
if ( ++nNodes > (int)Limit )
{
for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
M[i][0] = 0;
return NULL;
}
}
break;
}
if ( k == -1 )
{
pRow = M[0];
if ( pRow[0] == 0 )
pRow[0] = pCut1->pLeaves[i], pRow[1] = 0;
else if ( pRow[1] == 0 )
pRow[1] = pCut1->pLeaves[i], pRow[2] = 0;
else if ( pRow[2] == 0 )
pRow[2] = pCut1->pLeaves[i];
else
assert( 0 );
if ( ++nNodes > (int)Limit )
{
for ( i = 0; i <= (int)pCut0->nLeaves; i++ )
M[i][0] = 0;
return NULL;
}
continue;
}
}
pRes = Cut_CutAlloc( p );
if ( !p->pParams->fTruth )
{
for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
{
if ( i > 0 )
pRes->pLeaves[Count++] = pCut0->pLeaves[i-1];
pRow = M[i];
if ( pRow[0] )
{
pRes->pLeaves[Count++] = pRow[0];
if ( pRow[1] )
{
pRes->pLeaves[Count++] = pRow[1];
if ( pRow[2] )
pRes->pLeaves[Count++] = pRow[2];
}
pRow[0] = 0;
}
}
assert( Count == nNodes );
pRes->nLeaves = nNodes;
/*
// make sure that the cut is correct
{
for ( i = 1; i < (int)pRes->nLeaves; i++ )
if ( pRes->pLeaves[i-1] >= pRes->pLeaves[i] )
{
int v = 0;
}
}
*/
return pRes;
}
uSign0 = uSign1 = 0;
for ( Count = 0, i = 0; i <= (int)pCut0->nLeaves; i++ )
{
if ( i > 0 )
{
uSign0 |= (1 << Count);
pRes->pLeaves[Count++] = pCut1->pLeaves[i-1];
}
pRow = M[i];
if ( pRow[0] )
{
uSign1 |= (1 << Count);
pRes->pLeaves[Count++] = pRow[0];
if ( pRow[1] )
{
uSign1 |= (1 << Count);
pRes->pLeaves[Count++] = pRow[1];
if ( pRow[2] )
{
uSign1 |= (1 << Count);
pRes->pLeaves[Count++] = pRow[2];
}
}
pRow[0] = 0;
}
}
assert( Count == nNodes );
pRes->nLeaves = nNodes;
pRes->uTruth = (uSign1 << 8) | uSign0;
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/cutNode.c 0 → 100644
/**CFile****************************************************************
FileName [cutNode.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Procedures to compute cuts for a node.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutNode.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
#include "cutList.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node );
static inline void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut );
static inline int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList );
static void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
static void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList );
// iterator through all the cuts of the list
#define Cut_ListForEachCut( pList, pCut ) \
for ( pCut = pList; \
pCut; \
pCut = pCut->pNext )
#define Cut_ListForEachCutStop( pList, pCut, pStop ) \
for ( pCut = pList; \
pCut != pStop; \
pCut = pCut->pNext )
#define Cut_ListForEachCutSafe( pList, pCut, pCut2 ) \
for ( pCut = pList, \
pCut2 = pCut? pCut->pNext: NULL; \
pCut; \
pCut = pCut2, \
pCut2 = pCut? pCut->pNext: NULL )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Returns the pointer to the linked list of cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_NodeReadCuts( Cut_Man_t * p, int Node )
{
return Vec_PtrEntry( p->vCuts, Node );
}
/**Function*************************************************************
Synopsis [Returns the pointer to the linked list of cuts.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_NodeWriteCuts( Cut_Man_t * p, int Node, Cut_Cut_t * pList )
{
Vec_PtrWriteEntry( p->vCuts, Node, pList );
}
/**Function*************************************************************
Synopsis [Sets the trivial cut for the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_NodeSetTriv( Cut_Man_t * p, int Node )
{
assert( Cut_NodeReadCuts(p, Node) == NULL );
Cut_NodeWriteCuts( p, Node, Cut_CutCreateTriv(p, Node) );
}
/**Function*************************************************************
Synopsis [Deallocates the cuts at the node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_NodeFreeCuts( Cut_Man_t * p, int Node )
{
Cut_Cut_t * pList, * pCut, * pCut2;
pList = Cut_NodeReadCuts( p, Node );
if ( pList == NULL )
return;
Cut_ListForEachCutSafe( pList, pCut, pCut2 )
Cut_CutRecycle( p, pCut );
Cut_NodeWriteCuts( p, Node, NULL );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_NodeSetComputedAsNew( Cut_Man_t * p, int Node )
{
}
/**Function*************************************************************
Synopsis [Computes the cuts by merging cuts at two nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1 )
{
Cut_List_t SuperList;
Cut_Cut_t * pList0, * pList1, * pStop0, * pStop1, * pTemp0, * pTemp1;
int i, Limit = p->pParams->nVarsMax;
int clk = clock();
assert( p->pParams->nVarsMax <= 6 );
// start the new list
Cut_ListStart( &SuperList );
// get the cut lists of children
pList0 = Cut_NodeReadCuts( p, Node0 );
pList1 = Cut_NodeReadCuts( p, Node1 );
assert( pList0 && pList1 );
// get the simultation bit of the node
p->fSimul = (fCompl0 ^ pList0->fSimul) & (fCompl1 ^ pList1->fSimul);
// set temporary variables
p->fCompl0 = fCompl0;
p->fCompl1 = fCompl1;
// find the point in the list where the max-var cuts begin
Cut_ListForEachCut( pList0, pStop0 )
if ( pStop0->nLeaves == (unsigned)Limit )
break;
Cut_ListForEachCut( pList1, pStop1 )
if ( pStop1->nLeaves == (unsigned)Limit )
break;
// start with the elementary cut
pTemp0 = Cut_CutCreateTriv( p, Node );
Cut_ListAdd( &SuperList, pTemp0 );
p->nCutsNode = 1;
// small by small
Cut_ListForEachCutStop( pList0, pTemp0, pStop0 )
Cut_ListForEachCutStop( pList1, pTemp1, pStop1 )
if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
goto finish;
// all by large
Cut_ListForEachCut( pList0, pTemp0 )
Cut_ListForEachCut( pStop1, pTemp1 )
if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
goto finish;
// all by large
Cut_ListForEachCut( pList1, pTemp1 )
Cut_ListForEachCut( pStop0, pTemp0 )
if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
goto finish;
// large by large
Cut_ListForEachCut( pStop0, pTemp0 )
Cut_ListForEachCut( pStop1, pTemp1 )
{
assert( pTemp0->nLeaves == (unsigned)Limit && pTemp1->nLeaves == (unsigned)Limit );
for ( i = 0; i < Limit; i++ )
if ( pTemp0->pLeaves[i] != pTemp1->pLeaves[i] )
break;
if ( i < Limit )
continue;
if ( Cut_CutProcessTwo( p, Node, pTemp0, pTemp1, &SuperList ) )
goto finish;
}
finish :
// set the list at the node
assert( Cut_NodeReadCuts(p, Node) == NULL );
pList0 = Cut_ListFinish( &SuperList );
Cut_NodeWriteCuts( p, Node, pList0 );
// clear the hash table
if ( p->pParams->fHash && !p->pParams->fSeq )
Cut_TableClear( p->tTable );
// consider dropping the fanins cuts
if ( p->pParams->fDrop )
{
Cut_NodeTryDroppingCuts( p, Node0 );
Cut_NodeTryDroppingCuts( p, Node1 );
}
p->timeMerge += clock() - clk;
// filter the cuts
clk = clock();
if ( p->pParams->fFilter )
Cut_CutFilter( p, pList0 );
p->timeFilter += clock() - clk;
return pList0;
}
/**Function*************************************************************
Synopsis [Processes two cuts.]
Description [Returns 1 if the limit has been reached.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cut_CutProcessTwo( Cut_Man_t * p, int Root, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, Cut_List_t * pSuperList )
{
Cut_Cut_t * pCut;
// merge the cuts
if ( pCut0->nLeaves >= pCut1->nLeaves )
pCut = Cut_CutMergeTwo( p, pCut0, pCut1 );
else
pCut = Cut_CutMergeTwo( p, pCut1, pCut0 );
if ( pCut == NULL )
return 0;
assert( pCut->nLeaves > 1 );
// add the root if sequential
if ( p->pParams->fSeq )
pCut->pLeaves[pCut->nLeaves] = Root;
// check the lookup table
if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
{
Cut_CutRecycle( p, pCut );
return 0;
}
// compute the truth table
if ( p->pParams->fTruth )
Cut_TruthCompute( p, pCut, pCut0, pCut1 );
// add to the list
Cut_ListAdd( pSuperList, pCut );
// return status (0 if okay; 1 if exceeded the limit)
return ++p->nCutsNode == p->pParams->nKeepMax;
}
/**Function*************************************************************
Synopsis [Computes the cuts by unioning cuts at a choice node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
{
Cut_List_t SuperList;
Cut_Cut_t * pList, * pListStart, * pCut, * pCut2, * pTop;
int i, k, Node, Root, Limit = p->pParams->nVarsMax;
int clk = clock();
assert( p->pParams->nVarsMax <= 6 );
// start the new list
Cut_ListStart( &SuperList );
// remember the root node to save the resulting cuts
Root = Vec_IntEntry( vNodes, 0 );
p->nCutsNode = 1;
// collect small cuts first
Vec_PtrClear( p->vTemp );
Vec_IntForEachEntry( vNodes, Node, i )
{
// get the cuts of this node
pList = Cut_NodeReadCuts( p, Node );
Cut_NodeWriteCuts( p, Node, NULL );
assert( pList );
// remember the starting point
pListStart = pList->pNext;
// save or recycle the elementary cut
if ( i == 0 )
Cut_ListAdd( &SuperList, pList ), pTop = pList;
else
Cut_CutRecycle( p, pList );
// save all the cuts that are smaller than the limit
Cut_ListForEachCutSafe( pListStart, pCut, pCut2 )
{
if ( pCut->nLeaves == (unsigned)Limit )
{
Vec_PtrPush( p->vTemp, pCut );
break;
}
// check hash tables
if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
{
Cut_CutRecycle( p, pCut );
continue;
}
// set the complemented bit by comparing the first cut with the current cut
pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
// add to the list
Cut_ListAdd( &SuperList, pCut );
if ( ++p->nCutsNode == p->pParams->nKeepMax )
{
// recycle the rest of the cuts of this node
Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
Cut_CutRecycle( p, pCut );
// recycle all cuts of other nodes
Vec_IntForEachEntryStart( vNodes, Node, k, i+1 )
Cut_NodeFreeCuts( p, Node );
// recycle the saved cuts of other nodes
Vec_PtrForEachEntry( p->vTemp, pList, k )
Cut_ListForEachCutSafe( pList, pCut, pCut2 )
Cut_CutRecycle( p, pCut );
goto finish;
}
}
}
// collect larger cuts next
Vec_PtrForEachEntry( p->vTemp, pList, i )
{
Cut_ListForEachCutSafe( pList, pCut, pCut2 )
{
if ( p->pParams->fHash && Cut_TableLookup( p->tTable, pCut, !p->pParams->fSeq ) )
{
Cut_CutRecycle( p, pCut );
continue;
}
// set the complemented bit
pCut->fCompl = pTop->fSimul ^ pCut->fSimul;
// add to the list
Cut_ListAdd( &SuperList, pCut );
if ( ++p->nCutsNode == p->pParams->nKeepMax )
{
// recycle the rest of the cuts
Cut_ListForEachCutSafe( pCut->pNext, pCut, pCut2 )
Cut_CutRecycle( p, pCut );
// recycle the saved cuts of other nodes
Vec_PtrForEachEntryStart( p->vTemp, pList, k, i+1 )
Cut_ListForEachCutSafe( pList, pCut, pCut2 )
Cut_CutRecycle( p, pCut );
goto finish;
}
}
}
finish :
// set the cuts at the node
assert( Cut_NodeReadCuts(p, Root) == NULL );
pList = Cut_ListFinish( &SuperList );
Cut_NodeWriteCuts( p, Root, pList );
// clear the hash table
if ( p->pParams->fHash && !p->pParams->fSeq )
Cut_TableClear( p->tTable );
p->timeUnion += clock() - clk;
// filter the cuts
clk = clock();
if ( p->pParams->fFilter )
Cut_CutFilter( p, pList );
p->timeFilter += clock() - clk;
return pList;
}
/**Function*************************************************************
Synopsis [Start the cut computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutAlloc( Cut_Man_t * p )
{
Cut_Cut_t * pCut;
// cut allocation
pCut = (Cut_Cut_t *)Extra_MmFixedEntryFetch( p->pMmCuts );
memset( pCut, 0, sizeof(Cut_Cut_t) );
pCut->nVarsMax = p->pParams->nVarsMax;
pCut->fSeq = p->pParams->fSeq;
pCut->fSimul = p->fSimul;
// statistics
p->nCutsAlloc++;
p->nCutsCur++;
if ( p->nCutsPeak < p->nCutsAlloc - p->nCutsDealloc )
p->nCutsPeak = p->nCutsAlloc - p->nCutsDealloc;
return pCut;
}
/**Function*************************************************************
Synopsis [Start the cut computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_Cut_t * Cut_CutCreateTriv( Cut_Man_t * p, int Node )
{
Cut_Cut_t * pCut;
pCut = Cut_CutAlloc( p );
pCut->nLeaves = 1;
pCut->pLeaves[0] = Node;
if ( p->pParams->fTruth )
Cut_CutWriteTruth( pCut, p->uTruthVars[0] );
p->nCutsTriv++;
return pCut;
}
/**Function*************************************************************
Synopsis [Start the cut computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_CutRecycle( Cut_Man_t * p, Cut_Cut_t * pCut )
{
p->nCutsDealloc++;
p->nCutsCur--;
if ( pCut->nLeaves == 1 )
p->nCutsTriv--;
Extra_MmFixedEntryRecycle( p->pMmCuts, (char *)pCut );
}
/**Function*************************************************************
Synopsis [Consider dropping cuts if they are useless by now.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_NodeTryDroppingCuts( Cut_Man_t * p, int Node )
{
int nFanouts;
assert( p->vFanCounts );
nFanouts = Vec_IntEntry( p->vFanCounts, Node );
assert( nFanouts > 0 );
if ( --nFanouts == 0 )
Cut_NodeFreeCuts( p, Node );
Vec_IntWriteEntry( p->vFanCounts, Node, nFanouts );
}
/**Function*************************************************************
Synopsis [Print the cut.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_CutPrint( Cut_Cut_t * pCut )
{
int i;
assert( pCut->nLeaves > 1 );
printf( "%d : {", pCut->nLeaves );
for ( i = 0; i < (int)pCut->nLeaves; i++ )
printf( " %d", pCut->pLeaves[i] );
printf( " }" );
}
/**Function*************************************************************
Synopsis [Consider dropping cuts if they are useless by now.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_CutPrintMerge( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
printf( "\n" );
printf( "%d : %5d %5d %5d %5d %5d\n",
pCut0->nLeaves,
pCut0->nLeaves > 0 ? pCut0->pLeaves[0] : -1,
pCut0->nLeaves > 1 ? pCut0->pLeaves[1] : -1,
pCut0->nLeaves > 2 ? pCut0->pLeaves[2] : -1,
pCut0->nLeaves > 3 ? pCut0->pLeaves[3] : -1,
pCut0->nLeaves > 4 ? pCut0->pLeaves[4] : -1
);
printf( "%d : %5d %5d %5d %5d %5d\n",
pCut1->nLeaves,
pCut1->nLeaves > 0 ? pCut1->pLeaves[0] : -1,
pCut1->nLeaves > 1 ? pCut1->pLeaves[1] : -1,
pCut1->nLeaves > 2 ? pCut1->pLeaves[2] : -1,
pCut1->nLeaves > 3 ? pCut1->pLeaves[3] : -1,
pCut1->nLeaves > 4 ? pCut1->pLeaves[4] : -1
);
if ( pCut == NULL )
printf( "Cannot merge\n" );
else
printf( "%d : %5d %5d %5d %5d %5d\n",
pCut->nLeaves,
pCut->nLeaves > 0 ? pCut->pLeaves[0] : -1,
pCut->nLeaves > 1 ? pCut->pLeaves[1] : -1,
pCut->nLeaves > 2 ? pCut->pLeaves[2] : -1,
pCut->nLeaves > 3 ? pCut->pLeaves[3] : -1,
pCut->nLeaves > 4 ? pCut->pLeaves[4] : -1
);
}
/**Function*************************************************************
Synopsis [Filter the cuts using dominance.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_CutFilter( Cut_Man_t * p, Cut_Cut_t * pList )
{
Cut_Cut_t * pListR, ** ppListR = &pListR;
Cut_Cut_t * pCut, * pCut2, * pDom, * pPrev;
int i, k;
// save the first cut
*ppListR = pList, ppListR = &pList->pNext;
// try to filter out other cuts
pPrev = pList;
Cut_ListForEachCutSafe( pList->pNext, pCut, pCut2 )
{
assert( pCut->nLeaves > 1 );
// go through all the previous cuts up to pCut
Cut_ListForEachCutStop( pList->pNext, pDom, pCut )
{
if ( pDom->nLeaves >= pCut->nLeaves )
continue;
// check if every node in pDom is contained in pCut
for ( i = 0; i < (int)pDom->nLeaves; i++ )
{
for ( k = 0; k < (int)pCut->nLeaves; k++ )
if ( pDom->pLeaves[i] == pCut->pLeaves[k] )
break;
if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut
break;
}
if ( i == (int)pDom->nLeaves ) // every node in pDom is contained in pCut
break;
}
if ( pDom != pCut ) // pDom is contained in pCut - recycle pCut
{
// make sure cuts are connected after removing
pPrev->pNext = pCut->pNext;
/*
// report
printf( "Recycling cut: " );
Cut_CutPrint( pCut );
printf( "\n" );
printf( "As contained in: " );
Cut_CutPrint( pDom );
printf( "\n" );
*/
// recycle the cut
Cut_CutRecycle( p, pCut );
}
else // pDom is NOT contained in pCut - save pCut
{
*ppListR = pCut, ppListR = &pCut->pNext;
pPrev = pCut;
}
}
*ppListR = NULL;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/cutSeq.c 0 → 100644
/**CFile****************************************************************
FileName [cutSeq.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Sequential cut computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/cutTable.c 0 → 100644
/**CFile****************************************************************
FileName [cutTable.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Hashing cuts to prevent duplication.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutTable.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
struct Cut_HashTableStruct_t_
{
int nBins;
Cut_Cut_t ** pBins;
int nEntries;
int * pPlaces;
int nPlaces;
int timeLookup;
};
// iterator through all the cuts of the list
#define Cut_TableListForEachCut( pList, pCut ) \
for ( pCut = pList; \
pCut; \
pCut = pCut->pData )
#define Cut_TableListForEachCutSafe( pList, pCut, pCut2 ) \
for ( pCut = pList, \
pCut2 = pCut? pCut->pData: NULL; \
pCut; \
pCut = pCut2, \
pCut2 = pCut? pCut->pData: NULL )
// primes used to compute the hash key
static int s_HashPrimes[10] = { 109, 499, 557, 619, 631, 709, 797, 881, 907, 991 };
// hashing function
static inline unsigned Cut_HashKey( Cut_Cut_t * pCut )
{
unsigned i, uRes = pCut->nLeaves * s_HashPrimes[9];
for ( i = 0; i < pCut->nLeaves + pCut->fSeq; i++ )
uRes += s_HashPrimes[i] * pCut->pLeaves[i];
return uRes;
}
// hashing function
static inline int Cut_CompareTwo( Cut_Cut_t * pCut1, Cut_Cut_t * pCut2 )
{
unsigned i;
if ( pCut1->nLeaves != pCut2->nLeaves )
return 1;
for ( i = 0; i < pCut1->nLeaves; i++ )
if ( pCut1->pLeaves[i] != pCut2->pLeaves[i] )
return 1;
return 0;
}
static void Cut_TableResize( Cut_HashTable_t * pTable );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Starts the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Cut_HashTable_t * Cut_TableStart( int Size )
{
Cut_HashTable_t * pTable;
pTable = ALLOC( Cut_HashTable_t, 1 );
memset( pTable, 0, sizeof(Cut_HashTable_t) );
// allocate the table
pTable->nBins = Cudd_PrimeCopy( Size );
pTable->pBins = ALLOC( Cut_Cut_t *, pTable->nBins );
memset( pTable->pBins, 0, sizeof(Cut_Cut_t *) * pTable->nBins );
pTable->pPlaces = ALLOC( int, pTable->nBins );
return pTable;
}
/**Function*************************************************************
Synopsis [Stops the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TableStop( Cut_HashTable_t * pTable )
{
FREE( pTable->pPlaces );
free( pTable->pBins );
free( pTable );
}
/**Function*************************************************************
Synopsis [Check the existence of a cut in the lookup table]
Description [Returns 1 if the entry is found.]
SideEffects []
SeeAlso []
***********************************************************************/
int Cut_TableLookup( Cut_HashTable_t * pTable, Cut_Cut_t * pCut, int fStore )
{
Cut_Cut_t * pEnt;
unsigned Key;
int clk = clock();
Key = Cut_HashKey(pCut) % pTable->nBins;
Cut_TableListForEachCut( pTable->pBins[Key], pEnt )
{
if ( !Cut_CompareTwo( pEnt, pCut ) )
{
pTable->timeLookup += clock() - clk;
return 1;
}
}
if ( pTable->nEntries > 2 * pTable->nBins )
{
Cut_TableResize( pTable );
Key = Cut_HashKey(pCut) % pTable->nBins;
}
// remember the place
if ( fStore && pTable->pBins[Key] == NULL )
pTable->pPlaces[ pTable->nPlaces++ ] = Key;
// add the cut to the table
pCut->pData = pTable->pBins[Key];
pTable->pBins[Key] = pCut;
pTable->nEntries++;
pTable->timeLookup += clock() - clk;
return 0;
}
/**Function*************************************************************
Synopsis [Stops the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TableClear( Cut_HashTable_t * pTable )
{
int i;
assert( pTable->nPlaces <= pTable->nBins );
for ( i = 0; i < pTable->nPlaces; i++ )
{
assert( pTable->pBins[ pTable->pPlaces[i] ] );
pTable->pBins[ pTable->pPlaces[i] ] = NULL;
}
pTable->nPlaces = 0;
pTable->nEntries = 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TableResize( Cut_HashTable_t * pTable )
{
Cut_Cut_t ** pBinsNew;
Cut_Cut_t * pEnt, * pEnt2;
int nBinsNew, Counter, i, clk;
unsigned Key;
clk = clock();
// get the new table size
nBinsNew = Cudd_PrimeCopy( 3 * pTable->nBins );
// allocate a new array
pBinsNew = ALLOC( Cut_Cut_t *, nBinsNew );
memset( pBinsNew, 0, sizeof(Cut_Cut_t *) * nBinsNew );
// rehash the entries from the old table
Counter = 0;
for ( i = 0; i < pTable->nBins; i++ )
Cut_TableListForEachCutSafe( pTable->pBins[i], pEnt, pEnt2 )
{
Key = Cut_HashKey(pEnt) % nBinsNew;
pEnt->pData = pBinsNew[Key];
pBinsNew[Key] = pEnt;
Counter++;
}
assert( Counter == pTable->nEntries );
// printf( "Increasing the structural table size from %6d to %6d. ", pMan->nBins, nBinsNew );
// PRT( "Time", clock() - clk );
// replace the table and the parameters
free( pTable->pBins );
pTable->pBins = pBinsNew;
pTable->nBins = nBinsNew;
}
/**Function*************************************************************
Synopsis [Stops the hash table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cut_TableReadTime( Cut_HashTable_t * pTable )
{
if ( pTable == NULL )
return 0;
return pTable->timeLookup;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/cutTruth.c 0 → 100644
/**CFile****************************************************************
FileName [cutTruth.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [K-feasible cut computation package.]
Synopsis [Incremental truth table computation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: cutTruth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "cutInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
static void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
static void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline unsigned Cut_TruthPhase( Cut_Cut_t * pCut, Cut_Cut_t * pCut1 )
{
unsigned uPhase = 0;
int i, k;
for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
{
if ( k == (int)pCut1->nLeaves )
break;
if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
continue;
assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
uPhase |= (1 << i);
k++;
}
return uPhase;
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthCompute( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
int clk = clock();
if ( pCut->nVarsMax == 4 )
Cut_TruthCompute4( p, pCut, pCut0, pCut1 );
else if ( pCut->nVarsMax == 5 )
Cut_TruthCompute5( p, pCut, pCut0, pCut1 );
else // if ( pCut->nVarsMax == 6 )
Cut_TruthCompute6( p, pCut, pCut0, pCut1 );
p->timeTruth += clock() - clk;
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthCompute4( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
unsigned * puTruthCut0, * puTruthCut1;
unsigned uTruth0, uTruth1, uPhase;
puTruthCut0 = Cut_CutReadTruth(pCut0);
puTruthCut1 = Cut_CutReadTruth(pCut1);
uPhase = Cut_TruthPhase( pCut, pCut0 );
uTruth0 = Extra_TruthPerm4One( *puTruthCut0, uPhase );
uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
uPhase = Cut_TruthPhase( pCut, pCut1 );
uTruth1 = Extra_TruthPerm4One( *puTruthCut1, uPhase );
uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
uTruth1 = uTruth0 & uTruth1;
if ( pCut->fCompl )
uTruth1 = ~uTruth1;
if ( pCut->nVarsMax == 4 )
uTruth1 &= 0xFFFF;
Cut_CutWriteTruth( pCut, &uTruth1 );
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthCompute5( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
unsigned * puTruthCut0, * puTruthCut1;
unsigned uTruth0, uTruth1, uPhase;
puTruthCut0 = Cut_CutReadTruth(pCut0);
puTruthCut1 = Cut_CutReadTruth(pCut1);
uPhase = Cut_TruthPhase( pCut, pCut0 );
uTruth0 = Extra_TruthPerm5One( *puTruthCut0, uPhase );
uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
uPhase = Cut_TruthPhase( pCut, pCut1 );
uTruth1 = Extra_TruthPerm5One( *puTruthCut1, uPhase );
uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
uTruth1 = uTruth0 & uTruth1;
if ( pCut->fCompl )
uTruth1 = ~uTruth1;
Cut_CutWriteTruth( pCut, &uTruth1 );
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthCompute6( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
unsigned * puTruthCut0, * puTruthCut1;
unsigned uTruth0[2], uTruth1[2], uPhase;
puTruthCut0 = Cut_CutReadTruth(pCut0);
puTruthCut1 = Cut_CutReadTruth(pCut1);
uPhase = Cut_TruthPhase( pCut, pCut0 );
Extra_TruthPerm6One( puTruthCut0, uPhase, uTruth0 );
uTruth0[0] = p->fCompl0? ~uTruth0[0]: uTruth0[0];
uTruth0[1] = p->fCompl0? ~uTruth0[1]: uTruth0[1];
uPhase = Cut_TruthPhase( pCut, pCut1 );
Extra_TruthPerm6One( puTruthCut1, uPhase, uTruth1 );
uTruth1[0] = p->fCompl1? ~uTruth1[0]: uTruth1[0];
uTruth1[1] = p->fCompl1? ~uTruth1[1]: uTruth1[1];
uTruth1[0] = uTruth0[0] & uTruth1[0];
uTruth1[1] = uTruth0[1] & uTruth1[1];
if ( pCut->fCompl )
{
uTruth1[0] = ~uTruth0[0];
uTruth1[1] = ~uTruth0[1];
}
Cut_CutWriteTruth( pCut, uTruth1 );
}
/**Function*************************************************************
Synopsis [Performs truth table computation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Cut_TruthComputeOld( Cut_Man_t * p, Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1 )
{
unsigned uTruth0, uTruth1, uPhase;
int clk = clock();
assert( pCut->nVarsMax < 6 );
// assign the truth table
if ( pCut0->nLeaves == pCut->nLeaves )
uTruth0 = *Cut_CutReadTruth(pCut0);
else
{
assert( pCut0->nLeaves < pCut->nLeaves );
uPhase = Cut_TruthPhase( pCut, pCut0 );
if ( pCut->nVarsMax == 4 )
{
assert( pCut0->nLeaves < 4 );
assert( uPhase < 16 );
uTruth0 = p->pPerms43[pCut0->uTruth & 0xFF][uPhase];
}
else
{
assert( pCut->nVarsMax == 5 );
assert( pCut0->nLeaves < 5 );
assert( uPhase < 32 );
if ( pCut0->nLeaves == 4 )
{
// Count4++;
/*
if ( uPhase == 31-16 ) // 01111
uTruth0 = pCut0->uTruth;
else if ( uPhase == 31-8 ) // 10111
uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][0];
else if ( uPhase == 31-4 ) // 11011
uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][1];
else if ( uPhase == 31-2 ) // 11101
uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][2];
else if ( uPhase == 31-1 ) // 11110
uTruth0 = p->pPerms54[pCut0->uTruth & 0xFFFF][3];
else
assert( 0 );
*/
uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
}
else
{
// Count5++;
// uTruth0 = p->pPerms53[pCut0->uTruth & 0xFF][uPhase];
uTruth0 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut0), uPhase );
}
}
}
uTruth0 = p->fCompl0? ~uTruth0: uTruth0;
// assign the truth table
if ( pCut1->nLeaves == pCut->nLeaves )
uTruth0 = *Cut_CutReadTruth(pCut1);
else
{
assert( pCut1->nLeaves < pCut->nLeaves );
uPhase = Cut_TruthPhase( pCut, pCut1 );
if ( pCut->nVarsMax == 4 )
{
assert( pCut1->nLeaves < 4 );
assert( uPhase < 16 );
uTruth1 = p->pPerms43[pCut1->uTruth & 0xFF][uPhase];
}
else
{
assert( pCut->nVarsMax == 5 );
assert( pCut1->nLeaves < 5 );
assert( uPhase < 32 );
if ( pCut1->nLeaves == 4 )
{
// Count4++;
/*
if ( uPhase == 31-16 ) // 01111
uTruth1 = pCut1->uTruth;
else if ( uPhase == 31-8 ) // 10111
uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][0];
else if ( uPhase == 31-4 ) // 11011
uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][1];
else if ( uPhase == 31-2 ) // 11101
uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][2];
else if ( uPhase == 31-1 ) // 11110
uTruth1 = p->pPerms54[pCut1->uTruth & 0xFFFF][3];
else
assert( 0 );
*/
uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
}
else
{
// Count5++;
// uTruth1 = p->pPerms53[pCut1->uTruth & 0xFF][uPhase];
uTruth1 = Extra_TruthPerm5One( *Cut_CutReadTruth(pCut1), uPhase );
}
}
}
uTruth1 = p->fCompl1? ~uTruth1: uTruth1;
uTruth1 = uTruth0 & uTruth1;
if ( pCut->fCompl )
uTruth1 = ~uTruth1;
if ( pCut->nVarsMax == 4 )
uTruth1 &= 0xFFFF;
Cut_CutWriteTruth( pCut, &uTruth1 );
p->timeTruth += clock() - clk;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
src/opt/cut/module.make 0 → 100644
SRC += src/opt/cut/cutMan.c \
src/opt/cut/cutMerge.c \
src/opt/cut/cutNode.c \
src/opt/cut/cutSeq.c \
src/opt/cut/cutTable.c \
src/opt/cut/cutTruth.c
src/opt/fxu/module.make
SRC += fxu.c \
fxuCreate.c \
fxuHeapD.c \
fxuHeapS.c \
fxuList.c \
fxuMatrix.c \
fxuPair.c \
fxuPrint.c \
fxuReduce.c \
fxuSelect.c \
fxuSingle.c \
fxuUpdate.c
SRC += src/opt/fxu/fxu.c \
src/opt/fxu/fxuCreate.c \
src/opt/fxu/fxuHeapD.c \
src/opt/fxu/fxuHeapS.c \
src/opt/fxu/fxuList.c \
src/opt/fxu/fxuMatrix.c \
src/opt/fxu/fxuPair.c \
src/opt/fxu/fxuPrint.c \
src/opt/fxu/fxuReduce.c \
src/opt/fxu/fxuSelect.c \
src/opt/fxu/fxuSingle.c \
src/opt/fxu/fxuUpdate.c
src/opt/rwr/module.make
SRC += rwrCut.c \
rwrEva.c \
rwrExp.c \
rwrLib.c \
rwrMan.c \
rwrUtil.c
SRC += src/opt/rwr/rwrCut.c \
src/opt/rwr/rwrEva.c \
src/opt/rwr/rwrExp.c \
src/opt/rwr/rwrLib.c \
src/opt/rwr/rwrMan.c \
src/opt/rwr/rwrPrint.c \
src/opt/rwr/rwrUtil.c
src/opt/rwr/rwrCut.c
......@@ -245,6 +245,8 @@ Rwr_Cut_t * Rwr_CutCreateTriv( Rwr_Man_t * p, Abc_Obj_t * pNode )
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/sat/sim/module.make
SRC += simMan.c \
simSat.c \
simSupp.c \
simSym.c \
simUnate.c \
simUtils.c
SRC += src/sat/sim/simMan.c \
src/sat/sim/simSat.c \
src/sat/sim/simSupp.c \
src/sat/sim/simSym.c \
src/sat/sim/simUnate.c \
src/sat/sim/simUtils.c
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