summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c106
-rw-r--r--src/base/abci/abcClpBdd.c19
-rw-r--r--src/base/abci/abcDar.c6
-rw-r--r--src/base/abci/abcReorder.c2
-rw-r--r--src/base/abci/abcXsim.c13
5 files changed, 134 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f4ad2eaf..da07a936 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -64,6 +64,7 @@ static int Abc_CommandRenode ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFastExtract ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandEliminate ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -239,6 +240,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "cleanup", Abc_CommandCleanup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "sweep", Abc_CommandSweep, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "fx", Abc_CommandFastExtract, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "eliminate", Abc_CommandEliminate, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "dsd", Abc_CommandDisjoint, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "lutpack", Abc_CommandLutpack, 1 );
@@ -2727,6 +2729,97 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandEliminate( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ Abc_Ntk_t * pNtk;
+ FILE * pOut, * pErr;
+ int nMaxSize;
+ int fReverse;
+ int fVerbose;
+ int c;
+ extern int Abc_NtkEliminate( Abc_Ntk_t * pNtk, int nMaxSize, int fReverse, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set the defaults
+ nMaxSize = 8;
+ fReverse = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( (c = Extra_UtilGetopt(argc, argv, "Nrvh")) != EOF )
+ {
+ switch (c)
+ {
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by a positive integer.\n" );
+ goto usage;
+ }
+ nMaxSize = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nMaxSize <= 0 )
+ goto usage;
+ break;
+ case 'r':
+ fReverse ^= 1;
+ break;
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ break;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ if ( Abc_NtkNodeNum(pNtk) == 0 )
+ {
+ fprintf( pErr, "The network does not have internal nodes.\n" );
+ return 1;
+ }
+
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ fprintf( pErr, "This command can only be applied to a logic network (run \"renode\" or \"if\").\n" );
+ return 1;
+ }
+
+ // the nodes to be merged are linked into the special linked list
+ Abc_NtkEliminate( pNtk, nMaxSize, fReverse, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: eliminate [-N num] [-rvh]\n");
+ fprintf( pErr, "\t greedily eliminates nodes by collapsing them into fanouts\n");
+ fprintf( pErr, "\t-N num : the maximum support size after collapsing [default = %d]\n", nMaxSize );
+ fprintf( pErr, "\t-r : use the reverse topological order [default = %s]\n", fReverse? "yes": "no" );
+ fprintf( pErr, "\t-v : print 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_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -2958,6 +3051,7 @@ int Abc_CommandImfs( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: imfs [-W <NM>] [-L <num>] [-C <num>] [-S <num>] [-avwh]\n" );
fprintf( pErr, "\t performs resubstitution-based resynthesis with interpolation\n" );
+ fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"lutpack\")\n" );
fprintf( pErr, "\t-W <NM> : fanin/fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
fprintf( pErr, "\t-C <num> : the max number of resub candidates (1 <= n) [default = %d]\n", pPars->nCands );
fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
@@ -3106,6 +3200,7 @@ usage:
fprintf( pErr, "\t performs \"rewriting\" for LUT networks;\n" );
fprintf( pErr, "\t determines LUT size as the max fanin count of a node;\n" );
fprintf( pErr, "\t if the network is not LUT-mapped, packs it into 6-LUTs\n" );
+ fprintf( pErr, "\t (there is another command for resynthesis after LUT mapping, \"imfs\")\n" );
fprintf( pErr, "\t-N <num> : the max number of LUTs in the structure (2 <= num) [default = %d]\n", pPars->nLutsMax );
fprintf( pErr, "\t-Q <num> : the max number of LUTs not in MFFC (0 <= num) [default = %d]\n", pPars->nLutsOver );
fprintf( pErr, "\t-S <num> : the max number of LUT inputs shared (0 <= num <= 3) [default = %d]\n", pPars->nVarsShared );
@@ -6213,7 +6308,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk );
extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
- extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
+// extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
extern void Abc_NtkDarTestBlif( char * pFileName );
@@ -6222,8 +6317,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
pOut = Abc_FrameReadOut(pAbc);
pErr = Abc_FrameReadErr(pAbc);
- printf( "This command is temporarily disabled.\n" );
- return 0;
+// printf( "This command is temporarily disabled.\n" );
+// return 0;
// set defaults
fVeryVerbose = 0;
@@ -8399,6 +8494,7 @@ usage:
sprintf( Buffer, "%d", pParams->nBTLimit );
fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" );
fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" );
+ fprintf( pErr, "\t (there are also newer fraiging commands, \"ifraig\" and \"dfraig\")\n" );
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-C num : number of backtracks for one SAT problem [default = %s]\n", pParams->nBTLimit==-1? "infinity" : Buffer );
@@ -10891,6 +10987,7 @@ int Abc_CommandDRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
int fFastAlgo;
int fVerbose;
int c;
+ extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
extern Abc_Ntk_t * Abc_NtkDarRetimeF( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@@ -12290,6 +12387,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-srvh] <file1> <file2>\n" );
fprintf( pErr, "\t performs bounded sequential equivalence checking\n" );
+ fprintf( pErr, "\t (there is also an unbounded SEC commands, \"dsec\" and \"dprove\")\n" );
fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
fprintf( pErr, "\t-r : toggles retiming verification [default = %s]\n", fVerbose? "yes": "no" );
fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
@@ -12616,6 +12714,7 @@ usage:
fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
fprintf( pErr, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
fprintf( pErr, "\t derives CNF from the current network and leave it unchanged\n" );
+ fprintf( pErr, "\t (there is also a newer SAT solving command \"dsat\")\n" );
fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -12912,6 +13011,7 @@ usage:
fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-I num] [-rfbvh]\n" );
fprintf( pErr, "\t solves combinational miter by rewriting, FRAIGing, and SAT\n" );
fprintf( pErr, "\t replaces the current network by the cone modified by rewriting\n" );
+ fprintf( pErr, "\t (there are also newer CEC commands, \"iprove\" and \"dprove\")\n" );
fprintf( pErr, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax );
fprintf( pErr, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart );
fprintf( pErr, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart );
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index 341ff5b0..a6b3a770 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "abc.h"
+//#include "reo.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -87,6 +88,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
return pNtkNew;
}
+
+//int runtime1, runtime2;
+
/**Function*************************************************************
Synopsis [Derives the network with the given global BDD.]
@@ -100,12 +104,19 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
{
+// extern void Extra_ShuffleTest( reo_man * p, DdManager * dd, DdNode * Func );
+// reo_man * pReo;
+
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pDriver, * pNodeNew;
// DdManager * dd = pNtk->pManGlob;
DdManager * dd = Abc_NtkGlobalBddMan( pNtk );
int i;
+
+// pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
+// runtime1 = runtime2 = 0;
+
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
// make sure the new manager has the same number of inputs
@@ -124,8 +135,16 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
// pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Abc_ObjGlobalBdd(pNode) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+
+// Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) );
+
}
Extra_ProgressBarStop( pProgress );
+
+// Extra_ReorderQuit( pReo );
+//PRT( "Reo ", runtime1 );
+//PRT( "Cudd", runtime2 );
+
return pNtkNew;
}
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 3729fef8..29b1ea14 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1506,12 +1506,16 @@ void Abc_NtkDarTestBlif( char * pFileName )
printf( "Abc_NtkDarTestBlif(): Reading BLIF has failed.\n" );
return;
}
+ Ntl_ManPrintStats( p );
+/*
if ( !Ntl_ManInsertTest( p ) )
{
printf( "Abc_NtkDarTestBlif(): Tranformation of the netlist has failed.\n" );
return;
}
- sprintf( Buffer, "%s_.blif", p->pName );
+*/
+// sprintf( Buffer, "%s_.blif", p->pName );
+ sprintf( Buffer, "test_.blif", p->pName );
Ioa_WriteBlif( p, Buffer );
Ntl_ManFree( p );
}
diff --git a/src/base/abci/abcReorder.c b/src/base/abci/abcReorder.c
index d6dee49b..182780cd 100644
--- a/src/base/abci/abcReorder.c
+++ b/src/base/abci/abcReorder.c
@@ -77,6 +77,8 @@ void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
reo_man * p;
Abc_Obj_t * pNode;
int i;
+ Abc_NtkRemoveDupFanins( pNtk );
+ Abc_NtkMinimumBase( pNtk );
p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
Abc_NtkForEachNode( pNtk, pNode, i )
{
diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c
index 5d9e4634..e5656170 100644
--- a/src/base/abci/abcXsim.c
+++ b/src/base/abci/abcXsim.c
@@ -190,28 +190,25 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fXInputs, int fXS
***********************************************************************/
void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
-{
+{
Abc_Obj_t * pObj;
int i, f;
assert( Abc_NtkIsStrash(pNtk) );
srand( 0x12341234 );
// initialize the values
Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 );
- Abc_NtkForEachPi( pNtk, pObj, i )
- Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
Abc_NtkForEachLatch( pNtk, pObj, i )
- Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
+// Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 );
+ Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchInit(pObj) );
// simulate for the given number of timeframes
for ( f = 0; f < nFrames; f++ )
{
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
Abc_AigForEachAnd( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) );
Abc_NtkForEachCo( pNtk, pObj, i )
Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) );
- // assign input values
- Abc_NtkForEachPi( pNtk, pObj, i )
- Abc_ObjSetXsim( pObj, Abc_XsimRand2() );
- // transfer the latch values
Abc_NtkForEachLatch( pNtk, pObj, i )
Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) );
}