summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c665
-rw-r--r--src/base/abci/abcAttach.c2
-rw-r--r--src/base/abci/abcCut.c1
-rw-r--r--src/base/abci/abcDress.c209
-rw-r--r--src/base/abci/abcIvy.c74
-rw-r--r--src/base/abci/abcMiter.c6
-rw-r--r--src/base/abci/abcNtbdd.c2
-rw-r--r--src/base/abci/abcPga.c154
-rw-r--r--src/base/abci/abcPrint.c28
-rw-r--r--src/base/abci/abcProve.c9
-rw-r--r--src/base/abci/abcRewrite.c7
-rw-r--r--src/base/abci/abcStrash.c2
-rw-r--r--src/base/abci/abcUnreach.c14
-rw-r--r--src/base/abci/abcVerify.c1
-rw-r--r--src/base/abci/module.make1
15 files changed, 648 insertions, 527 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 278812ef..65f1a75f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -67,6 +67,7 @@ static int Abc_CommandResubstitute ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandRr ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandComb ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -88,9 +89,7 @@ static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -112,6 +111,7 @@ static int Abc_CommandFraigStore ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigClean ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraigSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigDress ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandUnmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -133,6 +133,8 @@ static int Abc_CommandSeqFpga ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSeqMap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -194,11 +196,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 );
- Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 );
+// Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 );
Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 );
+ Cmd_CommandAdd( pAbc, "Various", "comb", Abc_CommandComb, 1 );
Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 );
Cmd_CommandAdd( pAbc, "Various", "demiter", Abc_CommandDemiter, 1 );
Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 );
@@ -220,9 +223,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 );
Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 );
- Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
- Cmd_CommandAdd( pAbc, "Various", "xsim", Abc_CommandXsim, 0 );
- Cmd_CommandAdd( pAbc, "Various", "cycle", Abc_CommandCycle, 1 );
+// Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
@@ -244,6 +245,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_restore", Abc_CommandFraigRestore, 1 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_clean", Abc_CommandFraigClean, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig_sweep", Abc_CommandFraigSweep, 1 );
+ Cmd_CommandAdd( pAbc, "Fraiging", "dress", Abc_CommandFraigDress, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "map", Abc_CommandMap, 1 );
Cmd_CommandAdd( pAbc, "SC mapping", "unmap", Abc_CommandUnmap, 1 );
@@ -265,6 +267,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Cmd_CommandAdd( pAbc, "Sequential", "smap", Abc_CommandSeqMap, 1 );
// Cmd_CommandAdd( pAbc, "Sequential", "ssweep", Abc_CommandSeqSweep, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
+ Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 );
@@ -860,6 +864,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk;
int c;
+ int fStruct;
int fVerbose;
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
@@ -869,12 +874,16 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
+ fStruct = 1;
fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
{
switch ( c )
{
+ case 's':
+ fStruct ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -892,12 +901,15 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// print support information
- Abc_NtkPrintStrSupports( pNtk );
- return 0;
+ if ( fStruct )
+ {
+ Abc_NtkPrintStrSupports( pNtk );
+ return 0;
+ }
if ( !Abc_NtkIsComb(pNtk) )
{
- fprintf( pErr, "This command works only for combinational networks.\n" );
+ fprintf( pErr, "This command works only for combinational networks (run \"comb\").\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pNtk) )
@@ -911,8 +923,9 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: print_supp [-vh]\n" );
+ fprintf( pErr, "usage: print_supp [-svh]\n" );
fprintf( pErr, "\t prints the supports of the CO nodes\n" );
+ fprintf( pErr, "\t-s : toggle printing structural support only [default = %s].\n", fStruct? "yes": "no" );
fprintf( pErr, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -979,7 +992,7 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkIsComb(pNtk) )
{
- fprintf( pErr, "This command works only for combinational networks.\n" );
+ fprintf( pErr, "This command works only for combinational networks (run \"comb\").\n" );
return 1;
}
if ( Abc_NtkIsStrash(pNtk) )
@@ -1354,18 +1367,12 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Printing logic sharing does not work for sequential AIGs.\n" );
- return 1;
- }
-
Abc_NtkPrintSharing( pNtk );
return 0;
usage:
fprintf( pErr, "usage: print_sharing [-h]\n" );
- fprintf( pErr, "\t prints the number of shared nodes in the TFO cones of the COs\n" );
+ fprintf( pErr, "\t prints the number of shared nodes in the TFI cones of the COs\n" );
// fprintf( pErr, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
@@ -1859,12 +1866,6 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Balancing cannot be applied to a sequential AIG.\n" );
- return 1;
- }
-
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
{
@@ -1932,7 +1933,7 @@ int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv )
nThresh = 1;
nFaninMax = 20;
fCnf = 0;
- fMulti = 0;
+ fMulti = 1;
fSimple = 0;
fFactor = 0;
Extra_UtilGetoptReset();
@@ -2532,9 +2533,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
bool fPrecompute;
bool fUseZeros;
bool fVerbose;
+ bool fVeryVerbose;
// external functions
extern void Rwr_Precompute();
- extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -2545,8 +2546,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fPrecompute = 0;
fUseZeros = 0;
fVerbose = 0;
+ fVeryVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvwh" ) ) != EOF )
{
switch ( c )
{
@@ -2562,6 +2564,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'v':
fVerbose ^= 1;
break;
+ case 'w':
+ fVeryVerbose ^= 1;
+ break;
case 'h':
goto usage;
default:
@@ -2592,7 +2597,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// modify the current network
- if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose ) )
+ if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose ) )
{
fprintf( pErr, "Rewriting has failed.\n" );
return 1;
@@ -2600,11 +2605,12 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
- fprintf( pErr, "usage: rewrite [-lzvh]\n" );
+ fprintf( pErr, "usage: rewrite [-lzvwh]\n" );
fprintf( pErr, "\t performs technology-independent rewriting of the AIG\n" );
fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" );
fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-w : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
@@ -3127,6 +3133,65 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandComb( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk, * pNtkRes;
+ int c;
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsComb(pNtk) )
+ {
+ fprintf( pErr, "The network is already combinational.\n" );
+ return 0;
+ }
+
+ // get the new network
+ pNtkRes = Abc_NtkDup( pNtk );
+ Abc_NtkMakeComb( pNtkRes );
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: comb [-h]\n" );
+ fprintf( pErr, "\t makes the current network combinational by replacing latches by PI/PO pairs\n" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -3349,7 +3414,7 @@ usage:
***********************************************************************/
int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- FILE * pOut, * pErr, * pFile;
+ FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtk2;
char * FileName;
int fComb;
@@ -3386,25 +3451,11 @@ int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- // get the input file name
- FileName = argv[globalUtilOptind];
- if ( (pFile = fopen( FileName, "r" )) == NULL )
- {
- fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
- if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
- fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
- fprintf( pAbc->Err, "\n" );
- return 1;
- }
- fclose( pFile );
-
// read the second network
- pNtk2 = Io_Read( FileName, 1 );
+ FileName = argv[globalUtilOptind];
+ pNtk2 = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
if ( pNtk2 == NULL )
- {
- fprintf( pAbc->Err, "Reading network from file has failed.\n" );
return 1;
- }
// check if the second network is combinational
if ( Abc_NtkLatchNum(pNtk2) )
@@ -4430,7 +4481,7 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
fclose( pFile );
// set the new network
- pNtkNew = Io_Read( FileName, 1 );
+ pNtkNew = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
if ( pNtkNew == NULL )
{
fprintf( pAbc->Err, "Reading network from file has failed.\n" );
@@ -4697,11 +4748,13 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
+/*
if ( !Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Sequential cuts can be computed for sequential AIGs (run \"seq\").\n" );
return 1;
}
+*/
if ( pParams->nVarsMax < CUT_SIZE_MIN || pParams->nVarsMax > CUT_SIZE_MAX )
{
fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", CUT_SIZE_MIN, CUT_SIZE_MAX );
@@ -5025,168 +5078,6 @@ usage:
return 1;
}
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;
- int c;
- int nFrames;
- int fInputs;
- int fVerbose;
- extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
-
- pNtk = Abc_FrameReadNtk(pAbc);
- pOut = Abc_FrameReadOut(pAbc);
- pErr = Abc_FrameReadErr(pAbc);
-
- // set defaults
- nFrames = 10;
- fInputs = 0;
- fVerbose = 0;
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'F':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
- goto usage;
- }
- nFrames = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( nFrames < 0 )
- goto usage;
- break;
- case 'i':
- fInputs ^= 1;
- break;
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
- }
- }
- if ( pNtk == NULL )
- {
- fprintf( pErr, "Empty network.\n" );
- return 1;
- }
-
- if ( !Abc_NtkIsStrash(pNtk) )
- {
- fprintf( pErr, "Only works for strashed networks.\n" );
- return 1;
- }
-
- Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
- return 0;
-
-usage:
- fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
- fprintf( pErr, "\t performs X-valued simulation of the AIG\n" );
- fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
- fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
- fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : print the command usage\n");
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;
- int c;
- int nFrames;
- int fVerbose;
- extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
- extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
-
- pNtk = Abc_FrameReadNtk(pAbc);
- pOut = Abc_FrameReadOut(pAbc);
- pErr = Abc_FrameReadErr(pAbc);
-
- // set defaults
- nFrames = 100;
- fVerbose = 0;
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'F':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
- goto usage;
- }
- nFrames = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( nFrames < 0 )
- goto usage;
- break;
- case 'v':
- fVerbose ^= 1;
- break;
- case 'h':
- goto usage;
- default:
- goto usage;
- }
- }
- if ( pNtk == NULL )
- {
- fprintf( pErr, "Empty network.\n" );
- return 1;
- }
-
- if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) )
- {
- fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
- return 1;
- }
-
- if ( Abc_NtkIsStrash(pNtk) )
- Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
- else
- Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
- return 0;
-
-usage:
- fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
- fprintf( pErr, "\t cycles sequiential circuit for the given number of timeframes\n" );
- fprintf( pErr, "\t to derive a new initial state (which may be on the envelope)\n" );
- fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
- fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : print the command usage\n");
- return 1;
-}
/**Function*************************************************************
@@ -5433,11 +5324,6 @@ int Abc_CommandIStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtkTemp = Abc_NtkStrash( pNtk, 0, 1 );
@@ -5513,11 +5399,6 @@ int Abc_CommandICut( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
Abc_NtkIvyCuts( pNtk, nInputs );
return 0;
@@ -5581,11 +5462,6 @@ int Abc_CommandIRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
pNtkRes = Abc_NtkIvyRewrite( pNtk, fUpdateLevel, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@@ -5658,11 +5534,6 @@ int Abc_CommandIRewriteSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
pNtkRes = Abc_NtkIvyRewriteSeq( pNtk, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@@ -5731,11 +5602,6 @@ int Abc_CommandIResyn( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
pNtkRes = Abc_NtkIvyResyn( pNtk, fUpdateLevel, fVerbose );
if ( pNtkRes == NULL )
@@ -5817,11 +5683,6 @@ int Abc_CommandISat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
pNtkRes = Abc_NtkIvySat( pNtk, nConfLimit, fVerbose );
if ( pNtkRes == NULL )
@@ -5861,7 +5722,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int c, fProve, fVerbose, fDoSparse;
int nConfLimit;
- extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose );
+ extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -5908,13 +5769,8 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
- pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, fVerbose );
+ pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -5985,12 +5841,6 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
-
clk = clock();
@@ -6091,11 +5941,6 @@ int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
pNtkRes = Abc_NtkIvyHaig( pNtk, nIters, fUseZeroCost, fVerbose );
if ( pNtkRes == NULL )
@@ -6156,11 +6001,6 @@ int Abc_CommandMini( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
if ( !Abc_NtkIsStrash(pNtk) )
{
fprintf( pErr, "Only works for combinatinally strashed AIG networks.\n" );
@@ -6247,11 +6087,6 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Only works for non-sequential networks.\n" );
- return 1;
- }
if ( Abc_NtkIsStrash(pNtk) )
Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
else
@@ -6754,6 +6589,78 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandFraigDress( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ char * pFileName;
+ int c;
+ int fVerbose;
+ extern void Abc_NtkDress( Abc_Ntk_t * pNtk, char * pFileName, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+ if ( Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "This command works only for logic networks.\n" );
+ return 1;
+ }
+ if ( argc != globalUtilOptind && argc != globalUtilOptind + 1 )
+ goto usage;
+ if ( argc == globalUtilOptind && Abc_NtkSpec(pNtk) == NULL )
+ {
+ fprintf( pErr, "The current network has no spec.\n" );
+ return 1;
+ }
+ // get the input file name
+ pFileName = (argc == globalUtilOptind + 1) ? argv[globalUtilOptind] : Abc_NtkSpec(pNtk);
+ // modify the current network
+ Abc_NtkDress( pNtk, pFileName, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: dress [-vh] <file>\n" );
+ fprintf( pErr, "\t transfers internal node names from file to the current network\n" );
+ fprintf( pErr, "\t<file> : network with names (if not given, the current network spec is used)\n" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -6831,12 +6738,6 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Cannot map a sequential AIG.\n" );
- return 1;
- }
-
if ( !Abc_NtkIsStrash(pNtk) )
{
pNtk = Abc_NtkStrash( pNtk, 0, 0 );
@@ -7281,12 +7182,6 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
- return 1;
- }
-
// create the new LUT library
if ( nLutSize >= 3 && nLutSize <= 10 )
Fpga_SetSimpleLutLib( nLutSize );
@@ -7438,12 +7333,6 @@ int Abc_CommandFpgaFast( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Cannot FPGA map a sequential AIG.\n" );
- return 1;
- }
-
if ( !Abc_NtkIsStrash(pNtk) )
{
// strash and balance the network
@@ -7791,12 +7680,6 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
- return 1;
- }
-
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The current network is combinational.\n" );
@@ -7895,12 +7778,6 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Does not work for a sequentail AIG (run \"unseq\").\n" );
- return 1;
- }
-
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The current network is combinational.\n" );
@@ -7959,12 +7836,6 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "The current network is already a sequential AIG.\n" );
- return 1;
- }
-
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
fprintf( pErr, "The network has no latches.\n" );
@@ -8040,13 +7911,13 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
-
+/*
if ( !Abc_NtkIsSeq(pNtk) )
{
fprintf( pErr, "Conversion to combinational AIG works only for sequential AIG (run \"seq\").\n" );
return 1;
}
-
+*/
// share the latches on the fanout edges
// if ( fShare )
// Seq_NtkShareFanouts(pNtk);
@@ -8540,12 +8411,6 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( pErr, "Sequential sweep works only for combinational networks (run \"unseq\").\n" );
- return 1;
- }
-
if ( Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
@@ -8660,6 +8525,169 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int fVerbose;
+ extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+ extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 100;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) )
+ {
+ fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" );
+ return 1;
+ }
+
+ if ( Abc_NtkIsStrash(pNtk) )
+ Abc_NtkCycleInitState( pNtk, nFrames, fVerbose );
+ else
+ Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: cycle [-F num] [-vh]\n" );
+ fprintf( pErr, "\t cycles sequiential circuit for the given number of timeframes\n" );
+ fprintf( pErr, "\t to derive a new initial state (which may be on the envelope)\n" );
+ fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandXsim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int fInputs;
+ int fVerbose;
+ extern void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 10;
+ fInputs = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "Fivh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFrames = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nFrames < 0 )
+ goto usage;
+ break;
+ case 'i':
+ fInputs ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for strashed networks.\n" );
+ return 1;
+ }
+
+ Abc_NtkXValueSimulate( pNtk, nFrames, fInputs, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: xsim [-F num] [-ivh]\n" );
+ fprintf( pErr, "\t performs X-valued simulation of the AIG\n" );
+ fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-i : toggle X-valued state or X-valued inputs [default = %s]\n", fInputs? "inputs": "state" );
+ fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
@@ -9002,11 +9030,6 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
return 0;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
- return 0;
- }
clk = clock();
if ( Abc_NtkIsStrash(pNtk) )
@@ -9183,12 +9206,6 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( stdout, "Currently can only solve the miter with one output.\n" );
return 0;
}
- if ( Abc_NtkIsSeq(pNtk) )
- {
- fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
- return 0;
- }
-
clk = clock();
if ( Abc_NtkIsStrash(pNtk) )
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index bf40e45b..d5d2aa16 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -142,7 +142,7 @@ int Abc_NtkAttach( Abc_Ntk_t * pNtk )
Abc_NtkForEachNode( pNtk, pNode, i )
pNode->pData = pNode->pCopy, pNode->pCopy = NULL;
pNtk->ntkFunc = ABC_FUNC_MAP;
- Extra_MmFlexStop( pNtk->pManFunc, 0 );
+ Extra_MmFlexStop( pNtk->pManFunc );
pNtk->pManFunc = pGenlib;
printf( "Library gates are successfully attached to the nodes.\n" );
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index f1dd4ab5..d399ce5f 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -20,7 +20,6 @@
#include "abc.h"
#include "cut.h"
-//#include "seqInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
new file mode 100644
index 00000000..d7bb70fe
--- /dev/null
+++ b/src/base/abci/abcDress.c
@@ -0,0 +1,209 @@
+/**CFile****************************************************************
+
+ FileName [abcDress.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Transfers names from one netlist to the other.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcDress.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "io.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static stmm_table * Abc_NtkDressDeriveMapping( Abc_Ntk_t * pNtk );
+static void Abc_NtkDressTransferNames( Abc_Ntk_t * pNtk, stmm_table * tMapping, int fVerbose );
+
+extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Transfers names from one netlist to the other.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDress( Abc_Ntk_t * pNtkLogic, char * pFileName, int fVerbose )
+{
+ Abc_Ntk_t * pNtkOrig, * pNtkLogicOrig;
+ Abc_Ntk_t * pMiter, * pMiterFraig;
+ stmm_table * tMapping;
+
+ assert( Abc_NtkIsLogic(pNtkLogic) );
+
+ // get the original netlist
+ pNtkOrig = Io_ReadNetlist( pFileName, Io_ReadFileType(pFileName), 1 );
+ if ( pNtkOrig == NULL )
+ return;
+ assert( Abc_NtkIsNetlist(pNtkOrig) );
+
+ Abc_NtkCleanCopy(pNtkLogic);
+ Abc_NtkCleanCopy(pNtkOrig);
+
+ // convert it into the logic network
+ pNtkLogicOrig = Abc_NtkNetlistToLogic( pNtkOrig );
+ // check that the networks have the same PIs/POs/latches
+ if ( !Abc_NtkCompareSignals( pNtkLogic, pNtkLogicOrig, 1, 1 ) )
+ {
+ Abc_NtkDelete( pNtkOrig );
+ Abc_NtkDelete( pNtkLogicOrig );
+ return;
+ }
+
+ // convert the current logic network into an AIG
+ pMiter = Abc_NtkStrash( pNtkLogic, 1, 0 );
+
+ // convert it into the AIG and make the netlist point to the AIG
+ Abc_NtkAppend( pMiter, pNtkLogicOrig, 1 );
+ Abc_NtkTransferCopy( pNtkOrig );
+ Abc_NtkDelete( pNtkLogicOrig );
+
+if ( fVerbose )
+{
+printf( "After mitering:\n" );
+printf( "Logic: Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkLogic), Abc_NtkCountCopy(pNtkLogic) );
+printf( "Orig: Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkOrig), Abc_NtkCountCopy(pNtkOrig) );
+}
+
+ // fraig the miter (miter nodes point to the fraiged miter)
+ pMiterFraig = Abc_NtkIvyFraig( pMiter, 100, 1, 0, 1, 0 );
+ // make netlists point to the fraiged miter
+ Abc_NtkTransferCopy( pNtkLogic );
+ Abc_NtkTransferCopy( pNtkOrig );
+ Abc_NtkDelete( pMiter );
+
+if ( fVerbose )
+{
+printf( "After fraiging:\n" );
+printf( "Logic: Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkLogic), Abc_NtkCountCopy(pNtkLogic) );
+printf( "Orig: Nodes = %5d. Copy = %5d. \n", Abc_NtkNodeNum(pNtkOrig), Abc_NtkCountCopy(pNtkOrig) );
+}
+
+ // derive mapping from the fraiged nodes into their prototype nodes in the original netlist
+ tMapping = Abc_NtkDressDeriveMapping( pNtkOrig );
+
+ // transfer the names to the new netlist
+ Abc_NtkDressTransferNames( pNtkLogic, tMapping, fVerbose );
+
+ // clean up
+ stmm_free_table( tMapping );
+ Abc_NtkDelete( pMiterFraig );
+ Abc_NtkDelete( pNtkOrig );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns the mapping from the fraig nodes point into the nodes of the netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+stmm_table * Abc_NtkDressDeriveMapping( Abc_Ntk_t * pNtk )
+{
+ stmm_table * tResult;
+ Abc_Obj_t * pNode, * pNodeMap, * pNodeFraig;
+ int i;
+ assert( Abc_NtkIsNetlist(pNtk) );
+ tResult = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ // get the fraiged node
+ pNodeFraig = Abc_ObjRegular(pNode->pCopy);
+ // if this node is already mapped, skip
+ if ( stmm_is_member( tResult, (char *)pNodeFraig ) )
+ continue;
+ // get the mapping of this node
+ pNodeMap = Abc_ObjNotCond( pNode, Abc_ObjIsComplement(pNode->pCopy) );
+ // add the mapping
+ stmm_insert( tResult, (char *)pNodeFraig, (char *)pNodeMap );
+ }
+ return tResult;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Attaches the names of to the new netlist.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkDressTransferNames( Abc_Ntk_t * pNtk, stmm_table * tMapping, int fVerbose )
+{
+ Abc_Obj_t * pNet, * pNode, * pNodeMap, * pNodeFraig;
+ char * pName;
+ int i, Counter = 0, CounterInv = 0, CounterInit = stmm_count(tMapping);
+ assert( Abc_NtkIsLogic(pNtk) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ {
+ // if the node already has a name, quit
+ pName = Nm_ManFindNameById( pNtk->pManName, pNode->Id );
+ if ( pName != NULL )
+ continue;
+ // get the fraiged node
+ pNodeFraig = Abc_ObjRegular(pNode->pCopy);
+ // find the matching node of the original netlist
+ if ( !stmm_lookup( tMapping, (char *)pNodeFraig, (char **)&pNodeMap ) )
+ continue;
+ // find the true match
+ pNodeMap = Abc_ObjNotCond( pNodeMap, Abc_ObjIsComplement(pNode->pCopy) );
+ // get the name
+ pNet = Abc_ObjFanout0(Abc_ObjRegular(pNodeMap));
+ pName = Nm_ManFindNameById( pNet->pNtk->pManName, pNet->Id );
+ assert( pName != NULL );
+ // set the name
+ if ( Abc_ObjIsComplement(pNodeMap) )
+ {
+ Abc_ObjAssignName( pNode, pName, "_inv" );
+ CounterInv++;
+ }
+ else
+ {
+ Abc_ObjAssignName( pNode, pName, NULL );
+ Counter++;
+ }
+ // remove the name
+ stmm_delete( tMapping, (char **)&pNodeFraig, (char **)&pNodeMap );
+ }
+ if ( fVerbose )
+ {
+ printf( "Total number of names collected = %5d.\n", CounterInit );
+ printf( "Total number of names assigned = %5d. (Dir = %5d. Compl = %5d.)\n",
+ Counter + CounterInv, Counter, CounterInv );
+ }
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index be8b8ec5..9ce1ad26 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -76,7 +76,6 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc )
int fCleanup = 1;
//timeRetime = clock();
assert( !Abc_NtkIsNetlist(pNtk) );
- assert( !Abc_NtkIsSeq(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
@@ -373,6 +372,43 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
/**Function*************************************************************
+ Synopsis [Sets the final nodes to point to the original nodes.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkTransferPointers( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig )
+{
+ Abc_Obj_t * pObj;
+ Ivy_Obj_t * pObjIvy, * pObjFraig;
+ int i;
+ pObj = Abc_AigConst1(pNtk);
+ pObj->pCopy = Abc_AigConst1(pNtkAig);
+ Abc_NtkForEachCi( pNtk, pObj, i )
+ pObj->pCopy = Abc_NtkCi(pNtkAig, i);
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ pObj->pCopy = Abc_NtkCo(pNtkAig, i);
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ pObj->pCopy = Abc_NtkBox(pNtkAig, i);
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ pObjIvy = (Ivy_Obj_t *)pObj->pCopy;
+ if ( pObjIvy == NULL )
+ continue;
+ pObjFraig = Ivy_ObjEquiv( pObjIvy );
+ if ( pObjFraig == NULL )
+ continue;
+ pObj->pCopy = Abc_EdgeToNode( pNtkAig, Ivy_Regular(pObjFraig)->TravId );
+ pObj->pCopy = Abc_ObjNotCond( pObj->pCopy, Ivy_IsComplement(pObjFraig) );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Gives the current ABC network to AIG manager for processing.]
Description []
@@ -382,7 +418,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose )
SeeAlso []
***********************************************************************/
-Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose )
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
{
Ivy_FraigParams_t Params, * pParams = &Params;
Abc_Ntk_t * pNtkAig;
@@ -396,8 +432,19 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
pParams->fProve = fProve;
pParams->fDoSparse = fDoSparse;
pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
+ // transfer the pointers
+ if ( fTransfer == 1 )
+ {
+ Vec_Ptr_t * vCopies;
+ vCopies = Abc_NtkSaveCopy( pNtk );
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+ Abc_NtkLoadCopy( pNtk, vCopies );
+ Vec_PtrFree( vCopies );
+ Abc_NtkTransferPointers( pNtk, pNtkAig );
+ }
+ else
+ pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pTemp );
- pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
Ivy_ManStop( pMan );
return pNtkAig;
}
@@ -417,6 +464,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
{
Prove_Params_t * pParams = pPars;
Abc_Ntk_t * pNtk = *ppNtk, * pNtkTemp;
+ Abc_Obj_t * pObj, * pFanin;
Ivy_Man_t * pMan;
int RetValue;
assert( Abc_NtkIsStrash(pNtk) || Abc_NtkIsLogic(pNtk) );
@@ -432,6 +480,16 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
Abc_NtkDelete( pNtkTemp );
}
+ // check the case when the 0000 simulation pattern detect the bug
+ pObj = Abc_NtkPo(pNtk,0);
+ pFanin = Abc_ObjFanin0(pObj);
+ if ( Abc_ObjFanin0(pObj)->fPhase != (unsigned)Abc_ObjFaninC0(pObj) )
+ {
+ pNtk->pModel = ALLOC( int, Abc_NtkPiNum(pNtk) );
+ memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkPiNum(pNtk) );
+ return 0;
+ }
+
// if SAT only, solve without iteration
RetValue = Abc_NtkMiterSat( pNtk, 2*(sint64)pParams->nMiteringLimitStart, (sint64)0, 0, 0, NULL, NULL );
if ( RetValue >= 0 )
@@ -441,15 +499,16 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
if ( pParams->fUseRewriting && Abc_NtkNodeNum(pNtk) > 500 )
{
pParams->fUseRewriting = 0;
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 );
Abc_NtkDelete( pNtkTemp );
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
}
// convert ABC network into IVY network
pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+
// solve the CEC problem
RetValue = Ivy_FraigProve( &pMan, pParams );
// convert IVY network into ABC network
@@ -503,7 +562,6 @@ Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
Vec_Int_t * vInit = Abc_NtkCollectLatchValuesIvy( pNtk, 0 );
assert( !Abc_NtkIsNetlist(pNtk) );
- assert( !Abc_NtkIsSeq(pNtk) );
if ( Abc_NtkIsBddLogic(pNtk) )
{
if ( !Abc_NtkBddToSop(pNtk, 0) )
@@ -624,14 +682,14 @@ Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
vNodes = Ivy_ManDfs( pMan );
Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
{
- // add the first fanins
+ // add the first fanin
pFaninNew0 = Abc_ObjFanin0Ivy( pNtk, pNode );
if ( Ivy_ObjIsBuf(pNode) )
{
pNode->TravId = Abc_EdgeFromNode( pFaninNew0 );
continue;
}
- // add the first second
+ // add the second fanin
pFaninNew1 = Abc_ObjFanin1Ivy( pNtk, pNode );
// create the new node
if ( Ivy_ObjIsExor(pNode) )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 0ee1e804..ddbbf671 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1028,6 +1028,12 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk )
printf( "First cone = %6d. Second cone = %6d. Common = %6d.\n", vNodes1->nSize, vNodes2->nSize, nCommon );
Vec_PtrFree( vNodes1 );
Vec_PtrFree( vNodes2 );
+
+ // reorder the latches
+ Abc_NtkOrderCisCos( pNtk );
+ // make sure that everything is okay
+ if ( !Abc_NtkCheck( pNtk ) )
+ printf( "Abc_NtkDemiter: The network check has failed.\n" );
return 1;
}
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 8793ce53..f127811e 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -256,7 +256,7 @@ DdManager * Abc_NtkBuildGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fDrop
Abc_AigCleanup( pNtk->pManFunc );
// start the manager
- assert( Abc_NtkGlobalBdds(pNtk) == NULL );
+ assert( Abc_NtkGlobalBdd(pNtk) == NULL );
dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
pAttMan = Vec_AttAlloc( 0, Abc_NtkObjNumMax(pNtk) + 1, dd, Extra_StopManager, NULL, Cudd_RecursiveDeref );
Vec_PtrWriteEntry( pNtk->vAttrs, VEC_ATTR_GLOBAL_BDD, pAttMan );
diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c
deleted file mode 100644
index 1227d7b8..00000000
--- a/src/base/abci/abcPga.c
+++ /dev/null
@@ -1,154 +0,0 @@
-/**CFile****************************************************************
-
- FileName [abcPga.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Network and node package.]
-
- Synopsis [Interface with the FPGA mapping package.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: abcPga.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "fraig.h"
-#include "fpga.h"
-#include "pga.h"
-#include "cut.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Interface with the FPGA mapping package.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
-{
- Abc_Ntk_t * pNtkNew, * pNtk = pParams->pNtk;
- Pga_Man_t * pMan;
- Vec_Ptr_t * vNodeCuts;
-
- assert( Abc_NtkIsStrash(pNtk) );
-
- // print a warning about choice nodes
- if ( Abc_NtkGetChoiceNum( pNtk ) )
- printf( "Performing FPGA mapping with choices.\n" );
-
- // start the mapping manager
- pMan = Pga_ManStart( pParams );
- if ( pMan == NULL )
- return NULL;
-
- // perform mapping
- vNodeCuts = Pga_DoMapping( pMan );
-
- // transform the result of mapping into a BDD logic network
- pNtkNew = Abc_NtkFromPga( pNtk, vNodeCuts );
- if ( pNtkNew == NULL )
- return NULL;
- Pga_ManStop( pMan );
- Vec_PtrFree( vNodeCuts );
-
- // make the network minimum base
- Abc_NtkMinimumBase( pNtkNew );
-
- if ( pNtk->pExdc )
- pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
-
- // make sure that everything is okay
- if ( !Abc_NtkCheck( pNtkNew ) )
- {
- printf( "Abc_NtkPga: The network check has failed.\n" );
- Abc_NtkDelete( pNtkNew );
- return NULL;
- }
- return pNtkNew;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Creates the mapped network.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkFromPga( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodeCuts )
-{
- ProgressBar * pProgress;
- DdManager * dd;
- Abc_Ntk_t * pNtkNew;
- Abc_Obj_t * pNode, * pFanin, * pNodeNew;
- Cut_Cut_t * pCut;
- Vec_Ptr_t * vLeaves, * vVisited;
- int i, k, nDupGates;
- // create the new network
- pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
- dd = pNtkNew->pManFunc;
- // add new nodes in topologic order
- vLeaves = Vec_PtrAlloc( 6 );
- vVisited = Vec_PtrAlloc( 100 );
- pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(vNodeCuts) );
- Vec_PtrForEachEntry( vNodeCuts, pCut, i )
- {
- Extra_ProgressBarUpdate( pProgress, i, NULL );
- // create the new node
- pNodeNew = Abc_NtkCreateNode( pNtkNew );
- Vec_PtrClear( vLeaves );
- for ( k = 0; k < (int)pCut->nLeaves; k++ )
- {
- // add the node representing the old fanin in the new network
- pFanin = Abc_NtkObj( pNtk, pCut->pLeaves[k] );
- Vec_PtrPush( vLeaves, pFanin );
- Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
- }
- // set the new node at the old node
- pNode = Abc_NtkObj( pNtk, pCut->uSign ); // pCut->uSign contains the ID of the root node
- pNode->pCopy = pNodeNew;
- // create the function of the new node
- pNodeNew->pData = Abc_NodeConeBdd( dd, dd->vars, pNode, vLeaves, vVisited ); Cudd_Ref( pNodeNew->pData );
- }
- Extra_ProgressBarStop( pProgress );
- Vec_PtrFree( vVisited );
- Vec_PtrFree( vLeaves );
- // finalize the new network
- Abc_NtkFinalize( pNtk, pNtkNew );
- // decouple the PO driver nodes to reduce the number of levels
- nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
-// if ( nDupGates && Fpga_ManReadVerbose(pMan) )
-// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates );
- return pNtkNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 6698e738..e162ada4 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -51,28 +51,20 @@ int s_MappingMem = 0;
***********************************************************************/
void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
{
- int Num;//, Num2;
-
-// Abc_NtkDetectMatching( pNtk );
-// return;
+ int Num;
fprintf( pFile, "%-13s:", pNtk->pName );
if ( Abc_NtkAssertNum(pNtk) )
fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
else
fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
-
-// if ( !Abc_NtkIsSeq(pNtk) )
- fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
-// else
-// fprintf( pFile, " lat = %4d(%d,%d)", Seq_NtkLatchNum(pNtk), Seq_NtkLatchNumShared(pNtk), Seq_NtkLatchNumMax(pNtk) );
-
+ fprintf( pFile, " lat = %4d", Abc_NtkLatchNum(pNtk) );
if ( Abc_NtkIsNetlist(pNtk) )
{
fprintf( pFile, " net = %5d", Abc_NtkNetNum(pNtk) );
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
fprintf( pFile, " box = %5d", Abc_NtkBoxNum(pNtk) );
}
- else if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) )
+ else if ( Abc_NtkIsStrash(pNtk) )
{
fprintf( pFile, " and = %5d", Abc_NtkNodeNum(pNtk) );
if ( Num = Abc_NtkGetChoiceNum(pNtk) )
@@ -87,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
else
fprintf( pFile, " nd = %5d", Abc_NtkNodeNum(pNtk) );
- if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) || Abc_NtkIsNetlist(pNtk) )
+ if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
{
}
else if ( Abc_NtkHasSop(pNtk) )
@@ -114,7 +106,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
if ( Abc_NtkIsStrash(pNtk) )
fprintf( pFile, " lev = %3d", Abc_AigLevel(pNtk) );
- else if ( !Abc_NtkIsSeq(pNtk) )
+ else
fprintf( pFile, " lev = %3d", Abc_NtkLevel(pNtk) );
fprintf( pFile, "\n" );
@@ -260,16 +252,6 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk )
int InitNums[4], Init;
assert( !Abc_NtkIsNetlist(pNtk) );
-/*
- if ( Abc_NtkIsSeq(pNtk) )
- {
- Seq_NtkLatchGetInitNums( pNtk, InitNums );
- fprintf( pFile, "%-15s: ", pNtk->pName );
- fprintf( pFile, "Latch = %6d. No = %4d. Zero = %4d. One = %4d. DC = %4d.\n",
- Abc_NtkLatchNum(pNtk), InitNums[0], InitNums[1], InitNums[2], InitNums[3] );
- return;
- }
-*/
if ( Abc_NtkLatchNum(pNtk) == 0 )
{
fprintf( pFile, "The network is combinational.\n" );
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index fcd44d30..d206ae6e 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -26,7 +26,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose );
extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
@@ -134,13 +133,13 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
break;
*/
/*
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
break;
if ( --Counter == 0 )
break;
*/
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
break;
if ( --Counter == 0 )
@@ -329,9 +328,9 @@ void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose
Abc_Ntk_t * Abc_NtkMiterRwsat( Abc_Ntk_t * pNtk )
{
Abc_Ntk_t * pNtkTemp;
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp );
- Abc_NtkRewrite( pNtk, 0, 0, 0 );
+ Abc_NtkRewrite( pNtk, 0, 0, 0, 0 );
Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 );
return pNtk;
}
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 151b5256..e7dbf3a1 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -51,7 +51,7 @@ static void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
SeeAlso []
***********************************************************************/
-int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose )
+int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose )
{
ProgressBar * pProgress;
Cut_Man_t * pManCut;
@@ -76,6 +76,9 @@ clk = clock();
Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
pNtk->pManCut = pManCut;
+ if ( fVeryVerbose )
+ Rwr_ScoresClean( pManRwr );
+
// resynthesize each node once
nNodes = Abc_NtkObjNumMax(pNtk);
pProgress = Extra_ProgressBarStart( stdout, nNodes );
@@ -147,6 +150,8 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
if ( fVerbose )
Rwr_ManPrintStats( pManRwr );
// Rwr_ManPrintStatsFile( pManRwr );
+ if ( fVeryVerbose )
+ Rwr_ScoresReport( pManRwr );
// delete the managers
Rwr_ManStop( pManRwr );
Cut_ManStop( pManCut );
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 2e1b3eb1..9af6dc00 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -285,7 +285,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld )
pMan = pNodeOld->pNtk->pManFunc;
pRoot = pNodeOld->pData;
// check the constant case
- if ( Abc_NodeIsConst(pNodeOld) )
+ if ( Abc_NodeIsConst(pNodeOld) || Hop_Regular(pRoot) == Hop_ManConst1(pMan) )
return Abc_ObjNotCond( Abc_AigConst1(pNtkNew), Hop_IsComplement(pRoot) );
// set elementary variables
Abc_ObjForEachFanin( pNodeOld, pFanin, i )
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index acd63771..7697fde1 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -280,7 +280,6 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b
***********************************************************************/
Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach )
{
-/*
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pNodeNew;
int * pPermute;
@@ -292,14 +291,14 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
pNtkNew->pSpec = NULL;
// create PIs corresponding to LOs
- Abc_NtkForEachLatch( pNtk, pNode, i )
+ Abc_NtkForEachLatchOutput( pNtk, pNode, i )
Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL );
// cannot ADD POs here because pLatch->pCopy point to the PIs
// create a new node
pNodeNew = Abc_NtkCreateNode(pNtkNew);
// add the fanins corresponding to latch outputs
- Abc_NtkForEachLatch( pNtk, pNode, i )
+ Abc_NtkForEachLatchOutput( pNtk, pNode, i )
Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
// create the logic function
@@ -317,14 +316,14 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
Abc_NtkForEachPo( pNtk, pNode, i )
if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
- Abc_NtkForEachLatch( pNtk, pNode, i )
- Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in"), NULL );
+ Abc_NtkForEachLatchInput( pNtk, pNode, i )
+ Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL );
// link to the POs of the network
Abc_NtkForEachPo( pNtk, pNode, i )
if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
- Abc_NtkForEachLatch( pNtk, pNode, i )
+ Abc_NtkForEachLatchInput( pNtk, pNode, i )
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
// remove the extra nodes
@@ -340,8 +339,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
return NULL;
}
return pNtkNew;
-*/
- return NULL;
+// return NULL;
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index f4717eda..ec0ba8ca 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -176,6 +176,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
Prove_ParamsSetDefault( pParams );
pParams->nItersMax = 5;
// RetValue = Abc_NtkMiterProve( &pMiter, pParams );
+// pParams->fVerbose = 1;
RetValue = Abc_NtkIvyProve( &pMiter, pParams );
if ( RetValue == -1 )
printf( "Networks are undecided (resource limits is reached).\n" );
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 7e674fbe..169ab577 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -7,6 +7,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcClpSop.c \
src/base/abci/abcCut.c \
src/base/abci/abcDebug.c \
+ src/base/abci/abcDress.c \
src/base/abci/abcDsd.c \
src/base/abci/abcEspresso.c \
src/base/abci/abcExtract.c \
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 06:16:55 +0000