luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Merge remote-tracking branch 'upstream/master' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2026-03-27 08:39:51 +01:00
parent b4a657e75b 6aaf0db1e1
commit de0ebae1c5
19 changed files with 1176 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -4510,6 +4510,10 @@ SOURCE=.\src\map\if\ifUtil.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifTrace.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifDecJ.c
# End Source File
# End Group

69
src/aig/gia/giaIf.c
View File

@ -1190,7 +1190,7 @@ int Gia_ManFromIfLogicCreateLutSpecialJ( Gia_Man_t * pNew, word * pRes, Vec_Int_
{
word Truth;
int i, iObjLit1, iObjLit2, iObjLit3;
word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1 );
word z = If_CutPerformDeriveJ( NULL, (unsigned *)pRes, Vec_IntSize(vLeaves), Vec_IntSize(vLeaves), NULL, 1, 0 );
assert( z != 0 );
if ( ((z >> 63) & 1) == 0 )
{
@ -2124,6 +2124,24 @@ void Gia_ManConfigPrint2( unsigned char * pConfigData, int nLeaves )
}
}
static inline word Gia_ManFromIfPermuteTruth4( word Truth, int nLeaves, word z )
{
word TruthNew = 0;
int i, k, x;
assert( nLeaves >= 1 && nLeaves <= 4 );
for ( i = 0; i < 16; i++ )
{
x = 0;
for ( k = 0; k < nLeaves; k++ )
{
int v = (int)((z >> (2 * k)) & 3);
x |= ((i >> k) & 1) << v;
}
TruthNew |= ((Truth >> x) & 1) << i;
}
return TruthNew;
}
/**Function*************************************************************
Synopsis [Derive configurations.]
@ -2135,33 +2153,42 @@ void Gia_ManConfigPrint2( unsigned char * pConfigData, int nLeaves )
SeeAlso []
***********************************************************************/
void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves )
void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves, int fDelay )
{
int i, CellId;
int startPos = Vec_StrSize(vConfigs2);
If_LibCell_t * pCellLib = pIfMan && pIfMan->pPars ? pIfMan->pPars->pCellLib : NULL;
assert( pCellLib != NULL );
// Determine cell type based on the number of leaves and configuration
if ( nLeaves <= 4 ) // 7 bytes = 1 byte CellId + 4 bytes mapping + 2 bytes truth table
{
word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1, fDelay );
int fHavePerm = (z != 0) && ((z & ABC_CONST(0x4000000000000000)) != 0);
word Truth = pTruth[0];
// Cell type 0: Simple LUT4
CellId = 0;
// Write CellId
Vec_StrPush( vConfigs2, (char)CellId );
// Write mapping
for ( i = 0; i < nLeaves; i++ )
Vec_StrPush( vConfigs2, 2+i );
{
int v = fHavePerm ? (int)((z >> (2 * i)) & 3) : i;
Vec_StrPush( vConfigs2, 2 + v );
}
for ( ; i < 4; i++ )
Vec_StrPush( vConfigs2, 0 );
// Write truth table (16 bits for LUT4)
word Truth = pTruth[0];
if ( fHavePerm )
Truth = Gia_ManFromIfPermuteTruth4( Truth, nLeaves, z );
Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) );
assert( startPos + 7 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
//Gia_ManConfigPrint( Truth, 0, nLeaves );
}
else // 12 bytes = 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
{
word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1 );
word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1, fDelay );
//Gia_ManConfigPrint( 0, z, nLeaves );
if ( ((z >> 63) & 1) == 0 )
{
@ -2201,7 +2228,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 12 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
}
else // 14 bytes = 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
{
@ -2226,7 +2253,7 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 14 == Vec_StrSize(vConfigs2) );
assert( startPos + pCellLib->pCellRecordSizes[CellId] == Vec_StrSize(vConfigs2) );
}
}
if ( pIfMan->pPars->fVerboseTrace )
@ -2551,7 +2578,16 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLeaves), k );
if ( Abc_LitIsCompl(pIfObj->iCopy) ^ pCutBest->fCompl )
Abc_TtNot( pTruth, Abc_TtWordNum(pCutBest->nLeaves) );
Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pTruth, pCutBest->nLeaves );
if ( pIfMan->pPars->fDelayOptCell )
{
pIfMan->nCutLeavesCur = pCutBest->nLeaves;
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
{
pIfMan->pCutLeavesCur[k] = pIfLeaf->Id;
pIfMan->pCutLeafArrCur[k] = If_ObjCutBest(pIfLeaf)->Delay;
}
}
Gia_ManFromIfGetConfig2( vConfigs2, pIfMan, pTruth, pCutBest->nLeaves, pIfMan->pPars->fDelayOptCell );
}
}
else
@ -2964,6 +3000,20 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
pPars->pTimesReq[i] = EntryF;
}
*/
if ( p->pManTime && pPars->pTimesArr == NULL )
{
Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
pPars->pTimesArr = ABC_CALLOC( float, Gia_ManCiNum(p) );
for ( i = 0; i < Gia_ManCiNum(p); i++ )
pPars->pTimesArr[i] = Tim_ManGetCiArrival( pManTime, i );
}
if ( p->pManTime && pPars->pTimesReq == NULL )
{
Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
pPars->pTimesReq = ABC_CALLOC( float, Gia_ManCoNum(p) );
for ( i = 0; i < Gia_ManCoNum(p); i++ )
pPars->pTimesReq[i] = Tim_ManGetCoRequired( pManTime, i );
}
ABC_FREE( p->pCellStr );
Vec_IntFreeP( &p->vConfigs );
Vec_StrFreeP( &p->vConfigs2 );
@ -3337,4 +3387,3 @@ Gia_Man_t * Gia_ManDupUnhashMapping( Gia_Man_t * p )
ABC_NAMESPACE_IMPL_END

98
src/aig/gia/giaSpeedup.c
View File

@ -33,6 +33,53 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
static int Gia_ManConfig2GetBytePos( Gia_Man_t * p, int iObj, If_LibCell_t * pCellLib )
{
int iLut, bytePos = 0;
if ( p == NULL || p->vConfigs2 == NULL || pCellLib == NULL )
return -1;
Gia_ManForEachLut( p, iLut )
{
unsigned char CellId;
int nRecordSize;
if ( bytePos >= Vec_StrSize(p->vConfigs2) )
return -1;
if ( iLut == iObj )
return bytePos;
CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos );
if ( CellId >= IF_MAX_LUTSIZE )
return -1;
nRecordSize = pCellLib->pCellRecordSizes[CellId];
if ( nRecordSize <= 0 )
return -1;
bytePos += nRecordSize;
}
return -1;
}
int Gia_ManConfig2DerivePinDelays( Gia_Man_t * p, int iObj, If_LibCell_t * pCellLib, int * pPinDelay, int nLutSize )
{
int bytePos, i, nPins;
unsigned char CellId;
if ( pCellLib == NULL || pPinDelay == NULL || nLutSize < 1 || nLutSize > 32 )
return 0;
for ( i = 0; i < nLutSize; i++ )
pPinDelay[i] = 1;
bytePos = Gia_ManConfig2GetBytePos( p, iObj, pCellLib );
if ( bytePos < 0 || bytePos >= Vec_StrSize(p->vConfigs2) )
return 0;
CellId = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos );
if ( CellId >= pCellLib->nCellNum )
return 0;
nPins = Abc_MinInt( pCellLib->nCellInputs[CellId], 9 );
for ( i = 0; i < nPins; i++ )
{
int v = (unsigned char)Vec_StrEntry( p->vConfigs2, bytePos + 1 + i );
if ( v >= 2 && v < 2 + nLutSize )
pPinDelay[v - 2] = Abc_MaxInt( pPinDelay[v - 2], pCellLib->pCellPinDelays[CellId][i] );
}
return 1;
}
/**Function*************************************************************
Synopsis [Sorts the pins in the decreasing order of delays.]
@ -113,7 +160,7 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting )
If_LibLut_t * pLutLib = (If_LibLut_t *)p->pLutLib;
If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib;
Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
int k, iFanin, pPinPerm[32];
int k, iFanin, pPinPerm[32], pPinDelay[32];
float pPinDelays[32];
float tArrival, * pDelays;
if ( Gia_ObjIsCi(pObj) )
@ -132,15 +179,17 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting )
{
// Handle cell library delays (use integer delays directly)
int nLutSize = Gia_ObjLutSize(p, iObj);
int fHaveCfg2 = Gia_ManConfig2DerivePinDelays( p, iObj, pCellLib, pPinDelay, nLutSize );
// Find matching cell (simple approach: use first cell with enough inputs)
int cellId = -1;
int i;
for ( i = 0; i < pCellLib->nCellNum; i++ )
if ( pCellLib->nCellInputs[i] >= nLutSize )
{
cellId = i;
break;
}
if ( !fHaveCfg2 )
for ( i = 0; i < pCellLib->nCellNum; i++ )
if ( pCellLib->nCellInputs[i] >= nLutSize )
{
cellId = i;
break;
}
if ( cellId >= 0 )
{
// Use cell delays as integers from the library
@ -151,6 +200,15 @@ float Gia_ObjComputeArrival( Gia_Man_t * p, int iObj, int fUseSorting )
tArrival = Gia_ObjTimeArrival(p, iFanin) + delay;
}
}
else if ( fHaveCfg2 )
{
Gia_LutForEachFanin( p, iObj, iFanin, k )
{
float delay = (float)pPinDelay[k];
if ( tArrival < Gia_ObjTimeArrival(p, iFanin) + delay )
tArrival = Gia_ObjTimeArrival(p, iFanin) + delay;
}
}
else
{
// Fall back to default delay if no matching cell
@ -204,7 +262,7 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting )
{
If_LibLut_t * pLutLib = (If_LibLut_t *)p->pLutLib;
If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib;
int k, iFanin, pPinPerm[32];
int k, iFanin, pPinPerm[32], pPinDelay[32];
float pPinDelays[32];
float tRequired = 0.0; // Suppress "might be used uninitialized"
float * pDelays;
@ -223,15 +281,17 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting )
{
// Handle cell library delays (use integer delays directly)
int nLutSize = Gia_ObjLutSize(p, iObj);
int fHaveCfg2 = Gia_ManConfig2DerivePinDelays( p, iObj, pCellLib, pPinDelay, nLutSize );
// Find matching cell (simple approach: use first cell with enough inputs)
int cellId = -1;
int i;
for ( i = 0; i < pCellLib->nCellNum; i++ )
if ( pCellLib->nCellInputs[i] >= nLutSize )
{
cellId = i;
break;
}
if ( !fHaveCfg2 )
for ( i = 0; i < pCellLib->nCellNum; i++ )
if ( pCellLib->nCellInputs[i] >= nLutSize )
{
cellId = i;
break;
}
if ( cellId >= 0 )
{
// Use cell delays as integers from the library
@ -243,6 +303,15 @@ float Gia_ObjPropagateRequired( Gia_Man_t * p, int iObj, int fUseSorting )
Gia_ObjSetTimeRequired( p, iFanin, tRequired );
}
}
else if ( fHaveCfg2 )
{
Gia_LutForEachFanin( p, iObj, iFanin, k )
{
tRequired = Gia_ObjTimeRequired( p, iObj ) - (float)pPinDelay[k];
if ( Gia_ObjTimeRequired(p, iFanin) > tRequired )
Gia_ObjSetTimeRequired( p, iFanin, tRequired );
}
}
else
{
// Fall back to default delay if no matching cell
@ -977,4 +1046,3 @@ Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerb
ABC_NAMESPACE_IMPL_END

62
src/base/abci/abc.c
View File

@ -22286,7 +22286,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
If_ManSetDefaultPars( pPars );
pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYUZDEWSJqalepmrsdbgxyzuojiktncfvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRNTXYZUDEWSJqalepmrsdbgxyzuoiktncfvh" ) ) != EOF )
{
switch ( c )
{
@ -22536,9 +22536,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'o':
pPars->fUseBuffs ^= 1;
break;
case 'j':
pPars->fEnableCheck07 ^= 1;
break;
//case 'j':
// pPars->fEnableCheck07 ^= 1;
// break;
case 'i':
pPars->fUseCofVars ^= 1;
break;
@ -22868,7 +22868,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
Abc_Print( -2, "usage: if [-KCFAGRNTXYUZ num] [-DEW float] [-SJ str] [-qarlepmsdbgxyuojiktnczfvh]\n" );
Abc_Print( -2, "usage: if [-KCFAGRNTXYZMU num] [-DEW float] [-SJ str] [-qarlepmsdbgxyuoiktnczfvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@ -22902,7 +22902,7 @@ usage:
Abc_Print( -2, "\t-y : toggles delay optimization with recorded library [default = %s]\n", pPars->fUserRecLib? "yes": "no" );
Abc_Print( -2, "\t-u : toggles delay optimization with SAT-based library [default = %s]\n", pPars->fUserSesLib? "yes": "no" );
Abc_Print( -2, "\t-o : toggles using buffers to decouple combinational outputs [default = %s]\n", pPars->fUseBuffs? "yes": "no" );
Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
//Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
Abc_Print( -2, "\t-k : toggles matching based on precomputed DSD manager [default = %s]\n", pPars->fUseDsdTune? "yes": "no" );
Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
@ -44082,8 +44082,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_FrameSetLibLut( If_LibLutSetSimple( 6 ) );
}
pPars->pLutLib = (If_LibLut_t *)Abc_FrameReadLibLut();
pPars->pCellLib = (If_LibCell_t *)Abc_FrameReadLibCell();
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSJTXYZqalepmrsdbgxyofuijkztncvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSJTXYZMqalepmrsdbgxyofuijkztncvwh" ) ) != EOF )
{
switch ( c )
{
@ -44099,6 +44100,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
// if the LUT size is specified, disable library
pPars->pLutLib = NULL;
pPars->pCellLib = NULL;
break;
case 'C':
if ( globalUtilOptind >= argc )
@ -44188,6 +44190,21 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nAndDelay < 0 )
goto usage;
break;
case 'M':
{
int Value;
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by 0 or 1.\n" );
goto usage;
}
Value = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( Value < 0 || Value > 1 )
goto usage;
pPars->fDelayOptCell = Value;
break;
}
case 'D':
if ( globalUtilOptind >= argc )
{
@ -44364,6 +44381,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Auto-detected K=%d from cell library (max inputs).\n", nMaxInputs );
// Disable LUT library since we're using K from cell library
pPars->pLutLib = NULL;
pPars->pCellLib = pCellLib;
}
}
}
@ -44552,6 +44570,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutSize = 4;
}
if ( pPars->fEnableCheck07 )
pPars->nCutsMax = Abc_MaxInt( pPars->nCutsMax, 16 );
else
pPars->pCellLib = NULL;
// enable truth table computation if cut minimization is selected
if ( pPars->fCutMin || pPars->fDeriveLuts )
{
@ -44687,7 +44710,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
Abc_Print( -2, "usage: &if [-KCFAGRTXY num] [-DEW float] [-SJ str] [-qarlepmsdbgxyofuijkztnchvw]\n" );
Abc_Print( -2, "usage: &if [-KCFAGRTXYZM num] [-DEW float] [-SJ str] [-qarlepmsdbgxyofuijkztnchvw]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@ -44698,6 +44721,7 @@ usage:
Abc_Print( -2, "\t-T num : the type of LUT structures [default = any]\n", pPars->nStructType );
Abc_Print( -2, "\t-X num : delay of AND-gate in LUT library units [default = %d]\n", pPars->nAndDelay );
Abc_Print( -2, "\t-Y num : area of AND-gate in LUT library units [default = %d]\n", pPars->nAndArea );
Abc_Print( -2, "\t-M num : enables delay-driven decomposition [default = %d]\n", pPars->fDelayOptCell );
Abc_Print( -2, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );
Abc_Print( -2, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );
Abc_Print( -2, "\t-W float : sets wire delay between adjects LUTs [default = %f]\n", pPars->WireDelay );
@ -48600,22 +48624,13 @@ int Abc_CommandAbc9Trace( Abc_Frame_t * pAbc, int argc, char ** argv )
pAbc->pGia->pLutLib = fUseLutLib ? Abc_FrameReadLibLut() : NULL;
pAbc->pGia->pCellLib = fUseCellLib ? Abc_FrameReadLibCell() : NULL;
if ( pFileName )
{
// Dump the delay trace to file
Gia_ManDelayTraceDump( pAbc->pGia, (char *)pFileName );
}
else
{
// Print the delay trace to console
Gia_ManDelayTraceLutPrint( pAbc->pGia, fVerbose );
}
Gia_ManDelayTraceDump( pAbc->pGia, (char *)pFileName );
return 0;
usage:
Abc_Print( -2, "usage: &trace [-F file] [-lcvh]\n" );
Abc_Print( -2, "\t performs delay trace of LUT-mapped network\n" );
Abc_Print( -2, "\t-F file : dump the critical path to a file [default = console output]\n" );
Abc_Print( -2, "\t-F file : dump the critical path to a file [default = stdout]\n" );
Abc_Print( -2, "\t-l : toggle using LUT-library-delay model [default = %s]\n", fUseLutLib? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using cell-library-delay model [default = %s]\n", fUseCellLib? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" );
@ -51413,7 +51428,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
int c, nProcs = 6, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
int c, nProcs = 6, nProcsNew = 0, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF )
{
@ -51425,10 +51440,11 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
goto usage;
}
nProcs = atoi(argv[globalUtilOptind]);
nProcsNew = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nProcs <= 0 )
if ( nProcsNew <= 0 || nProcsNew > 6 )
goto usage;
nProcs = nProcsNew;
break;
case 'T':
if ( globalUtilOptind >= argc )
@ -51526,7 +51542,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: &sprove [-PTUW num] [-usvwh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-P num : the number of concurrent processes (1 <= num <= 6) [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 );

16
src/map/if/if.h
View File

@ -126,6 +126,7 @@ struct If_Par_t_
int fCutMin; // performs cut minimization by removing functionally reducdant variables
int fDelayOpt; // special delay optimization
int fDelayOptLut; // delay optimization for LUTs
int fDelayOptCell; // delay optimization for cells
int fDsdBalance; // special delay optimization
int fUserRecLib; // use recorded library
int fUserSesLib; // use SAT-based synthesis
@ -175,6 +176,7 @@ struct If_Par_t_
float FinalDelay; // final delay after mapping
float FinalArea; // final area after mapping
If_LibLut_t * pLutLib; // the LUT library
If_LibCell_t * pCellLib; // the cell library
float * pTimesArr; // arrival times
float * pTimesReq; // required times
int (* pFuncCost) (If_Man_t *, If_Cut_t *); // procedure to compute the user's cost of a cut
@ -201,6 +203,7 @@ struct If_LibCell_t_
char * pName; // the name of the LUT library
int nCellNum; // the number of cells in the library
int nCellInputs[IF_MAX_LUTSIZE];
int pCellRecordSizes[IF_MAX_LUTSIZE];
char * pCellNames[IF_MAX_LUTSIZE];
float pCellAreas[IF_MAX_LUTSIZE];
int pCellPinDelays[IF_MAX_LUTSIZE][IF_MAX_LUTSIZE];
@ -299,6 +302,14 @@ struct If_Man_t_
Vec_Int_t * vVisited2;
Vec_Int_t * vCuts;
Vec_Int_t * vCutCosts;
// current cut context for user callbacks
If_Obj_t * pCutObjCur; // current object whose cut is being checked
If_Cut_t * pCutCur; // current cut being checked
int nCutLeavesCur; // number of leaves in current cut
int pCutLeavesCur[IF_MAX_LUTSIZE]; // current cut leaves (IDs)
float pCutLeafArrCur[IF_MAX_LUTSIZE]; // current cut leaf arrivals
float CutDelayCur; // current cut delay returned by user callback
int fCutDelayCurValid; // indicates CutDelayCur is valid
// timing manager
Tim_Man_t * pManTim;
@ -319,6 +330,7 @@ struct If_Cut_t_
float Edge; // the edge flow
float Power; // the power flow
float Delay; // delay of the cut
word Config; // configuration string
int iCutFunc; // TT ID of the cut
int uMaskFunc; // polarity bitmask
unsigned uSign; // cut signature
@ -564,7 +576,8 @@ extern float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj
extern float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot );
/*=== ifDec.c =============================================================*/
extern word If_CutPerformDerive07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
extern word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive );
extern word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive, int fDelay );
extern void If_CutComputeIntrinsicJ( If_Man_t * p, word Config, int nLeaves, int * pIntrinsicDelays );
extern int If_CutPerformCheck07( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
extern int If_CutPerformCheck08( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
extern int If_CutPerformCheck10( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr );
@ -741,4 +754,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/map/if/ifCore.c
View File

@ -207,4 +207,3 @@ int If_ManPerformMappingComb( If_Man_t * p )
ABC_NAMESPACE_IMPL_END

11
src/map/if/ifDecJ.c
View File

@ -1,6 +1,6 @@
/**CFile****************************************************************
FileName [ifDec07.c]
FileName [ifDecJ.c]
SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifDec07.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
Revision [$Id: ifDecJ.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
@ -35,14 +35,14 @@ int If_CutPerformCheckJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves
{
return 1;
}
word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive )
word If_CutPerformDeriveJ( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr, int fDerive, int fDelay )
{
return 0;
}
void If_PermUnpack( unsigned Value, int Pla2Var[9] )
void If_CutComputeIntrinsicJ( If_Man_t * p, word Config, int nLeaves, int * pIntrinsicDelays )
{
}
void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName )
void If_PermUnpack( unsigned Value, int Pla2Var[9] )
{
}
@ -52,4 +52,3 @@ void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName )
ABC_NAMESPACE_IMPL_END

34
src/map/if/ifLibLut.c
View File

@ -388,6 +388,39 @@ If_LibCell_t * If_LibCellAlloc( void )
return p;
}
/**Function*************************************************************
Synopsis [Computes the record size.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int If_LibCellComputeRecordSize( char * pFuncDesc, int nInputs )
{
int i, nMapBytes, nRecordSize;
assert( pFuncDesc != NULL );
nMapBytes = (Abc_Base2Log(nInputs + 2) + 7) / 8;
nRecordSize = 1 + nInputs * nMapBytes;
for ( i = 0; pFuncDesc[i]; i++ )
{
int nLutVars = 0;
if ( pFuncDesc[i] != '{' )
continue;
for ( i++; pFuncDesc[i] && pFuncDesc[i] != '}'; i++ )
if ( pFuncDesc[i] >= 'a' && pFuncDesc[i] <= 'z' )
nLutVars++;
assert( nLutVars < 31 );
nRecordSize += ((1 << nLutVars) + 7) / 8;
if ( pFuncDesc[i] == 0 )
break;
}
return nRecordSize;
}
/**Function*************************************************************
Synopsis [Reads the description of cells from the cell library file.]
@ -471,6 +504,7 @@ If_LibCell_t * If_LibCellRead( char * FileName )
nInputs = maxChar - 'a' + 1;
}
p->nCellInputs[CellId] = nInputs;
p->pCellRecordSizes[CellId] = If_LibCellComputeRecordSize( FuncDesc, nInputs );
// Read Area
pToken = strtok( NULL, " \t\n" );

3
src/map/if/ifMan.c
View File

@ -226,7 +226,7 @@ void If_ManSimpleSort( int * pArray, int nSize )
void If_ManDumpCut( If_Cut_t * pCut, int nLutSize, Vec_Int_t * vCuts )
{
int i;
for ( i = 0; i < pCut->nLeaves; i++ )
for ( i = 0; i < (int)pCut->nLeaves; i++ )
Vec_IntPush( vCuts, pCut->pLeaves[i] );
for ( ; i < nLutSize; i++ )
Vec_IntPush( vCuts, -1 );
@ -719,6 +719,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] );
pCut->iCutFunc = p->pPars->fUseTtPerm ? 3 : (p->pPars->fTruth ? 2: -1);
pCut->uMaskFunc = 0;
pCut->Config = 0;
assert( pCut->pLeaves[0] < p->vObjs->nSize );
}

75
src/map/if/ifMap.c
View File

@ -162,12 +162,13 @@ int * If_CutArrTimeProfile( If_Man_t * p, If_Cut_t * pCut )
void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess, int fFirst )
{
If_Set_t * pCutSet;
If_Obj_t * pLeaf;
If_Cut_t * pCut0, * pCut1, * pCut;
If_Cut_t * pCut0R, * pCut1R;
int fFunc0R, fFunc1R;
int i, k, v, iCutDsd, fChange;
int fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUserLutDec || p->pPars->fUserLut2D ||
p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2;
p->pPars->fUseDsdTune || p->pPars->fUseCofVars || p->pPars->fUseAndVars || p->pPars->fUse34Spec || p->pPars->pLutStruct || p->pPars->pFuncCell2 || p->pPars->fUseCheck1 || p->pPars->fUseCheck2 || p->pPars->fEnableCheck07;
int fUseAndCut = (p->pPars->nAndDelay > 0) || (p->pPars->nAndArea > 0);
assert( !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
assert( !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
@ -193,6 +194,30 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL );
else if ( p->pPars->fDsdBalance )
pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell )
{
int iLeaf, Intrinsic[IF_MAX_LUTSIZE];
float Delay = -IF_FLOAT_LARGE;
if ( pCut->nLeaves == 0 )
{
pCut->fUseless = 0;
pCut->Delay = 0.0;
goto IfMapBestCutDone;
}
assert( pCut->nLeaves == 1 || pCut->Config );
If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic );
If_CutForEachLeaf( p, pCut, pLeaf, iLeaf )
{
If_Cut_t * pBestCut = If_ObjCutBest( pLeaf );
assert( pBestCut != NULL );
assert( pBestCut->fUseless == 0 );
Delay = IF_MAX( Delay, If_ObjArrTime(pLeaf) + (float)Intrinsic[iLeaf] );
}
pCut->fUseless = (Delay > IF_FLOAT_LARGE/2);
pCut->Delay = Delay;
IfMapBestCutDone:
;
}
else if ( p->pPars->fUserRecLib )
pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj );
else if ( p->pPars->fUserSesLib )
@ -268,7 +293,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if ( !If_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
continue;
}
if ( p->pPars->fUserLutDec && !fFirst && pCut->nLeaves > p->pPars->nLutDecSize )
if ( p->pPars->fUserLutDec && !fFirst && (int)pCut->nLeaves > p->pPars->nLutDecSize )
continue;
if ( pObj->fSpec && pCut->nLeaves == (unsigned)p->pPars->nLutSize )
continue;
@ -324,12 +349,32 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
assert( p->pPars->fUseTtPerm == 0 );
assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 );
pCut->Config = 0;
if ( p->pPars->fUseDsd )
pCut->fUseless = If_DsdManCheckDec( p->pIfDsdMan, If_CutDsdLit(p, pCut) );
else if ( p->pPars->pFuncCell2 )
pCut->fUseless = !p->pPars->pFuncCell2( p, (word *)If_CutTruthW(p, pCut), pCut->nLeaves, NULL, NULL );
else
{
int iLeaf;
// Expose current cut context for user callbacks.
p->pCutObjCur = pObj;
p->pCutCur = pCut;
p->nCutLeavesCur = pCut->nLeaves;
for ( iLeaf = 0; iLeaf < p->nCutLeavesCur; iLeaf++ )
{
If_Obj_t * pLeaf = If_CutLeaf( p, pCut, iLeaf );
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && pCut->nLeaves > 1 )
{
If_Cut_t * pBestCut = If_ObjCutBest( pLeaf );
assert( pBestCut != NULL );
assert( pBestCut->fUseless == 0 );
}
p->pCutLeavesCur[iLeaf] = pLeaf->Id;
p->pCutLeafArrCur[iLeaf] = If_ObjArrTime( pLeaf );
}
pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), Abc_MaxInt(6, pCut->nLeaves), pCut->nLeaves, p->pPars->pLutStruct );
}
p->nCutsUselessAll += pCut->fUseless;
p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
p->nCutsCountAll++;
@ -427,6 +472,27 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
pCut->Delay = If_CutSopBalanceEval( p, pCut, NULL );
else if ( p->pPars->fDsdBalance )
pCut->Delay = If_CutDsdBalanceEval( p, pCut, NULL );
else if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell )
{
if ( pCut->nLeaves == 0 )
{
pCut->Delay = 0.0;
pCut->fUseless = 0;
goto IfMapCutEvalDone;
}
if ( pCut->nLeaves == 1 )
{
pLeaf = If_ManObj( p, pCut->pLeaves[0] );
pCut->Delay = If_ObjArrTime( pLeaf );
pCut->fUseless = 0;
goto IfMapCutEvalDone;
}
assert( pCut->fUseless || p->fCutDelayCurValid );
assert( pCut->fUseless || pCut->Config != 0 );
pCut->Delay = pCut->fUseless ? IF_FLOAT_LARGE : p->CutDelayCur;
IfMapCutEvalDone:
;
}
else if ( p->pPars->fUserRecLib )
pCut->Delay = If_CutDelayRecCost3( p, pCut, pObj );
else if ( p->pPars->fUserLutDec )
@ -502,7 +568,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if ( Mode && pObj->nRefs > 0 )
If_CutAreaRef( p, If_ObjCutBest(pObj) );
if ( If_ObjCutBest(pObj)->fUseless )
Abc_Print( 1, "The best cut is useless.\n" );
Abc_Print( 1, "The best cut is useless. Please increase the number of cuts used by the mapper, for example: \"&if -C 32\"\n" );
// call the user specified function for each cut
if ( p->pPars->pFuncUser )
If_ObjForEachCut( pObj, pCut, i )
@ -527,7 +593,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
If_Set_t * pCutSet;
If_Obj_t * pTemp;
If_Cut_t * pCutTemp, * pCut;
int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUse34Spec || p->pPars->fUserLutDec || p->pPars->fUserLut2D;
int i, fSave0 = p->pPars->fDelayOpt || p->pPars->fDelayOptLut || p->pPars->fDsdBalance || p->pPars->fUserRecLib || p->pPars->fUserSesLib || p->pPars->fUse34Spec || p->pPars->fUserLutDec || p->pPars->fUserLut2D || p->pPars->fEnableCheck07;
assert( pObj->pEquiv != NULL );
// prepare
@ -702,4 +768,3 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
ABC_NAMESPACE_IMPL_END

47
src/map/if/ifTime.c
View File

@ -131,6 +131,20 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
}
else
{
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib )
{
int Intrinsic[IF_MAX_LUTSIZE];
if ( pCut->nLeaves == 0 )
return 0.0;
assert( pCut->nLeaves == 1 || pCut->Config != 0 );
If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic );
If_CutForEachLeaf( p, pCut, pLeaf, i )
{
DelayCur = If_ObjCutBest(pLeaf)->Delay + (float)Intrinsic[i];
Delay = IF_MAX( Delay, DelayCur );
}
return Delay;
}
if ( pCut->fUser )
{
assert( !p->pPars->fLiftLeaves );
@ -219,6 +233,17 @@ void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, fl
}
else
{
if ( p->pPars->fEnableCheck07 && p->pPars->fDelayOptCell && p->pPars->pCellLib )
{
int Intrinsic[IF_MAX_LUTSIZE];
if ( pCut->nLeaves == 0 )
return;
assert( (pObj && pObj->Id == 0) || pCut->nLeaves == 1 || pCut->Config != 0 );
If_CutComputeIntrinsicJ( p, pCut->Config, pCut->nLeaves, Intrinsic );
If_CutForEachLeaf( p, pCut, pLeaf, i )
pLeaf->Required = IF_MIN( pLeaf->Required, ObjRequired - (float)Intrinsic[i] );
return;
}
if ( pCut->fUser )
{
char Perm[IF_MAX_FUNC_LUTSIZE], * pPerm = Perm;
@ -452,7 +477,26 @@ void If_ManComputeRequired( If_Man_t * p )
return;
// set the required times for the POs
Tim_ManIncrementTravId( p->pManTim );
if ( p->vCoAttrs )
if ( p->pPars->pTimesReq )
{
Counter = 0;
If_ManForEachCo( p, pObj, i )
{
reqTime = p->pPars->pTimesReq[i];
if ( If_ObjArrTime(If_ObjFanin0(pObj)) > reqTime + p->fEpsilon )
{
reqTime = If_ObjArrTime(If_ObjFanin0(pObj));
Counter++;
}
Tim_ManSetCoRequired( p->pManTim, i, reqTime );
}
if ( Counter && !p->fReqTimeWarn )
{
Abc_Print( 0, "Required times are exceeded at %d output%s. The earliest arrival times are used.\n", Counter, Counter > 1 ? "s":"" );
p->fReqTimeWarn = 1;
}
}
else if ( p->vCoAttrs )
{
assert( If_ManCoNum(p) == Vec_IntSize(p->vCoAttrs) );
If_ManForEachCo( p, pObj, i )
@ -528,4 +572,3 @@ void If_ManComputeRequired( If_Man_t * p )
ABC_NAMESPACE_IMPL_END

42
src/map/if/ifTrace.c Normal file
View File

@ -0,0 +1,42 @@
/**CFile****************************************************************
FileName [ifTrace.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [Public stub for delay trace dumping.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - March 23, 2026.]
Revision [$Id: ifTrace.c,v 1.00 2026/03/23 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
#include "aig/gia/gia.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
void Gia_ManDelayTraceDump( Gia_Man_t * p, char * pFileName )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

9
src/map/if/ifTune.c
View File

@ -1031,12 +1031,14 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
{
Gia_Man_t * p = (Gia_Man_t *)pGia;
Gia_Man_t * pNew, * pTemp;
If_LibCell_t * pCellLib = (If_LibCell_t *)p->pCellLib;
Vec_Int_t * vCover, * vLeaves;
Gia_Obj_t * pObj;
unsigned char * pConfigData;
int k, i, iLut, iVar;
int Count = 0;
assert( p->vConfigs2 != NULL );
assert( pCellLib != NULL );
assert( Gia_ManHasMapping(p) );
// create new manager
pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 );
@ -1078,7 +1080,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
Truth = Abc_Tt6Stretch( Truth, 4 );
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
Gia_ManObj(p, iLut)->Value = Kit_TruthToGia( pNew, (unsigned *)&Truth, Vec_IntSize(vLeaves), vCover, vLeaves, 1 );
bytePos += 7; // 1 byte CellId + 4 bytes mapping + 2 bytes truth table
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else if ( CellId == 1 )
{
@ -1122,7 +1124,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 );
Gia_ManObj(p, iLut)->Value = iObjLit2;
Vec_IntFree( vLeavesTemp );
bytePos += 12; // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else if ( CellId == 2 )
{
@ -1177,7 +1179,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
iObjLit3 = Gia_ManHashMux( pNew, iSelectLit, iObjLit2, iObjLit1 );
Gia_ManObj(p, iLut)->Value = iObjLit3;
Vec_IntFree( vLeavesTemp );
bytePos += 14; // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
bytePos += pCellLib->pCellRecordSizes[CellId];
}
else
{
@ -1755,4 +1757,3 @@ void Ifn_NtkRead()
ABC_NAMESPACE_IMPL_END

1
src/map/if/module.make
View File

@ -10,6 +10,7 @@ SRC += src/map/if/ifCom.c \
src/map/if/ifDec66.c \
src/map/if/ifDec75.c \
src/map/if/ifDecJ.c \
src/map/if/ifTrace.c \
src/map/if/ifDelay.c \
src/map/if/ifDsd.c \
src/map/if/ifLibBox.c \

164
src/proof/cec/cecProve.c
View File

@ -79,12 +79,15 @@ typedef struct Par_ThData_t_
Gia_Man_t * p;
int iEngine;
int fWorking;
int fStop;
int nTimeOut;
int Result;
int fVerbose;
int nTimeOutU;
Wlc_Ntk_t * pWlc;
Par_Share_t * pShare;
pthread_mutex_t Mutex;
pthread_cond_t Cond;
} Par_ThData_t;
typedef struct Cec_ScorrStop_t_
{
@ -98,12 +101,12 @@ static inline const char * Cec_SolveEngineName( int iEngine )
if ( iEngine == 0 ) return "rar";
if ( iEngine == 1 ) return "bmc";
if ( iEngine == 2 ) return "pdr";
if ( iEngine == 3 ) return "bmc-glucose";
if ( iEngine == 4 ) return "pdr-abs";
if ( iEngine == 3 ) return "bmc-g";
if ( iEngine == 4 ) return "pdr-t";
if ( iEngine == 5 ) return "bmcg";
if ( iEngine == PAR_ENGINE_UFAR ) return "ufar";
if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new";
if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old";
if ( iEngine == PAR_ENGINE_SCORR1 ) return "scnew";
if ( iEngine == PAR_ENGINE_SCORR2 ) return "scold";
if ( iEngine == PAR_ENGINE_GLA ) return "gla-q";
return "unknown";
}
@ -189,12 +192,12 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 )
{
if ( fVerbose )
printf( "Engine %d skipped because the current miter is combinational.\n", iEngine );
printf( "Engine %d (%-5s) skipped because the current miter is combinational.\n", iEngine, Cec_SolveEngineName(iEngine) );
return -1;
}
//abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock();
if ( fVerbose )
printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut );
printf( "Calling engine %d (%-5s) with timeout %d sec.\n", iEngine, Cec_SolveEngineName(iEngine), nTimeOut );
Abc_CexFreeP( &p->pCexSeq );
if ( iEngine == 0 )
{
@ -324,7 +327,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
if ( pThData && pThData->pShare && RetValue != -1 )
Cec_SProveCallback( (void *)pThData, 1, (unsigned)RetValue );
if ( fVerbose ) {
printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " );
printf( "Engine %d (%-5s) finished and %ssolved the problem. ", iEngine, Cec_SolveEngineName(iEngine), RetValue != -1 ? " " : "not " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return RetValue;
@ -379,30 +382,86 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare )
void * Cec_GiaProveWorkerThread( void * pArg )
{
Par_ThData_t * pThData = (Par_ThData_t *)pArg;
volatile int * pPlace = &pThData->fWorking;
int status, Result;
status = pthread_mutex_lock( &pThData->Mutex );
assert( status == 0 );
while ( 1 )
{
while ( *pPlace == 0 );
assert( pThData->fWorking );
if ( pThData->p == NULL )
while ( !pThData->fWorking && !pThData->fStop )
{
pthread_exit( NULL );
assert( 0 );
return NULL;
status = pthread_cond_wait( &pThData->Cond, &pThData->Mutex );
assert( status == 0 );
}
pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData );
if ( pThData->fStop )
break;
status = pthread_mutex_unlock( &pThData->Mutex );
assert( status == 0 );
Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData );
status = pthread_mutex_lock( &pThData->Mutex );
assert( status == 0 );
pThData->Result = Result;
pThData->fWorking = 0;
status = pthread_cond_broadcast( &pThData->Cond );
assert( status == 0 );
}
assert( 0 );
status = pthread_mutex_unlock( &pThData->Mutex );
assert( status == 0 );
return NULL;
}
void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fUseUif, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare )
static void Cec_GiaStartThreads( Par_ThData_t * ThData, int nWorkers )
{
int i, status;
for ( i = 0; i < nWorkers; i++ )
{
status = pthread_mutex_lock( &ThData[i].Mutex );
assert( status == 0 );
assert( !ThData[i].fStop );
assert( !ThData[i].fWorking );
ThData[i].fWorking = 1;
status = pthread_cond_signal( &ThData[i].Cond );
assert( status == 0 );
status = pthread_mutex_unlock( &ThData[i].Mutex );
assert( status == 0 );
}
}
static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, int fUseUif, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare )
{
int i, status;
assert( nWorkers <= PAR_THR_MAX );
for ( i = 0; i < nWorkers; i++ )
{
ThData[i].p = Gia_ManDup(p);
if ( WorkerThread )
{
ThData[i].p = Gia_ManDup( p );
Cec_CopyGiaName( p, ThData[i].p );
if ( fUseUif && i == nWorkers - 1 )
ThData[i].iEngine = PAR_ENGINE_UFAR;
else if ( !fUseUif && nWorkers == 6 && i == 5 )
ThData[i].iEngine = PAR_ENGINE_GLA;
else
ThData[i].iEngine = i;
ThData[i].fWorking = 0;
ThData[i].fStop = 0;
ThData[i].nTimeOut = nTimeOut;
ThData[i].Result = -1;
ThData[i].fVerbose = fVerbose;
ThData[i].nTimeOutU= nTimeOutU;
ThData[i].pWlc = pWlc;
ThData[i].pShare = pShare;
status = pthread_mutex_init( &ThData[i].Mutex, NULL );
assert( status == 0 );
status = pthread_cond_init( &ThData[i].Cond, NULL );
assert( status == 0 );
status = pthread_create( WorkerThread + i, NULL, Cec_GiaProveWorkerThread, (void *)(ThData + i) );
assert( status == 0 );
continue;
}
status = pthread_mutex_lock( &ThData[i].Mutex );
assert( status == 0 );
assert( !ThData[i].fStop );
assert( !ThData[i].fWorking );
Gia_ManStopP( &ThData[i].p );
ThData[i].p = Gia_ManDup( p );
Cec_CopyGiaName( p, ThData[i].p );
if ( fUseUif && i == nWorkers - 1 )
ThData[i].iEngine = PAR_ENGINE_UFAR;
@ -411,31 +470,58 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
else
ThData[i].iEngine = i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
ThData[i].fVerbose = fVerbose;
ThData[i].nTimeOutU= nTimeOutU;
ThData[i].pWlc = pWlc;
ThData[i].pShare = pShare;
if ( !WorkerThread )
continue;
status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
status = pthread_mutex_unlock( &ThData[i].Mutex );
assert( status == 0 );
}
for ( i = 0; i < nWorkers; i++ )
ThData[i].fWorking = 1;
Cec_GiaStartThreads( ThData, nWorkers );
}
int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine )
static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers )
{
int i;
int i, status;
for ( i = 0; i < nWorkers; i++ )
{
if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) {
status = pthread_mutex_lock( &ThData[i].Mutex );
assert( status == 0 );
ThData[i].fStop = 1;
status = pthread_cond_signal( &ThData[i].Cond );
assert( status == 0 );
status = pthread_mutex_unlock( &ThData[i].Mutex );
assert( status == 0 );
}
for ( i = 0; i < nWorkers; i++ )
{
status = pthread_join( WorkerThread[i], NULL );
assert( status == 0 );
Gia_ManStopP( &ThData[i].p );
status = pthread_cond_destroy( &ThData[i].Cond );
assert( status == 0 );
status = pthread_mutex_destroy( &ThData[i].Mutex );
assert( status == 0 );
}
}
static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine )
{
int i, status, fWorking;
for ( i = 0; i < nWorkers; i++ )
{
status = pthread_mutex_lock( &ThData[i].Mutex );
assert( status == 0 );
fWorking = ThData[i].fWorking;
if ( RetValue == -1 && !fWorking && ThData[i].Result != -1 )
{
RetValue = ThData[i].Result;
*pRetEngine = ThData[i].iEngine;
if ( !p->pCexSeq && ThData[i].p->pCexSeq )
p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 );
}
if ( ThData[i].fWorking )
status = pthread_mutex_unlock( &ThData[i].Mutex );
assert( status == 0 );
if ( fWorking )
i = -1;
}
return RetValue;
@ -447,8 +533,10 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
Par_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
Par_Share_t Share;
int i, nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1;
int nWorkers = nProcs + (fUseUif ? 1 : 0), RetValue = -1, RetEngine = -1;
memset( &Share, 0, sizeof(Par_Share_t) );
memset( ThData, 0, sizeof(ThData) );
memset( WorkerThread, 0, sizeof(WorkerThread) );
Abc_CexFreeP( &p->pCexComb );
Abc_CexFreeP( &p->pCexSeq );
if ( !fSilent && fVerbose )
@ -457,7 +545,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
fflush( stdout );
assert( nProcs == 3 || nProcs == 5 || nProcs == 6 );
assert( nProcs >= 1 && nProcs <= 6 );
assert( nWorkers <= PAR_THR_MAX );
Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share );
@ -465,7 +553,12 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
Gia_Man_t * pScorr = Cec_GiaScorrNew( p, nTimeOut, &Share );
clkScorr = Abc_Clock() - clkTotal;
if ( Gia_ManAndNum(pScorr) == 0 )
{
Share.fSolved = 1;
Share.Result = 1;
Share.iEngine = PAR_ENGINE_SCORR1;
RetValue = 1, RetEngine = PAR_ENGINE_SCORR1;
}
RetValue = Cec_GiaWaitThreads( ThData, nWorkers, p, RetValue, &RetEngine );
if ( RetValue == -1 )
@ -484,7 +577,12 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr, nTimeOut3, &Share );
clkScorr2 = Abc_Clock() - clkStart;
if ( Gia_ManAndNum(pScorr2) == 0 )
{
Share.fSolved = 1;
Share.Result = 1;
Share.iEngine = PAR_ENGINE_SCORR2;
RetValue = 1, RetEngine = PAR_ENGINE_SCORR2;
}
if ( RetValue == -1 )
{
@ -503,11 +601,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
Gia_ManStop( pScorr );
// stop threads
for ( i = 0; i < nWorkers; i++ )
{
ThData[i].p = NULL;
ThData[i].fWorking = 1;
}
Cec_GiaStopThreads( ThData, WorkerThread, nWorkers );
if ( !fSilent )
{
char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p);

162
src/sat/bmc/bmcMaj.c
View File

@ -1363,6 +1363,161 @@ static void Exa3_ManPrintPerm( Exa3_Man_t * p )
}
}
}
static void Exa3_ManDumpVerilogName( Exa3_Man_t * p, char * pBase )
{
char Flags[32];
int n = 0;
if ( p->pPars->pSymStr )
snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr );
else
snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr );
if ( p->pPars->fUseIncr ) Flags[n++] = 'i';
if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a';
if ( p->pPars->fFewerVars ) Flags[n++] = 'o';
if ( p->pPars->fLutCascade ) Flags[n++] = 'r';
if ( p->pPars->fLutInFixed ) Flags[n++] = 'f';
if ( p->pPars->fGlucose ) Flags[n++] = 'g';
if ( p->pPars->fCadical ) Flags[n++] = 'c';
if ( p->pPars->fKissat ) Flags[n++] = 'k';
if ( p->pPars->fDumpBlif ) Flags[n++] = 'd';
if ( p->pPars->fMinNodes ) Flags[n++] = 'm';
if ( p->pPars->fUsePerm ) Flags[n++] = 'p';
Flags[n] = '\0';
snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags );
}
static int Exa3_ManDumpCascadeVerilog( Exa3_Man_t * p, int fCompl )
{
static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" };
int i, k, iVar;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" );
return 0;
}
Exa3_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iSlice = iNode / 8;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
if ( p->nLutSize < 6 )
Truth = Abc_Tt6Stretch( Truth, p->nLutSize );
fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n",
iSlice, iSlice, pBels[iNode % 8] );
fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode );
for ( k = 0; k < 6; k++ )
{
fprintf( pFile, " .I%d(", k );
if ( k < p->nLutSize )
{
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
}
else
fprintf( pFile, "1'b0" );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName );
return 1;
}
static int Exa3_ManDumpVerilog( Exa3_Man_t * p, int fCompl )
{
int i, k, iVar;
int nBits = 1 << p->nLutSize;
int nDigits = (nBits + 3) >> 2;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" );
return 0;
}
Exa3_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode );
for ( k = 0; k < p->nLutSize; k++ )
{
fprintf( pFile, " .I%d(", k );
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -1713,7 +1868,13 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( !pPars->fSilent && (p->nUsed[0] || p->nUsed[1]) ) printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
if ( !pPars->fSilent ) Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( iMint == -1 && pPars->fDumpBlif )
{
Exa3_ManDumpBlif( p, fCompl );
if ( pPars->fLutCascade )
Exa3_ManDumpCascadeVerilog( p, fCompl );
else
Exa3_ManDumpVerilog( p, fCompl );
}
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa3_ManFree( p );
@ -4344,4 +4505,3 @@ void Exa_NpnCascadeTest6()
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

163
src/sat/bmc/bmcMaj2.c
View File

@ -1236,6 +1236,157 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
ABC_FREE( pStr );
}
static void Exa3_ManDumpVerilogName( Exa3_Man_t * p, char * pBase )
{
char Flags[32];
int n = 0;
if ( p->pPars->pSymStr )
snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr );
else
snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr );
if ( p->pPars->fUseIncr ) Flags[n++] = 'i';
if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a';
if ( p->pPars->fFewerVars ) Flags[n++] = 'o';
if ( p->pPars->fLutCascade ) Flags[n++] = 'r';
if ( p->pPars->fLutInFixed ) Flags[n++] = 'f';
if ( p->pPars->fGlucose ) Flags[n++] = 'g';
if ( p->pPars->fCadical ) Flags[n++] = 'c';
if ( p->pPars->fKissat ) Flags[n++] = 'k';
if ( p->pPars->fDumpBlif ) Flags[n++] = 'd';
if ( p->pPars->fMinNodes ) Flags[n++] = 'm';
if ( p->pPars->fUsePerm ) Flags[n++] = 'p';
Flags[n] = '\0';
snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags );
}
static int Exa3_ManDumpCascadeVerilog( Exa3_Man_t * p, int fCompl )
{
static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" };
int i, k, iVar;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" );
return 0;
}
Exa3_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iSlice = iNode / 8;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( sat_solver_var_value(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
if ( p->nLutSize < 6 )
Truth = Abc_Tt6Stretch( Truth, p->nLutSize );
fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n",
iSlice, iSlice, pBels[iNode % 8] );
fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode );
for ( k = 0; k < 6; k++ )
{
fprintf( pFile, " .I%d(", k );
if ( k < p->nLutSize )
{
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
}
else
fprintf( pFile, "1'b0" );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName );
return 1;
}
static int Exa3_ManDumpVerilog( Exa3_Man_t * p, int fCompl )
{
int i, k, iVar;
int nBits = 1 << p->nLutSize;
int nDigits = (nBits + 3) >> 2;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" );
return 0;
}
Exa3_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( sat_solver_var_value(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode );
for ( k = 0; k < p->nLutSize; k++ )
{
fprintf( pFile, " .I%d(", k );
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
return 1;
}
/**Function*************************************************************
@ -1445,7 +1596,16 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
Exa3_ManPrintSolution( p, fCompl );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa3_ManDumpBlif( p, fCompl );
{
if ( pPars->fDumpBlif )
{
Exa3_ManDumpBlif( p, fCompl );
if ( pPars->fLutCascade )
Exa3_ManDumpCascadeVerilog( p, fCompl );
else
Exa3_ManDumpVerilog( p, fCompl );
}
}
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa3_ManFree( p );
@ -1458,4 +1618,3 @@ void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars )
ABC_NAMESPACE_IMPL_END

161
src/sat/bmc/bmcMaj7.c
View File

@ -477,6 +477,161 @@ static void Exa7_ManPrintPerm( Exa7_Man_t * p )
}
}
}
static void Exa7_ManDumpVerilogName( Exa7_Man_t * p, char * pBase )
{
char Flags[32];
int n = 0;
if ( p->pPars->pSymStr )
snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr );
else
snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr );
if ( p->pPars->fUseIncr ) Flags[n++] = 'i';
if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a';
if ( p->pPars->fFewerVars ) Flags[n++] = 'o';
if ( p->pPars->fLutCascade ) Flags[n++] = 'r';
if ( p->pPars->fLutInFixed ) Flags[n++] = 'f';
if ( p->pPars->fGlucose ) Flags[n++] = 'g';
if ( p->pPars->fCadical ) Flags[n++] = 'c';
if ( p->pPars->fKissat ) Flags[n++] = 'k';
if ( p->pPars->fDumpBlif ) Flags[n++] = 'd';
if ( p->pPars->fMinNodes ) Flags[n++] = 'm';
if ( p->pPars->fUsePerm ) Flags[n++] = 'p';
Flags[n] = '\0';
snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags );
}
static int Exa7_ManDumpCascadeVerilog( Exa7_Man_t * p, int fCompl )
{
static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" };
int i, k, iVar;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" );
return 0;
}
Exa7_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iSlice = iNode / 8;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
if ( p->nLutSize < 6 )
Truth = Abc_Tt6Stretch( Truth, p->nLutSize );
fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n",
iSlice, iSlice, pBels[iNode % 8] );
fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode );
for ( k = 0; k < 6; k++ )
{
fprintf( pFile, " .I%d(", k );
if ( k < p->nLutSize )
{
iVar = Exa7_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
}
else
fprintf( pFile, "1'b0" );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName );
return 1;
}
static int Exa7_ManDumpVerilog( Exa7_Man_t * p, int fCompl )
{
int i, k, iVar;
int nBits = 1 << p->nLutSize;
int nDigits = (nBits + 3) >> 2;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" );
return 0;
}
Exa7_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( cadical_solver_get_var_value(p->pSat, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode );
for ( k = 0; k < p->nLutSize; k++ )
{
fprintf( pFile, " .I%d(", k );
iVar = Exa7_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
return 1;
}
/**Function*************************************************************
@ -829,7 +984,13 @@ int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars )
Exa7_ManPrintPerm( p );
printf( "\".\n" );
if ( pPars->fDumpBlif )
{
Exa7_ManDumpBlif( p, fCompl );
if ( pPars->fLutCascade )
Exa7_ManDumpCascadeVerilog( p, fCompl );
else
Exa7_ManDumpVerilog( p, fCompl );
}
if ( p->pPars->fGenTruths ) {
if ( p->pPars->vTruths )
Vec_WrdFreeP( &p->pPars->vTruths );

161
src/sat/bmc/bmcMaj8.c
View File

@ -485,6 +485,161 @@ static void Exa8_ManPrintPerm( Exa8_Man_t * p )
}
}
}
static void Exa8_ManDumpVerilogName( Exa8_Man_t * p, char * pBase )
{
char Flags[32];
int n = 0;
if ( p->pPars->pSymStr )
snprintf( pBase, 128, "Y%.*s", 15, p->pPars->pSymStr );
else
snprintf( pBase, 128, "%.*s", 16, p->pPars->pTtStr );
if ( p->pPars->fUseIncr ) Flags[n++] = 'i';
if ( p->pPars->fOnlyAnd ) Flags[n++] = 'a';
if ( p->pPars->fFewerVars ) Flags[n++] = 'o';
if ( p->pPars->fLutCascade ) Flags[n++] = 'r';
if ( p->pPars->fLutInFixed ) Flags[n++] = 'f';
if ( p->pPars->fGlucose ) Flags[n++] = 'g';
if ( p->pPars->fCadical ) Flags[n++] = 'c';
if ( p->pPars->fKissat ) Flags[n++] = 'k';
if ( p->pPars->fDumpBlif ) Flags[n++] = 'd';
if ( p->pPars->fMinNodes ) Flags[n++] = 'm';
if ( p->pPars->fUsePerm ) Flags[n++] = 'p';
Flags[n] = '\0';
snprintf( pBase + strlen(pBase), 128 - strlen(pBase), "_K%d_M%d_%s", p->nLutSize, p->nNodes, Flags );
}
static int Exa8_ManDumpCascadeVerilog( Exa8_Man_t * p, int fCompl )
{
static const char * pBels[8] = { "A6LUT", "B6LUT", "C6LUT", "D6LUT", "E6LUT", "F6LUT", "G6LUT", "H6LUT" };
int i, k, iVar;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT cascade dumping supports only LUTs with up to 6 inputs. Falling back to BLIF dumping.\n" );
return 0;
}
Exa8_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_cascade_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT cascade for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " (* KEEP = \"yes\", DONT_TOUCH = \"yes\" *) wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iSlice = iNode / 8;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << (1 << p->nLutSize)) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( Exa8_KissatVarValue(p, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
if ( p->nLutSize < 6 )
Truth = Abc_Tt6Stretch( Truth, p->nLutSize );
fprintf( pFile, " (* HU_SET = \"hu_lut_cascade_%d\", RLOC = \"X0Y%d\", BEL = \"%s\", DONT_TOUCH = \"yes\", KEEP = \"yes\", IS_BEL_FIXED = \"yes\" *)\n",
iSlice, iSlice, pBels[iNode % 8] );
fprintf( pFile, " LUT6 #(.INIT(64'h%016llX)) u_lut%d (\n", (unsigned long long)Truth, iNode );
for ( k = 0; k < 6; k++ )
{
fprintf( pFile, " .I%d(", k );
if ( k < p->nLutSize )
{
iVar = Exa8_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
}
else
fprintf( pFile, "1'b0" );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT cascade into file \"%s\".\n", pFileName );
return 1;
}
static int Exa8_ManDumpVerilog( Exa8_Man_t * p, int fCompl )
{
int i, k, iVar;
int nBits = 1 << p->nLutSize;
int nDigits = (nBits + 3) >> 2;
char pBase[128], pFileName[132], pModuleName[160];
FILE * pFile;
if ( p->nLutSize > 6 )
{
if ( !p->pPars->fSilent )
printf( "Vivado LUT dumping supports only LUTs with up to 6 inputs. Skipping Verilog dump.\n" );
return 0;
}
Exa8_ManDumpVerilogName( p, pBase );
snprintf( pFileName, sizeof(pFileName), "%s.v", pBase );
snprintf( pModuleName, sizeof(pModuleName), "lut_net_%s", pBase );
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
return 0;
fprintf( pFile, "// Vivado LUT net for the %d-input function %s synthesized by ABC on %s\n", p->nVars, pBase, Extra_TimeStamp() );
fprintf( pFile, "module %s (\n", pModuleName );
fprintf( pFile, " input wire [%d:0] x,\n", p->nVars - 1 );
fprintf( pFile, " output wire y\n" );
fprintf( pFile, ");\n" );
for ( i = 0; i < p->nNodes - 1; i++ )
fprintf( pFile, " wire n%d;\n", i );
if ( p->nNodes > 1 )
fprintf( pFile, "\n" );
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iNode = i - p->nVars;
int iVarStart = 1 + p->LutMask * iNode;
word Truth = 0;
word Mask = p->nLutSize == 6 ? ~(word)0 : ((((word)1) << nBits) - 1);
for ( k = 0; k < p->LutMask; k++ )
if ( Exa8_KissatVarValue(p, iVarStart + k) )
Truth |= ((word)1) << (k + 1);
if ( i == p->nObjs - 1 && fCompl )
Truth = (~Truth) & Mask;
fprintf( pFile, " LUT%d #(.INIT(%d'h%0*llX)) u_lut%d (\n", p->nLutSize, nBits, nDigits, (unsigned long long)Truth, iNode );
for ( k = 0; k < p->nLutSize; k++ )
{
fprintf( pFile, " .I%d(", k );
iVar = Exa8_ManFindFanin( p, i, k );
if ( iVar < p->nVars )
fprintf( pFile, "x[%d]", iVar );
else
fprintf( pFile, "n%d", iVar - p->nVars );
fprintf( pFile, "),\n" );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " .O(y)\n" );
else
fprintf( pFile, " .O(n%d)\n", iNode );
fprintf( pFile, " );\n\n" );
}
fprintf( pFile, "endmodule\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent )
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
return 1;
}
/**Function*************************************************************
@ -789,7 +944,13 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
Exa8_ManPrintPerm(p);
printf( "\".\n" );
if ( pPars->fDumpBlif )
{
Exa8_ManDumpBlif( p, fCompl );
if ( pPars->fLutCascade )
Exa8_ManDumpCascadeVerilog( p, fCompl );
else
Exa8_ManDumpVerilog( p, fCompl );
}
if ( p->pPars->fGenTruths ) {
if ( p->pPars->vTruths )
Vec_WrdFreeP( &p->pPars->vTruths );