mirror of https://github.com/YosysHQ/abc.git
Special BLIF writing.
This commit is contained in:
parent
ef6778b8fe
commit
26fb1fcd14
|
|
@ -837,6 +837,7 @@ extern ABC_DLL char * Abc_SopEncoderLog( Mem_Flex_t * pMan, int iBit
|
|||
extern ABC_DLL char * Abc_SopDecoderPos( Mem_Flex_t * pMan, int nValues );
|
||||
extern ABC_DLL char * Abc_SopDecoderLog( Mem_Flex_t * pMan, int nValues );
|
||||
extern ABC_DLL word Abc_SopToTruth( char * pSop, int nInputs );
|
||||
extern ABC_DLL void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] );
|
||||
/*=== abcStrash.c ==========================================================*/
|
||||
extern ABC_DLL Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, int fAllNodes, int fCleanup, int fRecord );
|
||||
extern ABC_DLL Abc_Obj_t * Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int fRecord );
|
||||
|
|
|
|||
|
|
@ -1201,6 +1201,66 @@ word Abc_SopToTruth( char * pSop, int nInputs )
|
|||
return Result;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Computes truth table of the node.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Abc_SopToTruth7( char * pSop, int nInputs, word r[2] )
|
||||
{
|
||||
static word Truth[7][2] = {
|
||||
{0xAAAAAAAAAAAAAAAA,0xAAAAAAAAAAAAAAAA},
|
||||
{0xCCCCCCCCCCCCCCCC,0xCCCCCCCCCCCCCCCC},
|
||||
{0xF0F0F0F0F0F0F0F0,0xF0F0F0F0F0F0F0F0},
|
||||
{0xFF00FF00FF00FF00,0xFF00FF00FF00FF00},
|
||||
{0xFFFF0000FFFF0000,0xFFFF0000FFFF0000},
|
||||
{0xFFFFFFFF00000000,0xFFFFFFFF00000000},
|
||||
{0x0000000000000000,0xFFFFFFFFFFFFFFFF},
|
||||
};
|
||||
word Cube[2];
|
||||
int v, lit = 0;
|
||||
int nVars = Abc_SopGetVarNum(pSop);
|
||||
assert( nVars >= 0 && nVars <= 7 );
|
||||
assert( nVars == nInputs );
|
||||
r[0] = r[1] = 0;
|
||||
do {
|
||||
Cube[0] = Cube[1] = ~0;
|
||||
for ( v = 0; v < nVars; v++, lit++ )
|
||||
{
|
||||
if ( pSop[lit] == '1' )
|
||||
{
|
||||
Cube[0] &= Truth[v][0];
|
||||
Cube[1] &= Truth[v][1];
|
||||
}
|
||||
else if ( pSop[lit] == '0' )
|
||||
{
|
||||
Cube[0] &= ~Truth[v][0];
|
||||
Cube[1] &= ~Truth[v][1];
|
||||
}
|
||||
else if ( pSop[lit] != '-' )
|
||||
assert( 0 );
|
||||
}
|
||||
r[0] |= Cube[0];
|
||||
r[1] |= Cube[1];
|
||||
assert( pSop[lit] == ' ' );
|
||||
lit++;
|
||||
lit++;
|
||||
assert( pSop[lit] == '\n' );
|
||||
lit++;
|
||||
} while ( pSop[lit] );
|
||||
if ( Abc_SopIsComplement(pSop) )
|
||||
{
|
||||
r[0] = ~r[0];
|
||||
r[1] = ~r[1];
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
|
|
|
|||
|
|
@ -8553,6 +8553,29 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Gia_Man_t * pGia = Abc_ManReadAig( "bug\\61\\tmp.out", "aig:" );
|
||||
Gia_ManStop( pGia );
|
||||
}
|
||||
*/
|
||||
/*
|
||||
{
|
||||
extern void Abc_BddTest( Aig_Man_t * pAig, int fNew );
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
|
||||
Abc_BddTest( pAig, fVeryVerbose );
|
||||
Aig_ManStop( pAig );
|
||||
}
|
||||
*/
|
||||
/*
|
||||
{
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
extern Abc_Cex_t * Saig_PhaseTranslateCex( Aig_Man_t * p, Abc_Cex_t * pCex );
|
||||
if ( pAbc->pCex && pNtk )
|
||||
{
|
||||
Abc_Cex_t * pNew;
|
||||
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
pNew = Saig_PhaseTranslateCex( pAig, pAbc->pCex );
|
||||
Aig_ManStop( pAig );
|
||||
Abc_FrameReplaceCex( pAbc, &pNew );
|
||||
}
|
||||
}
|
||||
*/
|
||||
return 0;
|
||||
usage:
|
||||
|
|
|
|||
|
|
@ -1533,13 +1533,16 @@ usage:
|
|||
int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
|
||||
{
|
||||
char * pFileName;
|
||||
int c;
|
||||
int c, fSpecial = 0;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "jh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'j':
|
||||
fSpecial ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
|
|
@ -1556,12 +1559,16 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
// get the output file name
|
||||
pFileName = argv[globalUtilOptind];
|
||||
// call the corresponding file writer
|
||||
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
|
||||
// if ( fSpecial )
|
||||
// Io_WriteBlifSpecial( pAbc->pNtkCur, pFileName );
|
||||
// else
|
||||
Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_BLIF );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: write_blif [-h] <file>\n" );
|
||||
fprintf( pAbc->Err, "usage: write_blif [-jh] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t writes the network into a BLIF file\n" );
|
||||
fprintf( pAbc->Err, "\t-j : enables special BLIF writing [default = %s]\n", fSpecial? "yes" : "no" );;
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .blif)\n" );
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -105,6 +105,7 @@ extern void Io_WriteBblif( Abc_Ntk_t * pNtk, char * pFileName );
|
|||
extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches );
|
||||
extern void Io_WriteBlif( Abc_Ntk_t * pNtk, char * pFileName, int fWriteLatches, int fBb2Wb, int fSeq );
|
||||
extern void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk );
|
||||
extern void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName );
|
||||
/*=== abcWriteBlifMv.c ==========================================================*/
|
||||
extern void Io_WriteBlifMv( Abc_Ntk_t * pNtk, char * FileName );
|
||||
/*=== abcWriteBench.c =========================================================*/
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@
|
|||
#include "ioAbc.h"
|
||||
#include "main.h"
|
||||
#include "mio.h"
|
||||
#include "kit.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
|
|
@ -624,6 +625,248 @@ void Abc_NtkConvertBb2Wb( char * pFileNameIn, char * pFileNameOut, int fSeq, int
|
|||
Abc_NtkDelete( pNetlist );
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Transforms truth table into an SOP.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
char * Io_NtkDeriveSop( Mem_Flex_t * pMem, unsigned uTruth, int nVars )
|
||||
{
|
||||
char * pSop;
|
||||
Vec_Int_t * vCover = Vec_IntAlloc( 100 );
|
||||
int RetValue = Kit_TruthIsop( &uTruth, nVars, vCover, 1 );
|
||||
assert( RetValue == 0 || RetValue == 1 );
|
||||
// check the case of constant cover
|
||||
assert( !(Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0)) );
|
||||
// derive the AIG for that tree
|
||||
pSop = Abc_SopCreateFromIsop( pMem, nVars, vCover );
|
||||
if ( RetValue )
|
||||
Abc_SopComplement( pSop );
|
||||
Vec_IntFree( vCover );
|
||||
return pSop;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the node into a file.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_NtkWriteNodeInt( FILE * pFile, Abc_Obj_t * pNode )
|
||||
{
|
||||
Abc_Obj_t * pNet;
|
||||
int i, nVars = Abc_ObjFaninNum(pNode);
|
||||
if ( nVars > 7 )
|
||||
{
|
||||
printf( "Node \"%s\" has more than 7 inputs. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
return;
|
||||
}
|
||||
if ( nVars <= 4 )
|
||||
{
|
||||
// write the .names line
|
||||
fprintf( pFile, ".names" );
|
||||
Abc_ObjForEachFanin( pNode, pNet, i )
|
||||
fprintf( pFile, " %s", Abc_ObjName(pNet) );
|
||||
// get the output name
|
||||
fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
// write the cubes
|
||||
fprintf( pFile, "%s", (char*)Abc_ObjData(pNode) );
|
||||
}
|
||||
else
|
||||
{
|
||||
extern int If_Dec6PickBestMux( word t, word Cofs[2] );
|
||||
extern int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] );
|
||||
extern word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars );
|
||||
extern void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars );
|
||||
extern word If_Dec6Perform( word t, int fDerive );
|
||||
extern word If_Dec7Perform( word t[2], int fDerive );
|
||||
|
||||
char * pSop;
|
||||
word z, uTruth6, uTruth7[2], Cofs6[2], Cofs7[2][2];
|
||||
int c, iVar, nVarsMin[2], pVars[2][10];
|
||||
|
||||
// collect variables
|
||||
Abc_ObjForEachFanin( pNode, pNet, i )
|
||||
pVars[0][i] = pVars[1][i] = i;
|
||||
|
||||
// derive truth table
|
||||
if ( nVars == 7 )
|
||||
{
|
||||
Abc_SopToTruth7( (char*)Abc_ObjData(pNode), nVars, uTruth7 );
|
||||
iVar = If_Dec7PickBestMux( uTruth7, Cofs7[0], Cofs7[1] );
|
||||
}
|
||||
else
|
||||
{
|
||||
uTruth6 = Abc_SopToTruth( (char*)Abc_ObjData(pNode), nVars );
|
||||
iVar = If_Dec6PickBestMux( uTruth6, Cofs6 );
|
||||
}
|
||||
// perform MUX decomposition
|
||||
if ( iVar >= 0 )
|
||||
{
|
||||
if ( nVars == 7 )
|
||||
{
|
||||
If_Dec7MinimumBase( Cofs7[0], pVars[0], nVars, &nVarsMin[0] );
|
||||
If_Dec7MinimumBase( Cofs7[1], pVars[1], nVars, &nVarsMin[1] );
|
||||
}
|
||||
else
|
||||
{
|
||||
Cofs6[0] = If_Dec6MinimumBase( Cofs6[0], pVars[0], nVars, &nVarsMin[0] );
|
||||
Cofs6[1] = If_Dec6MinimumBase( Cofs6[1], pVars[1], nVars, &nVarsMin[1] );
|
||||
}
|
||||
assert( nVarsMin[0] < 5 );
|
||||
assert( nVarsMin[1] < 5 );
|
||||
// write cofactors
|
||||
for ( c = 0; c < 2; c++ )
|
||||
{
|
||||
pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc,
|
||||
(unsigned)(nVars == 7 ? Cofs7[c][0] : Cofs6[c]), nVarsMin[c] );
|
||||
fprintf( pFile, ".names" );
|
||||
for ( i = 0; i < nVarsMin[c]; i++ )
|
||||
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
|
||||
fprintf( pFile, " %s_cascade%d\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c );
|
||||
fprintf( pFile, "%s", pSop );
|
||||
}
|
||||
// write MUX
|
||||
fprintf( pFile, ".names" );
|
||||
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,iVar)) );
|
||||
fprintf( pFile, " %s_cascade0", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
fprintf( pFile, " %s_cascade1", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
fprintf( pFile, " %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
fprintf( pFile, "1-1 1\n01- 1\n" );
|
||||
return;
|
||||
}
|
||||
|
||||
// try cascade decomposition
|
||||
if ( nVars == 7 )
|
||||
z = If_Dec7Perform( uTruth7, 1 );
|
||||
else
|
||||
z = If_Dec6Perform( uTruth6, 1 );
|
||||
if ( z == 0 )
|
||||
{
|
||||
printf( "Node \"%s\" is not decomposable. Writing BLIF has failed.\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
return;
|
||||
}
|
||||
|
||||
// collect the nodes
|
||||
for ( c = 0; c < 2; i++ )
|
||||
{
|
||||
uTruth7[c] = ((c ? z >> 32 : z) & 0xffff);
|
||||
uTruth7[c] |= (uTruth7[c] << 16);
|
||||
uTruth7[c] |= (uTruth7[c] << 32);
|
||||
for ( i = 0; i < 4; i++ )
|
||||
pVars[c][i] = (z >> (c*32+16+4*i)) & 7;
|
||||
|
||||
// minimize truth table
|
||||
Cofs6[i] = If_Dec6MinimumBase( uTruth7[i], pVars[i], 4, &nVarsMin[i] );
|
||||
assert( c ? nVarsMin[0] == 4 : nVarsMin[1] <= 4 );
|
||||
|
||||
// write the nodes
|
||||
pSop = Io_NtkDeriveSop( (Mem_Flex_t *)Abc_ObjNtk(pNode)->pManFunc, (unsigned)Cofs6[c], nVarsMin[c] );
|
||||
fprintf( pFile, ".names" );
|
||||
for ( i = 0; i < nVarsMin[c]; i++ )
|
||||
if ( pVars[c][i] == 7 )
|
||||
fprintf( pFile, " %s_cascade", Abc_ObjName(Abc_ObjFanout0(pNode)) );
|
||||
else
|
||||
fprintf( pFile, " %s", Abc_ObjName(Abc_ObjFanin(pNode,pVars[c][i])) );
|
||||
fprintf( pFile, " %s%s\n", Abc_ObjName(Abc_ObjFanout0(pNode)), c? "_cascade" : "" );
|
||||
fprintf( pFile, "%s", pSop );
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the network into a BLIF file with the given name.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_WriteBlifInt( Abc_Ntk_t * pNtk, char * FileName )
|
||||
{
|
||||
FILE * pFile;
|
||||
Abc_Obj_t * pNode, * pLatch;
|
||||
int i;
|
||||
assert( Abc_NtkIsNetlist(pNtk) );
|
||||
// start writing the file
|
||||
pFile = fopen( FileName, "w" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
fprintf( stdout, "Io_WriteBlifInt(): Cannot open the output file.\n" );
|
||||
return;
|
||||
}
|
||||
fprintf( pFile, "# Benchmark \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() );
|
||||
// write the model name
|
||||
fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
|
||||
// write the PIs
|
||||
fprintf( pFile, ".inputs" );
|
||||
Io_NtkWritePis( pFile, pNtk, 1 );
|
||||
fprintf( pFile, "\n" );
|
||||
// write the POs
|
||||
fprintf( pFile, ".outputs" );
|
||||
Io_NtkWritePos( pFile, pNtk, 1 );
|
||||
fprintf( pFile, "\n" );
|
||||
// write the latches
|
||||
if ( Abc_NtkLatchNum(pNtk) )
|
||||
fprintf( pFile, "\n" );
|
||||
Abc_NtkForEachLatch( pNtk, pLatch, i )
|
||||
Io_NtkWriteLatch( pFile, pLatch );
|
||||
if ( Abc_NtkLatchNum(pNtk) )
|
||||
fprintf( pFile, "\n" );
|
||||
// write each internal node
|
||||
Abc_NtkForEachNode( pNtk, pNode, i )
|
||||
Io_NtkWriteNodeInt( pFile, pNode );
|
||||
// write the end
|
||||
fprintf( pFile, ".end\n\n" );
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Write the network into a BLIF file with the given name.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Io_WriteBlifSpecial( Abc_Ntk_t * pNtk, char * FileName )
|
||||
{
|
||||
Abc_Ntk_t * pNtkTemp;
|
||||
assert( Abc_NtkIsLogic(pNtk) );
|
||||
Abc_NtkToSop( pNtk, 0 );
|
||||
// derive the netlist
|
||||
pNtkTemp = Abc_NtkToNetlist(pNtk);
|
||||
if ( pNtkTemp == NULL )
|
||||
{
|
||||
fprintf( stdout, "Writing BLIF has failed.\n" );
|
||||
return;
|
||||
}
|
||||
Io_WriteBlifInt( pNtkTemp, FileName );
|
||||
Abc_NtkDelete( pNtkTemp );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -390,6 +390,14 @@ static inline int If_Dec6HasVar( word t, int v )
|
|||
{
|
||||
return ((t & Truth6[v]) >> (1<<v)) != (t & ~Truth6[v]);
|
||||
}
|
||||
static inline int If_Dec7HasVar( word t[2], int v )
|
||||
{
|
||||
assert( v >= 0 && v < 7 );
|
||||
if ( v == 6 )
|
||||
return t[0] != t[1];
|
||||
return ((t[0] & Truth6[v]) >> (1<<v)) != (t[0] & ~Truth6[v])
|
||||
|| ((t[1] & Truth6[v]) >> (1<<v)) != (t[1] & ~Truth6[v]);
|
||||
}
|
||||
|
||||
static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
|
||||
{
|
||||
|
|
@ -397,7 +405,7 @@ static inline void If_DecVerifyPerm( int Pla2Var[6], int Var2Pla[6] )
|
|||
for ( i = 0; i < 6; i++ )
|
||||
assert( Pla2Var[Var2Pla[i]] == i );
|
||||
}
|
||||
static word If_Dec6Perform( word t, int fDerive )
|
||||
word If_Dec6Perform( word t, int fDerive )
|
||||
{
|
||||
word r = 0;
|
||||
int i, v, u, x, Count, Pla2Var[6], Var2Pla[6];
|
||||
|
|
@ -437,7 +445,7 @@ static word If_Dec6Perform( word t, int fDerive )
|
|||
assert( i == 15 );
|
||||
return r;
|
||||
}
|
||||
static word If_Dec7Perform( word t0[2], int fDerive )
|
||||
word If_Dec7Perform( word t0[2], int fDerive )
|
||||
{
|
||||
word t[2] = {t0[0], t0[1]};
|
||||
int i, v, u, y, Pla2Var[7], Var2Pla[7];
|
||||
|
|
@ -468,6 +476,190 @@ static word If_Dec7Perform( word t0[2], int fDerive )
|
|||
}
|
||||
|
||||
|
||||
// support minimization
|
||||
static inline int If_DecSuppIsMinBase( int Supp )
|
||||
{
|
||||
return (Supp & (Supp+1)) == 0;
|
||||
}
|
||||
static inline word If_Dec6TruthShrink( word uTruth, int nVars, int nVarsAll, unsigned Phase )
|
||||
{
|
||||
int i, k, Var = 0;
|
||||
assert( nVarsAll <= 6 );
|
||||
for ( i = 0; i < nVarsAll; i++ )
|
||||
if ( Phase & (1 << i) )
|
||||
{
|
||||
for ( k = i-1; k >= Var; k-- )
|
||||
uTruth = If_Dec6SwapAdjacent( uTruth, k );
|
||||
Var++;
|
||||
}
|
||||
assert( Var == nVars );
|
||||
return uTruth;
|
||||
}
|
||||
word If_Dec6MinimumBase( word uTruth, int * pSupp, int nVarsAll, int * pnVars )
|
||||
{
|
||||
int v, iVar = 0, uSupp = 0;
|
||||
assert( nVarsAll <= 6 );
|
||||
for ( v = 0; v < nVarsAll; v++ )
|
||||
if ( If_Dec6HasVar( uTruth, v ) )
|
||||
{
|
||||
uSupp |= (1 << v);
|
||||
if ( pSupp )
|
||||
pSupp[iVar] = pSupp[v];
|
||||
iVar++;
|
||||
}
|
||||
if ( pnVars )
|
||||
*pnVars = iVar;
|
||||
if ( If_DecSuppIsMinBase( uSupp ) )
|
||||
return uTruth;
|
||||
return If_Dec6TruthShrink( uTruth, iVar, nVarsAll, uSupp );
|
||||
}
|
||||
|
||||
static inline void If_Dec7TruthShrink( word uTruth[2], int nVars, int nVarsAll, unsigned Phase )
|
||||
{
|
||||
int i, k, Var = 0;
|
||||
assert( nVarsAll <= 7 );
|
||||
for ( i = 0; i < nVarsAll; i++ )
|
||||
if ( Phase & (1 << i) )
|
||||
{
|
||||
for ( k = i-1; k >= Var; k-- )
|
||||
If_Dec7SwapAdjacent( uTruth, k );
|
||||
Var++;
|
||||
}
|
||||
assert( Var == nVars );
|
||||
}
|
||||
void If_Dec7MinimumBase( word uTruth[2], int * pSupp, int nVarsAll, int * pnVars )
|
||||
{
|
||||
int v, iVar = 0, uSupp = 0;
|
||||
assert( nVarsAll <= 7 );
|
||||
for ( v = 0; v < nVarsAll; v++ )
|
||||
if ( If_Dec7HasVar( uTruth, v ) )
|
||||
{
|
||||
uSupp |= (1 << v);
|
||||
if ( pSupp )
|
||||
pSupp[iVar] = pSupp[v];
|
||||
iVar++;
|
||||
}
|
||||
if ( pnVars )
|
||||
*pnVars = iVar;
|
||||
if ( If_DecSuppIsMinBase( uSupp ) )
|
||||
return;
|
||||
If_Dec7TruthShrink( uTruth, iVar, nVarsAll, uSupp );
|
||||
}
|
||||
|
||||
|
||||
|
||||
// check for MUX decomposition
|
||||
static inline int If_Dec6SuppSize( word t )
|
||||
{
|
||||
int v, Count = 0;
|
||||
for ( v = 0; v < 6; v++ )
|
||||
if ( If_Dec6Cofactor(t, v, 0) != If_Dec6Cofactor(t, v, 1) )
|
||||
Count++;
|
||||
return Count;
|
||||
}
|
||||
static inline int If_Dec6CheckMux( word t )
|
||||
{
|
||||
int v;
|
||||
for ( v = 0; v < 6; v++ )
|
||||
if ( If_Dec6SuppSize(If_Dec6Cofactor(t, v, 0)) < 5 &&
|
||||
If_Dec6SuppSize(If_Dec6Cofactor(t, v, 1)) < 5 )
|
||||
return v;
|
||||
return -1;
|
||||
}
|
||||
|
||||
// check for MUX decomposition
|
||||
static inline void If_Dec7Cofactor( word t[2], int iVar, int fCof1, word r[2] )
|
||||
{
|
||||
assert( iVar >= 0 && iVar < 7 );
|
||||
if ( iVar == 6 )
|
||||
{
|
||||
if ( fCof1 )
|
||||
r[0] = r[1] = t[1];
|
||||
else
|
||||
r[0] = r[1] = t[0];
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( fCof1 )
|
||||
{
|
||||
r[0] = (t[0] & Truth6[iVar]) | ((t[0] & Truth6[iVar]) >> (1<<iVar));
|
||||
r[1] = (t[1] & Truth6[iVar]) | ((t[1] & Truth6[iVar]) >> (1<<iVar));
|
||||
}
|
||||
else
|
||||
{
|
||||
r[0] = (t[0] &~Truth6[iVar]) | ((t[0] &~Truth6[iVar]) << (1<<iVar));
|
||||
r[1] = (t[1] &~Truth6[iVar]) | ((t[1] &~Truth6[iVar]) << (1<<iVar));
|
||||
}
|
||||
}
|
||||
}
|
||||
static inline int If_Dec7SuppSize( word t[2] )
|
||||
{
|
||||
word c0[2], c1[2];
|
||||
int v, Count = 0;
|
||||
for ( v = 0; v < 7; v++ )
|
||||
{
|
||||
If_Dec7Cofactor( t, v, 0, c0 );
|
||||
If_Dec7Cofactor( t, v, 1, c1 );
|
||||
if ( c0[0] != c1[0] || c0[1] != c1[1] )
|
||||
Count++;
|
||||
}
|
||||
return Count;
|
||||
}
|
||||
static inline int If_Dec7CheckMux( word t[2] )
|
||||
{
|
||||
word c0[2], c1[2];
|
||||
int v;
|
||||
for ( v = 0; v < 7; v++ )
|
||||
{
|
||||
If_Dec7Cofactor( t, v, 0, c0 );
|
||||
If_Dec7Cofactor( t, v, 1, c1 );
|
||||
if ( If_Dec7SuppSize(c0) < 5 && If_Dec7SuppSize(c1) < 5 )
|
||||
return v;
|
||||
}
|
||||
return -1;
|
||||
}
|
||||
|
||||
// find the best MUX decomposition
|
||||
int If_Dec6PickBestMux( word t, word Cofs[2] )
|
||||
{
|
||||
int v, vBest = -1, Count0, Count1, CountBest = 1000;
|
||||
for ( v = 0; v < 6; v++ )
|
||||
{
|
||||
Count0 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 0) );
|
||||
Count1 = If_Dec6SuppSize( If_Dec6Cofactor(t, v, 1) );
|
||||
if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
|
||||
{
|
||||
CountBest = Count0 + Count1;
|
||||
vBest = v;
|
||||
Cofs[0] = If_Dec6Cofactor(t, v, 0);
|
||||
Cofs[1] = If_Dec6Cofactor(t, v, 1);
|
||||
}
|
||||
}
|
||||
return vBest;
|
||||
}
|
||||
int If_Dec7PickBestMux( word t[2], word c0r[2], word c1r[2] )
|
||||
{
|
||||
word c0[2], c1[2];
|
||||
int v, vBest = -1, Count0, Count1, CountBest = 1000;
|
||||
for ( v = 0; v < 6; v++ )
|
||||
{
|
||||
If_Dec7Cofactor( t, v, 0, c0 );
|
||||
If_Dec7Cofactor( t, v, 1, c1 );
|
||||
Count0 = If_Dec7SuppSize(c0);
|
||||
Count1 = If_Dec7SuppSize(c1);
|
||||
if ( Count0 < 5 && Count1 < 5 && CountBest > Count0 + Count1 )
|
||||
{
|
||||
CountBest = Count0 + Count1;
|
||||
vBest = v;
|
||||
c0r[0] = c0[0]; c0r[1] = c0[1];
|
||||
c1r[0] = c1[0]; c1r[1] = c1[1];
|
||||
}
|
||||
}
|
||||
return vBest;
|
||||
}
|
||||
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs additional check.]
|
||||
|
|
@ -486,17 +678,21 @@ int If_CutPerformCheckInt( unsigned * pTruth, int nVars, int nLeaves )
|
|||
return 1;
|
||||
if ( nLeaves == 6 )
|
||||
{
|
||||
word t = ((word *)pTruth)[0];
|
||||
word z = If_Dec6Perform( t, fDerive );
|
||||
word z, t = ((word *)pTruth)[0];
|
||||
if ( If_Dec6CheckMux(t) >= 0 )
|
||||
return 1;
|
||||
z = If_Dec6Perform( t, fDerive );
|
||||
if ( fDerive && z )
|
||||
If_Dec6Verify( t, z );
|
||||
return z != 0;
|
||||
}
|
||||
if ( nLeaves == 7 )
|
||||
{
|
||||
word t[2], z;
|
||||
word z, t[2];
|
||||
t[0] = ((word *)pTruth)[0];
|
||||
t[1] = ((word *)pTruth)[1];
|
||||
if ( If_Dec7CheckMux(t) >= 0 )
|
||||
return 1;
|
||||
z = If_Dec7Perform( t, fDerive );
|
||||
if ( fDerive && z )
|
||||
If_Dec7Verify( t, z );
|
||||
|
|
|
|||
Loading…
Reference in New Issue