summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c32
-rw-r--r--src/opt/sbd/sbd.c28
-rw-r--r--src/sat/bmc/bmcMaj.c24
3 files changed, 52 insertions, 32 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5caf8145..ad3673d0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8072,17 +8072,17 @@ usage:
***********************************************************************/
int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose );
- int c, nVars = 3, nNodes = 1, fUseConst = 0, fVerbose = 1;
+ extern void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose );
+ int c, nVars = 3, nNodes = 1, fUseConst = 0, fUseLine = 0, fVerbose = 1;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "NMcvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "INfcvh" ) ) != EOF )
{
switch ( c )
{
- case 'N':
+ case 'I':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nVars = atoi(argv[globalUtilOptind]);
@@ -8090,10 +8090,10 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nVars < 0 )
goto usage;
break;
- case 'M':
+ case 'N':
if ( globalUtilOptind >= argc )
{
- Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nNodes = atoi(argv[globalUtilOptind]);
@@ -8101,9 +8101,12 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nNodes < 0 )
goto usage;
break;
- case 'c':
+ case 'f':
fUseConst ^= 1;
break;
+ case 'c':
+ fUseLine ^= 1;
+ break;
case 'v':
fVerbose ^= 1;
break;
@@ -8118,15 +8121,16 @@ int Abc_CommandMajExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Cannot sythesize MAJ gate with an even number of inputs (%d).\n", nVars );
return 1;
}
- Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fVerbose );
+ Maj_ManExactSynthesis( nVars, nNodes, fUseConst, fUseLine, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: majexact [-NM <num>] [-cvh]\n" );
- Abc_Print( -2, "\t exactly synthesizes N-input MAJ using MAJ3 gates\n" );
- Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", nVars );
- Abc_Print( -2, "\t-M <num> : the number of MAJ3 nodes [default = %d]\n", nNodes );
- Abc_Print( -2, "\t-c : toggle using constant fanins [default = %s]\n", fUseConst ? "yes" : "no" );
+ Abc_Print( -2, "usage: majexact [-IN <num>] [-fcvh]\n" );
+ Abc_Print( -2, "\t exact synthesis of multi-input MAJ using MAJ3 gates\n" );
+ Abc_Print( -2, "\t-I <num> : the number of input variables [default = %d]\n", nVars );
+ Abc_Print( -2, "\t-N <num> : the number of MAJ3 nodes [default = %d]\n", nNodes );
+ Abc_Print( -2, "\t-f : toggle using constant fanins [default = %s]\n", fUseConst ? "yes" : "no" );
+ Abc_Print( -2, "\t-c : toggle using cascade topology [default = %s]\n", fUseLine ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
return 1;
diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
index 5c5b1f2b..75fc8750 100644
--- a/src/opt/sbd/sbd.c
+++ b/src/opt/sbd/sbd.c
@@ -43,14 +43,14 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
+int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars, int Degree )
{
int i, k, Entry = 0, Entry2, Count = 0, Below;
int Prev = Vec_IntEntry( vSet, 0 );
Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
{
- assert( 2*Prev >= Entry );
- if ( 2*Prev == Entry )
+ assert( Degree*Prev >= Entry );
+ if ( Degree*Prev == Entry )
{
Prev = Entry;
continue;
@@ -58,19 +58,24 @@ int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
Below = nVars;
Vec_IntForEachEntryStart( vSet, Entry2, k, i )
Below += Entry2;
- Count += Below * (2*Prev - 1);
+ Count += Below * (Degree*Prev - 1);
Prev = Entry;
}
- Count += nVars * 2*Prev;
+ Count += nVars * Degree*Prev;
return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
}
void Sbd_CountTopos()
{
- Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
+ int nInputs = 9;
+ int nNodes = 10;
+ int Degree = 3;
+ int fVerbose = 1;
+ Hsh_VecMan_t * p = Hsh_VecManStart( 10000 ); // hash table for arrays
Vec_Int_t * vSet = Vec_IntAlloc( 100 );
int i, k, e, Start, Stop;
+ printf( "Counting topologies for %d inputs and %d degree-%d nodes.\n", nInputs, nNodes, Degree );
Start = Hsh_VecManAdd( p, vSet );
- for ( i = 1; i < 9; i++ )
+ for ( i = 1; i <= nNodes; i++ )
{
Stop = Hsh_VecSize( p );
for ( e = Start; e < Stop; e++ )
@@ -81,7 +86,7 @@ void Sbd_CountTopos()
for ( k = 0; k < Vec_IntSize(vSet); k++ )
{
// skip if the number of entries on this level is equal to the number of fanins on the previous level
- if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
+ if ( k ? (Vec_IntEntry(vSet, k) == Degree*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
continue;
Vec_IntAddToEntry( vSet, k, 1 );
Hsh_VecManAdd( p, vSet );
@@ -90,15 +95,16 @@ void Sbd_CountTopos()
Vec_IntPush( vSet, 1 );
Hsh_VecManAdd( p, vSet );
}
- printf( "%2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
- if ( 0 )
+ printf( "Nodes = %2d : This = %8d All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
+ if ( fVerbose )
{
for ( e = Stop; e < Hsh_VecSize(p); e++ )
{
Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
- printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, 5) );
+ printf( "Params = %3d. ", Sbd_CountConfigVars(vTemp, nInputs, Degree) );
Vec_IntPrint( vTemp );
}
+ printf( "\n" );
}
Start = Stop;
}
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 749be285..31460b0e 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -41,6 +41,7 @@ struct Maj_Man_t_
int nWords; // the truth table size in 64-bit words
int iVar; // the next available SAT variable
int fUseConst; // use constant fanins
+ int fUseLine; // use cascade topology
Vec_Wrd_t * vInfo; // Const0 + Const1 + nVars + nNodes + Maj(nVars)
int VarMarks[MAJ_NOBJS][3][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS+2]; // values of the first 2 + nVars variables
@@ -103,6 +104,13 @@ int Maj_ManMarkup( Maj_Man_t * p )
{
for ( k = 0; k < 3; k++ )
{
+ if ( p->fUseLine && k == 0 )
+ {
+ j = i-1;
+ Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
+ p->VarMarks[i][k][j] = p->iVar++;
+ continue;
+ }
for ( j = (p->fUseConst && k == 2) ? 0 : 2; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
@@ -119,19 +127,20 @@ int Maj_ManMarkup( Maj_Man_t * p )
for ( j = 0; j < p->nObjs; j++ )
{
for ( k = 0; k < 3; k++ )
- printf( "%2d ", p->VarMarks[i][k][j] );
+ printf( "%3d ", p->VarMarks[i][k][j] );
printf( "\n" );
}
}
return p->iVar;
}
-Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst )
+Maj_Man_t * Maj_ManAlloc( int nVars, int nNodes, int fUseConst, int fUseLine )
{
Maj_Man_t * p = ABC_CALLOC( Maj_Man_t, 1 );
p->nVars = nVars;
p->nNodes = nNodes;
p->nObjs = 2 + nVars + nNodes;
p->fUseConst = fUseConst;
+ p->fUseLine = fUseLine;
p->nWords = Abc_TtWordNum(nVars);
p->vOutLits = Vec_WecStart( p->nObjs );
p->iVar = Maj_ManMarkup( p );
@@ -207,10 +216,11 @@ void Maj_ManPrintSolution( Maj_Man_t * p )
{
int i, k, iVar;
printf( "Realization of %d-input majority using %d MAJ3 gates:\n", p->nVars, p->nNodes );
- for ( i = p->nVars + 2; i < p->nObjs; i++ )
+// for ( i = p->nVars + 2; i < p->nObjs; i++ )
+ for ( i = p->nObjs - 1; i >= p->nVars + 2; i-- )
{
printf( "%02d = MAJ(", i-2 );
- for ( k = 0; k < 3; k++ )
+ for ( k = 2; k >= 0; k-- )
{
iVar = Maj_ManFindFanin( p, i, k );
if ( iVar >= 2 && iVar < p->nVars + 2 )
@@ -335,11 +345,11 @@ int Maj_ManAddCnf( Maj_Man_t * p, int iMint )
p->iVar += 4*p->nNodes;
return 1;
}
-void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose )
+void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fUseLine, int fVerbose )
{
int i, iMint = 0;
abctime clkTotal = Abc_Clock();
- Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst );
+ Maj_Man_t * p = Maj_ManAlloc( nVars, nNodes, fUseConst, fUseLine );
int status = Maj_ManAddCnfStart( p );
assert( status );
printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", p->nVars, p->nNodes );
@@ -355,7 +365,7 @@ void Maj_ManExactSynthesis( int nVars, int nNodes, int fUseConst, int fVerbose )
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
printf( " Var =%5d ", p->iVar );
printf( "Cla =%6d ", bmcg_sat_solver_clausenum(p->pSat) );
- printf( "Conf =%8d ", bmcg_sat_solver_conflictnum(p->pSat) );
+ printf( "Conf =%9d ", bmcg_sat_solver_conflictnum(p->pSat) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
if ( status == GLUCOSE_UNSAT )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 03:00:03 +0000