summaryrefslogtreecommitdiffstats
path: root/src/base/abci
diff options
context:
space:
mode:
Diffstat (limited to 'src/base/abci')
-rw-r--r--src/base/abci/abc.c129
-rw-r--r--src/base/abci/abcBalance.c39
-rw-r--r--src/base/abci/abcFraig.c2
-rw-r--r--src/base/abci/abcPrint.c50
-rw-r--r--src/base/abci/abcRewrite.c1
-rw-r--r--src/base/abci/abcSat.c61
-rw-r--r--src/base/abci/abcStrash.c37
7 files changed, 291 insertions, 28 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b6de6cbf..71b76cf6 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -77,6 +77,7 @@ static int Abc_CommandExdcFree ( Abc_Frame_t * pAbc, int argc, char ** argv
static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -173,6 +174,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 );
Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 );
Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 );
+ Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 );
Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
@@ -648,6 +650,7 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk;
Abc_Obj_t * pNode;
int c;
+ int fListNodes;
int fProfile;
pNtk = Abc_FrameReadNet(pAbc);
@@ -655,12 +658,16 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
pErr = Abc_FrameReadErr(pAbc);
// set defaults
- fProfile = 1;
+ fListNodes = 0;
+ fProfile = 1;
util_getopt_reset();
- while ( ( c = util_getopt( argc, argv, "ph" ) ) != EOF )
+ while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF )
{
switch ( c )
{
+ case 'n':
+ fListNodes ^= 1;
+ break;
case 'p':
fProfile ^= 1;
break;
@@ -701,12 +708,13 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// process all COs
- Abc_NtkPrintLevel( pOut, pNtk, fProfile );
+ Abc_NtkPrintLevel( pOut, pNtk, fProfile, fListNodes );
return 0;
usage:
- fprintf( pErr, "usage: print_level [-ph] <node>\n" );
+ fprintf( pErr, "usage: print_level [-nph] <node>\n" );
fprintf( pErr, "\t prints information about node level and cone size\n" );
+ fprintf( pErr, "\t-n : toggles printing nodes by levels [default = %s]\n", fListNodes? "yes": "no" );
fprintf( pErr, "\t-p : toggles printing level profile [default = %s]\n", fProfile? "yes": "no" );
fprintf( pErr, "\t-h : print the command usage\n");
fprintf( pErr, "\tnode : (optional) one node to consider\n");
@@ -732,6 +740,7 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
int fVerbose;
extern Vec_Ptr_t * Sim_ComputeFunSupp( Abc_Ntk_t * pNtk, int fVerbose );
+ extern void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk );
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -759,6 +768,11 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
+
+ // print support information
+ Abc_NtkPrintStrSupports( pNtk );
+ return 0;
+
if ( !Abc_NtkIsComb(pNtk) )
{
fprintf( pErr, "This command works only for combinational networks.\n" );
@@ -3649,11 +3663,102 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
Abc_Ntk_t * pNtk, * pNtkRes;
int c;
+ int fVerbose;
+ int fUseInvs;
+ int nFaninMax;
+ extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+
+ pNtk = Abc_FrameReadNet(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ fUseInvs = 1;
+ nFaninMax = 128;
+ util_getopt_reset();
+ while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'N':
+ if ( util_optind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nFaninMax = atoi(argv[util_optind]);
+ util_optind++;
+ if ( nFaninMax < 0 )
+ goto usage;
+ break;
+ case 'i':
+ fUseInvs ^= 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;
+ }
+
+ // run the command
+ pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 0, 0, fUseInvs, fVerbose );
+ if ( pNtkRes == NULL )
+ {
+ fprintf( pErr, "Command has failed.\n" );
+ return 1;
+ }
+ // replace the current network
+ Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" );
+ fprintf( pErr, "\t specilized AND/OR/EXOR decomposition\n" );
+ fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
+ fprintf( pErr, "\t-i : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" );
+ 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_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;//, * pNtkRes;
+ int c;
pNtk = Abc_FrameReadNet(pAbc);
pOut = Abc_FrameReadOut(pAbc);
@@ -3676,6 +3781,18 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
fprintf( pErr, "Empty network.\n" );
return 1;
}
+
+ if ( !Abc_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for strashed networks.\n" );
+ return 1;
+ }
+
+// Abc_NtkDeriveEsops( pNtk );
+// Abc_NtkXyz( pNtk, 128, 0, 0, 0 );
+ printf( "This command is currently not used.\n" );
+
+/*
// run the command
pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
if ( pNtkRes == NULL )
@@ -3685,6 +3802,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+*/
return 0;
usage:
@@ -3696,7 +3814,6 @@ usage:
-
/**Function*************************************************************
Synopsis []
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 1adbfef7..fed89dbb 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -102,6 +102,42 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica
/**Function*************************************************************
+ Synopsis [Randomizes the node positions.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper )
+{
+ Abc_Obj_t * pNode1, * pNode2;
+ int i, Signature;
+ if ( Vec_PtrSize(vSuper) < 3 )
+ return;
+ pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 );
+ pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 );
+ if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+ return;
+ // some reordering will be performed
+ Signature = rand();
+ for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- )
+ {
+ pNode1 = Vec_PtrEntry( vSuper, i );
+ pNode2 = Vec_PtrEntry( vSuper, i-1 );
+ if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level )
+ return;
+ if ( Signature & (1 << (i % 10)) )
+ continue;
+ Vec_PtrWriteEntry( vSuper, i, pNode2 );
+ Vec_PtrWriteEntry( vSuper, i-1, pNode1 );
+ }
+}
+
+/**Function*************************************************************
+
Synopsis [Rebalances the multi-input node rooted at pNodeOld.]
Description []
@@ -143,6 +179,9 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
assert( vSuper->nSize > 1 );
while ( vSuper->nSize > 1 )
{
+ // randomize the node positions
+// Abc_NodeBalanceRandomize( vSuper );
+ // pull out the last two nodes
pNode1 = Vec_PtrPop(vSuper);
pNode2 = Vec_PtrPop(vSuper);
Abc_VecObjPushUniqueOrderByLevel( vSuper, Abc_AigAnd(pMan, pNode1, pNode2) );
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index bfc992ef..d59f21a0 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -56,7 +56,7 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int f
{
Fraig_Params_t * pPars = pParams;
Abc_Ntk_t * pNtkNew;
- Fraig_Man_t * pMan;
+ Fraig_Man_t * pMan;
// check if EXDC is present
if ( fExdc && pNtk->pExdc == NULL )
fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 82325619..6791f08c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -79,7 +79,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
fprintf( pFile, " lit(fac) = %5d", Abc_NtkGetLitFactNum(pNtk) );
}
else if ( Abc_NtkHasBdd(pNtk) )
- fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) );
+ fprintf( pFile, " bdd = %5d", Abc_NtkGetBddNodeNum(pNtk) );
else if ( Abc_NtkHasMapping(pNtk) )
{
fprintf( pFile, " area = %5.2f", Abc_NtkGetMappedArea(pNtk) );
@@ -423,10 +423,26 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames )
SeeAlso []
***********************************************************************/
-void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile )
+void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes )
{
Abc_Obj_t * pNode;
- int i, Length;
+ int i, k, Length;
+
+ if ( fListNodes )
+ {
+ int nLevels;
+ nLevels = Abc_NtkGetLevelNum(pNtk);
+ printf( "Nodes by level:\n" );
+ for ( i = 0; i <= nLevels; i++ )
+ {
+ printf( "%2d : ", i );
+ Abc_NtkForEachNode( pNtk, pNode, k )
+ if ( (int)pNode->Level == i )
+ printf( " %s", Abc_ObjName(pNode) );
+ printf( "\n" );
+ }
+ return;
+ }
// print the delay profile
if ( fProfile && Abc_NtkHasMapping(pNtk) )
@@ -716,6 +732,34 @@ void Abc_NtkPrintSharing( Abc_Ntk_t * pNtk )
printf( "\n" );
}
+/**Function*************************************************************
+
+ Synopsis [Prints info for each output cone.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkPrintStrSupports( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vSupp, * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+ printf( "Structural support info:\n" );
+ Abc_NtkForEachCo( pNtk, pObj, i )
+ {
+ vSupp = Abc_NtkNodeSupport( pNtk, &pObj, 1 );
+ vNodes = Abc_NtkDfsNodes( pNtk, &pObj, 1 );
+ printf( "%20s : Cone = %5d. Supp = %5d.\n",
+ Abc_ObjName(pObj), vNodes->nSize, vSupp->nSize );
+ Vec_PtrFree( vNodes );
+ Vec_PtrFree( vSupp );
+ }
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index ab594667..b3b30d9a 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -109,6 +109,7 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart );
// print stats
if ( fVerbose )
Rwr_ManPrintStats( pManRwr );
+// Rwr_ManPrintStatsFile( pManRwr );
// delete the managers
Rwr_ManStop( pManRwr );
Cut_ManStop( pManCut );
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 1a35d143..4a65659c 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -24,8 +24,8 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
-static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars );
+static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -57,6 +57,8 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
// load clauses into the solver
clk = clock();
pSat = Abc_NtkMiterSatCreate( pNtk );
+ if ( pSat == NULL )
+ return 1;
// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) );
// PRT( "Time", clock() - clk );
@@ -69,7 +71,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose )
{
solver_delete( pSat );
// printf( "The problem is UNSATISFIABLE after simplification.\n" );
- return -1;
+ return 1;
}
// solve the miter
@@ -143,13 +145,19 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
// derive SOPs for both phases of the node
Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 );
// add the clauses to the solver
- Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars );
+ if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) )
+ {
+ solver_delete( pSat );
+ return NULL;
+ }
}
- // add clauses for each PO
-// Abc_NtkForEachPo( pNtk, pNode, i )
-// Abc_NodeAddClausesTop( pSat, pNode, vVars );
-
- Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars );
+ // add clauses for the POs
+ if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) )
+ {
+ solver_delete( pSat );
+ return NULL;
+ }
+// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 );
// delete
Vec_StrFree( vCube );
@@ -169,7 +177,7 @@ solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
-void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
int i, c, nFanins;
@@ -177,6 +185,16 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
nFanins = Abc_ObjFaninNum( pNode );
assert( nFanins == Abc_SopGetVarNum( pSop0 ) );
+
+ if ( nFanins == 0 )
+ {
+ vVars->nSize = 0;
+ if ( Abc_SopIsConst1(pSop1) )
+ Vec_IntPush( vVars, toLit(pNode->Id) );
+ else
+ Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ }
// add clauses for the negative phase
for ( c = 0; ; c++ )
@@ -195,7 +213,8 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
}
// add clauses for the positive phase
@@ -215,8 +234,10 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
}
Vec_IntPush( vVars, toLit(pNode->Id) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
}
+ return 1;
}
/**Function*************************************************************
@@ -230,7 +251,7 @@ void Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t *
SeeAlso []
***********************************************************************/
-void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
+int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars )
{
Abc_Obj_t * pFanin;
@@ -240,29 +261,33 @@ void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, toLit(pNode->Id) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
}
else
{
vVars->nSize = 0;
Vec_IntPush( vVars, neg(toLit(pFanin->Id)) );
Vec_IntPush( vVars, toLit(pNode->Id) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pFanin->Id) );
Vec_IntPush( vVars, neg(toLit(pNode->Id)) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) )
+ return 0;
}
vVars->nSize = 0;
Vec_IntPush( vVars, toLit(pNode->Id) );
- solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
+ return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize );
}
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index d1734d88..72f4215b 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -29,6 +29,7 @@
// static functions
static void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
static Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
+static Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop );
extern char * Mio_GateReadSop( void * pGate );
@@ -182,6 +183,7 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
{
int fUseFactor = 1;
char * pSop;
+ extern int Abc_SopIsExorType( char * pSop );
assert( Abc_ObjIsNode(pNode) );
@@ -203,6 +205,10 @@ Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode )
if ( Abc_NodeIsConst(pNode) )
return Abc_ObjNotCond( Abc_NtkConst1(pNtkNew), Abc_SopIsConst0(pSop) );
+ // consider the special case of EXOR function
+ if ( Abc_SopIsExorType(pSop) )
+ return Abc_NodeStrashExor( pNtkNew, pNode, pSop );
+
// decide when to use factoring
if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
return Abc_NodeStrashFactor( pNtkNew, pNode, pSop );
@@ -254,6 +260,37 @@ Abc_Obj_t * Abc_NodeStrashSop( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pS
/**Function*************************************************************
+ Synopsis [Strashed n-input XOR function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeStrashExor( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, char * pSop )
+{
+ Abc_Aig_t * pMan = pNtkNew->pManFunc;
+ Abc_Obj_t * pFanin, * pSum;
+ int i, nFanins;
+ // get the number of node's fanins
+ nFanins = Abc_ObjFaninNum( pNode );
+ assert( nFanins == Abc_SopGetVarNum(pSop) );
+ // go through the cubes of the node's SOP
+ pSum = Abc_ObjNot( Abc_NtkConst1(pNtkNew) );
+ for ( i = 0; i < nFanins; i++ )
+ {
+ pFanin = Abc_ObjFanin( pNode, i );
+ pSum = Abc_AigXor( pMan, pSum, pFanin->pCopy );
+ }
+ if ( Abc_SopIsComplement(pSop) )
+ pSum = Abc_ObjNot(pSum);
+ return pSum;
+}
+
+/**Function*************************************************************
+
Synopsis [Strashes one logic node using its SOP.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 14:42:36 +0000