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

Merge commit 'ba852596b4a11e492e9682662a3e8d1a9be4d765' into yosys-experimental

This commit is contained in:
Miodrag Milanovic 2025-11-25 11:28:55 +01:00
parent 1c5ed1ce37 ba852596b4
commit 131a50dd77
52 changed files with 5693 additions and 360 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -12,7 +12,6 @@ lib/abc*
lib/m114*
lib/bip*
docs/
.vscode/
.cache/
src/ext*

1
src/aig/gia/gia.h
View File

@ -374,6 +374,7 @@ struct Jf_Par_t_
int nCutNumMax;
int nProcNumMax;
int nLutSizeMux;
int nMaxMatches;
word Delay;
word Area;
word Edge;

18
src/aig/gia/giaAiger.c
View File

@ -652,6 +652,9 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
pNew->vInArrs = Vec_FltStart( nInputs );
memcpy( Vec_FltArray(pNew->vInArrs), pCur, (size_t)4*nInputs ); pCur += 4*nInputs;
if ( fVerbose ) printf( "Finished reading extension \"i\".\n" );
//if ( Vec_FltSize(pNew->vInArrs) == Gia_ManPiNum(pNew) )
// Vec_FltFillExtra(pNew->vInArrs, Gia_ManCiNum(pNew), 0);
//assert( Vec_FltSize(pNew->vInArrs) == Gia_ManCiNum(pNew) );
}
else if ( *pCur == 'o' )
{
@ -660,6 +663,9 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi
pNew->vOutReqs = Vec_FltStart( nOutputs );
memcpy( Vec_FltArray(pNew->vOutReqs), pCur, (size_t)4*nOutputs ); pCur += 4*nOutputs;
if ( fVerbose ) printf( "Finished reading extension \"o\".\n" );
//if ( Vec_FltSize(pNew->vOutReqs) == Gia_ManPoNum(pNew) )
// Vec_FltFillExtra(pNew->vOutReqs, Gia_ManCoNum(pNew), 0);
//assert( Vec_FltSize(pNew->vOutReqs) == Gia_ManCoNum(pNew) );
}
// read equivalence classes
else if ( *pCur == 'e' )
@ -1577,11 +1583,11 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
{
unsigned char CellId = (unsigned char)Vec_StrEntry(p->vConfigs2, i);
if ( CellId == 0 )
i += 4; // 1 byte CellId + 2 bytes truth table + 1 padding
i += 7; // 1 byte CellId + 4 bytes mapping + 2 bytes truth table
else if ( CellId == 1 )
i += 12; // 1 byte CellId + 4 bytes mapping + 4 bytes truth tables + 3 padding
i += 12; // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
else if ( CellId == 2 )
i += 12; // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables + 2 padding
i += 14; // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
else
assert( 0 ); // Unknown cell type
nInstances++;
@ -1613,15 +1619,15 @@ void Gia_AigerWriteS( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, in
// Write cell type 0 (LUT4)
Gia_FileWriteBufferSize( pFile, 0 ); // CellId
fwrite( pCell0, 1, strlen(pCell0) + 1, pFile );
Gia_FileWriteBufferSize( pFile, 4 ); // 1 byte CellId + 2 bytes truth table, rounded to 4
Gia_FileWriteBufferSize( pFile, 7 ); // 1 byte CellId + 4 bytes mapping + 2 bytes truth table
// Write cell type 1 (S44)
Gia_FileWriteBufferSize( pFile, 1 ); // CellId
fwrite( pCell1, 1, strlen(pCell1) + 1, pFile );
Gia_FileWriteBufferSize( pFile, 12 ); // 1 byte CellId + 4 bytes mapping + 4 bytes truth tables, rounded to 12
Gia_FileWriteBufferSize( pFile, 12 ); // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
// Write cell type 2 (9-input)
Gia_FileWriteBufferSize( pFile, 2 ); // CellId
fwrite( pCell2, 1, strlen(pCell2) + 1, pFile );
Gia_FileWriteBufferSize( pFile, 12 ); // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables (LUT4s only), rounded to 12
Gia_FileWriteBufferSize( pFile, 14 ); // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
// Write total instances
Gia_FileWriteBufferSize( pFile, nInstances );
// Write instance data as raw bytes

254
src/aig/gia/giaCut.c
View File

@ -29,9 +29,9 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define GIA_MAX_CUTSIZE 8
#define GIA_MAX_CUTNUM 257
#define GIA_MAX_TT_WORDS ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1)
#define GIA_MAX_CUTSIZE 14
#define GIA_MAX_CUTNUM 257
#define GIA_MAX_TT_WORDS ((GIA_MAX_CUTSIZE > 6) ? 1 << (GIA_MAX_CUTSIZE-6) : 1)
#define GIA_CUT_NO_LEAF 0xF
@ -649,7 +649,7 @@ void Gia_StoComputeCuts( Gia_Man_t * pGia )
printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
printf( "\n" );
printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ",
printf( "The number of nodes with maximum cut count (%d cuts) = %d nodes (out of %d). ",
p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
}
@ -724,7 +724,7 @@ Vec_Wec_t * Gia_ManExtractCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int
printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
printf( "\n" );
printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ",
printf( "The number of nodes with maximum cut count (%d cuts) = %d nodes (out of %d). ",
p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
}
@ -999,7 +999,7 @@ Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int
printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
printf( "\n" );
printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ",
printf( "The number of nodes with maximum cut count (%d cuts) = %d nodes (out of %d). ",
p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
}
@ -1027,12 +1027,12 @@ void Gia_ManExploreCutsTest( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fV
SeeAlso []
***********************************************************************/
Gia_Sto_t * Gia_ManMatchCutsInt( Gia_Man_t * pGia, int nCutSize0, int nCutNum0, int fVerbose0 )
Gia_Sto_t * Gia_ManMatchCutsInt( Gia_Man_t * pGia, int nCutSize0, int nCutNum0, int fTruth0, int fVerbose0 )
{
int nCutSize = nCutSize0;
int nCutNum = nCutNum0;
int fCutMin = 1;
int fTruthMin = 1;
int fCutMin = fTruth0;
int fTruthMin = fTruth0;
int fVerbose = fVerbose0;
Gia_Sto_t * p = Gia_StoAlloc( pGia, nCutSize, nCutNum, fCutMin, fTruthMin, fVerbose );
Gia_Obj_t * pObj; int i, iObj;
@ -1057,15 +1057,200 @@ Gia_Sto_t * Gia_ManMatchCutsInt( Gia_Man_t * pGia, int nCutSize0, int nCutNum0,
printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
printf( "\n" );
printf( "The number of nodes with cut count over the limit (%d cuts) = %d nodes (out of %d). ",
printf( "The number of nodes with maximum cut count (%d cuts) = %d nodes (out of %d). ",
p->nCutNum, p->nCutsOver, Gia_ManAndNum(pGia) );
Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
}
return p;
}
int Gia_ManCountSelfCuts( Gia_Man_t * p, Gia_Sto_t * pSto )
{
Vec_Int_t * vLevel; int i, k, * pCut, nNodes = 0;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
Gia_Obj_t * pObj = Gia_ManObj(p, i);
if ( !Gia_ObjIsAnd(pObj) )
continue;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k )
nNodes += pCut[0] == 2 && pCut[1] == Gia_ObjFaninId0p(p, pObj) && pCut[2] == Gia_ObjFaninId1p(p, pObj);
}
return nNodes;
}
void Gia_ManEvalCutHashing( Gia_Man_t * p, Gia_Sto_t * pSto )
{
Hsh_VecMan_t * pHash = Hsh_VecManStart( 100000 );
Vec_Int_t vTemp = {0};
Vec_Int_t * vLevel; int i, k, * pCut, nBytes = 0, nCuts = 0;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
Gia_Obj_t * pObj = Gia_ManObj(p, i);
if ( !Gia_ObjIsAnd(pObj) )
continue;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) {
vTemp.nSize = vTemp.nCap = pCut[0];
vTemp.pArray = pCut+1;
Hsh_VecManAdd( pHash, &vTemp );
nBytes += 4*(pCut[0]+1);
nCuts++;
}
}
printf( "Total cuts = %d. Unique = %d. Memory = %.2f MB. With hashing = %.2f MB.\n",
nCuts, Hsh_VecSize(pHash), 1.0*nBytes/(1<<20), Hsh_VecManMemory(pHash)/(1<<20) );
Hsh_VecManStop( pHash );
}
void Gia_ManDumpCutsText( Gia_Man_t * p, Gia_Sto_t * pSto, FILE * pFile, int fVerbose, char * pFileName )
{
Vec_Int_t * vLevel; int i, k, c, * pCut, nCuts = 0, nNodes = 0;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
continue;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) {
if ( pCut[0] == 1 )
continue;
fprintf( pFile, "%d ", i );
for ( c = 1; c <= pCut[0]; c++ )
fprintf( pFile, "%d ", pCut[c] );
fprintf( pFile, "1\n" );
nCuts++;
}
nNodes++;
}
Gia_Obj_t * pObj;
Gia_ManForEachCo( p, pObj, i )
fprintf( pFile, "%d %d 0\n", Gia_ObjId(p, pObj), Gia_ObjFaninId0p(p, pObj) );
if ( fVerbose )
printf( "Dumped %d cuts for %d nodes into text file \"%s\".\n", nCuts, nNodes, pFileName ? pFileName : "stdout" );
}
void Gia_ManDumpCutsPrint( Gia_Man_t * p, Vec_Int_t * vStore, int nCutSize, int nCutNum )
{
int o, f, c;
int nObjs = Gia_ManObjNum( p );
int * pStore = Vec_IntArray( vStore );
if ( nCutSize == 0 || nCutNum == 0 )
return;
for ( o = 0; o < nObjs; o++ ) {
Gia_Obj_t * pObj = Gia_ManObj( p, o );
int * pNodeStore;
if ( !Gia_ObjIsAnd(pObj) && !Gia_ObjIsCo(pObj) )
continue;
pNodeStore = pStore + o * nCutSize * nCutNum;
printf( "Node %d has %d cuts:\n", o, nCutNum );
for ( f = 0; f < nCutSize; f++ ) {
printf( "Fanin %d:", f );
for ( c = 0; c < nCutNum; c++ )
printf( " %4d", pNodeStore[f * nCutNum + c] );
printf( "\n" );
}
}
}
void Gia_ManDumpCutsBin( Gia_Man_t * p, Gia_Sto_t * pSto, FILE * pFile, int nCutSize, int nCutNum, int fVerbose, char * pFileName )
{
Vec_Int_t * vLevel; int i, k, c, * pCut, Num, RetValue, nCuts = 0, nNodes = 0;
Vec_Int_t * vStore = Vec_IntStart( Gia_ManObjNum(p) * nCutSize * nCutNum );
int * pStore = Vec_IntArray( vStore );
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
Gia_Obj_t * pObj = Gia_ManObj(p, i);
int CutIndex = 0;
int * pNodeStore;
if ( !Gia_ObjIsAnd(pObj) )
continue;
pNodeStore = pStore + i * nCutSize * nCutNum;
// flatten cuts as [object][leaf][cut], so each leaf spans nCutNum consecutive entries
// add the mandatory two-leaf cut composed of the current node's fanins
if ( nCutNum > 0 ) {
pNodeStore[CutIndex] = Gia_ObjFaninId0p( p, pObj );
pNodeStore[nCutNum + CutIndex] = Gia_ObjFaninId1p( p, pObj );
CutIndex++;
nCuts++;
}
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) {
if ( pCut[0] == 1 )
continue;
if ( CutIndex >= nCutNum )
break;
assert( pCut[0] <= nCutSize );
for ( c = 0; c < pCut[0]; c++ )
pNodeStore[c * nCutNum + CutIndex] = pCut[c+1];
CutIndex++;
nCuts++;
}
nNodes++;
}
// add unit cuts for primary outputs driven by arbitrary objects (const, PI, or internal node)
if ( nCutSize > 0 && nCutNum > 0 ) {
Gia_Obj_t * pObj;
Gia_ManForEachCo( p, pObj, i ) {
int ObjId = Gia_ObjId( p, pObj );
int * pNodeStore = pStore + ObjId * nCutSize * nCutNum;
pNodeStore[0] = Gia_ObjFaninId0p( p, pObj );
nCuts++;
}
}
// the number of dimension
Num = 3;
RetValue = fwrite( &Num, 4, 1, pFile );
assert( RetValue == 1 );
// the number of objects
Num = Gia_ManObjNum(p);
RetValue = fwrite( &Num, 4, 1, pFile );
assert( RetValue == 1 );
// the cut size
Num = nCutSize;
RetValue = fwrite( &Num, 4, 1, pFile );
assert( RetValue == 1 );
// the cut count
Num = nCutNum;
RetValue = fwrite( &Num, 4, 1, pFile );
assert( RetValue == 1 );
// the cuts themselves
RetValue = fwrite( Vec_IntArray(vStore), 4, Vec_IntSize(vStore), pFile );
assert( RetValue == Vec_IntSize(vStore) );
if ( fVerbose )
printf( "Dumped %d cuts for %d nodes into binary file \"%s\" (%.2f MB).\n", nCuts, nNodes, pFileName, Vec_IntMemory(vStore)/(1<<20) );
//Gia_ManDumpCutsPrint( p, vStore, nCutSize, nCutNum );
Vec_IntFree( vStore );
}
void Gia_ManComputeCutsCore( Gia_Man_t * pGia, int nCutSize, int nCutNum, int fTruth, int fVerbose, int fDumpText, int fDumpBin, char * pFileName )
{
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fTruth, fVerbose );
if ( fDumpText ) {
FILE * pFile = pFileName ? fopen(pFileName, "wb") : stdout;
if ( !pFile ) return;
Gia_ManDumpCutsText( pGia, pSto, pFile, fVerbose, pFileName );
fclose( pFile );
}
else if ( fDumpBin ) {
FILE * pFile = pFileName ? fopen(pFileName, "wb") : NULL;
if ( !pFile ) return;
Gia_ManDumpCutsBin( pGia, pSto, pFile, nCutSize, nCutNum, fVerbose, pFileName );
fclose( pFile );
}
//printf( "The number of nodes with self-cuts = %d (out of %d).\n", Gia_ManCountSelfCuts(pGia, pSto), Gia_ManAndNum(pGia) );
//Gia_ManEvalCutHashing( pGia, pSto );
Gia_StoFree( pSto );
}
Vec_Wec_t * Gia_ManCompute54Cuts( Gia_Man_t * pGia, int fVerbose )
{
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( pGia, 5, 16, 0, fVerbose );
Vec_Wec_t * vRes = Vec_WecAlloc( 1000 );
Vec_Int_t * vLevel; int i, k, c, * pCut;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
if ( !Gia_ObjIsAnd(Gia_ManObj(pGia, i)) )
continue;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) {
if ( pCut[0] != 4 && pCut[0] != 5 )
continue;
Vec_Int_t * vCut = Vec_WecPushLevel( vRes );
for ( c = 1; c <= pCut[0]; c++ )
Vec_IntPush( vCut, pCut[c] );
Vec_IntPush( vCut, i );
}
}
Gia_StoFree( pSto );
return vRes;
}
void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose )
{
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose );
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, 1, fVerbose );
Vec_Int_t * vLevel; int i, j, k, * pCut;
Vec_Int_t * vNodes = Vec_IntAlloc( 100 );
Vec_Wec_t * vCuts = Vec_WecAlloc( 100 );
@ -1101,7 +1286,7 @@ void Gia_ManMatchCuts( Vec_Mem_t * vTtMem, Gia_Man_t * pGia, int nCutSize, int n
Vec_Ptr_t * Gia_ManMatchCutsArray( Vec_Ptr_t * vTtMems, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose )
{
Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_PtrSize(vTtMems) );
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose );
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, 1, fVerbose );
Vec_Int_t * vLevel, * vTemp; int i, k, c, * pCut;
abctime clkStart = Abc_Clock();
for ( i = 0; i < Vec_PtrSize(vTtMems); i++ )
@ -1136,7 +1321,7 @@ Vec_Ptr_t * Gia_ManMatchCutsArray( Vec_Ptr_t * vTtMems, Gia_Man_t * pGia, int nC
}
Vec_Ptr_t * Gia_ManMatchCutsMany( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nFuncs, Gia_Man_t * pGia, int nCutSize, int nCutNum, int fVerbose )
{
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, fVerbose );
Gia_Sto_t * p = Gia_ManMatchCutsInt( pGia, nCutSize, nCutNum, 1, fVerbose );
Vec_Int_t * vLevel; int i, j, k, * pCut;
abctime clkStart = Abc_Clock();
assert( Abc_Truth6WordNum(nCutSize) == Vec_MemEntrySize(vTtMem) );
@ -1168,46 +1353,6 @@ Vec_Ptr_t * Gia_ManMatchCutsMany( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nFun
return vRes;
}
/**Function*************************************************************
Synopsis [Function enumeration.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDumpCuts( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose )
{
FILE * pFile = fopen( "input.txt", "wb" ); if ( !pFile ) return;
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 0 );
Vec_Int_t * vLevel; int i, k, c, * pCut, nCuts = 0, nNodes = 0;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) {
if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) )
continue;
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) {
if ( pCut[0] == 1 )
continue;
fprintf( pFile, "%d ", i );
for ( c = 1; c <= pCut[0]; c++ )
fprintf( pFile, "%d ", pCut[c] );
fprintf( pFile, "1\n" );
nCuts += pCut[0];
nNodes++;
}
}
Gia_Obj_t * pObj;
Gia_ManForEachCo( p, pObj, i ) {
fprintf( pFile, "%d %d 0\n", Gia_ObjId(p, pObj), Gia_ObjFaninId0p(p, pObj) );
}
fclose( pFile );
Gia_StoFree( pSto );
if ( fVerbose )
printf( "Dumped %d cuts for %d nodes into file \"input.txt\".\n", nCuts, nNodes );
}
/**Function*************************************************************
Synopsis [Function enumeration.]
@ -1221,7 +1366,7 @@ void Gia_ManDumpCuts( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose )
***********************************************************************/
Vec_Wrd_t * Gia_ManCollectCutFuncs( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose )
{
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 0 );
Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 1, 0 );
Vec_Wrd_t * vFuncs = Vec_WrdAlloc( 1000 ); Vec_Int_t * vLevel; int i, k, * pCut;
Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) )
Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) if ( pCut[0] == nCutSize ) {
@ -1426,4 +1571,3 @@ void Gia_ManMatchConesOutput( Gia_Man_t * pBig, Gia_Man_t * pSmall, int nCutNum,
ABC_NAMESPACE_IMPL_END

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

@ -2003,6 +2003,127 @@ void Gia_ManConfigPrint( word Truth4, word z, int nLeaves )
}
}
/**Function*************************************************************
Synopsis [Print cell configuration data.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManConfigPrint2( unsigned char * pConfigData, int nLeaves )
{
unsigned char CellId = pConfigData[0];
int i;
static int Count = 0;
printf( "%6d : ", Count++ ); // Print instance number
printf( "[Cell %d with %d leaves] ", CellId, nLeaves );
if ( CellId == 0 )
{
assert( nLeaves <= 4 );
// Extract 16-bit truth table
word Truth = ((word)pConfigData[5] << 8) | pConfigData[6];
printf( "e=%04lX{", (unsigned long)Truth );
// Print as simple {abcd} since it's just a direct LUT4
for ( i = 0; i < nLeaves; i++ )
printf( "%c", 'a' + i );
for ( ; i < 4; i++ )
printf( "%c", '0' );
printf( "}\n" );
}
else if ( CellId == 1 )
{
// First LUT4
word Truth1 = ((word)pConfigData[8] << 8) | pConfigData[9];
printf( "h=%04lX{", (unsigned long)Truth1 );
for ( i = 0; i < 4; i++ )
{
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
printf( "1");
else if ( v >= 2 && v < 2 + nLeaves )
printf( "%c", 'a' + (v-2));
else
printf( "?");
}
printf( "};");
// Second LUT4
word Truth2 = ((word)pConfigData[10] << 8) | pConfigData[11];
printf( "i=%04lX{", (unsigned long)Truth2 );
for ( i = 4; i < 7; i++ )
{
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
printf( "1");
else if ( v >= 2 && v < 2 + nLeaves )
printf( "%c", 'a' + (v-2));
else if ( v == 9 )
printf( "h"); // Output of first LUT
else
printf( "?");
}
printf( "h}\n" );
}
else if ( CellId == 2 )
{
// First LUT4
word Truth1 = ((word)pConfigData[10] << 8) | pConfigData[11];
printf( "j=%04lX{", (unsigned long)Truth1 );
for ( i = 0; i < 4; i++ )
{
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
printf( "1");
else if ( v >= 2 && v < 2 + nLeaves )
printf( "%c", 'a' + (v-2));
else
printf( "?");
}
printf( "};");
// Second LUT4
word Truth2 = ((word)pConfigData[12] << 8) | pConfigData[13];
printf( "k=%04lX{", (unsigned long)Truth2 );
for ( i = 4; i < 8; i++ )
{
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
printf( "1");
else if ( v >= 2 && v < 2 + nLeaves )
printf( "%c", 'a' + (v-2));
else
printf( "?");
}
printf( "};");
// final node
printf( "l=<");
int v = pConfigData[1+8];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
printf( "1");
else if ( v >= 2 && v < 2 + nLeaves )
printf( "%c", 'a' + (v-2));
else
printf( "?");
printf( "jk>\n" );
}
else
{
printf( "Unknown cell type %d!\n", CellId );
}
}
/**Function*************************************************************
Synopsis [Derive configurations.]
@ -2016,73 +2137,73 @@ void Gia_ManConfigPrint( word Truth4, word z, int nLeaves )
***********************************************************************/
void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * pTruth, int nLeaves )
{
int i, CellId, nBytes;
int i, CellId;
int startPos = Vec_StrSize(vConfigs2);
// Determine cell type based on the number of leaves and configuration
if ( nLeaves <= 4 )
if ( nLeaves <= 4 ) // 7 bytes = 1 byte CellId + 4 bytes mapping + 2 bytes truth table
{
// Cell type 0: Simple LUT4
CellId = 0;
nBytes = 3; // 1 byte CellId + 2 bytes truth table (16 bits)
// Write CellId
Vec_StrPush( vConfigs2, (char)CellId );
// Write mapping
for ( i = 0; i < nLeaves; i++ )
Vec_StrPush( vConfigs2, 2+i );
for ( ; i < 4; i++ )
Vec_StrPush( vConfigs2, 0 );
// Write truth table (16 bits for LUT4)
word Truth = pTruth[0];
Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth >> 8) & 0xFF) );
// Pad to 4-byte boundary
while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 )
Vec_StrPush( vConfigs2, 0 );
//Gia_ManConfigPrint( Truth, 0, pCutBest->nLeaves );
Vec_StrPush( vConfigs2, (char)(Truth & 0xFF) );
assert( startPos + 7 == Vec_StrSize(vConfigs2) );
//Gia_ManConfigPrint( Truth, 0, nLeaves );
}
else
else // 12 bytes = 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
{
word z = If_CutPerformDeriveJ( pIfMan, (unsigned *)pTruth, nLeaves, nLeaves, NULL, 1 );
//Gia_ManConfigPrint( 0, z, pCutBest->nLeaves );
//Gia_ManConfigPrint( 0, z, nLeaves );
if ( ((z >> 63) & 1) == 0 )
{
CellId = 1;
unsigned char mappingBytes[4] = {0};
// Write CellId
Vec_StrPush( vConfigs2, (char)CellId );
// Write input mappings for first LUT4 (4 inputs)
// Write input mapping
for ( i = 0; i < 4; i++ )
{
int v = (int)((z >> (16 + (i << 2))) & 7);
if ( v == 6 && nLeaves == 5 )
mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0
Vec_StrPush( vConfigs2, 0 );
else
mappingBytes[i / 2] |= ((v+2) << ((i % 2) * 4)); // leaf v (direct mapping)
Vec_StrPush( vConfigs2, 2+v );
}
Vec_StrPush( vConfigs2, (char)mappingBytes[0] );
Vec_StrPush( vConfigs2, (char)mappingBytes[1] );
// Write input mappings for second LUT4 (4 inputs)
mappingBytes[0] = mappingBytes[1] = 0;
int iSpecial = -1;
for ( i = 0; i < 4; i++ )
{
int v = (int)((z >> (48 + (i << 2))) & 7);
if ( v == 6 && nLeaves == 5 )
mappingBytes[i / 2] |= (0 << ((i % 2) * 4)); // constant 0
Vec_StrPush( vConfigs2, 0 );
else if ( v != 7 )
Vec_StrPush( vConfigs2, 2+v );
else if ( v == 7 )
mappingBytes[i / 2] |= ((7+2) << ((i % 2) * 4)); // output of first LUT at index N+2 where N=7
else
mappingBytes[i / 2] |= ((v+2) << ((i % 2) * 4)); // leaf v (direct mapping)
iSpecial = i;
}
Vec_StrPush( vConfigs2, (char)mappingBytes[0] );
Vec_StrPush( vConfigs2, (char)mappingBytes[1] );
// Transform the truth table
assert( iSpecial >= 0 );
word Truth = (z >> 32) & 0xFFFF;
Truth = Abc_Tt6Stretch( Truth, 4 );
for ( int v = iSpecial; v < 3; v++ )
Truth = Abc_Tt6SwapAdjacent( Truth, v );
// Write truth tables
word Truth1 = z & 0xFFFF;
word Truth2 = (z >> 32) & 0xFFFF;
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
//word Truth2 = (z >> 32) & 0xFFFF;
word Truth2 = Truth & 0xFFFF;
Vec_StrPush( vConfigs2, (char)((Truth1 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
// Pad to 4-byte boundary
while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 )
Vec_StrPush( vConfigs2, 0 );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 12 == Vec_StrSize(vConfigs2) );
}
else
else // 14 bytes = 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
{
CellId = 2;
int Pla2Var[9];
@ -2090,41 +2211,26 @@ void Gia_ManFromIfGetConfig2( Vec_Str_t * vConfigs2, If_Man_t * pIfMan, word * p
If_PermUnpack( (unsigned)(z >> 32), Pla2Var );
// Write CellId
Vec_StrPush( vConfigs2, (char)CellId );
// Write input mappings (9 inputs, 4 bits each, packed)
unsigned char mappingByte = 0;
int bitPos = 0;
// Write input mapping
for ( i = 0; i < 9; i++ )
{
int v;
if ( Pla2Var[i] == 9 ) // constant 0
v = 0;
else // leaf index
v = Pla2Var[i] + 2;
if ( bitPos == 0 ) {
mappingByte = v & 0xF;
bitPos = 4;
}
else {
mappingByte |= (v & 0xF) << 4;
Vec_StrPush( vConfigs2, (char)mappingByte );
bitPos = 0;
}
}
// Push last byte if needed
if ( bitPos != 0 )
Vec_StrPush( vConfigs2, (char)mappingByte );
if ( Pla2Var[i] == 9 )
Vec_StrPush( vConfigs2, 0 );
else
Vec_StrPush( vConfigs2, Pla2Var[i] + 2 );
}
// Write truth tables for the two LUT4s only (MUX is structural, not a LUT)
word Truth1 = z & 0xFFFF;
word Truth2 = (z >> 16) & 0xFFFF;
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth1 >> 8) & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
Vec_StrPush( vConfigs2, (char)(Truth1 & 0xFF) );
Vec_StrPush( vConfigs2, (char)((Truth2 >> 8) & 0xFF) );
// Pad to 4-byte boundary
while ( (Vec_StrSize(vConfigs2) - startPos) % 4 != 0 )
Vec_StrPush( vConfigs2, 0 );
Vec_StrPush( vConfigs2, (char)(Truth2 & 0xFF) );
assert( startPos + 14 == Vec_StrSize(vConfigs2) );
}
}
if ( pIfMan->pPars->fVerboseTrace )
Gia_ManConfigPrint2( (unsigned char*)Vec_StrEntryP(vConfigs2, startPos), nLeaves );
}
int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vConfigs )
{
@ -2924,7 +3030,7 @@ Gia_Man_t * Gia_ManPerformMappingInt( Gia_Man_t * p, If_Par_t * pPars )
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
// print delay trace
if ( pPars->fVerboseTrace )
if ( pPars->fVerboseTrace && !pPars->fEnableCheck07 )
{
pNew->pLutLib = pPars->pLutLib;
Gia_ManDelayTraceLutPrint( pNew, 1 );

296
src/aig/gia/giaLutCas.c Normal file
View File

@ -0,0 +1,296 @@
/**CFile****************************************************************
FileName [giaLutCas.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [LUT cascade generator.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaLutCas.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "gia.h"
#include "sat/cnf/cnf.h"
#include "misc/util/utilTruth.h"
#include "sat/cadical/cadicalSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManGenSymFun_rec( Gia_Man_t * p, word Str, int nChars, Vec_Ptr_t * vStrs, Vec_Wec_t * vLits, Vec_Int_t * vIns )
{
if ( Str == 0 ) return 0;
if ( Str == Abc_Tt6Mask(nChars) ) return 1;
assert( nChars > 1 );
Vec_Wrd_t * vStore = (Vec_Wrd_t *)Vec_PtrEntry(vStrs, nChars-1);
Vec_Int_t * vValue = Vec_WecEntry(vLits, nChars-1);
int Index;
if ( (Index = Vec_WrdFind(vStore, Str)) >= 0 )
return Vec_IntEntry(vValue, Index);
word Str0 = Str & ~Abc_Tt6MaskI(nChars-1);
word Str1 = Str >> 1;
int Lit0 = Gia_ManGenSymFun_rec( p, Str0, nChars-1, vStrs, vLits, vIns );
int Lit1 = Gia_ManGenSymFun_rec( p, Str1, nChars-1, vStrs, vLits, vIns );
int Lit = Gia_ManAppendMux2( p, Vec_IntEntry(vIns, nChars-2), Lit1, Lit0 );
Vec_WrdPush( vStore, Str );
Vec_WrdPush( vStore, ~Str & Abc_Tt6Mask(nChars) );
Vec_IntPush( vValue, Lit );
Vec_IntPush( vValue, Abc_LitNot(Lit) );
return Lit;
}
Gia_Man_t * Gia_ManGenSymFun( Vec_Wrd_t * vFuns, int nChars, int fVerbose )
{
assert( nChars <= 64 );
word Str; int i;
Vec_Ptr_t * vStrs = Vec_PtrAlloc(nChars);
for ( i = 0; i < nChars; i++ )
Vec_PtrPush( vStrs, Vec_WrdAlloc(0) );
Vec_Wec_t * vLits = Vec_WecStart(nChars);
Vec_Int_t * vOuts = Vec_IntAlloc(Vec_WrdSize(vFuns));
Gia_Man_t * pNew = Gia_ManStart( 10000 );
pNew->pName = Abc_UtilStrsav( "sym" );
Vec_Int_t * vIns = Vec_IntAlloc(nChars-1);
for ( i = 0; i < nChars-1; i++ )
Vec_IntPush(vIns, Gia_ManAppendCi(pNew));
Vec_WrdForEachEntry( vFuns, Str, i )
Vec_IntPush( vOuts, Gia_ManGenSymFun_rec(pNew, Str, nChars, vStrs, vLits, vIns ) );
Vec_WrdForEachEntry( vFuns, Str, i )
Gia_ManAppendCo(pNew, Vec_IntEntry(vOuts,i) );
for ( i = 0; i < nChars; i++ )
Vec_WrdFree( (Vec_Wrd_t *)Vec_PtrEntry(vStrs, i) );
Vec_PtrFree(vStrs);
Vec_WecFree(vLits);
Vec_IntFree(vOuts);
Vec_IntFree(vIns);
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Gia_LutCasSort( char * pStr, int iStart, int nChars )
{
int i, j;
for ( i = iStart; i < iStart + nChars - 1; i++ )
for ( j = i + 1; j < iStart + nChars; j++ )
if ( pStr[i] > pStr[j] )
ABC_SWAP( char, pStr[i], pStr[j] );
}
char * Gia_LutCasPerm( int nVars, int nLuts, int LutSize )
{
assert( nVars <= 26 && nLuts <= 100 );
int nStrLen = nLuts * LutSize;
char * pRes = ABC_CALLOC( char, nStrLen+1 );
int i, j, iVar, pPerm[26], nVarCount[100] = {0};
// create a random permutation
for ( i = 0; i < nVars; i++ )
pPerm[i] = i;
for ( i = nVars - 1; i > 0; i-- ) {
j = rand() % (i + 1);
ABC_SWAP( int, pPerm[i], pPerm[j] );
}
// assign the first variable
for ( i = 0; i < nLuts; i++ ) {
pRes[i * LutSize] = i ? '_' : 'a' + pPerm[0];
nVarCount[i] = 1;
}
// First pass: distribute each variable (starting from the second in permutation) to at least one LUT
for ( i = 1; i < nVars; i++ ) {
// Find a LUT with space that doesn't have this variable
int Tries = 0, iLut = rand() % nLuts;
while ( nVarCount[iLut] >= LutSize && Tries++ < nLuts )
iLut = (iLut + 1) % nLuts;
// the variables are unique - no need to check this
pRes[iLut * LutSize + nVarCount[iLut]] = 'a' + pPerm[i];
nVarCount[iLut]++;
}
// Second pass: fill remaining slots with random variables (cycling through permutation)
for ( i = 0; i < nLuts; i++ ) {
while ( nVarCount[i] < LutSize ) {
iVar = pPerm[rand() % nVars];
// Check this LUT already has this variable
for ( j = 0; j < nVarCount[i]; j++ )
if ( pRes[i * LutSize + j] == 'a' + iVar )
break;
if ( j == nVarCount[i] ) { // does not have
pRes[i * LutSize + nVarCount[i]] = 'a' + iVar;
nVarCount[i]++;
}
}
}
// Sort inputs within each LUT (skip '_' for non-first LUTs)
Gia_LutCasSort( pRes, 0, LutSize );
for ( i = 1; i < nLuts; i++ )
Gia_LutCasSort( pRes + i * LutSize, 1, LutSize-1 );
return pRes;
}
int Gia_ManGenLutCas_rec( Gia_Man_t * pNew, Vec_Int_t * vCtrls, int iCtrl, Vec_Int_t * vDatas, int Shift, int Offset )
{
if ( iCtrl-- == 0 )
return Vec_IntEntry( vDatas, Shift );
int iLit0 = Gia_ManGenLutCas_rec( pNew, vCtrls, iCtrl, vDatas, Shift, Offset );
int iLit1 = Gia_ManGenLutCas_rec( pNew, vCtrls, iCtrl, vDatas, Shift + (1<<iCtrl), Offset );
return Gia_ManAppendMux( pNew, Vec_IntEntry(vCtrls, iCtrl+Offset), iLit1, iLit0 );
}
int Gia_ManGenWire( Gia_Man_t * pNew, Vec_Int_t * vCtrls, Vec_Int_t * vParams2, int iParam2 )
{
int nVars = Vec_IntSize(vCtrls);
int nBits = Abc_Base2Log(nVars);
while ( Vec_IntSize(vCtrls) < (1 << nBits) )
Vec_IntPush( vCtrls, 0 );
int iRes = Gia_ManGenLutCas_rec( pNew, vParams2, nBits, vCtrls, 0, iParam2 );
Vec_IntShrink( vCtrls, nVars );
return iRes;
}
Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose )
{
if ( Seed )
srand(Seed);
else {
struct timespec ts;
clock_gettime(CLOCK_REALTIME, &ts);
unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec);
srand(seed);
}
int fOwnPerm = (pPermStr == NULL);
char * pPerm = fOwnPerm ? Gia_LutCasPerm( nVars, nLuts, LutSize ) : pPermStr;
int nParams = nLuts * (1 << LutSize);
// count how many variables are unassigned in the permutation
int nParams2 = 0;
for ( int v = 0; v < strlen(pPerm); v++ )
if ( pPerm[v] == '*' )
nParams2 += Abc_Base2Log(nVars);
if ( fVerbose )
printf( "Generating AIG with %d parameters (%d functional + %d structural) and %d inputs using fanin assignment \"%s\".\n",
nParams+nParams2, nParams, nParams2, nVars, pPerm );
Gia_Man_t * pNew = Gia_ManStart( nParams + nVars );
pNew->pName = Abc_UtilStrsav( pPerm );
Vec_Int_t * vDatas = Vec_IntAlloc( nParams );
Vec_Int_t * vWires = Vec_IntAlloc( nParams2 );
Vec_Int_t * vCtrls = Vec_IntAlloc( nVars );
for ( int i = 0; i < nParams; i++ )
Vec_IntPush( vDatas, Gia_ManAppendCi(pNew) );
for ( int i = 0; i < nParams2; i++ )
Vec_IntPush( vWires, Gia_ManAppendCi(pNew) );
for ( int i = 0; i < nVars; i++ )
Vec_IntPush( vCtrls, Gia_ManAppendCi(pNew) );
Vec_Int_t * vLits = Vec_IntStart( LutSize );
Vec_IntWriteEntry( vLits, 0, pPerm[0] == '*' ? Gia_ManGenWire(pNew, vCtrls, vWires, 0) : Vec_IntEntry(vCtrls, (int)(pPerm[0]-'a')) );
int iWireVars = pPerm[0] == '*' ? Abc_Base2Log(nVars) : 0;
char * pCur = pPerm;
for ( int i = 0; i < nLuts; i++ ) {
assert( i == 0 || *pCur == '_' );
pCur++;
for ( int k = 1; k < LutSize; k++ ) {
Vec_IntWriteEntry( vLits, k, *pCur == '*' ? Gia_ManGenWire(pNew, vCtrls, vWires, iWireVars) : Vec_IntEntry(vCtrls, (int)(*pCur - 'a')) );
iWireVars += *pCur++ == '*' ? Abc_Base2Log(nVars) : 0;
}
Vec_IntWriteEntry( vLits, 0, Gia_ManGenLutCas_rec(pNew, vLits, LutSize, vDatas, i * (1 << LutSize), 0) );
}
assert( iWireVars == nParams2 );
// if the AIG is given, create a miter
int iLit = Vec_IntEntry(vLits, 0);
if ( p ) {
assert( Gia_ManCiNum(p) == nVars );
assert( Gia_ManCoNum(p) == 1 );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_Obj_t * pObj; int i;
Gia_ManForEachCi( p, pObj, i )
pObj->Value = Vec_IntEntry(vCtrls, i);
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
iLit = Gia_ManAppendXor( pNew, iLit, Gia_ObjFanin0Copy(Gia_ManCo(p, 0)) );
iLit = Abc_LitNot(iLit);
}
Gia_ManAppendCo( pNew, iLit );
Vec_IntFree( vDatas );
Vec_IntFree( vCtrls );
Vec_IntFree( vWires );
Vec_IntFree( vLits );
if ( fOwnPerm )
ABC_FREE( pPerm );
return pNew;
}
/*
int Gia_ManGenLutCasSolve( int nVars, int nLuts, int LutSize, char * pTtStr, int fVerbose )
{
extern Gia_Man_t * Gia_QbfQuantifyAll( Gia_Man_t * p, int nPars, int fAndAll, int fOrAll );
assert( strlen(pTtStr) <= 1024 );
word pTruth[64] = {0};
int i, Id, nVars = Abc_TtReadHex( pTruth, pTtStr );
assert( nVars <= 12 );
int nParams = nLuts * (1 << LutSize);
Gia_Man_t * pCas = Gia_ManGenLutCas( NULL, NULL, nVars, nLuts, LutSize, 0, fVerbose );
Gia_Man_t * pCofs = Gia_QbfQuantifyAll( pCas, nParams, 0, 0 );
Gia_ManFree( pCas );
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCofs, 8, 0, 0, 0, 0 );
cadical_solver* pSat = cadical_solver_new(void);
cadical_solver_setnvars( pSat, pCnf->nVars );
// add output literals
assert( Gia_ManCoNum(pCofs) == (1 << nVars) );
Gia_ManForEachCoId( pCofs, Id, i ) {
int Lit = Abc_Var2Lit(pCnf->pVarNums[Id], Abc_TtGetBit(pTruth, i));
int status = cadical_solver_addclause( pSat, &Lit, &Lit+1 );
}
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !cadical_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) {
Cnf_DataFree( pCnf );
return 0;
}
Cnf_DataFree( pCnf );
Gia_ManFree( pCofs );
int status = cadical_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
for ( i = 0; i < nLuts; i++, printf(" ") )
for ( k = 0; k < (1 << LutSize); k++ ) {
int Value = cadical_solver_get_var_value(pSat, i*(1 << LutSize) + k);
printf( "%d", Value );
}
cadical_solver_delete( pSat );
return 1;
}
*/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

38
src/aig/gia/giaMulFind.c
View File

@ -661,15 +661,15 @@ Vec_Wec_t * Gia_ManMulFindBInputs( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMulFindTfo( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1 )
Vec_Int_t * Gia_ManMulFindTfo( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1, int fLits )
{
Vec_Int_t * vTfo = Vec_IntAlloc( 100 );
Gia_Obj_t * pObj; int i, Obj;
Gia_ManIncrementTravId( p );
Vec_IntForEachEntry( vIn0, Obj, i )
Gia_ObjSetTravIdCurrentId( p, Obj );
Gia_ObjSetTravIdCurrentId( p, fLits ? Abc_Lit2Var(Obj) : Obj );
Vec_IntForEachEntry( vIn1, Obj, i )
Gia_ObjSetTravIdCurrentId( p, Obj );
Gia_ObjSetTravIdCurrentId( p, fLits ? Abc_Lit2Var(Obj) : Obj );
Gia_ManForEachAnd( p, pObj, i ) {
if ( Gia_ObjIsTravIdCurrentId(p, i) )
continue;
@ -678,15 +678,15 @@ Vec_Int_t * Gia_ManMulFindTfo( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1
}
return vTfo;
}
Vec_Wrd_t * Gia_ManMulFindSimCone( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1, Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, Vec_Int_t * vTfo )
Vec_Wrd_t * Gia_ManMulFindSimCone( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t * vIn1, Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, Vec_Int_t * vTfo, int fLits )
{
Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_IntSize(vTfo) );
Vec_Wrd_t * vSims = Vec_WrdStart( Gia_ManObjNum(p) );
Gia_Obj_t * pObj; int i, Obj;
Vec_IntForEachEntry( vIn0, Obj, i )
Vec_WrdWriteEntry( vSims, Obj, Vec_WrdEntry(vSim0, i) );
Vec_WrdWriteEntry( vSims, fLits ? Abc_Lit2Var(Obj) : Obj, (fLits && Abc_LitIsCompl(Obj)) ? ~Vec_WrdEntry(vSim0, i) : Vec_WrdEntry(vSim0, i) );
Vec_IntForEachEntry( vIn1, Obj, i )
Vec_WrdWriteEntry( vSims, Obj, Vec_WrdEntry(vSim1, i) );
Vec_WrdWriteEntry( vSims, fLits ? Abc_Lit2Var(Obj) : Obj, (fLits && Abc_LitIsCompl(Obj)) ? ~Vec_WrdEntry(vSim1, i) : Vec_WrdEntry(vSim1, i) );
Gia_ManForEachObjVec( vTfo, p, pObj, i ) {
word Sim0 = Vec_WrdEntry(vSims, Gia_ObjFaninId0p(p, pObj) );
word Sim1 = Vec_WrdEntry(vSims, Gia_ObjFaninId1p(p, pObj) );
@ -697,17 +697,17 @@ Vec_Wrd_t * Gia_ManMulFindSimCone( Gia_Man_t * p, Vec_Int_t * vIn0, Vec_Int_t *
Vec_WrdFree( vSims );
return vRes;
}
int Gia_ManMulFindGetArg( Vec_Wrd_t * vSim, int i, int fSigned )
iword Gia_ManMulFindGetArg( Vec_Wrd_t * vSim, int i, int fSigned )
{
int w, Res = 0; word Word = 0;
int w; iword Res = 0; word Word = 0;
Vec_WrdForEachEntry( vSim, Word, w )
if ( (Word >> i) & 1 )
Res |= (1 << w);
Res |= ((iword)1 << w);
if ( fSigned && ((Word >> i) & 1) )
Res |= ~0 << Vec_WrdSize(vSim);
Res |= ~(iword)0 << Vec_WrdSize(vSim);
return Res;
}
void Gia_ManMulFindSetArg( Vec_Wrd_t * vSim, int i, int iNum )
void Gia_ManMulFindSetArg( Vec_Wrd_t * vSim, int i, iword iNum )
{
int w; word * pWords = Vec_WrdArray(vSim);
for ( w = 0; w < Vec_WrdSize(vSim); w++ )
@ -716,17 +716,17 @@ void Gia_ManMulFindSetArg( Vec_Wrd_t * vSim, int i, int iNum )
}
Vec_Wrd_t * Gia_ManMulFindSim( Vec_Wrd_t * vSim0, Vec_Wrd_t * vSim1, int fSigned )
{
assert( Vec_WrdSize(vSim0) + Vec_WrdSize(vSim1) <= 30 );
assert( Vec_WrdSize(vSim0) + Vec_WrdSize(vSim1) <= 62 );
Vec_Wrd_t * vRes = Vec_WrdStart( Vec_WrdSize(vSim0) + Vec_WrdSize(vSim1) );
for ( int i = 0; i < 64; i++ )
{
int a = Gia_ManMulFindGetArg( vSim0, i, fSigned );
int b = Gia_ManMulFindGetArg( vSim1, i, fSigned );
iword a = Gia_ManMulFindGetArg( vSim0, i, fSigned );
iword b = Gia_ManMulFindGetArg( vSim1, i, fSigned );
Gia_ManMulFindSetArg( vRes, i, a * b );
}
return vRes;
}
void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose )
void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fLits, int fVerbose )
{
Abc_Random(1);
for ( int m = 0; m < Vec_WecSize(vTerms)/3; m++ ) {
@ -737,8 +737,8 @@ void Gia_ManMulFindOutputs( Gia_Man_t * p, Vec_Wec_t * vTerms, int fVerbose )
Vec_Wrd_t * vSim1 = Vec_WrdStartRandom( Vec_IntSize(vIn1) );
Vec_Wrd_t * vSimU = Gia_ManMulFindSim( vSim0, vSim1, 0 );
Vec_Wrd_t * vSimS = Gia_ManMulFindSim( vSim0, vSim1, 1 );
Vec_Int_t * vTfo = Gia_ManMulFindTfo( p, vIn0, vIn1 );
Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo );
Vec_Int_t * vTfo = Gia_ManMulFindTfo( p, vIn0, vIn1, fLits );
Vec_Wrd_t * vSims = Gia_ManMulFindSimCone( p, vIn0, vIn1, vSim0, vSim1, vTfo, fLits );
Vec_Int_t * vOutU = Vec_IntAlloc( 100 );
Vec_Int_t * vOutS = Vec_IntAlloc( 100 );
word Word; int w, iPlace;
@ -814,7 +814,7 @@ Vec_Wec_t * Gia_ManMulFindA( Gia_Man_t * p, Vec_Wec_t * vCuts3, int fVerbose )
Vec_Wec_t * vXors = Gia_ManMulFindXors( p, vCuts3, fVerbose );
Vec_Wec_t * vTerms = Gia_ManMulFindAInputs2( p, fVerbose );
if ( Vec_WecSize(vTerms) )
Gia_ManMulFindOutputs( p, vTerms, fVerbose );
Gia_ManMulFindOutputs( p, vTerms, 0, fVerbose );
Vec_WecFree( vXors );
return vTerms;
}
@ -824,7 +824,7 @@ Vec_Wec_t * Gia_ManMulFindB( Gia_Man_t * p, Vec_Wec_t * vCuts4, Vec_Wec_t * vCut
if ( Vec_WecSize(vCuts4) && Vec_WecSize(vCuts5) )
vTerms = Gia_ManMulFindBInputs2( p, vCuts4, vCuts5, fVerbose );
if ( Vec_WecSize(vTerms) )
Gia_ManMulFindOutputs( p, vTerms, fVerbose );
Gia_ManMulFindOutputs( p, vTerms, 0, fVerbose );
return vTerms;
}
void Gia_ManMulFindPrintSet( Vec_Int_t * vSet, int fLit, int fSkipLast )

48
src/aig/gia/giaMulFind3.c Normal file
View File

@ -0,0 +1,48 @@
/**CFile****************************************************************
FileName [giaMulFind3.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Scalable AIG package.]
Synopsis [Multiplier detection.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: giaMulFind3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include <math.h>
#include "gia.h"
#include "misc/vec/vecHsh.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
void Gia_ManMulFindNew( Gia_Man_t * p, int nABits, int nFanLim, int fLits, int fVerbose )
{
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

161
src/aig/gia/giaNf.c
View File

@ -2241,9 +2241,159 @@ void Nf_ManDumpMatches( Nf_Man_t * p )
Nf_CutForEachVarCompl( pCut, pM->Cfg, iVar, fCompl, k )
fprintf( pFile, " %d", Abc_Var2Lit(iVar, fCompl) );
fprintf( pFile, "\n" );
}
}
fclose( pFile );
}
void Nf_ManDumpMatchesPrint( Gia_Man_t * pGia, Vec_Int_t * vStore, int nCutSize, int nMaxMatches )
{
int iObj, n, f, m;
int nObjs = Gia_ManObjNum( pGia );
int * pData;
if ( vStore == NULL || nCutSize == 0 || nMaxMatches == 0 )
return;
pData = Vec_IntArray( vStore );
for ( iObj = 0; iObj < nObjs; iObj++ )
{
Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj );
int fPrint = 0;
if ( Gia_ObjIsAnd(pObj) && !Gia_ObjIsBuf(pObj) )
fPrint = 1;
else if ( Gia_ObjIsCo(pObj) )
fPrint = 1;
if ( !fPrint )
continue;
for ( n = 0; n < 2; n++ )
{
int * pNodeStore = pData + (2 * iObj + n) * nCutSize * nMaxMatches;
printf( "Node %d (%s) polarity %d has %d matches:\n", iObj, Gia_ObjIsCo(pObj) ? "CO" : "AND", n, nMaxMatches );
for ( f = 0; f < nCutSize; f++ )
{
printf( " Input %d:", f );
for ( m = 0; m < nMaxMatches; m++ )
printf( " %4d", pNodeStore[f * nMaxMatches + m] );
printf( "\n" );
}
}
}
}
void Nf_ManDumpMatchesBin( Nf_Man_t * p, int nMaxMatches )
{
const char * pNameNA = "n/a";
Gia_Obj_t * pObj;
Vec_Int_t * vStore;
int * pData;
int iObj, n, nMatches = 0;
int nCutSize = p->pPars->nLutSize;
int nObjs = Gia_ManObjNum(p->pGia);
char * pFileNameBin = NULL, * pFileNameGates = NULL;
FILE * pFileBin = NULL, * pFileGates = NULL;
if ( nMaxMatches <= 0 )
return;
if ( p->pPars->ZFile == NULL )
return;
assert( nCutSize > 0 && nCutSize <= NF_LEAF_MAX );
vStore = Vec_IntStart( 2 * nObjs * nCutSize * nMaxMatches );
pData = Vec_IntArray( vStore );
pFileNameBin = Abc_UtilStrsav( Extra_FileNameGenericAppend( p->pPars->ZFile, ".bin" ) );
pFileNameGates = Abc_UtilStrsav( Extra_FileNameGenericAppend( p->pPars->ZFile, ".gates" ) );
pFileBin = fopen( pFileNameBin, "wb" );
pFileGates = fopen( pFileNameGates, "wb" );
if ( pFileBin == NULL || pFileGates == NULL ) {
printf( "Cannot open match dump files \"%s\" and \"%s\".\n", pFileNameBin, pFileNameGates );
if ( pFileBin ) fclose( pFileBin );
if ( pFileGates ) fclose( pFileGates );
ABC_FREE( pFileNameBin );
ABC_FREE( pFileNameGates );
Vec_IntFree( vStore );
return;
}
for ( iObj = 0; iObj < nObjs; iObj++ ) {
pObj = Gia_ManObj( p->pGia, iObj );
assert( !Gia_ObjIsBuf(pObj) );
for ( n = 0; n < 2; n++ ) {
int Slot = 0;
int k;
int LitBuffer[NF_LEAF_MAX];
int * pNodeStore = pData + (2 * iObj + n) * nCutSize * nMaxMatches;
memset( pNodeStore, 0, sizeof(int) * nCutSize * nMaxMatches );
if ( Gia_ObjIsCo(pObj) && n == 0 && Slot < nMaxMatches ) {
pNodeStore[Slot] = Gia_ObjFaninLit0p( p->pGia, pObj );
fprintf( pFileGates, "%s %.2f\n", pNameNA, 0.0 );
Slot++;
nMatches++;
}
if ( Gia_ObjIsAnd(pObj) ) {
int c, * pCut, * pCutSet = Nf_ObjCutSet( p, iObj );
Nf_SetForEachCut( pCutSet, pCut, c )
{
int iFuncLit, fComplExt;
Vec_Int_t * vVec;
int j, Info, Offset;
if ( Slot == nMaxMatches )
break;
if ( Abc_Lit2Var(Nf_CutFunc(pCut)) >= Vec_WecSize(p->vTt2Match) )
continue;
if ( Nf_CutIsTriv(pCut, iObj) )
continue;
assert( Nf_CutSize(pCut) <= nCutSize );
iFuncLit = Nf_CutFunc(pCut);
fComplExt = Abc_LitIsCompl(iFuncLit);
vVec = Vec_WecEntry( p->vTt2Match, Abc_Lit2Var(iFuncLit) );
Vec_IntForEachEntryDouble( vVec, Info, Offset, j )
{
Nf_Cfg_t Cfg = Nf_Int2Cfg( Offset );
int fCompl = Cfg.fCompl ^ fComplExt;
Mio_Cell2_t * pCell = NULL;
const char * pGateName;
float Area = 0.0;
int iFanin, fComplF, nLitCount = 0;
if ( fCompl != n )
continue;
if ( Slot == nMaxMatches )
break;
if ( Info >= 0 )
pCell = Nf_ManCell( p, Info );
pGateName = (pCell && pCell->pName) ? pCell->pName : pNameNA;
Area = pCell ? pCell->AreaF : 0.0f;
Nf_CutForEachVarCompl( pCut, Cfg, iFanin, fComplF, k )
LitBuffer[nLitCount++] = Abc_Var2Lit( iFanin, fComplF );
for ( k = 0; k < nCutSize; k++ )
pNodeStore[k * nMaxMatches + Slot] = 0;
for ( k = 0; k < nLitCount; k++ )
pNodeStore[k * nMaxMatches + Slot] = LitBuffer[k];
fprintf( pFileGates, "%s %.2f\n", pGateName, Area );
Slot++;
nMatches++;
}
}
}
while ( Slot < nMaxMatches ) {
fprintf( pFileGates, "%s %.2f\n", pNameNA, 0.0 );
Slot++;
}
}
}
{
int Num = 3;
fwrite( &Num, 4, 1, pFileBin );
Num = 2 * nObjs;
fwrite( &Num, 4, 1, pFileBin );
Num = nCutSize;
fwrite( &Num, 4, 1, pFileBin );
Num = nMaxMatches;
fwrite( &Num, 4, 1, pFileBin );
}
fwrite( pData, 4, Vec_IntSize(vStore), pFileBin );
if ( p->pPars->fVerbose )
printf( "Dumped %d matches (limit %d) into binary file \"%s\" (%.2f MB).\n",
nMatches, nMaxMatches, pFileNameBin, Vec_IntMemory(vStore)/(1<<20) );
fclose( pFileBin );
fclose( pFileGates );
//Nf_ManDumpMatchesPrint( p->pGia, vStore, nCutSize, nMaxMatches );
Vec_IntFree( vStore );
ABC_FREE( pFileNameBin );
ABC_FREE( pFileNameGates );
}
/**Function*************************************************************
@ -2300,8 +2450,12 @@ Gia_Man_t * Nf_ManDeriveMapping( Nf_Man_t * p )
}
// assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
p->pGia->vCellMapping = vMapping;
if ( p->pPars->ZFile )
Nf_ManDumpMatches( p );
if ( p->pPars->ZFile ) {
if ( p->pPars->nMaxMatches )
Nf_ManDumpMatchesBin( p, p->pPars->nMaxMatches );
else
Nf_ManDumpMatches( p );
}
return p->pGia;
}
void Nf_ManUpdateStats( Nf_Man_t * p )
@ -2775,4 +2929,3 @@ Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * p, Jf_Par_t * pPars )
ABC_NAMESPACE_IMPL_END

64
src/aig/gia/giaQbf.c
View File

@ -23,6 +23,7 @@
#include "sat/bsat/satStore.h"
#include "misc/extra/extra.h"
#include "sat/glucose/AbcGlucose.h"
#include "sat/cadical/cadicalSolver.h"
#include "misc/util/utilTruth.h"
#include "base/io/ioResub.h"
@ -45,6 +46,7 @@ struct Qbf_Man_t_
sat_solver * pSatVer; // verification instance
sat_solver * pSatSyn; // synthesis instance
bmcg_sat_solver*pSatSynG; // synthesis instance
cadical_solver* pSatSynC; // synthesis instance
Vec_Int_t * vValues; // variable values
Vec_Int_t * vParMap; // parameter mapping
Vec_Int_t * vLits; // literals for the SAT solver
@ -534,7 +536,7 @@ void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars )
SeeAlso []
***********************************************************************/
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose )
Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fCadical, int fVerbose )
{
Qbf_Man_t * p;
Cnf_Dat_t * pCnf;
@ -551,11 +553,13 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbos
p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
p->pSatSyn = sat_solver_new();
p->pSatSynG = fGlucose ? bmcg_sat_solver_start() : NULL;
p->pSatSynC = fCadical ? cadical_solver_new() : NULL;
p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) );
p->vParMap = Vec_IntStartFull( nPars );
p->vLits = Vec_IntAlloc( nPars );
sat_solver_setnvars( p->pSatSyn, nPars );
if ( p->pSatSynG ) bmcg_sat_solver_set_nvars( p->pSatSynG, nPars );
if ( p->pSatSynC ) cadical_solver_setnvars( p->pSatSynC, nPars );
Cnf_DataFree( pCnf );
return p;
}
@ -564,6 +568,7 @@ void Gia_QbfFree( Qbf_Man_t * p )
sat_solver_delete( p->pSatVer );
sat_solver_delete( p->pSatSyn );
if ( p->pSatSynG ) bmcg_sat_solver_stop( p->pSatSynG );
if ( p->pSatSynC ) cadical_solver_delete( p->pSatSynC );
Vec_IntFree( p->vLits );
Vec_IntFree( p->vValues );
Vec_IntFree( p->vParMap );
@ -749,6 +754,21 @@ int Gia_QbfAddCofactorG( Qbf_Man_t * p, Gia_Man_t * pCof )
Cnf_DataFree( pCnf );
return 1;
}
int Gia_QbfAddCofactorC( Qbf_Man_t * p, Gia_Man_t * pCof )
{
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 );
int i, iFirstVar = pCnf->nVars - Gia_ManPiNum(pCof); //-1
pCnf->pMan = NULL;
Cnf_SpecialDataLift( pCnf, cadical_solver_nvars(p->pSatSynC), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !cadical_solver_addclause( p->pSatSynC, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
{
Cnf_DataFree( pCnf );
return 0;
}
Cnf_DataFree( pCnf );
return 1;
}
/**Function*************************************************************
@ -766,16 +786,20 @@ void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues )
int i;
Vec_IntClear( vValues );
for ( i = 0; i < p->nPars; i++ )
Vec_IntPush( vValues, p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) );
Vec_IntPush( vValues, p->pSatSynC ? cadical_solver_get_var_value(p->pSatSynC, i) :
p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) );
}
void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter )
{
printf( "%5d : ", Iter );
assert( Vec_IntSize(vValues) == p->nVars );
Vec_IntPrintBinary( vValues ); printf( " " );
printf( "Var =%7d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) );
printf( "Cla =%7d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) );
printf( "Conf =%9d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
printf( "Var =%7d ", p->pSatSynC ? cadical_solver_nvars(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) );
printf( "Cla =%7d ", p->pSatSynC ? cadical_solver_nclauses(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) );
printf( "Conf =%9d ", p->pSatSynC ? cadical_solver_nconflicts(p->pSatSynC) :
p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) );
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
}
@ -869,9 +893,9 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues )
SeeAlso []
***********************************************************************/
int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose )
int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fSilent, int fVerbose )
{
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose );
Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fCadical, fVerbose );
Gia_Man_t * pCof;
int i, status, RetValue = 0;
abctime clk;
@ -886,12 +910,15 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
// generate next constraint
assert( Vec_IntSize(p->vValues) == p->nVars );
pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap );
status = p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof );
status = p->pSatSynC ? Gia_QbfAddCofactorC( p, pCof ) :
p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof );
Gia_ManStop( pCof );
if ( status == 0 ) { RetValue = 1; break; }
// synthesize next assignment
clk = Abc_Clock();
if ( p->pSatSynG )
if ( p->pSatSynC )
status = cadical_solver_solve( p->pSatSynC, NULL, NULL, 0, 0, 0, 0 );
else if ( p->pSatSynG )
status = bmcg_sat_solver_solve( p->pSatSynG, NULL, 0 );
else
status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 );
@ -912,9 +939,18 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
if ( RetValue == 0 )
{
int nZeros = Vec_IntCountZero( p->vValues );
printf( "Parameters: " );
printf( "Parameters (%d): 0x", nPars );
assert( Vec_IntSize(p->vValues) == nPars );
Vec_IntPrintBinary( p->vValues );
//Vec_IntPrintBinary( p->vValues );
while ( Vec_IntSize(p->vValues) % 4 )
Vec_IntPush(p->vValues, 0);
for ( int i = Vec_IntSize(p->vValues)/4 - 1; i >= 0; i-- ) {
int Digit = Vec_IntEntry(p->vValues, 4*i+0);
Digit |= Vec_IntEntry(p->vValues, 4*i+1) << 1;
Digit |= Vec_IntEntry(p->vValues, 4*i+2) << 2;
Digit |= Vec_IntEntry(p->vValues, 4*i+3) << 3;
printf( "%x", Digit );
}
printf( " Statistics: 0=%d 1=%d\n", nZeros, Vec_IntSize(p->vValues) - nZeros );
if ( nEncVars )
{
@ -929,9 +965,9 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
printf( "The problem aborted after %d conflicts. ", nConfLimit );
else if ( RetValue == -1 && nIterLimit )
printf( "The problem aborted after %d iterations. ", nIterLimit );
else if ( RetValue == 1 )
else if ( RetValue == 1 && !fSilent )
printf( "The problem is UNSAT after %d iterations. ", i );
else
else if ( !fSilent )
printf( "The problem is SAT after %d iterations. ", i );
if ( fVerbose )
{
@ -940,7 +976,7 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i
Abc_PrintTime( 1, "Other", Abc_Clock() - p->clkStart - p->clkSat );
Abc_PrintTime( 1, "TOTAL", Abc_Clock() - p->clkStart );
}
else
else if ( !fSilent )
Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart );
Gia_QbfFree( p );
return RetValue;

4
src/aig/gia/giaSweep.c
View File

@ -751,7 +751,7 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
if ( pNew == NULL )
return NULL;
Gia_ManTransferTiming( pNew, p );
nFlops = Vec_IntCountEntry(pNew->vRegClasses, 1);
nFlops = pNew->vRegClasses ? Vec_IntCountEntry(pNew->vRegClasses, 1) : 0;
// find global equivalences
pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, pParsC ? 0 : 1 );
//Gia_DumpAiger( pClp, p->pSpec, 1, 1 );
@ -775,7 +775,7 @@ Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS,
pNew = Gia_ManDupWithBoxes( pTemp = pNew, pParsC ? 0 : 1 );
Gia_ManStop( pTemp );
// report
nFlopsNew = Vec_IntCountEntry(pNew->vRegClasses, 1);
nFlopsNew = pNew->vRegClasses ? Vec_IntCountEntry(pNew->vRegClasses, 1) : 0;
pFlopTypes[2] = nFlops - nFlopsNew - (pFlopTypes[0] + pFlopTypes[1]);
if ( fVerbEquivs )
{

9
src/aig/gia/giaTsim.c
View File

@ -84,9 +84,11 @@ Gia_ManTer_t * Gia_ManTerCreate( Gia_Man_t * pAig )
p = ABC_CALLOC( Gia_ManTer_t, 1 );
p->pAig = Gia_ManFront( pAig );
p->nIters = 300;
p->pDataSim = ABC_ALLOC( unsigned, Abc_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_ALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// these buffers are accessed through XOR-based setters that read the current word first,
// so they must be zero-initialized to avoid touching undefined data on the first update
p->pDataSim = ABC_CALLOC( unsigned, Abc_BitWordNum(2*p->pAig->nFront) );
p->pDataSimCis = ABC_CALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCiNum(p->pAig)) );
p->pDataSimCos = ABC_CALLOC( unsigned, Abc_BitWordNum(2*Gia_ManCoNum(p->pAig)) );
// allocate storage for terminary states
p->nStateWords = Abc_BitWordNum( 2*Gia_ManRegNum(pAig) );
p->vStates = Vec_PtrAlloc( 1000 );
@ -754,4 +756,3 @@ Gia_Man_t * Gia_ManReduceConst( Gia_Man_t * pAig, int fVerbose )
ABC_NAMESPACE_IMPL_END

2
src/aig/gia/module.make
View File

@ -50,6 +50,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaJf.c \
src/aig/gia/giaKf.c \
src/aig/gia/giaLf.c \
src/aig/gia/giaLutCas.c \
src/aig/gia/giaMf.c \
src/aig/gia/giaMan.c \
src/aig/gia/giaMem.c \
@ -58,6 +59,7 @@ SRC += src/aig/gia/giaAig.c \
src/aig/gia/giaMinLut.c \
src/aig/gia/giaMinLut2.c \
src/aig/gia/giaMulFind.c \
src/aig/gia/giaMulFind3.c \
src/aig/gia/giaMuxes.c \
src/aig/gia/giaNf.c \
src/aig/gia/giaOf.c \

2
src/base/abc/abc.h
View File

@ -1046,7 +1046,7 @@ extern ABC_DLL Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
extern ABC_DLL Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
extern ABC_DLL Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
// extern ABC_DLL int Abc_ObjPointerCompare( void ** pp1, void ** pp2 );
extern ABC_DLL void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkInvertConstraints( Abc_Ntk_t * pNtk );
extern ABC_DLL void Abc_NtkPrintCiLevels( Abc_Ntk_t * pNtk );

30
src/base/abc/abcUtil.c
View File

@ -1925,25 +1925,16 @@ void Abc_NtkDetectMatching( Abc_Ntk_t * pNtk )
}
/**Function*************************************************************
Synopsis [Compares the pointers.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_ObjPointerCompare( void ** pp1, void ** pp2 )
{
if ( *pp1 < *pp2 )
return -1;
if ( *pp1 > *pp2 )
return 1;
return 0;
}
/// The legacy `Abc_ObjPointerCompare()` comparator is unused; keep the code here
/// commented to document its previous behavior without exposing a prototype.
// int Abc_ObjPointerCompare( void ** pp1, void ** pp2 )
// {
// if ( *pp1 < *pp2 )
// return -1;
// if ( *pp1 > *pp2 )
// return 1;
// return 0;
// }
/**Function*************************************************************
@ -3564,4 +3555,3 @@ void Abc_NtkATMap( int nXVars, int nYVars, int nAdder, char ** pGPCs0, int nGPCs
ABC_NAMESPACE_IMPL_END

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

@ -89,6 +89,7 @@ static int Abc_CommandPrintMffc ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandPrintFactor ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintLevel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPrintNpn ( Abc_Frame_t * pAbc, int argc, char ** argv );
#ifdef ABC_USE_CUDD
static int Abc_CommandPrintMint ( Abc_Frame_t * pAbc, int argc, char ** argv );
#endif
@ -519,6 +520,7 @@ static int Abc_CommandAbc9Nf ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Of ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Simap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exmap ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SymFun ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Pack ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Edge ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatLut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -580,6 +582,7 @@ static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Qbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9QVar ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9GenLutCas ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9HomoQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatFx ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -643,8 +646,10 @@ static int Abc_CommandAbc9FunAbs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9DsdInfo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9FunTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MulFind ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9MulFind3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9BsFind ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9AndCare ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Cuts ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -907,6 +912,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "print_level", Abc_CommandPrintLevel, 0 );
Cmd_CommandAdd( pAbc, "Printing", "psu", Abc_CommandPrintSupport, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_supp", Abc_CommandPrintSupport, 0 );
Cmd_CommandAdd( pAbc, "Printing", "print_npn", Abc_CommandPrintNpn, 0 );
#ifdef ABC_USE_CUDD
Cmd_CommandAdd( pAbc, "Printing", "print_mint", Abc_CommandPrintMint, 0 );
#endif
@ -1340,6 +1346,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&of", Abc_CommandAbc9Of, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&simap", Abc_CommandAbc9Simap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exmap", Abc_CommandAbc9Exmap, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&symfun", Abc_CommandAbc9SymFun, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&pack", Abc_CommandAbc9Pack, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&edge", Abc_CommandAbc9Edge, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satlut", Abc_CommandAbc9SatLut, 0 );
@ -1401,6 +1408,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&qbf", Abc_CommandAbc9Qbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&qvar", Abc_CommandAbc9QVar, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&genqbf", Abc_CommandAbc9GenQbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&genlutcas", Abc_CommandAbc9GenLutCas, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&homoqbf", Abc_CommandAbc9HomoQbf, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satfx", Abc_CommandAbc9SatFx, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&satclp", Abc_CommandAbc9SatClp, 0 );
@ -1469,9 +1477,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&funabs", Abc_CommandAbc9FunAbs, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&dsdinfo", Abc_CommandAbc9DsdInfo, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&funtrace", Abc_CommandAbc9FunTrace, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mulfind", Abc_CommandAbc9MulFind, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mulfind", Abc_CommandAbc9MulFind, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&mulfind3", Abc_CommandAbc9MulFind3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bsfind", Abc_CommandAbc9BsFind, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&andcare", Abc_CommandAbc9AndCare, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&cuts", Abc_CommandAbc9Cuts, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
@ -2272,6 +2282,61 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandPrintNpn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Dau_PrintNpnFunctions( word * p, int nVars, int fVerbose );
char * pTruthStr = NULL;
word pTruth[16] = {0};
int c, nVars, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( globalUtilOptind != argc-1 )
{
Abc_Print( -1, "The command expects the truth table on the command line.\n" );
goto usage;
}
pTruthStr = argv[globalUtilOptind];
nVars = Abc_TtReadHex( pTruth, pTruthStr );
assert( nVars <= 10 );
Dau_PrintNpnFunctions( pTruth, nVars, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: print_npn [-vh] <truth>\n" );
Abc_Print( -2, "\t prints the NPN members of the given function\n" );
Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t<truth> : the truth table in hexadecimal notation\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -7781,6 +7846,7 @@ int Abc_CommandRunScript( Abc_Frame_t * pAbc, int argc, char ** argv )
pSpot = strstr( pScript, "*" );
if ( pSpot == NULL )
{
abctime clkTotal = Abc_Clock();
for ( c = 0; c < nIters; c++ )
{
if ( fVerbose )
@ -7790,27 +7856,33 @@ int Abc_CommandRunScript( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
printf( "Finished iterating script %d times.\n", nIters );
printf( "Finished iterating script %d times. ", nIters );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return 0;
}
assert( *pSpot == '*' );
for ( c = 0; c < nIters; c++ )
else
{
char pCommLine[1000] = {0};
char pNumber[10] = {0};
sprintf( pNumber, "%d", fReverse ? nBeg - c*nAdd : nBeg + c*nAdd );
strcpy( pCommLine, pScript );
pCommLine[(int)(pSpot - pScript)] = 0;
strcat( pCommLine, pNumber );
strcat( pCommLine, pSpot+1 );
if ( fVerbose )
printf( "ITERATION %3d : %s\n", c, pCommLine );
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), pCommLine) ) {
Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCommLine );
goto usage;
}
abctime clkTotal = Abc_Clock();
assert( *pSpot == '*' );
for ( c = 0; c < nIters; c++ )
{
char pCommLine[1000] = {0};
char pNumber[10] = {0};
sprintf( pNumber, "%d", fReverse ? nBeg - c*nAdd : nBeg + c*nAdd );
strcpy( pCommLine, pScript );
pCommLine[(int)(pSpot - pScript)] = 0;
strcat( pCommLine, pNumber );
strcat( pCommLine, pSpot+1 );
if ( fVerbose )
printf( "ITERATION %3d : %s\n", c, pCommLine );
if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), pCommLine) ) {
Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCommLine );
goto usage;
}
}
printf( "Finished iterating script %d times. ", nIters );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
}
printf( "Finished iterating script %d times.\n", nIters );
return 0;
usage:
@ -10685,6 +10757,9 @@ usage:
***********************************************************************/
int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
extern int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars );
extern void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars );
@ -10693,7 +10768,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYiaorfgdvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKTFUSYPiaorfgckdsmvh" ) ) != EOF )
{
switch ( c )
{
@ -10779,6 +10854,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->pSymStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a string.\n" );
goto usage;
}
pPars->pPermStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'i':
pPars->fUseIncr ^= 1;
break;
@ -10797,9 +10881,21 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
pPars->fGlucose ^= 1;
break;
case 'c':
pPars->fCadical ^= 1;
break;
case 'k':
pPars->fKissat ^= 1;
break;
case 'd':
pPars->fDumpBlif ^= 1;
break;
case 's':
pPars->fSilent ^= 1;
break;
case 'm':
pPars->fMinNodes ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -10809,6 +10905,14 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage;
}
}
if ( pPars->pPermStr && (pPars->nLutSize * pPars->nNodes != (int)strlen(pPars->pPermStr)) )
{
Abc_Print( -1, "Permutation \"%s\" has %d symbols instead of expected %d = %d * %d symbols (LutSize * nLuts).\n",
pPars->pPermStr, (int)strlen(pPars->pPermStr), pPars->nLutSize * pPars->nNodes, pPars->nLutSize, pPars->nNodes );
return 1;
}
if ( pPars->pPermStr && !pPars->fLutCascade )
Abc_Print( 0, "If LUT mapping is not enabled (switch \"-r\"), permutation has not effect.\n" );
if ( argc == globalUtilOptind + 1 )
pPars->pTtStr = argv[globalUtilOptind];
else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
@ -10822,11 +10926,15 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Truth table should be given on the command line.\n" );
return 1;
}
if ( pPars->nVars == 0 && pPars->pTtStr )
pPars->nVars = 2 + Abc_Base2Log((int)strlen(pPars->pTtStr));
if ( pPars->pTtStr && (1 << (pPars->nVars-2)) != (int)strlen(pPars->pTtStr) )
{
Abc_Print( -1, "Truth table is expected to have %d hex digits (instead of %d).\n", (1 << (pPars->nVars-2)), strlen(pPars->pTtStr) );
return 1;
}
if ( pPars->nVars == 0 && pPars->pSymStr )
pPars->nVars = (int)strlen(pPars->pSymStr) - 1;
if ( pPars->pSymStr && pPars->nVars+1 != strlen(pPars->pSymStr) )
{
Abc_Print( -1, "The char string of the %d-variable symmetric function should have %d zeros and ones (instead of %d).\n", pPars->nVars, pPars->nVars+1, strlen(pPars->pSymStr) );
@ -10839,7 +10947,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pPars->nVars > 12 )
{
Abc_Print( -1, "Function should not have more than 10 inputs.\n" );
Abc_Print( -1, "Function should not have more than 12 inputs.\n" );
return 1;
}
if ( pPars->nLutSize > 6 )
@ -10853,6 +10961,10 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else if ( pPars->fGlucose )
Exa3_ManExactSynthesis( pPars );
else if ( pPars->fCadical )
Exa7_ManExactSynthesis( pPars );
else if ( pPars->fKissat )
Exa8_ManExactSynthesis( pPars );
else
Exa3_ManExactSynthesis2( pPars );
if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
@ -10860,7 +10972,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-iaorfgdvh] <hex>\n" );
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t-N <num> : the number of input variables [default = %d]\n", pPars->nVars );
Abc_Print( -2, "\t-M <num> : the number of K-input nodes [default = %d]\n", pPars->nNodes );
@ -10869,14 +10981,19 @@ usage:
Abc_Print( -2, "\t-F <num> : the number of random functions to try [default = unused]\n" );
Abc_Print( -2, "\t-U <num> : the number of positive minterms in the random function [default = unused]\n" );
Abc_Print( -2, "\t-S <num> : the random seed for random function generation with -F <num> [default = %d]\n", pPars->Seed );
Abc_Print( -2, "\t-Y <str> : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr );
Abc_Print( -2, "\t-Y <str> : charasteristic string of a symmetric function [default = %s]\n", pPars->pSymStr ? pPars->pSymStr : "unused" );
Abc_Print( -2, "\t-P <str> : variable permutation (for example, \"abcd_aef\" for S44) [default = %s]\n", pPars->pPermStr ? pPars->pPermStr : "unused" );
Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" );
Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" );
Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" );
Abc_Print( -2, "\t-r : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" );
Abc_Print( -2, "\t-f : toggle fixing LUT inputs in cascade mapping [default = %s]\n", pPars->fLutInFixed ? "yes" : "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" );
Abc_Print( -2, "\t-c : toggle using CaDiCal 2.2.0-rc1 by Armin Biere et al [default = %s]\n", pPars->fCadical ? "yes" : "no" );
Abc_Print( -2, "\t-k : toggle using Kissat 4.0.2 by Armin Biere [default = %s]\n", pPars->fKissat ? "yes" : "no" );
Abc_Print( -2, "\t-d : toggle dumping decomposed networks into BLIF files [default = %s]\n", pPars->fDumpBlif ? "yes" : "no" );
Abc_Print( -2, "\t-s : toggle silent computation (no messages, except when a solution is found) [default = %s]\n", pPars->fSilent ? "yes" : "no" );
Abc_Print( -2, "\t-m : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<hex> : truth table in hex notation\n" );
@ -18571,7 +18688,7 @@ usage:
Abc_Print( -2, "\t > 10 1\n" );
Abc_Print( -2, "\t > .end\n\n" );
Abc_Print( -2, "\t > # file i.blif\n" );
Abc_Print( -2, "\t > .model mux21\n" );
Abc_Print( -2, "\t > .model mux41\n" );
Abc_Print( -2, "\t > .inputs d0 d1 d2 d3 a b\n" );
Abc_Print( -2, "\t > .outputs F\n" );
Abc_Print( -2, "\t > .names d0 d1 d2 d3 a b F\n" );
@ -43587,7 +43704,7 @@ usage:
Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
Abc_Print( -2, "\t-i : toggles using cofactoring variables [default = %s]\n", pPars->fUseCofVars? "yes": "no" );
Abc_Print( -2, "\t-j : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck07? "yes": "no" );
Abc_Print( -2, "\t-j : toggles using AND bi-decomposition [default = %s]\n", pPars->fUseAndVars? "yes": "no" );
// Abc_Print( -2, "\t-j : toggles using AND bi-decomposition [default = %s]\n", pPars->fUseAndVars? "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-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
Abc_Print( -2, "\t-t : toggles optimizing average rather than maximum level [default = %s]\n", pPars->fDoAverage? "yes": "no" );
@ -44791,7 +44908,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_Man_t * pNew; int c;
Nf_ManSetDefaultPars( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQWZakpqfvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQMWZakpqfvwh" ) ) != EOF )
{
switch ( c )
{
@ -44892,7 +45009,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'Q':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer number.\n" );
Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer number.\n" );
goto usage;
}
pPars->nReqTimeFlex = atoi(argv[globalUtilOptind]);
@ -44900,6 +45017,17 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nReqTimeFlex < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer number.\n" );
goto usage;
}
pPars->nMaxMatches = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nMaxMatches < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
@ -44973,7 +45101,7 @@ usage:
sprintf(Buffer, "best possible" );
else
sprintf(Buffer, "%d", pPars->DelayTarget );
Abc_Print( -2, "usage: &nf [-KCFARLEDQ num] [-Z file] [-akpqfvwh]\n" );
Abc_Print( -2, "usage: &nf [-KCFARLEDQM num] [-Z file] [-akpqfvwh]\n" );
Abc_Print( -2, "\t performs technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum );
@ -44984,6 +45112,7 @@ usage:
Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner );
Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer );
Abc_Print( -2, "\t-Q num : internal parameter impacting area of the mapping [default = %d]\n", pPars->nReqTimeFlex );
Abc_Print( -2, "\t-M num : the max number of matches to dump into a binary file [default = %d]\n", pPars->nMaxMatches );
Abc_Print( -2, "\t-Z file : the output file name to dump internal match info [default = unused]\n" );
Abc_Print( -2, "\t-a : toggles SAT-based area-oriented mapping (experimental) [default = %s]\n", pPars->fAreaOnly? "yes": "no" );
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" );
@ -45480,6 +45609,127 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9SymFun( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManGenSymFun( Vec_Wrd_t * vFuns, int nChars, int fVerbose );
Gia_Man_t * pNew = NULL;
Vec_Wrd_t * vFuns = NULL;
int c, nChars = 0, nMaj = 0, nHot = 0, nXor = 0, nWgt = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "MHXWvh" ) ) != EOF )
{
switch ( c )
{
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by a file name.\n" );
goto usage;
}
nMaj = atoi(argv[globalUtilOptind++]);
break;
case 'H':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-H\" should be followed by a file name.\n" );
goto usage;
}
nHot = atoi(argv[globalUtilOptind++]);
break;
case 'X':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-X\" should be followed by a file name.\n" );
goto usage;
}
nXor = atoi(argv[globalUtilOptind++]);
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by a file name.\n" );
goto usage;
}
nWgt = atoi(argv[globalUtilOptind++]);
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
default:
goto usage;
}
}
if ( nMaj ) {
nChars = nMaj+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, Abc_Tt6Mask(nMaj/2+1) << (nMaj/2+1) );
}
else if ( nHot ) {
nChars = nHot+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, 2 );
}
else if ( nXor ) {
nChars = nXor+1;
vFuns = Vec_WrdAlloc(1);
Vec_WrdPush( vFuns, s_Truths6[0] & Abc_Tt6Mask(nChars) );
}
else if ( nWgt ) {
int nOuts = Abc_Base2Log(nWgt+1);
nChars = nWgt+1;
vFuns = Vec_WrdAlloc(nOuts);
for ( int i = 0; i < nOuts; i++ )
Vec_WrdPush( vFuns, s_Truths6[i] & Abc_Tt6Mask(nChars) );
}
else {
if ( argc == globalUtilOptind ) {
printf( "One or more characteristic strings should be given on the command line.\n" );
return 0;
}
nChars = (int)strlen(argv[globalUtilOptind]);
for ( c = globalUtilOptind+1; c < argc; c++ )
if ( nChars != (int)strlen(argv[c]) ) {
printf( "Char strings have different lengths. Quitting.\n" );
return 0;
}
vFuns = Vec_WrdAlloc( argc );
for ( c = globalUtilOptind; c < argc; c++ )
Vec_WrdPush( vFuns, Abc_TtReadBin64(argv[c]) );
}
if ( nChars > 64 ) {
printf( "Currently can handle functions up to 63 inputs. Quitting.\n" );
return 0;
}
pNew = Gia_ManGenSymFun( vFuns, nChars, fVerbose );
Abc_FrameUpdateGia( pAbc, pNew );
Vec_WrdFree( vFuns );
return 0;
usage:
Abc_Print( -2, "usage: &symfun [-MHXW num] [-vh] <str0> <str1> ... <str(N-1)>\n" );
Abc_Print( -2, "\t derives AIG of a multi-output symmetric function\n" );
Abc_Print( -2, "\t-M <num> : generate the majority gate with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-H <num> : generate the 1-hot condition with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-X <num> : generate the xor-gate with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-W <num> : generate the weight(W) function with the given input count [default = unused]\n" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
Abc_Print( -2, "\t<str0> <str1> ... <str(N-1)> : char strings in binary notation LSB first\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -51303,7 +51553,7 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars );
extern void Gia_QbfDumpFileInv( Gia_Man_t * pGia, int nPars );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fVerbose );
extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int nEncVars, int fGlucose, int fCadical, int fSilent, int fVerbose );
int c, nPars = -1;
int nIterLimit = 0;
int nConfLimit = 0;
@ -51312,9 +51562,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
int fDumpCnf = 0;
int fDumpCnf2 = 0;
int fGlucose = 0;
int fCadical = 0;
int fSilent = 0;
int fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PICTKdegcsvh" ) ) != EOF )
{
switch ( c )
{
@ -51382,6 +51634,12 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'g':
fGlucose ^= 1;
break;
case 'c':
fCadical ^= 1;
break;
case 's':
fSilent ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -51416,11 +51674,11 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv )
else if ( fDumpCnf2 )
Gia_QbfDumpFileInv( pAbc->pGia, nPars );
else
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fVerbose );
Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, nEncVars, fGlucose, fCadical, fSilent, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &qbf [-PICTK num] [-degvh]\n" );
Abc_Print( -2, "usage: &qbf [-PICTK num] [-degcsvh]\n" );
Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIterLimit );
@ -51430,6 +51688,8 @@ usage:
Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving (complemented QBF) [default = %s]\n", fDumpCnf? "yes": "no" );
Abc_Print( -2, "\t-e : toggle dumping QDIMACS file instead of solving (original QBF) [default = %s]\n", fDumpCnf2? "yes": "no" );
Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" );
Abc_Print( -2, "\t-c : toggle using CaDiCaL by Armin Biere [default = %s]\n", fCadical? "yes": "no" );
Abc_Print( -2, "\t-s : no printout except when a solution is found [default = %s]\n", fSilent? "yes": "no" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n\n");
Abc_Print( -2, "\t As an example of using this command, consider specification (the three-input AND-gate) and implementation\n");
@ -51666,6 +51926,150 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9GenLutCas( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManGenLutCas( Gia_Man_t * p, char * pPermStr, int nVars, int nLuts, int LutSize, int Seed, int fVerbose );
int nVars = 0;
int nLuts = 2;
int LutSize = 6;
int Seed = 0;
int fVerbose = 0;
int c;
char * pPermStr = NULL;
Gia_Man_t * pTemp;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMKSPvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nVars < 0 )
goto usage;
break;
case 'M':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
goto usage;
}
nLuts = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLuts < 0 )
goto usage;
break;
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
LutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( LutSize < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( Seed < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by a string.\n" );
goto usage;
}
pPermStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL && nVars == 0 )
{
Abc_Print( -1, "The number of inputs (%d) should be specified on the command line.\n", nVars );
return 1;
}
if ( pAbc->pGia )
nVars = Gia_ManCiNum(pAbc->pGia);
if ( pPermStr && (nLuts * LutSize != (int)strlen(pPermStr)) )
{
Abc_Print( -1, "Permutation \"%s\" has %d symbols instead of expected %d = %d * %d symbols (LutSize * nLuts).\n",
pPermStr, (int)strlen(pPermStr), LutSize * nLuts, LutSize, nLuts );
return 1;
}
if ( nVars <= LutSize )
{
Abc_Print( -1, "The number of inputs (%d) should be more than LUT size (%d).\n", nVars, LutSize );
return 1;
}
if ( nVars > 100 )
{
Abc_Print( -1, "The number of inputs (%d) should be less than 100.\n", nVars );
return 1;
}
if ( nLuts < 2 || nLuts > 100 )
{
Abc_Print( -1, "The LUT count (%d) should be morein the range [2;100].\n", nLuts );
return 1;
}
if ( LutSize < 2 || LutSize > 12 )
{
Abc_Print( -1, "The LUT size (%d) should be in the range [2;12].\n", LutSize );
return 1;
}
if ( nVars > (nLuts-1)*(LutSize-1) + LutSize )
{
Abc_Print( -1, "Function with %d variables is too large for a cascade composed of %d connected %d-LUTs.\n", nVars, nLuts, LutSize );
return 1;
}
pTemp = Gia_ManGenLutCas( pAbc->pGia, pPermStr, nVars, nLuts, LutSize, Seed, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &genlutcas[-NMKS num] [-P str] [-vh]\n" );
Abc_Print( -2, "\t generates a miter for synthesizing the LUT cascade\n" );
Abc_Print( -2, "\t-N num : the number of primary inputs [default = %d]\n", nVars );
Abc_Print( -2, "\t-M num : the number of LUTs [default = %d]\n", nLuts );
Abc_Print( -2, "\t-K num : the LUT size [default = %d]\n", LutSize );
Abc_Print( -2, "\t-S num : the random seed [default = %d]\n", Seed );
Abc_Print( -2, "\t-P str : variable permutation (for example, \"abcd_aef\" for S44) [default = %s]\n", pPermStr ? pPermStr : "unused" );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -57597,6 +58001,79 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9MulFind3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManMulFindNew( Gia_Man_t * p, int nABits, int nFanLim, int fLits, int fVerbose );
int c, nABits = 0, nFanLim = 4, fLits = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "IFlvh" ) ) != EOF )
{
switch ( c )
{
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nABits = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nABits < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFanLim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFanLim < 0 )
goto usage;
break;
case 'l':
fLits ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9MulFind(): There is no AIG.\n" );
return 0;
}
Gia_ManMulFindNew( pAbc->pGia, nABits, nFanLim, fLits, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &mulfind3 [-IF num] [-lvh]\n" );
Abc_Print( -2, "\t detects multipliers in the given AIG\n" );
Abc_Print( -2, "\t-I num : the bit-width of the first input if known [default = %d]\n", nABits );
Abc_Print( -2, "\t-F num : the fanout limit [default = %d]\n", nFanLim );
Abc_Print( -2, "\t-l : toggles using literals instead of nodes [default = %s]\n", fLits ? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -57750,6 +58227,114 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Cuts( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_ManComputeCutsCore( Gia_Man_t * pGia, int nCutSize0, int nCutNum0, int fTruth0, int fVerbose0, int fDumpText, int fDumpBin, char * pFileName );
int nCutSize = 6;
int nCutNum = 16;
int fTruth = 1;
int fVerbose = 1;
int fDumpText = 0;
int fDumpBin = 0;
int c;
char * pFileName = NULL;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KCtdbvh" ) ) != EOF )
{
switch ( c )
{
case 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nCutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCutSize < 0 )
goto usage;
break;
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCutNum = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCutNum < 0 )
goto usage;
break;
case 't':
fTruth ^= 1;
break;
case 'd':
fDumpText ^= 1;
break;
case 'b':
fDumpBin ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cuts(): There is no AIG.\n" );
return 0;
}
if ( argc == globalUtilOptind + 1 )
pFileName = argv[globalUtilOptind];
else if ( argc != globalUtilOptind )
{
Abc_Print( 1,"Abc_CommandAbc9Cuts(): Trailing arguments on the command line.\n" );
return 0;
}
if ( nCutSize < 2 || nCutSize > 14 )
{
Abc_Print( -1, "The number of cut leaves should belong to the range: %d <= K <= %d.\n", 2, 14 );
return 1;
}
if ( nCutNum < 2 || nCutNum > 256 )
{
Abc_Print( -1, "The number of cuts per node should belong to the range: %d <= C <= %d.\n", 2, 256 );
return 1;
}
if ( fDumpBin && !pFileName )
{
Abc_Print( -1, "Output binary file name should be provided on the command line.\n" );
return 1;
}
Gia_ManComputeCutsCore( pAbc->pGia, nCutSize, nCutNum, fTruth, fVerbose, fDumpText, fDumpBin, pFileName );
return 0;
usage:
Abc_Print( -2, "usage: cuts [-KC num] [-tdbvh]\n" );
Abc_Print( -2, "\t computes K-input cuts for the nodes in the current AIG\n" );
Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", 2, 14, nCutSize );
Abc_Print( -2, "\t-C num : max number of cuts at a node (%d <= num <= %d) [default = %d]\n", 2, 256, nCutNum );
Abc_Print( -2, "\t-t : toggle truth table computation and cut minimization [default = %s]\n", fTruth? "yes": "no" );
Abc_Print( -2, "\t-d : toggle dumping cuts into a text file [default = %s]\n", fDumpText? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fDumpBin? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************

7
src/base/abci/abcLutmin.c
View File

@ -1083,8 +1083,10 @@ Abc_Obj_t * Abc_NtkBddDecompose( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, int nLu
}
// cofactor w.r.t. the bound set variables
vCofs = Abc_NtkBddCofactors( dd, (DdNode *)pNode->pData, nLutSize );
vUniq = Vec_PtrDup( vCofs );
Vec_PtrUniqify( vUniq, (int (*)(const void *, const void *))Vec_PtrSortCompare );
// collect unique cofactors in the order they appear
vUniq = Vec_PtrAlloc( Vec_PtrSize(vCofs) );
Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
Vec_PtrPushUnique( vUniq, bCof );
// only perform decomposition which it is support reducing with two less vars
if( Vec_PtrSize(vUniq) > (1 << (nLutSize-2)) )
{
@ -1257,4 +1259,3 @@ void Abc_NtkBddDecExplore( Abc_Obj_t * pNode ) {}
ABC_NAMESPACE_IMPL_END

4
src/base/abci/abcSweep.c
View File

@ -885,10 +885,9 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk )
continue;
}
assert( !Abc_ObjIsLatch(pFanin) );
Vec_PtrPush( vNodes, pFanin );
Vec_PtrPushUnique( vNodes, pFanin );
}
}
Vec_PtrUniqify( vNodes, (int (*)(const void *, const void *))Abc_ObjPointerCompare );
// replace these nodes by the PIs
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
{
@ -1027,4 +1026,3 @@ int Abc_NtkSweepBufsInvs( Abc_Ntk_t * pNtk, int fVerbose )
ABC_NAMESPACE_IMPL_END

3
src/base/abci/abcSymm.c
View File

@ -327,7 +327,10 @@ void Ntk_SymFunGenerate( int nVars, int fVerbose )
if ( fVerbose )
Extra_PrintHex( stdout, (unsigned *)pFun, nVars );
Ntk_SymFunDeriveNpn( pFun, nVars, pComp );
//int nClasses = Vec_MemEntryNum( vTtMem );
Class = Vec_MemHashInsert( vTtMem, pFun );
//if ( Class == nClasses )
//printf( "Class %3d : %s\n", nClasses, Ones );
if ( fVerbose )
{
printf( " : NPN " );

41
src/base/cmd/cmdHist.c
View File

@ -50,7 +50,7 @@ ABC_NAMESPACE_IMPL_START
void Cmd_HistoryAddCommand( Abc_Frame_t * p, const char * command )
{
int nLastLooked = 10; // do not add history if the same entry appears among the last entries
int nLastSaved = 10000; // when saving a file, save no more than this number of last entries
int nLastSaved = 20000; // when saving a file, save no more than this number of last entries
char Buffer[ABC_MAX_STR];
int Len;
if ( p->fBatchMode )
@ -117,6 +117,7 @@ void Cmd_HistoryRead( Abc_Frame_t * p )
Vec_PtrPush( p->aHistory, Extra_UtilStrsav(Buffer) );
}
fclose( pFile );
p->iStartHistory = Vec_PtrSize(p->aHistory);
#endif
}
@ -137,16 +138,38 @@ void Cmd_HistoryWrite( Abc_Frame_t * p, int Limit )
FILE * pFile;
char * pStr;
int i;
pFile = fopen( "abc.history", "wb" );
if ( pFile == NULL )
if ( 1 )
{
Abc_Print( 0, "Cannot open file \"abc.history\" for writing.\n" );
return;
pFile = fopen( "abc.history", "ab" );
if ( pFile == NULL )
{
Abc_Print( 0, "Cannot open file \"abc.history\" for writing.\n" );
return;
}
Vec_PtrForEachEntryStart( char *, p->aHistory, pStr, i, p->iStartHistory )
fprintf( pFile, "%s\n", pStr );
fclose( pFile );
p->iStartHistory = Vec_PtrSize(p->aHistory);
}
if ( Vec_PtrSize(p->aHistory) > Limit + 1000 )
{
pFile = fopen( "abc.history", "wb" );
if ( pFile == NULL )
{
Abc_Print( 0, "Cannot open file \"abc.history\" for writing.\n" );
return;
}
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
Vec_Ptr_t * aHistory= Vec_PtrAlloc(Vec_PtrSize(p->aHistory));
Vec_PtrForEachEntryStart( char *, p->aHistory, pStr, i, Limit ) {
fprintf( pFile, "%s\n", pStr );
Vec_PtrPush( aHistory, Abc_UtilStrsav(pStr) );
}
fclose( pFile );
Vec_PtrFreeFree( p->aHistory );
p->aHistory = aHistory;
p->iStartHistory = Vec_PtrSize(p->aHistory);
}
Limit = Abc_MaxInt( 0, Vec_PtrSize(p->aHistory)-Limit );
Vec_PtrForEachEntryStart( char *, p->aHistory, pStr, i, Limit )
fprintf( pFile, "%s\n", pStr );
fclose( pFile );
#endif
}

7
src/base/io/io.c
View File

@ -126,7 +126,6 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 );
@ -1078,10 +1077,10 @@ int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: read_dsd [-h] <formula>\n" );
fprintf( pAbc->Err, "\t parses a formula representing DSD of a function\n" );
fprintf( pAbc->Err, "usage: read_formula [-h] <formula>\n" );
fprintf( pAbc->Err, "\t reads a Boolean function represented by a formula\n" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tformula : the formula representing disjoint-support decomposition (DSD)\n" );
fprintf( pAbc->Err, "\tformula : the formula representing the function\n" );
fprintf( pAbc->Err, "\t Example of a formula: !(a*(b+CA(!d,e*f,c))*79B3(g,h,i,k))\n" );
fprintf( pAbc->Err, "\t where \'!\' is an INV, \'*\' is an AND, \'+\' is an XOR, \n" );
fprintf( pAbc->Err, "\t CA and 79B3 are hexadecimal representations of truth tables\n" );

1
src/base/main/mainInt.h
View File

@ -67,6 +67,7 @@ struct Abc_Frame_t_
st__table * tAliases; // the alias table
st__table * tFlags; // the flag table
Vec_Ptr_t * aHistory; // the command history
int iStartHistory; // beginning of the new history file
// the functionality
Abc_Ntk_t * pNtkCur; // the current network
Abc_Ntk_t * pNtkBestDelay; // the current network

2
src/base/main/mainReal.c
View File

@ -293,7 +293,7 @@ int Abc_RealMain( int argc, char * argv[] )
pAbc->pGia = Gia_ManFromBridge( stdin, NULL );
}
else if ( fBatch!=INTERACTIVE && fBatch!=BATCH_QUIET && fBatch!=BATCH_QUIET_THEN_INTERACTIVE && Vec_StrSize(sCommandUsr)>0 )
Abc_Print( 1, "ABC command line: \"%s\".\n\n", Vec_StrArray(sCommandUsr) );
Abc_Print( 1, "\n======== ABC command line \"%s\"\n", Vec_StrArray(sCommandUsr) );
if ( fBatch!=INTERACTIVE )
{

12
src/base/wlc/wlcBlast.c
View File

@ -1240,6 +1240,17 @@ Vec_Int_t * Wlc_BlastDecoder2( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t
Vec_IntFree( vRes2 );
return vRes;
}
void Wlc_DumpMatrix( Gia_Man_t * pNew, Vec_Wec_t * vProds )
{
char * pFileName = "booth_pps.aig";
Vec_Int_t * vLevel; int i, k, Entry;
Vec_WecForEachLevel( vProds, vLevel, i )
Vec_IntForEachEntry( vLevel, Entry, k )
Gia_ManAppendCo(pNew, Entry);
Gia_AigerWrite( pNew, pFileName, 0, 0, 0 );
printf( "Finished dumping Booth PPs into \"%s\".\n", pFileName );
exit(1);
}
void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose )
{
Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB + 3 );
@ -1324,6 +1335,7 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int
Vec_WecPrint( vProds, 0 );
if ( fVerbose )
printf( "Total PPs = %d.\n", Vec_WecSizeSize(vProds) );
//Wlc_DumpMatrix( pNew, vProds );
//Wlc_BlastPrintMatrix( pNew, vProds, 1 );
//printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) );
if ( pvProds )

131
src/base/wlc/wlcCom.c
View File

@ -32,6 +32,7 @@ ABC_NAMESPACE_IMPL_START
static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGenWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -79,6 +80,7 @@ void Wlc_Init( Abc_Frame_t * pAbc )
{
Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%gen", Abc_CommandGenWlc, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
@ -305,6 +307,134 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int Abc_CommandGenWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int miniver_translate(const char *input, char *out, size_t cap, int fShort);
char * pFileName = NULL;
int fShort = 1;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Fsvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
goto usage;
}
pFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 's':
fShort ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 ) {
printf( "The input string is not given on the command line.\n" );
goto usage;
}
else {
int Size = 10000;
char * pStr = argv[globalUtilOptind];
char * pOutStr = ABC_CALLOC( char, Size+1 );
int RetValue = miniver_translate( pStr, pOutStr, Size, fShort );
if ( !RetValue ) {
if ( fVerbose )
printf( "Entered Verilog design:\n%s", pOutStr );
if ( pFileName ) {
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
printf( "Cannot open output file \"%s\".\n", pFileName );
else {
fprintf( pFile, "// Design generated from mini-Verilog string: %s\n\n%s\n", pStr, pOutStr );
fclose( pFile );
printf( "Dumped the design generated from mini-Verilog string \"%s\" into file \"%s\".\n", pStr, pFileName );
}
}
else {
if ( fVerbose )
printf( "Reading generated Verilog using using command %%read...\n" );
Wlc_Ntk_t * pNtk = Wlc_ReadVer( NULL, pOutStr, 0 );
if ( pNtk )
Wlc_AbcUpdateNtk( pAbc, pNtk );
else {
printf( "The following design in Verilog, which was generated from string \"%s\",\n", pStr );
printf( "cannot be read into ABC due to the known limitations of command \"%%read\".\n" );
printf( "Please try the following \"%%gen -F <file.v> <string>; %%yosys -b <file.v>; &ps\".\n" );
printf( "Generated design:\n%s\n", pOutStr );
}
}
}
ABC_FREE( pOutStr );
}
return 0;
usage:
Abc_Print( -2, "\nusage: %%gen [-F file] [-svh] \"<mini_verilog_string>\"\n" );
Abc_Print( -2, "\t generates the design from a mini-Verilog string\n" );
Abc_Print( -2, "\t-F file : optional file name to save the design in standard Verilog [default = unused]\n" );
Abc_Print( -2, "\t (if a file name is provided, Verilog is dumped into a file and not read into ABC)\n" );
Abc_Print( -2, "\t-s : prints Verilog using a shorter format [default = %s]\n", fShort ? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\n" );
Abc_Print( -2, "A mini-Verilog design is a single string. Any spaces/tabs/newlines are ignored\n" );
Abc_Print( -2, "(handled internally). The string is split into clauses by semicolons ';'.\n" );
Abc_Print( -2, "\n" );
Abc_Print( -2, "Clause types (first character):\n" );
Abc_Print( -2, " - 'm<name>' : module name (appear once)\n" );
Abc_Print( -2, " - '{i|o|w}[s]<number><id_list>' : input/output/wire declarations\n" );
Abc_Print( -2, " where optional 's' = signed, <number> = bit-width (>0), <id_list> = id[,id]*\n" );
Abc_Print( -2, " Examples: i4a,b -> input [3:0] a, b;\n" );
Abc_Print( -2, " is8x,y -> input signed [7:0] x, y;\n" );
Abc_Print( -2, " w1t -> wire t; (width 1 prints without [0:0])\n" );
Abc_Print( -2, " - '{o|w}[s]<number><id>=<expr>' : declaration with assignment\n" );
Abc_Print( -2, " Examples: o8z=a*b -> output [7:0] z; assign z = a*b;\n" );
Abc_Print( -2, " w4t=a+b -> wire [3:0] t; assign t = a+b;\n" );
Abc_Print( -2, "\n" );
Abc_Print( -2, "Default names:\n" );
Abc_Print( -2, " - Outputs: if an 'o...' assignment omits a name (e.g., 'o8=<expr>'), the output name defaults to 'o'.\n" );
Abc_Print( -2, " - Inputs: if an 'i...' clause omits names (e.g., 'i4'), a single input is declared with an\n" );
Abc_Print( -2, " auto-generated unsigned name 'a', then 'b', then 'c', ... in the order of appearance (skipping\n" );
Abc_Print( -2, " names already used). This allows for specifying a 4-bit multiplier 'mul' as: \"mmul;i4;i4;o8=a*b\".\n" );
Abc_Print( -2, "\n" );
Abc_Print( -2, "Notes:\n" );
Abc_Print( -2, " * Only a single, non-hierarchical, combinational module is supported.\n" );
Abc_Print( -2, " * RHS expressions are passed through verbatim or with added spaces (must be in valid Verilog).\n" );
Abc_Print( -2, " * For the design to be readable into ABC, make sure each RHS has only one operator,\n" );
Abc_Print( -2, " with constant definition, bit-slicing, and concatenation being considered operators.\n" );
Abc_Print( -2, " * Alternatively, use any RHS style, which make have several operator per line,\n" );
Abc_Print( -2, " write the design by specifying the file name \"-F file\", and read it back using Yosys.\n" );
Abc_Print( -2, " Example: \"mtest;i4a,b,c;o4z=a*b+c\" is not readable into ABC directly but readable via Yosys:\n\n" );
Abc_Print( -2, " abc 01> %%gen \"mtest;i4a,b,c;o4z=a*b+c\"\n" );
Abc_Print( -2, " Warning: Trailing symbols \"+ c \" in line 6.\n\n" );
Abc_Print( -2, " abc 01> %%gen -F test.v \"mtest;i4a,b,c;o4z=a*b+c\"; %yosys -b test.v; &ps\n" );
Abc_Print( -2, " Dumped the design generated from mini-Verilog string \"mtest;i4a,b,c;o4z=a*b+c\" into file \"test.v\".\n" );
Abc_Print( -2, " test : i/o = 12/ 4 and = 61 lev = 15 (9.00) mem = 0.00 MB\n" );
return 1;
}
/**Function********************************************************************
Synopsis []
@ -2004,4 +2134,3 @@ usage:
ABC_NAMESPACE_IMPL_END

5
src/bdd/cudd/cuddGroup.c
View File

@ -679,11 +679,11 @@ ddUniqueCompareGroup(
int * ptrX,
int * ptrY)
{
#if 0
//#if 0
if (entry[*ptrY] == entry[*ptrX]) {
return((*ptrX) - (*ptrY));
}
#endif
//#endif
return(entry[*ptrY] - entry[*ptrX]);
} /* end of ddUniqueCompareGroup */
@ -2170,4 +2170,3 @@ ddIsVarHandled(
ABC_NAMESPACE_IMPL_END

5
src/bdd/cudd/cuddLinear.c
View File

@ -873,11 +873,11 @@ ddLinearUniqueCompare(
int * ptrX,
int * ptrY)
{
#if 0
//#if 0
if (entry[*ptrY] == entry[*ptrX]) {
return((*ptrX) - (*ptrY));
}
#endif
//#endif
return(entry[*ptrY] - entry[*ptrX]);
} /* end of ddLinearUniqueCompare */
@ -1370,4 +1370,3 @@ cuddXorLinear(
ABC_NAMESPACE_IMPL_END

5
src/bdd/cudd/cuddReorder.c
View File

@ -1325,11 +1325,11 @@ ddUniqueCompare(
int * ptrX,
int * ptrY)
{
#if 0
//#if 0
if (entry[*ptrY] == entry[*ptrX]) {
return((*ptrX) - (*ptrY));
}
#endif
//#endif
return(entry[*ptrY] - entry[*ptrX]);
} /* end of ddUniqueCompare */
@ -2140,4 +2140,3 @@ ddCheckPermuation(
ABC_NAMESPACE_IMPL_END

5
src/bdd/cudd/cuddSymmetry.c
View File

@ -609,11 +609,11 @@ ddSymmUniqueCompare(
int * ptrX,
int * ptrY)
{
#if 0
//#if 0
if (entry[*ptrY] == entry[*ptrX]) {
return((*ptrX) - (*ptrY));
}
#endif
//#endif
return(entry[*ptrY] - entry[*ptrX]);
} /* end of ddSymmUniqueCompare */
@ -1703,4 +1703,3 @@ ddSymmSummary(
ABC_NAMESPACE_IMPL_END

5
src/bdd/cudd/cuddZddGroup.c
View File

@ -610,11 +610,11 @@ zddUniqueCompareGroup(
int * ptrX,
int * ptrY)
{
#if 0
//#if 0
if (entry[*ptrY] == entry[*ptrX]) {
return((*ptrX) - (*ptrY));
}
#endif
//#endif
return(entry[*ptrY] - entry[*ptrX]);
} /* end of zddUniqueCompareGroup */
@ -1341,4 +1341,3 @@ zddMergeGroups(
ABC_NAMESPACE_IMPL_END

6
src/bdd/cudd/cuddZddReord.c
View File

@ -460,6 +460,11 @@ cuddZddUniqueCompare(
int * ptr_x,
int * ptr_y)
{
//#if 0
if (zdd_entry[*ptr_y] == zdd_entry[*ptr_x]) {
return((*ptr_x) - (*ptr_y));
}
//#endif
return(zdd_entry[*ptr_y] - zdd_entry[*ptr_x]);
} /* end of cuddZddUniqueCompare */
@ -1665,4 +1670,3 @@ zddFixTree(
ABC_NAMESPACE_IMPL_END

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

@ -911,12 +911,15 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
printf( "[%4d] ", Count++ ); // Print instance number
if ( CellId == 0 )
{
assert( nLeaves <= 4 );
// Extract 16-bit truth table
word Truth = ((word)pConfigData[2] << 8) | pConfigData[1];
word Truth = ((word)pConfigData[5] << 8) | pConfigData[6];
printf( "%04lX{", (unsigned long)Truth );
// Print as simple {abcd} since it's just a direct LUT4
for ( i = 0; i < nLeaves && i < 4; i++ )
for ( i = 0; i < nLeaves; i++ )
printf( "%c", 'a' + i );
for ( ; i < 4; i++ )
printf( "%c", '0' );
printf( "}" );
// Pad with spaces if less than 4 inputs
for ( i = nLeaves; i < 4; i++ )
@ -926,11 +929,11 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
else if ( CellId == 1 )
{
// First LUT4
word Truth1 = ((word)pConfigData[6] << 8) | pConfigData[5];
word Truth1 = ((word)pConfigData[8] << 8) | pConfigData[9];
printf( "h=%04lX{", (unsigned long)Truth1 );
for ( i = 0; i < 4; i++ )
{
int v = (pConfigData[1 + i/2] >> ((i%2) * 4)) & 0xF;
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
@ -942,11 +945,11 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
}
printf( "} ");
// Second LUT4
word Truth2 = ((word)pConfigData[8] << 8) | pConfigData[7];
word Truth2 = ((word)pConfigData[10] << 8) | pConfigData[11];
printf( "i=%04lX{", (unsigned long)Truth2 );
for ( i = 0; i < 4; i++ )
for ( i = 4; i < 7; i++ )
{
int v = (pConfigData[3 + i/2] >> ((i%2) * 4)) & 0xF;
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
@ -958,32 +961,16 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
else
printf( "?");
}
printf( "} [Cell %d, %d leaves]\n", CellId, nLeaves );
printf( "h} [Cell %d, %d leaves]\n", CellId, nLeaves );
}
else if ( CellId == 2 )
{
// Extract 9 input mappings
int inputs[9];
int bitPos = 0;
for ( i = 0; i < 9; i++ )
{
if ( bitPos == 0 )
{
inputs[i] = pConfigData[1 + i/2] & 0xF;
bitPos = 4;
}
else
{
inputs[i] = (pConfigData[1 + i/2] >> 4) & 0xF;
bitPos = 0;
}
}
// First LUT4
word Truth1 = ((word)pConfigData[7] << 8) | pConfigData[6];
word Truth1 = ((word)pConfigData[10] << 8) | pConfigData[11];
printf( "j=%04lX{", (unsigned long)Truth1 );
for ( i = 0; i < 4; i++ )
{
int v = inputs[i];
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
@ -995,11 +982,11 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
}
printf( "} ");
// Second LUT4
word Truth2 = ((word)pConfigData[9] << 8) | pConfigData[8];
word Truth2 = ((word)pConfigData[12] << 8) | pConfigData[13];
printf( "k=%04lX{", (unsigned long)Truth2 );
for ( i = 4; i < 8; i++ )
{
int v = inputs[i];
int v = pConfigData[1+i];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
@ -1012,7 +999,7 @@ void If_ManConfigPrint( unsigned char * pConfigData, int nLeaves )
printf( "} ");
// final node
printf( "l=<");
int v = inputs[8];
int v = pConfigData[1+8];
if ( v == 0 )
printf( "0");
else if ( v == 1 )
@ -1087,11 +1074,11 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
if ( CellId == 0 )
{
// Extract 16-bit truth table
word Truth = ((word)pConfigData[2] << 8) | pConfigData[1];
word Truth = ((word)pConfigData[5] << 8) | pConfigData[6];
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 += 4; // 1 byte CellId + 2 bytes truth table + 1 padding
bytePos += 7; // 1 byte CellId + 4 bytes mapping + 2 bytes truth table
}
else if ( CellId == 1 )
{
@ -1101,7 +1088,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
Vec_IntClear( vLeavesTemp );
for ( i = 0; i < 4; i++ )
{
int v = (pConfigData[1 + i/2] >> ((i%2) * 4)) & 0xF;
int v = pConfigData[1+i];
if ( v == 0 )
Vec_IntPush( vLeavesTemp, 0 ); // constant 0
else if ( v == 1 )
@ -1111,58 +1098,41 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
else
assert( 0 ); // Invalid value
}
word Truth1 = ((word)pConfigData[6] << 8) | pConfigData[5];
word Truth1 = ((word)pConfigData[8] << 8) | pConfigData[9];
Truth1 = Abc_Tt6Stretch( Truth1, 4 );
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)&Truth1, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 );
// Second LUT4 - extract inputs and truth table
Vec_IntClear( vLeavesTemp );
for ( i = 0; i < 4; i++ )
for ( i = 4; i < 7; i++ )
{
int v = (pConfigData[3 + i/2] >> ((i%2) * 4)) & 0xF;
int v = pConfigData[1+i];
if ( v == 0 )
Vec_IntPush( vLeavesTemp, 0 ); // constant 0
else if ( v == 1 )
Vec_IntPush( vLeavesTemp, 1 ); // constant 1
else if ( v >= 2 && v < 2 + Vec_IntSize(vLeaves) )
Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v - 2) ); // leaf (v-2)
else if ( v == 9 ) // N+2 where N=7 (number of S44 inputs)
Vec_IntPush( vLeavesTemp, iObjLit1 ); // output of first LUT (internal connection)
else
assert( 0 ); // Invalid value
}
word Truth2 = ((word)pConfigData[8] << 8) | pConfigData[7];
Vec_IntPush( vLeavesTemp, iObjLit1 ); // output of first LUT (internal connection)
word Truth2 = ((word)pConfigData[10] << 8) | pConfigData[11];
Truth2 = Abc_Tt6Stretch( Truth2, 4 );
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 + 4 bytes mapping + 4 bytes truth tables + 3 padding
bytePos += 12; // 1 byte CellId + 7 bytes mapping + 4 bytes truth tables
}
else if ( CellId == 2 )
{
Vec_Int_t * vLeavesTemp = Vec_IntAlloc( 4 );
int iObjLit1, iObjLit2, iObjLit3;
// Extract 9 input mappings (4 bits each, packed)
int inputs[9];
int bitPos = 0;
for ( i = 0; i < 9; i++ )
{
if ( bitPos == 0 )
{
inputs[i] = pConfigData[1 + i/2] & 0xF;
bitPos = 4;
}
else
{
inputs[i] = (pConfigData[1 + i/2] >> 4) & 0xF;
bitPos = 0;
}
}
// First LUT4 (inputs 0-3)
Vec_IntClear( vLeavesTemp );
for ( i = 0; i < 4; i++ )
{
int v = inputs[i];
int v = pConfigData[1+i];
if ( v == 0 )
Vec_IntPush( vLeavesTemp, 0 ); // constant 0
else if ( v == 1 )
@ -1172,7 +1142,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
else
assert( 0 ); // Invalid value
}
word Truth1 = ((word)pConfigData[7] << 8) | pConfigData[6];
word Truth1 = ((word)pConfigData[10] << 8) | pConfigData[11];
Truth1 = Abc_Tt6Stretch( Truth1, 4 );
extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash );
iObjLit1 = Kit_TruthToGia( pNew, (unsigned *)&Truth1, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 );
@ -1180,7 +1150,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
Vec_IntClear( vLeavesTemp );
for ( i = 4; i < 8; i++ )
{
int v = inputs[i];
int v = pConfigData[1+i];
if ( v == 0 )
Vec_IntPush( vLeavesTemp, 0 ); // constant 0
else if ( v == 1 )
@ -1190,12 +1160,12 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
else
assert( 0 ); // Invalid value
}
word Truth2 = ((word)pConfigData[9] << 8) | pConfigData[8];
word Truth2 = ((word)pConfigData[12] << 8) | pConfigData[13];
Truth2 = Abc_Tt6Stretch( Truth2, 4 );
iObjLit2 = Kit_TruthToGia( pNew, (unsigned *)&Truth2, Vec_IntSize(vLeavesTemp), vCover, vLeavesTemp, 1 );
// MUX (select is input 8) - structural implementation
int iSelectLit;
int v = inputs[8];
int v = pConfigData[1+8];
if ( v == 0 )
iSelectLit = 0; // constant 0 select
else if ( v == 1 )
@ -1207,7 +1177,7 @@ void * If_ManDeriveGiaFromCells2( void * pGia )
iObjLit3 = Gia_ManHashMux( pNew, iSelectLit, iObjLit2, iObjLit1 );
Gia_ManObj(p, iLut)->Value = iObjLit3;
Vec_IntFree( vLeavesTemp );
bytePos += 12; // 1 byte CellId + 5 bytes mapping + 4 bytes truth tables + 2 padding
bytePos += 14; // 1 byte CellId + 9 bytes mapping + 4 bytes truth tables
}
else
{

2
src/misc/util/module.make
View File

@ -1,10 +1,12 @@
SRC += src/misc/util/utilBridge.c \
src/misc/util/utilBipart.c \
src/misc/util/utilBSet.c \
src/misc/util/utilCex.c \
src/misc/util/utilColor.c \
src/misc/util/utilFile.c \
src/misc/util/utilIsop.c \
src/misc/util/utilLinear.c \
src/misc/util/utilMiniver.c \
src/misc/util/utilNam.c \
src/misc/util/utilPrefix.cpp \
src/misc/util/utilPth.c \

1324
src/misc/util/utilBipart.c Normal file
View File

File diff suppressed because it is too large Load Diff

40
src/misc/util/utilLinear.c
View File

@ -276,7 +276,7 @@ static int verify_solution(
}
// Checks whether a particular free-variable assignment yields an integer solution.
// Optionally enforces that the first two variables differ once rounded to integers.
// Optionally enforces that the first four variables differ once rounded to integers.
static int assign_and_check_integer(
const double *rref,
int nVars,
@ -292,7 +292,7 @@ static int assign_and_check_integer(
double *rounded,
double *out_solution,
int require_nonzero,
int require_distinct_first_two) {
int require_distinct_first_four) {
compute_solution_from_free(
rref,
nVars,
@ -334,9 +334,13 @@ static int assign_and_check_integer(
}
}
if (require_distinct_first_two && nVars >= 2) {
if (fabs(rounded[0] - rounded[1]) < INTEGER_TOLERANCE) {
return 0;
if (require_distinct_first_four && nVars >= 4) {
for (int i = 0; i < 4; ++i) {
for (int j = i + 1; j < 4; ++j) {
if (fabs(rounded[i] - rounded[j]) < INTEGER_TOLERANCE) {
return 0;
}
}
}
}
@ -367,7 +371,7 @@ static int search_integer_solutions(
double *rounded,
double *out_solution,
int require_nonzero,
int require_distinct_first_two,
int require_distinct_first_four,
int *explored,
int exploration_limit) {
if (*explored >= exploration_limit) {
@ -391,7 +395,7 @@ static int search_integer_solutions(
rounded,
out_solution,
require_nonzero,
require_distinct_first_two);
require_distinct_first_four);
}
for (int i = 0; i < candidate_count; ++i) {
@ -414,7 +418,7 @@ static int search_integer_solutions(
rounded,
out_solution,
require_nonzero,
require_distinct_first_two,
require_distinct_first_four,
explored,
exploration_limit)) {
return 1;
@ -440,7 +444,7 @@ static int try_integer_solution(
double *rounded,
double *out_solution,
int require_nonzero,
int require_distinct_first_two) {
int require_distinct_first_four) {
if (free_count == 0) {
return 0;
}
@ -496,7 +500,7 @@ static int try_integer_solution(
rounded,
out_solution,
require_nonzero,
require_distinct_first_two)) {
require_distinct_first_four)) {
free(free_values);
return 1;
}
@ -519,7 +523,7 @@ static int try_integer_solution(
rounded,
out_solution,
require_nonzero,
require_distinct_first_two,
require_distinct_first_four,
&explored,
exploration_limit);
@ -548,7 +552,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) {
int free_count = 0;
int homogeneous_rhs = 0;
int require_nonzero_integer = 0;
int require_distinct_first_two = 0;
int require_distinct_first_four = 0;
int pivot_row_index = 0;
int rank = 0;
double max_residual = 0.0;
@ -673,7 +677,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) {
// Only demand integer solutions when the system is homogeneous with free variables.
require_nonzero_integer = homogeneous_rhs && free_count > 0;
// Enforce distinct first two variables whenever multiple variables remain free.
require_distinct_first_two = (free_count > 0 && nVars >= 2);
require_distinct_first_four = (free_count > 0 && nVars >= 4);
solution = (double *)malloc((size_t)nVars * sizeof(double));
workspace = (double *)malloc((size_t)nVars * sizeof(double));
@ -711,7 +715,7 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) {
rounded,
solution,
require_nonzero_integer,
require_distinct_first_two)) {
require_distinct_first_four)) {
for (int i = 0; i < free_count; ++i) {
workspace[i] = 0.0;
}
@ -724,12 +728,12 @@ double *linear_equation_solver(double *pMatrix, int nEqus, int nVars) {
free_count,
workspace,
solution);
if (require_nonzero_integer && require_distinct_first_two) {
printf("Note: integer solution meeting non-negative and distinct-first-two constraints not found; returning floating-point solution.\n");
if (require_nonzero_integer && require_distinct_first_four) {
printf("Note: integer solution meeting non-negative and distinct-first-four constraints not found; returning floating-point solution.\n");
} else if (require_nonzero_integer) {
printf("Note: non-negative integer solution with mixed zero/positive entries not found; returning floating-point solution.\n");
} else if (require_distinct_first_two) {
printf("Note: integer solution with distinct first two variables not found; returning floating-point solution.\n");
} else if (require_distinct_first_four) {
printf("Note: integer solution with distinct first four variables not found; returning floating-point solution.\n");
} else {
printf("Note: integer solution not found; returning floating-point solution.\n");
}

629
src/misc/util/utilMiniver.c Normal file
View File

@ -0,0 +1,629 @@
/**CFile****************************************************************
FileName [utilMiniver.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Handling counter-examples.]
Synopsis [Handling counter-examples.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: utilMiniver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include <ctype.h>
#include <stdarg.h>
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include "misc/util/abc_global.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MINIVER_LIBRARY_ONLY
#define MAXSIG 1024
#define MAXSTR 65536
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct {
char name[128];
int width;
int is_signed;
} decl_t;
typedef struct {
char lhs[128];
char rhs[4096];
} asn_t;
// Parsing/collection context (encapsulates all state)
typedef struct {
char modname[128];
decl_t inputs[MAXSIG]; int ni;
decl_t outputs[MAXSIG]; int no;
decl_t wires[MAXSIG]; int nw;
asn_t assigns[MAXSIG]; int na;
int next_auto_in; // next index for auto-generated input names ('a' + idx)
} mv_ctx;
// -----------------------------------------------------------------------------
// Utilities
// -----------------------------------------------------------------------------
// Remove all ASCII whitespace from 's' into 'out'.
static void strip_ws(const char *s, char *out) {
while (*s) {
if (!isspace((unsigned char)*s)) {
*out++ = *s;
}
++s;
}
*out = 0;
}
static int is_ident_start(char c) {
return isalpha((unsigned char)c) || c == '_' || c == '$';
}
static int is_ident_char(char c) {
return isalnum((unsigned char)c) || c == '_' || c == '$';
}
// Parse a non-negative decimal integer from 's'; store value in *v and chars consumed in *nch.
static int parse_uint(const char *s, int *v, int *nch) {
int i = 0;
int d = 0;
if (!isdigit((unsigned char)s[0])) return 0;
while (isdigit((unsigned char)s[i])) {
d = d * 10 + (s[i] - '0');
++i;
}
*v = d;
*nch = i;
return 1;
}
// Check if a name is already used in any declaration.
static int name_exists(mv_ctx *ctx, const char *name) {
for (int i = 0; i < ctx->ni; ++i) if (!strcmp(ctx->inputs[i].name, name)) return 1;
for (int i = 0; i < ctx->no; ++i) if (!strcmp(ctx->outputs[i].name, name)) return 1;
for (int i = 0; i < ctx->nw; ++i) if (!strcmp(ctx->wires[i].name, name)) return 1;
return 0;
}
// Generate next auto input name: 'a','b','c',... then 'a0','a1',... if 26 exhausted.
static void gen_auto_in_name(mv_ctx *ctx, char *out, size_t out_sz) {
// try single letters first
for (; ctx->next_auto_in < 26; ++ctx->next_auto_in) {
char cand[3] = {(char)('a' + ctx->next_auto_in), 0, 0};
if (!name_exists(ctx, cand)) { strncpy(out, cand, out_sz-1); out[out_sz-1]=0; ++ctx->next_auto_in; return; }
}
// fallback to aN form
for (int n = 0;; ++n) {
char cand[32];
snprintf(cand, sizeof(cand), "a%d", n);
if (!name_exists(ctx, cand)) { strncpy(out, cand, out_sz-1); out[out_sz-1]=0; return; }
}
}
// Add (or deduplicate) declaration into an array.
static void add_decl(decl_t *arr, int *cnt, const char *name, int w, int sg) {
for (int k = 0; k < *cnt; ++k) {
if (!strcmp(arr[k].name, name)) return;
}
strncpy(arr[*cnt].name, name, sizeof(arr[*cnt].name) - 1);
arr[*cnt].width = w;
arr[*cnt].is_signed = sg;
++(*cnt);
}
// Record an assignment; returns non-zero on overflow.
static int add_asn(mv_ctx *ctx, const char *lhs, const char *rhs) {
if (ctx->na >= MAXSIG) {
printf("Too many assignments.\n");
return 1;
}
strncpy(ctx->assigns[ctx->na].lhs, lhs, sizeof(ctx->assigns[ctx->na].lhs) - 1);
strncpy(ctx->assigns[ctx->na].rhs, rhs, sizeof(ctx->assigns[ctx->na].rhs) - 1);
++ctx->na;
return 0;
}
// Append formatted text to user-provided buffer with capacity checks.
// On insufficient capacity, print message and return 1; otherwise 0.
static int out_cat(char **p, size_t *left, const char *fmt, ...) {
va_list ap;
va_start(ap, fmt);
int need = vsnprintf(NULL, 0, fmt, ap);
va_end(ap);
if (need < 0 || (size_t)need >= *left) {
printf("Output exceeds buffer capacity.\n");
return 1;
}
va_start(ap, fmt);
int wrote = vsnprintf(*p, *left, fmt, ap);
va_end(ap);
*p += wrote;
*left -= (size_t)wrote;
return 0;
}
// Emit declarations into the output buffer.
static int print_decl_to_buf(char **p, size_t *left, const char *kw, decl_t *arr, int n) {
for (int i = 0; i < n; ++i) {
int w = arr[i].width;
int sg = arr[i].is_signed;
const char *id = arr[i].name;
if (w == 1) {
if (out_cat(p, left, " %s %s%s;\n", kw, sg ? "signed " : "", id)) return 1;
} else {
if (out_cat(p, left, " %s %s[%d:0] %s;\n", kw, sg ? "signed " : "", w - 1, id)) return 1;
}
}
return 0;
}
static int print_decl_single(char **p, size_t *left, const char *kw, const decl_t *decl) {
if (out_cat(p, left, " %s ", kw)) return 1;
if (decl->is_signed) {
if (out_cat(p, left, "signed ")) return 1;
}
if (decl->width > 1) {
if (out_cat(p, left, "[%d:0] ", decl->width - 1)) return 1;
}
if (out_cat(p, left, "%s;\n", decl->name)) return 1;
return 0;
}
static int print_decl_with_assign(char **p, size_t *left, const char *kw, const decl_t *decl, const char *rhs) {
if (out_cat(p, left, " %s ", kw)) return 1;
if (decl->is_signed) {
if (out_cat(p, left, "signed ")) return 1;
}
if (decl->width > 1) {
if (out_cat(p, left, "[%d:0] ", decl->width - 1)) return 1;
}
if (out_cat(p, left, "%s = %s;\n", decl->name, rhs)) return 1;
return 0;
}
static int print_inputs_short(char **p, size_t *left, decl_t *arr, int n) {
for (int i = 0; i < n; ) {
int w = arr[i].width;
int sg = arr[i].is_signed;
if (out_cat(p, left, " input ")) return 1;
if (sg) {
if (out_cat(p, left, "signed ")) return 1;
}
if (w > 1) {
if (out_cat(p, left, "[%d:0] ", w - 1)) return 1;
}
int j = i;
while (j < n && arr[j].width == w && arr[j].is_signed == sg) {
if (out_cat(p, left, "%s%s", j == i ? "" : ", ", arr[j].name)) return 1;
++j;
}
if (out_cat(p, left, ";\n")) return 1;
i = j;
}
return 0;
}
static decl_t *find_decl_by_name(decl_t *arr, int n, const char *name) {
for (int i = 0; i < n; ++i) {
if (!strcmp(arr[i].name, name))
return &arr[i];
}
return NULL;
}
static int has_assignment(const mv_ctx *ctx, const char *name) {
for (int i = 0; i < ctx->na; ++i)
if (!strcmp(ctx->assigns[i].lhs, name))
return 1;
return 0;
}
// Add spaces around every alphanumeric/underscore sequence for readability.
// Example: "a*b+16'b0" -> " a * b + 16 ' b0 "
static void format_rhs_readable(const char *in, char *out, size_t cap) {
size_t o = 0;
for (size_t i = 0; in[i]; ) {
unsigned char c = (unsigned char)in[i];
if (isalnum(c) || c == '_') {
// start of a token
if (o + 1 >= cap) { if (o) out[o-1] = 0; else if (cap) out[0] = 0; return; }
out[o++] = ' ';
// copy token
size_t j = i;
while (in[j] && (isalnum((unsigned char)in[j]) || in[j] == '_')) {
if (o + 1 >= cap) { out[o-1] = 0; return; }
out[o++] = in[j++];
}
if (o + 1 >= cap) { out[o-1] = 0; return; }
out[o++] = ' ';
i = j;
} else {
if (o + 1 >= cap) { if (o) out[o-1] = 0; else if (cap) out[0] = 0; return; }
out[o++] = in[i++];
}
}
if (o < cap) out[o] = 0; else if (cap) out[cap-1] = 0;
}
static void trim_spaces(char *s) {
if (!s) return;
char *start = s;
while (*start && isspace((unsigned char)*start))
++start;
char *end = start + strlen(start);
while (end > start && isspace((unsigned char)*(end - 1)))
--end;
size_t len = (size_t)(end - start);
if (start != s)
memmove(s, start, len);
s[len] = 0;
}
// -----------------------------------------------------------------------------
// Parsing helpers that quote offending clauses
// -----------------------------------------------------------------------------
typedef int (*emit_fn)(mv_ctx *, const char *, int, int);
static int emit_in(mv_ctx *ctx, const char *id, int w, int sg) {
add_decl(ctx->inputs, &ctx->ni, id, w, sg);
return 0;
}
static int emit_wi(mv_ctx *ctx, const char *id, int w, int sg) {
add_decl(ctx->wires, &ctx->nw, id, w, sg);
return 0;
}
// Split an identifier list like "a,b,c" and emit each item. Quotes 'clause' in diagnostics.
static int split_ids(mv_ctx *ctx, const char *clause, const char *s, emit_fn emit, int w, int sg) {
char buf[128];
int j = 0;
for (int i = 0;; ++i) {
char c = s[i];
if (c == ',' || c == 0) {
if (j == 0) {
printf("Syntax error: empty identifier in expression \"%s\".\n", clause);
return 1;
}
buf[j] = 0;
if (emit(ctx, buf, w, sg)) return 1;
j = 0;
if (c == 0) break;
} else {
if (j >= 120) {
printf("Identifier too long in expression \"%s\".\n", clause);
return 1;
}
if (!((j ? is_ident_char(c) : is_ident_start(c)))) {
printf("Illegal identifier in expression \"%s\".\n", clause);
return 1;
}
buf[j++] = c;
}
}
return 0;
}
// Parse one clause (already whitespace-stripped). On error, prints a message including the clause.
static int parse_clause(mv_ctx *ctx, const char *q) {
if (!q || !*q) return 0;
if (q[0] == 'm') {
if (!is_ident_start(q[1])) {
printf("Syntax error after 'm' in expression \"%s\".\n", q);
return 1;
}
int i = 1;
while (q[i] && is_ident_char(q[i])) ++i;
if (q[i]) {
printf("Garbage after module name in expression \"%s\".\n", q);
return 1;
}
size_t n = (size_t)(i - 1);
if (n >= sizeof(ctx->modname)) n = sizeof(ctx->modname) - 1;
strncpy(ctx->modname, q + 1, n);
ctx->modname[n] = 0;
return 0;
}
if (q[0] != 'i' && q[0] != 'o' && q[0] != 'w') {
printf("Unknown clause start in expression \"%s\".\n", q);
return 1;
}
int kind = q[0];
int i = 1;
int sg = 0;
int w = 0;
int nconsumed = 0;
if (q[i] == 's') {
sg = 1;
++i;
}
if (!parse_uint(q + i, &w, &nconsumed)) {
printf("Width expected in expression \"%s\".\n", q);
return 1;
}
i += nconsumed;
if (w <= 0) {
printf("Non-positive width in expression \"%s\".\n", q);
return 1;
}
const char *eq = strchr(q + i, '=');
if (kind == 'i') {
// Support unnamed inputs: 'i4' -> auto-generate one input named a,b,c,...
if (!q[i]) {
char auto_name[32];
gen_auto_in_name(ctx, auto_name, sizeof(auto_name));
add_decl(ctx->inputs, &ctx->ni, auto_name, w, sg);
return 0;
}
if (eq) {
printf("Unexpected '=' in input clause in expression \"%s\".\n", q);
return 1;
}
return split_ids(ctx, q, q + i, emit_in, w, sg);
}
if (kind == 'w' && !eq) {
if (!q[i]) {
printf("Identifiers expected for wires in expression \"%s\".\n", q);
return 1;
}
return split_ids(ctx, q, q + i, emit_wi, w, sg);
}
if (!eq) {
printf("Assignment expected in expression \"%s\".\n", q);
return 1;
}
// Parse the LHS name for 'o' or 'w'. For 'o', allow omitted name (defaults to "o").
char lhs[128];
int lj = 0;
for (int k = i; k < (int)(eq - q); ++k) {
char c = q[k];
if (!lj && kind == 'o' && !is_ident_start(c)) {
lhs[0] = 'o';
lhs[1] = 0;
goto lhs_done;
}
if (!(lj ? is_ident_char(c) : is_ident_start(c))) {
printf("Illegal LHS identifier in expression \"%s\".\n", q);
return 1;
}
if (lj >= 120) {
printf("Identifier too long in expression \"%s\".\n", q);
return 1;
}
lhs[lj++] = c;
}
if (lj == 0) {
if (kind == 'o') {
lhs[0] = 'o';
lhs[1] = 0;
} else {
printf("Wire assignment needs a name in expression \"%s\".\n", q);
return 1;
}
} else {
lhs[lj] = 0;
}
lhs_done:;
const char *rhs = eq + 1;
if (!*rhs) {
printf("Empty RHS expression in expression \"%s\".\n", q);
return 1;
}
if (kind == 'o') add_decl(ctx->outputs, &ctx->no, lhs, w, sg);
if (kind == 'w') add_decl(ctx->wires, &ctx->nw, lhs, w, sg);
return add_asn(ctx, lhs, rhs);
}
// -----------------------------------------------------------------------------
// Public API
// -----------------------------------------------------------------------------
// Translate a raw mini-Verilog string 'input' into standard Verilog.
// The function strips whitespace internally, parses, and writes into 'out' (cap bytes).
// Returns 0 on success, 1 on error. Errors are printed (no exit()).
int miniver_translate(const char *input, char *out, size_t cap, int fShort) {
if (!input || !out || cap == 0) {
printf("Invalid arguments.\n");
return 1;
}
// Step 1: strip whitespace (per spec).
char flat[MAXSTR];
strip_ws(input, flat);
if (!*flat) {
printf("Empty input.\n");
return 1;
}
// Step 2: parse clauses into a context.
mv_ctx *ctx = (mv_ctx*)calloc(1, sizeof(mv_ctx));
if (!ctx) {
printf("Out of memory.\n");
return 1;
}
strncpy(ctx->modname, "top", sizeof(ctx->modname) - 1);
ctx->next_auto_in = 0;
// Make a modifiable copy to split on semicolons.
char *buf = (char*)malloc(strlen(flat) + 1);
if (!buf) {
printf("Out of memory.\n");
free(ctx);
return 1;
}
strcpy(buf, flat);
char *s = buf;
while (*s) {
char *semi = strchr(s, ';');
if (semi) *semi = 0;
if (parse_clause(ctx, s)) {
free(buf);
free(ctx);
return 1;
}
if (!semi) break;
s = semi + 1;
}
free(buf);
if (!*ctx->modname) {
printf("Module name missing.\n");
free(ctx);
return 1;
}
if (ctx->no == 0) {
printf("At least one output with assignment is required.\n");
free(ctx);
return 1;
}
// Step 3: emit Verilog into caller buffer.
char *p = out;
size_t left = cap;
if (out_cat(&p, &left, "module %s (", ctx->modname)) {
free(ctx); return 1;
}
for (int i = 0; i < ctx->ni; ++i) {
if (out_cat(&p, &left, "%s%s", i ? ", " : "", ctx->inputs[i].name)) {
free(ctx); return 1;
}
}
for (int i = 0; i < ctx->no; ++i) {
if (out_cat(&p, &left, "%s%s", (ctx->ni || i) ? ", " : "", ctx->outputs[i].name)) {
free(ctx); return 1;
}
}
if (out_cat(&p, &left, ");\n")) {
free(ctx); return 1;
}
if (!fShort) {
if (print_decl_to_buf(&p, &left, "input", ctx->inputs, ctx->ni)) { free(ctx); return 1; }
if (print_decl_to_buf(&p, &left, "output", ctx->outputs, ctx->no)) { free(ctx); return 1; }
if (print_decl_to_buf(&p, &left, "wire", ctx->wires, ctx->nw)) { free(ctx); return 1; }
for (int i = 0; i < ctx->na; ++i) {
char rhs_sp[8192];
format_rhs_readable(ctx->assigns[i].rhs, rhs_sp, sizeof(rhs_sp));
if (out_cat(&p, &left, " assign %s = %s;\n", ctx->assigns[i].lhs, rhs_sp)) {
free(ctx); return 1;
}
}
} else {
if (print_inputs_short(&p, &left, ctx->inputs, ctx->ni)) { free(ctx); return 1; }
for (int i = 0; i < ctx->nw; ++i) {
if (has_assignment(ctx, ctx->wires[i].name))
continue;
if (print_decl_single(&p, &left, "wire", &ctx->wires[i])) {
free(ctx); return 1;
}
}
for (int i = 0; i < ctx->na; ++i) {
char rhs_sp[8192];
format_rhs_readable(ctx->assigns[i].rhs, rhs_sp, sizeof(rhs_sp));
trim_spaces(rhs_sp);
const char *kw = "wire";
decl_t *decl = find_decl_by_name(ctx->outputs, ctx->no, ctx->assigns[i].lhs);
if (decl) {
kw = "output";
} else {
decl = find_decl_by_name(ctx->wires, ctx->nw, ctx->assigns[i].lhs);
}
if (decl) {
if (print_decl_with_assign(&p, &left, kw, decl, rhs_sp)) {
free(ctx); return 1;
}
} else {
if (out_cat(&p, &left, " assign %s = %s;\n", ctx->assigns[i].lhs, rhs_sp)) {
free(ctx); return 1;
}
}
}
}
if (out_cat(&p, &left, "endmodule\n")) {
free(ctx); return 1;
}
*p = 0;
free(ctx);
return 0;
}
// -----------------------------------------------------------------------------
// Optional CLI wrapper (define MINIVER_LIBRARY_ONLY to omit main)
// -----------------------------------------------------------------------------
#ifndef MINIVER_LIBRARY_ONLY
int main(int argc, char **argv) {
char in[MAXSTR] = {0};
if (argc >= 2) {
size_t L = strlen(argv[1]);
if (L >= MAXSTR - 1) {
printf("Input too long.\n");
return 1;
}
strcpy(in, argv[1]);
} else {
size_t off = 0;
int c = 0;
while ((c = fgetc(stdin)) != EOF) {
if (off >= MAXSTR - 1) {
printf("Input too long.\n");
return 1;
}
in[off++] = (char)c;
}
in[off] = 0;
}
char out[10240];
int rc = miniver_translate(in, out, sizeof(out), 0);
if (!rc) {
printf("%s", out);
}
return rc;
}
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

42
src/misc/util/utilTruth.h
View File

@ -230,7 +230,8 @@ static inline int Abc_TtHexDigitNum( int nVars ) { return nVars <= 2 ? 1 : 1 <<
SeeAlso []
***********************************************************************/
static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
static inline word Abc_Tt6MaskI( int iBit ) { assert( iBit >= 0 && iBit <= 64 ); return ((word)1) << iBit; }
static inline word Abc_Tt6Mask( int nBits ) { assert( nBits >= 0 && nBits <= 64 ); return (~(word)0) >> (64-nBits); }
static inline void Abc_TtMask( word * pTruth, int nWords, int nBits )
{
int w;
@ -1579,6 +1580,43 @@ static inline int Abc_TtReadHexNumber( word * pTruth, char * pString )
}
/**Function*************************************************************
Synopsis [Reads the integer number as a binary string.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Abc_TtReadBin( word * pWords, int nWords, char * pString )
{
int i, Len = (int)strlen(pString), nWords2 = (Len+63)/64;
assert( nWords2 <= nWords );
memset( pWords, 0, sizeof(word)*nWords );
for ( i = 0; i < Len; i++ )
if ( pString[i] == '1' )
Abc_TtSetBit(pWords, i);
else if ( pString[i] != '0' )
return 0;
return 1;
}
static inline word Abc_TtReadBin64( char * pString )
{
word Word = 0;
int Len = (int)strlen(pString);
assert( Len <= 64 );
int Res = Abc_TtReadBin( &Word, 1, pString );
if ( Res == 0 ) {
printf( "Reading binary string \"%s\" has failed.\n", pString );
Word = ~(word)0;
}
return Word;
}
/**Function*************************************************************
Synopsis []
@ -1602,7 +1640,7 @@ static inline void Abc_TtPrintBits2( word * pTruth, int nBits )
int k;
for ( k = nBits-1; k >= 0; k-- )
printf( "%d", Abc_InfoHasBit( (unsigned *)pTruth, k ) );
printf( "\n" );
//printf( "\n" );
}
static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
{

10
src/misc/vec/vecInt.h
View File

@ -1278,6 +1278,16 @@ static inline Vec_Int_t * Vec_IntInvert( Vec_Int_t * p, int Fill )
Vec_IntWriteEntry( vRes, Entry, i );
return vRes;
}
static inline Vec_Int_t * Vec_IntInvertSize( Vec_Int_t * p, int Size, int Fill )
{
Vec_Int_t * vMap = Vec_IntAlloc( 0 );
Vec_IntFill( vMap, Size, Fill );
int i, k;
Vec_IntForEachEntry( p, i, k )
if ( i != Fill )
Vec_IntWriteEntry( vMap, i, k );
return vMap;
}
/**Function*************************************************************

79
src/opt/dau/dauNpn.c
View File

@ -859,6 +859,85 @@ Vec_Mem_t * Dau_CollectNpnFunctions( word * p, int nVars, int fVerbose )
return vTtMem;
}
/**Function*************************************************************
Synopsis [Function enumeration.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_PrintNpnFunction( Vec_Mem_t * vTtMem, int nFuncs, word * pCopy, int nVars, int uPhase, int * pPerm, int fVerbose )
{
int nWords = Abc_Truth6WordNum(nVars);
if ( fVerbose ) {
printf( "%6d : ", nFuncs );
Abc_TtPrintBits2((word *)&uPhase, nVars);
printf( " " );
for ( int v = nVars-1; v >= 0; v-- )
printf( " %d", pPerm[v] );
printf( " F = " );
Abc_TtPrintHexRev( stdout, pCopy, nVars );
}
int Pos = Vec_MemHashInsert( vTtMem, pCopy );
Abc_TtNot( pCopy, nWords );
if ( fVerbose ) {
printf( " (%05d)", Pos );
printf( " ~F = " );
Abc_TtPrintHexRev( stdout, pCopy, nVars );
}
int Neg = Vec_MemHashInsert( vTtMem, pCopy );
Abc_TtNot( pCopy, nWords );
if ( fVerbose ) {
printf( " (%05d)", Neg );
printf( "\n" );
}
}
void Dau_PrintNpnFunctions( word * p, int nVars, int fVerbose )
{
int nWords = Abc_Truth6WordNum(nVars);
Vec_Mem_t * vTtMem = Vec_MemAllocForTTSimple( nVars );
word * pCopy = ABC_ALLOC( word, nWords );
word * pBest = ABC_ALLOC( word, nWords );
Abc_TtCopy( pCopy, p, nWords, 0 );
Abc_TtCopy( pBest, p, nWords, 0 );
int nPerms = Extra_Factorial( nVars );
int nMints = 1 << nVars;
int * pPerm = Extra_PermSchedule( nVars );
int * pComp = Extra_GreyCodeSchedule( nVars );
int m, i, k, nFuncs = 0;
int uVarPhase = 0;
int pVarPerm[32];
printf( "The number of NPN configurations is %d = %d complementations * %d permutations * 2 output polarities.\n", nMints*nPerms*2, nMints, nPerms );
for ( i = 0; i < nVars; i++ )
pVarPerm[i] = i;
for ( m = 0; m < nMints; m++ ) {
for ( k = 0; k < nPerms; k++ ) {
if ( Abc_TtCompare(pBest, pCopy, nWords) == 1 )
Abc_TtCopy( pBest, pCopy, nWords, 0 );
Dau_PrintNpnFunction( vTtMem, nFuncs++, pCopy, nVars, uVarPhase, pVarPerm, fVerbose );
Abc_TtSwapAdjacent( pCopy, nWords, pPerm[k] );
ABC_SWAP( int, pVarPerm[pPerm[k]], pVarPerm[pPerm[k]+1] );
}
if ( fVerbose ) printf( "\n" );
Abc_TtFlip( pCopy, nWords, pComp[m] );
uVarPhase ^= 1 << pComp[m];
}
assert( Abc_TtEqual(pCopy, p, nWords) );
printf( "The number of unique functions %d (out of %d). Frequency = %d. Representative: ", Vec_MemEntryNum(vTtMem), nMints*nPerms*2, nMints*nPerms*2/Vec_MemEntryNum(vTtMem) );
Abc_TtPrintHexRev( stdout, pBest, nVars );
printf( "\n" );
ABC_FREE( pPerm );
ABC_FREE( pComp );
ABC_FREE( pCopy );
ABC_FREE( pBest );
Vec_MemHashFree( vTtMem );
Vec_MemFree( vTtMem );
}
/**Function*************************************************************
Synopsis [Compute NPN class members.]

5
src/sat/bmc/bmc.h
View File

@ -57,6 +57,8 @@ struct Bmc_EsPar_t_
int fDynConstr;
int fDumpCnf;
int fGlucose;
int fCadical;
int fKissat;
int fCard;
int fOrderNodes;
int fEnumSols;
@ -65,14 +67,17 @@ struct Bmc_EsPar_t_
int fUniqFans;
int fLutCascade;
int fLutInFixed;
int fMinNodes;
int RuntimeLim;
int nRandFuncs;
int nMintNum;
int Seed;
int fDumpBlif;
int fVerbose;
int fSilent;
char * pTtStr;
char * pSymStr;
char * pPermStr;
char * pGuide;
};

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

@ -1063,7 +1063,7 @@ Vec_Wec_t * Exa3_ChooseInputVars_int( int nVars, int nLuts, int nLutSize )
Vec_Int_t * vLevel; int i;
Vec_WecForEachLevel( p, vLevel, i ) {
do {
int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
int iVar = rand() % nVars;
Vec_IntPushUniqueOrder( vLevel, iVar );
}
while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
@ -1079,8 +1079,16 @@ Vec_Int_t * Exa3_CountInputVars( int nVars, Vec_Wec_t * p )
Vec_IntAddToEntry( vCounts, Obj, 1 );
return vCounts;
}
Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize )
Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize, int Seed )
{
if ( Seed )
srand(Seed);
else {
struct timespec ts;
clock_gettime(CLOCK_REALTIME, &ts);
unsigned int seed = (unsigned int)(ts.tv_sec ^ ts.tv_nsec);
srand(seed);
}
for ( int i = 0; i < 1000; i++ ) {
Vec_Wec_t * p = Exa3_ChooseInputVars_int( nVars, nLuts, nLutSize );
Vec_Int_t * q = Exa3_CountInputVars( nVars, p );
@ -1093,6 +1101,18 @@ Vec_Wec_t * Exa3_ChooseInputVars( int nVars, int nLuts, int nLutSize )
assert( 0 );
return NULL;
}
Vec_Wec_t * Exa3_ChooseInputVars2( int nVars, int nLuts, int nLutSize, char * pPermStr )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i, Pos = 0;
assert( nLuts * nLutSize == (int)strlen(pPermStr) );
Vec_WecForEachLevel( p, vLevel, i ) {
for ( int k = 0; k < nLutSize; k++, Pos++ )
if ( pPermStr[Pos] != '_' )
Vec_IntPush( vLevel, pPermStr[Pos] == '*' ? -1 : (int)(pPermStr[Pos]-'a') );
}
return p;
}
/**Function*************************************************************
@ -1155,16 +1175,20 @@ static int Exa3_ManMarkup( Exa3_Man_t * p )
}
}
}
printf( "The number of parameter variables = %d.\n", p->iVar );
if ( p->pPars->fLutCascade && p->pPars->fLutInFixed ) {
p->vInVars = Exa3_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize );
if ( 1 ) {
if ( !p->pPars->fSilent ) printf( "The number of parameter variables = %d.\n", p->iVar );
if ( p->pPars->fLutCascade && (p->pPars->fLutInFixed || p->pPars->pPermStr) ) {
if ( p->pPars->pPermStr )
p->vInVars = Exa3_ChooseInputVars2( p->nVars, p->nNodes, p->nLutSize, p->pPars->pPermStr );
else
p->vInVars = Exa3_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize, p->pPars->Seed );
if ( !p->pPars->fSilent ) {
Vec_Int_t * vLevel; int i, Var;
printf( "Using fixed input assignment:\n" );
printf( "Using fixed input assignment %s%s:\n",
p->pPars->pPermStr ? "provided by the user " : "generated randomly", p->pPars->pPermStr ? p->pPars->pPermStr : "" );
Vec_WecForEachLevelReverse( p->vInVars, vLevel, i ) {
printf( "%02d : ", p->nVars+i );
printf( "%c : ", 'A'+p->nVars+i-p->nVars );
Vec_IntForEachEntry( vLevel, Var, k )
printf( "%c ", 'a'+Var );
printf( "%c ", Var < 0 ? '*' : 'a'+Var );
printf( "\n" );
}
}
@ -1291,7 +1315,7 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
printf( "%02d = %d\'b", i, 1 << p->nLutSize );
printf( "%c = %d\'b", 'A'+i-p->nVars, 1 << p->nLutSize );
for ( k = p->LutMask - 1; k >= 0; k-- )
{
Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+k);
@ -1311,12 +1335,26 @@ static void Exa3_ManPrintSolution( Exa3_Man_t * p, int fCompl )
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %02d", iVar );
printf( " %c", 'A'+iVar-p->nVars );
}
printf( " )\n" );
}
}
static void Exa3_ManPrintPerm( Exa3_Man_t * p )
{
int i, k, iVar;
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( i > p->nVars )
printf( "_" );
for ( k = p->nLutSize - 1; k >= 0; k-- )
{
iVar = Exa3_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( "%c", 'a'+iVar );
}
}
}
/**Function*************************************************************
Synopsis []
@ -1332,7 +1370,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
char * pStr = Abc_UtilStrsav(p->pPars->pTtStr);
char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr);
if ( strlen(pStr) > 16 ) {
pStr[16] = '_';
pStr[17] = '\0';
@ -1374,7 +1412,7 @@ static void Exa3_ManDumpBlif( Exa3_Man_t * p, int fCompl )
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
if ( !p->pPars->fSilent ) printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
ABC_FREE( pStr );
}
@ -1472,10 +1510,16 @@ static int Exa3_ManAddCnfStart( Exa3_Man_t * p, int fOnlyAnd )
}
if ( p->vInVars ) {
Vec_Int_t * vLevel; int Var;
//Vec_WecPrint( p->vInVars, 0 );
Vec_WecForEachLevel( p->vInVars, vLevel, i )
{
assert( Vec_IntSize(vLevel) > 0 );
Vec_IntForEachEntry( vLevel, Var, k ) {
if ( Var < 0 ) continue;
if ( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var] == 0 ) {
printf( "Skipping variable %d in place %d because it cannot be constrained.\n", Var, k );
continue;
}
pLits[0] = Abc_Var2Lit( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var], 0 ); assert(pLits[0]);
if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 1 ) )
return 0;
@ -1616,7 +1660,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
printf( "Generated symmetric function: %s\n", pPars->pTtStr );
if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
ABC_FREE( pFun );
}
if ( pPars->pTtStr )
@ -1628,7 +1672,7 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
status = Exa3_ManAddCnfStart( p, pPars->fOnlyAnd );
assert( status );
printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
if ( !pPars->fSilent ) printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
if ( pPars->fUseIncr )
{
bmcg_sat_solver_set_nvars( p->pSat, p->iVar + p->nNodes*(1 << p->nVars) );
@ -1648,14 +1692,18 @@ int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
}
if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( iMint == -1 )
if ( iMint == -1 ) {
Exa3_ManPrintSolution( p, fCompl ), Res = 1;
printf( "The variable permutation is \"" );
Exa3_ManPrintPerm(p);
printf( "\".\n" );
}
else if ( status == GLUCOSE_UNDEC )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
else
else if ( !p->pPars->fSilent )
printf( "The problem has no solution.\n" ), Res = 2;
printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
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->pSymStr )

767
src/sat/bmc/bmcMaj7.c Normal file
View File

@ -0,0 +1,767 @@
/**CFile****************************************************************
FileName [bmcMaj.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Exact synthesis with majority gates.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 1, 2017.]
Revision [$Id: bmcMaj.c,v 1.00 2017/10/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/cadical/cadicalSolver.h"
#include "sat/cadical/ccadical.h"
#include "aig/miniaig/miniaig.h"
#include "base/io/ioResub.h"
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#define CADICAL_UNSAT -1
#define CADICAL_SAT 1
#define CADICAL_UNDEC 0
ABC_NAMESPACE_IMPL_START
static inline void Exa7_CadicalSetRuntimeLimit( cadical_solver * pSat, int nSeconds )
{
if ( pSat == NULL || nSeconds <= 0 )
return;
ccadical_limit( (CCaDiCaL *)pSat->p, "seconds", nSeconds );
}
#ifdef WIN32
#include <process.h>
#define unlink _unlink
#else
#include <unistd.h>
#endif
#include <limits.h>
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
typedef struct Exa7_Man_t_ Exa7_Man_t;
struct Exa7_Man_t_
{
Bmc_EsPar_t * pPars; // parameters
int nVars; // inputs
int nNodes; // internal nodes
int nLutSize; // lut size
int LutMask; // lut mask
int nObjs; // total objects (nVars inputs + nNodes internal nodes)
int nWords; // the truth table size in 64-bit words
int iVar; // the next available SAT variable
word * pTruth; // truth table
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS]; // values of the first nVars variables
Vec_Wec_t * vOutLits; // output vars
Vec_Wec_t * vInVars; // input vars
cadical_solver * pSat; // SAT solver
int nVarAlloc; // total vars reserved in the solver
int nUsed[2];
};
static inline word * Exa7_ManTruth( Exa7_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
static inline int Exa7_ManIsUsed2( Exa7_Man_t * p, int m, int n, int i, int j )
{
int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j;
p->nUsed[0]++;
assert( i < n && j < n && i < j );
if ( Vec_BitEntry(p->vUsed2, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed2, Pos, 1 );
return 0;
}
static inline int Exa7_ManIsUsed3( Exa7_Man_t * p, int m, int n, int i, int j, int k )
{
int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k;
p->nUsed[0]++;
assert( i < n && j < n && k < n && i < j && j < k );
if ( Vec_BitEntry(p->vUsed3, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed3, Pos, 1 );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Exa7_ChooseInputVars_int( int nVars, int nLuts, int nLutSize )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i;
Vec_WecForEachLevel( p, vLevel, i ) {
do {
int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
Vec_IntPushUniqueOrder( vLevel, iVar );
}
while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
}
return p;
}
Vec_Int_t * Exa7_CountInputVars( int nVars, Vec_Wec_t * p )
{
Vec_Int_t * vLevel; int i, k, Obj;
Vec_Int_t * vCounts = Vec_IntStart( nVars );
Vec_WecForEachLevel( p, vLevel, i )
Vec_IntForEachEntry( vLevel, Obj, k )
Vec_IntAddToEntry( vCounts, Obj, 1 );
return vCounts;
}
Vec_Wec_t * Exa7_ChooseInputVars( int nVars, int nLuts, int nLutSize )
{
for ( int i = 0; i < 1000; i++ ) {
Vec_Wec_t * p = Exa7_ChooseInputVars_int( nVars, nLuts, nLutSize );
Vec_Int_t * q = Exa7_CountInputVars( nVars, p );
int RetValue = Vec_IntFind( q, 0 );
Vec_IntFree( q );
if ( RetValue == -1 )
return p;
Vec_WecFree( p );
}
assert( 0 );
return NULL;
}
Vec_Wec_t * Exa7_ChooseInputVars2( int nVars, int nLuts, int nLutSize, char * pPermStr )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i, Pos = 0;
assert( nLuts * nLutSize == (int)strlen(pPermStr) );
Vec_WecForEachLevel( p, vLevel, i ) {
for ( int k = 0; k < nLutSize; k++, Pos++ )
if ( pPermStr[Pos] != '_' )
Vec_IntPush( vLevel, pPermStr[Pos] == '*' ? -1 : (int)(pPermStr[Pos]-'a') );
}
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Wrd_t * Exa7_ManTruthTables( Exa7_Man_t * p )
{
Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
for ( i = 0; i < p->nVars; i++ )
Abc_TtIthVar( Exa7_ManTruth(p, i), i, p->nVars );
//Dau_DsdPrintFromTruth( Exa7_ManTruth(p, p->nObjs), p->nVars );
return vInfo;
}
static int Exa7_ManVarReserve( Exa7_Man_t * p )
{
int nMintMax = 1 << p->nVars;
int nVarsPerMint = p->pPars->fUseIncr ? p->nNodes : (p->nLutSize + 1) * p->nNodes;
int64_t nTotal = (int64_t)p->iVar + (int64_t)nVarsPerMint * nMintMax;
if ( nTotal > INT_MAX )
nTotal = INT_MAX;
return (int)nTotal;
}
static int Exa7_ManMarkup( Exa7_Man_t * p )
{
int i, k, j;
assert( p->nObjs <= MAJ_NOBJS );
// assign functionality variables
p->iVar = 1 + p->LutMask * p->nNodes;
// assign connectivity variables
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( p->pPars->fLutCascade )
{
if ( i > p->nVars )
{
Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][0][i-1] = p->iVar++;
}
for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ )
{
for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
}
}
continue;
}
for ( k = 0; k < p->nLutSize; k++ )
{
if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
}
}
}
if ( !p->pPars->fSilent ) printf( "The number of parameter variables = %d.\n", p->iVar );
if ( p->pPars->fLutCascade && (p->pPars->fLutInFixed || p->pPars->pPermStr) ) {
if ( p->pPars->pPermStr )
p->vInVars = Exa7_ChooseInputVars2( p->nVars, p->nNodes, p->nLutSize, p->pPars->pPermStr );
else
p->vInVars = Exa7_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize );
if ( !p->pPars->fSilent ) {
Vec_Int_t * vLevel; int i, Var;
printf( "Using fixed input assignment %s%s:\n",
p->pPars->pPermStr ? "provided by the user " : "generated randomly", p->pPars->pPermStr ? p->pPars->pPermStr : "" );
Vec_WecForEachLevelReverse( p->vInVars, vLevel, i ) {
printf( "%c : ", 'A'+p->nVars+i-p->nVars );
Vec_IntForEachEntry( vLevel, Var, k )
printf( "%c ", Var < 0 ? '*' : 'a'+Var );
printf( "\n" );
}
}
}
return p->iVar;
// printout
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
printf( " Node %2d\n", i );
for ( j = 0; j < p->nObjs; j++ )
{
printf( "Fanin %2d : ", j );
for ( k = 0; k < p->nLutSize; k++ )
printf( "%3d ", p->VarMarks[i][k][j] );
printf( "\n" );
}
}
return p->iVar;
}
static Exa7_Man_t * Exa7_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
{
Exa7_Man_t * p = ABC_CALLOC( Exa7_Man_t, 1 );
p->pPars = pPars;
p->nVars = pPars->nVars;
p->nNodes = pPars->nNodes;
p->nLutSize = pPars->nLutSize;
p->LutMask = (1 << pPars->nLutSize) - 1;
p->nObjs = pPars->nVars + pPars->nNodes;
p->nWords = Abc_TtWordNum(pPars->nVars);
p->pTruth = pTruth;
p->vOutLits = Vec_WecStart( p->nObjs );
p->iVar = Exa7_ManMarkup( p );
p->vInfo = Exa7_ManTruthTables( p );
if ( p->pPars->nLutSize == 2 )
p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
else if ( p->pPars->nLutSize == 3 )
p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
p->pSat = cadical_solver_new();
p->nVarAlloc = Exa7_ManVarReserve( p );
assert( p->nVarAlloc >= p->iVar );
cadical_solver_setnvars( p->pSat, p->nVarAlloc );
if ( pPars->RuntimeLim )
Exa7_CadicalSetRuntimeLimit( p->pSat, pPars->RuntimeLim );
return p;
}
static void Exa7_ManFree( Exa7_Man_t * p )
{
cadical_solver_delete( p->pSat );
Vec_WrdFree( p->vInfo );
Vec_BitFreeP( &p->vUsed2 );
Vec_BitFreeP( &p->vUsed3 );
Vec_WecFree( p->vOutLits );
Vec_WecFreeP( &p->vInVars );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Exa7_ManFindFanin( Exa7_Man_t * p, int i, int k )
{
int j, Count = 0, iVar = -1;
for ( j = 0; j < p->nObjs; j++ )
if ( p->VarMarks[i][k][j] && cadical_solver_get_var_value(p->pSat, p->VarMarks[i][k][j]) )
{
iVar = j;
Count++;
}
assert( Count == 1 );
return iVar;
}
static inline int Exa7_ManEval( Exa7_Man_t * p )
{
static int Flag = 0;
int i, k, j, iMint; word * pFanins[6];
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
pFanins[k] = Exa7_ManTruth( p, Exa7_ManFindFanin(p, i, k) );
Abc_TtConst0( Exa7_ManTruth(p, i), p->nWords );
for ( k = 1; k <= p->LutMask; k++ )
{
if ( !cadical_solver_get_var_value(p->pSat, iVarStart+k-1) )
continue;
// Abc_TtAndCompl( Exa7_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
Abc_TtConst1( Exa7_ManTruth(p, p->nObjs), p->nWords );
for ( j = 0; j < p->nLutSize; j++ )
Abc_TtAndCompl( Exa7_ManTruth(p, p->nObjs), Exa7_ManTruth(p, p->nObjs), 0, pFanins[j], !((k >> j) & 1), p->nWords );
Abc_TtOr( Exa7_ManTruth(p, i), Exa7_ManTruth(p, i), Exa7_ManTruth(p, p->nObjs), p->nWords );
}
}
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Exa7_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Exa7_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa7_ManPrintSolution( Exa7_Man_t * p, int fCompl )
{
int i, k, iVar;
printf( "Realization of given %d-input function using %d %d-input LUTs:\n", p->nVars, p->nNodes, p->nLutSize );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
printf( "%c = %d\'b", 'A'+i-p->nVars, 1 << p->nLutSize );
for ( k = p->LutMask - 1; k >= 0; k-- )
{
Val = cadical_solver_get_var_value(p->pSat, iVarStart+k);
if ( i == p->nObjs - 1 && fCompl )
printf( "%d", !Val );
else
printf( "%d", Val );
}
if ( i == p->nObjs - 1 && fCompl )
printf( "1(" );
else
printf( "0(" );
for ( k = p->nLutSize - 1; k >= 0; k-- )
{
iVar = Exa7_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %c", 'A'+iVar-p->nVars );
}
printf( " )\n" );
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa7_ManDumpBlif( Exa7_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr);
if ( strlen(pStr) > 16 ) {
pStr[16] = '_';
pStr[17] = '\0';
}
sprintf( pFileName, "%s.blif", pStr );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) return;
fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
fprintf( pFile, ".model %s\n", pStr );
fprintf( pFile, ".inputs" );
for ( k = 0; k < p->nVars; k++ )
fprintf( pFile, " %c", 'a'+k );
fprintf( pFile, "\n.outputs F\n" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
fprintf( pFile, ".names" );
for ( k = 0; k < p->nLutSize; k++ )
{
iVar = Exa7_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
fprintf( pFile, " %c", 'a'+iVar );
else
fprintf( pFile, " %02d", iVar );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " F\n" );
else
fprintf( pFile, " %02d\n", i );
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
int Val = cadical_solver_get_var_value(p->pSat, iVarStart+k);
if ( Val == 0 )
continue;
for ( b = 0; b < p->nLutSize; b++ )
fprintf( pFile, "%d", ((k+1) >> b) & 1 );
fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
}
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent ) printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
ABC_FREE( pStr );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Exa7_ManAddCnfStart( Exa7_Man_t * p, int fOnlyAnd )
{
int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
// input constraints
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
{
int nLits = 0;
for ( j = 0; j < p->nObjs; j++ )
if ( p->VarMarks[i][k][j] )
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
assert( nLits > 0 );
// input uniqueness
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + nLits ) )
return 0;
for ( n = 0; n < nLits; n++ )
for ( m = n+1; m < nLits; m++ )
{
pLits2[0] = Abc_LitNot(pLits[n]);
pLits2[1] = Abc_LitNot(pLits[m]);
if ( !cadical_solver_addclause( p->pSat, pLits2, pLits2 + 2 ) )
return 0;
}
if ( k == p->nLutSize - 1 )
break;
// symmetry breaking
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
if ( !cadical_solver_addclause( p->pSat, pLits2, pLits2 + 2 ) )
return 0;
}
}
//#ifdef USE_NODE_ORDER
// node ordering
if ( p->pPars->fOrderNodes )
{
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !cadical_solver_addclause( p->pSat, pLits2, pLits2 + 2 ) )
return 0;
}
}
//#endif
if ( p->nLutSize != 2 )
continue;
// two-input functions
for ( k = 0; k < 3; k++ )
{
pLits[0] = Abc_Var2Lit( iVarStart, k==1 );
pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + 3 ) )
return 0;
}
if ( fOnlyAnd )
{
pLits[0] = Abc_Var2Lit( iVarStart, 1 );
pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + 3 ) )
return 0;
}
}
// outputs should be used
for ( i = 0; i < p->nObjs - 1; i++ )
{
Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
int * pArray = Vec_IntArray( vArray );
int nArrayLits = Vec_IntSize( vArray );
assert( nArrayLits > 0 );
if ( !cadical_solver_addclause( p->pSat, pArray, pArray + nArrayLits ) )
return 0;
}
if ( p->vInVars ) {
Vec_Int_t * vLevel; int Var;
//Vec_WecPrint( p->vInVars, 0 );
Vec_WecForEachLevel( p->vInVars, vLevel, i )
{
assert( Vec_IntSize(vLevel) > 0 );
Vec_IntForEachEntry( vLevel, Var, k ) {
if ( Var < 0 ) continue;
if ( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var] == 0 ) {
printf( "Skipping variable %d in place %d because it cannot be constrained.\n", Var, k );
continue;
}
pLits[0] = Abc_Var2Lit( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var], 0 ); assert(pLits[0]);
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + 1 ) )
return 0;
}
}
}
return 1;
}
static int Exa7_ManAddCnf( Exa7_Man_t * p, int iMint )
{
// save minterm values
int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
for ( i = 0; i < p->nVars; i++ )
p->VarVals[i] = (iMint >> i) & 1;
// sat_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
cadical_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
//printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
for ( i = p->nVars; i < p->nObjs; i++ )
{
// fanin connectivity
int iVarStart = 1 + p->LutMask*(i - p->nVars);
int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
{
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
{
int iBaseSatVarJ = p->iVar + (p->nLutSize+1)*(j - p->nVars);
for ( n = 0; n < 2; n++ )
{
int pLits[3], nLits = 0;
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
if ( j >= p->nVars )
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + p->nLutSize, !n );
else if ( p->VarVals[j] == n )
continue;
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + nLits ) )
return 0;
}
}
}
// node functionality
for ( n = 0; n < 2; n++ )
{
if ( i == p->nObjs - 1 && n == Value )
continue;
for ( k = 0; k <= p->LutMask; k++ )
{
int pLits[16], nLits = 0;
if ( k == 0 && n == 1 )
continue;
//pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) );
//pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
//if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
for ( j = 0; j < p->nLutSize; j++ )
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, (k >> j) & 1 );
if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, !n );
if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
assert( nLits <= p->nLutSize+2 );
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + nLits ) )
return 0;
}
}
}
p->iVar += (p->nLutSize+1)*p->nNodes;
assert( p->iVar <= p->nVarAlloc );
return 1;
}
static int Exa7_ManAddCnf2( Exa7_Man_t * p, int iMint )
{
int iBaseSatVar = p->iVar + p->nNodes*iMint;
assert( iBaseSatVar + p->nNodes <= p->nVarAlloc );
// save minterm values
int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
for ( i = 0; i < p->nVars; i++ )
p->VarVals[i] = (iMint >> i) & 1;
//printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
for ( i = p->nVars; i < p->nObjs; i++ )
{
// int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
int iVarStart = 1 + p->LutMask*(i - p->nVars);
// collect fanin variables
int pFanins[16];
for ( j = 0; j < p->nLutSize; j++ )
pFanins[j] = Exa7_ManFindFanin(p, i, j);
// check cache
if ( p->pPars->nLutSize == 2 && Exa7_ManIsUsed2(p, iMint, i, pFanins[1], pFanins[0]) )
continue;
if ( p->pPars->nLutSize == 3 && Exa7_ManIsUsed3(p, iMint, i, pFanins[2], pFanins[1], pFanins[0]) )
continue;
// node functionality
for ( n = 0; n < 2; n++ )
{
if ( i == p->nObjs - 1 && n == Value )
continue;
for ( k = 0; k <= p->LutMask; k++ )
{
int pLits[16], nLits = 0;
if ( k == 0 && n == 1 )
continue;
for ( j = 0; j < p->nLutSize; j++ )
{
// pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, (k >> j) & 1 );
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][j][pFanins[j]], 1 );
if ( pFanins[j] >= p->nVars )
pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + pFanins[j] - p->nVars, (k >> j) & 1 );
else if ( p->VarVals[pFanins[j]] != ((k >> j) & 1) )
break;
}
if ( j < p->nLutSize )
continue;
// if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + j, !n );
if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVar + i - p->nVars, !n );
if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
assert( nLits <= 2*p->nLutSize+2 );
if ( !cadical_solver_addclause( p->pSat, pLits, pLits + nLits ) )
return 0;
}
}
}
return 1;
}
void Exa7_ManPrint( Exa7_Man_t * p, int i, int iMint, abctime clk )
{
printf( "Iter%6d : ", i );
Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
printf( " Var =%5d ", cadical_solver_nvars(p->pSat) );
printf( "Cla =%6d ", cadical_solver_nclauses(p->pSat) );
printf( "Conf =%9d ", cadical_solver_nconflicts(p->pSat) );
Abc_PrintTime( 1, "Time", clk );
}
int Exa7_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
int i, status, Res = 0, iMint = 1;
abctime clkTotal = Abc_Clock();
Exa7_Man_t * p; int fCompl = 0;
word pTruth[64];
if ( pPars->pSymStr ) {
word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
ABC_FREE( pFun );
}
if ( pPars->pTtStr )
Abc_TtReadHex( pTruth, pPars->pTtStr );
else assert( 0 );
assert( pPars->nVars <= 12 );
assert( pPars->nLutSize <= 6 );
p = Exa7_ManAlloc( pPars, pTruth );
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
status = Exa7_ManAddCnfStart( p, pPars->fOnlyAnd );
assert( status );
if ( !pPars->fSilent ) printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
if ( pPars->fUseIncr )
{
status = cadical_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
assert( status == CADICAL_SAT );
}
for ( i = 0; iMint != -1; i++ )
{
if ( pPars->fUseIncr ? !Exa7_ManAddCnf2( p, iMint ) : !Exa7_ManAddCnf( p, iMint ) )
break;
status = cadical_solver_solve( p->pSat, NULL, NULL, 0, 0, 0, 0 );
if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
Exa7_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( status == CADICAL_UNSAT || status == CADICAL_UNDEC )
break;
iMint = Exa7_ManEval( p );
}
if ( pPars->fVerbose && status != CADICAL_UNDEC )
Exa7_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa7_ManPrintSolution( p, fCompl ), Res = 1;
else if ( status == CADICAL_UNDEC )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
else if ( !p->pPars->fSilent )
printf( "The problem has no solution.\n" ), Res = 2;
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 )
Exa7_ManDumpBlif( p, fCompl );
if ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa7_ManFree( p );
return Res;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

847
src/sat/bmc/bmcMaj8.c Normal file
View File

@ -0,0 +1,847 @@
/**CFile****************************************************************
FileName [bmcMaj.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis [Exact synthesis with majority gates.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - October 1, 2017.]
Revision [$Id: bmcMaj.c,v 1.00 2017/10/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/kissat/kissat.h"
#include "aig/miniaig/miniaig.h"
#include "base/io/ioResub.h"
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#define KISSAT_UNSAT 20
#define KISSAT_SAT 10
#define KISSAT_UNDEC 0
ABC_NAMESPACE_IMPL_START
#ifdef WIN32
#include <process.h>
#define unlink _unlink
#else
#include <unistd.h>
#endif
#include <limits.h>
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
#define MAJ_NOBJS 64 // Const0 + Const1 + nVars + nNodes
typedef struct Exa8_Man_t_ Exa8_Man_t;
struct Exa8_Man_t_
{
Bmc_EsPar_t * pPars; // parameters
int nVars; // inputs
int nNodes; // internal nodes
int nLutSize; // lut size
int LutMask; // lut mask
int nObjs; // total objects (nVars inputs + nNodes internal nodes)
int nWords; // the truth table size in 64-bit words
int iVar; // the next available SAT variable
word * pTruth; // truth table
Vec_Wrd_t * vInfo; // nVars + nNodes + 1
Vec_Bit_t * vUsed2; // bit masks
Vec_Bit_t * vUsed3; // bit masks
int VarMarks[MAJ_NOBJS][6][MAJ_NOBJS]; // variable marks
int VarVals[MAJ_NOBJS]; // values of the first nVars variables
Vec_Wec_t * vOutLits; // output vars
Vec_Wec_t * vInVars; // input vars
kissat * pSat; // SAT solver
int nVarAlloc; // total vars reserved in the solver
abctime timeStop; // runtime limit (0 = unlimited)
int nUsed[2];
};
static inline int Exa8_LitToKissat( int Lit )
{
return Abc_LitIsCompl( Lit ) ? -(Abc_Lit2Var( Lit ) + 1) : (Abc_Lit2Var( Lit ) + 1);
}
static inline int Exa8_KissatAddClause( Exa8_Man_t * p, int * pLits, int nLits )
{
int i;
for ( i = 0; i < nLits; i++ )
kissat_add( p->pSat, Exa8_LitToKissat( pLits[i] ) );
kissat_add( p->pSat, 0 );
return !kissat_is_inconsistent( p->pSat );
}
static inline int Exa8_KissatVarValue( Exa8_Man_t * p, int v )
{
return kissat_value( p->pSat, v + 1 ) > 0;
}
static int Exa8_KissatTerminate( void * pData )
{
Exa8_Man_t * p = (Exa8_Man_t *)pData;
return p && p->timeStop && Abc_Clock() > p->timeStop;
}
static inline word * Exa8_ManTruth( Exa8_Man_t * p, int v ) { return Vec_WrdEntryP( p->vInfo, p->nWords * v ); }
static inline int Exa8_ManIsUsed2( Exa8_Man_t * p, int m, int n, int i, int j )
{
int Pos = ((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j;
p->nUsed[0]++;
assert( i < n && j < n && i < j );
if ( Vec_BitEntry(p->vUsed2, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed2, Pos, 1 );
return 0;
}
static inline int Exa8_ManIsUsed3( Exa8_Man_t * p, int m, int n, int i, int j, int k )
{
int Pos = (((m * p->pPars->nNodes + n - p->pPars->nVars) * p->nObjs + i) * p->nObjs + j) * p->nObjs + k;
p->nUsed[0]++;
assert( i < n && j < n && k < n && i < j && j < k );
if ( Vec_BitEntry(p->vUsed3, Pos) )
return 1;
p->nUsed[1]++;
Vec_BitWriteEntry( p->vUsed3, Pos, 1 );
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Exa8_ChooseInputVars_int( int nVars, int nLuts, int nLutSize )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i;
Vec_WecForEachLevel( p, vLevel, i ) {
do {
int iVar = (Abc_Random(0) ^ Abc_Random(0) ^ Abc_Random(0)) % nVars;
Vec_IntPushUniqueOrder( vLevel, iVar );
}
while ( Vec_IntSize(vLevel) < nLutSize-(int)(i>0) );
}
return p;
}
Vec_Int_t * Exa8_CountInputVars( int nVars, Vec_Wec_t * p )
{
Vec_Int_t * vLevel; int i, k, Obj;
Vec_Int_t * vCounts = Vec_IntStart( nVars );
Vec_WecForEachLevel( p, vLevel, i )
Vec_IntForEachEntry( vLevel, Obj, k )
Vec_IntAddToEntry( vCounts, Obj, 1 );
return vCounts;
}
Vec_Wec_t * Exa8_ChooseInputVars( int nVars, int nLuts, int nLutSize )
{
for ( int i = 0; i < 1000; i++ ) {
Vec_Wec_t * p = Exa8_ChooseInputVars_int( nVars, nLuts, nLutSize );
Vec_Int_t * q = Exa8_CountInputVars( nVars, p );
int RetValue = Vec_IntFind( q, 0 );
Vec_IntFree( q );
if ( RetValue == -1 )
return p;
Vec_WecFree( p );
}
assert( 0 );
return NULL;
}
Vec_Wec_t * Exa8_ChooseInputVars2( int nVars, int nLuts, int nLutSize, char * pPermStr )
{
Vec_Wec_t * p = Vec_WecStart( nLuts );
Vec_Int_t * vLevel; int i, Pos = 0;
assert( nLuts * nLutSize == (int)strlen(pPermStr) );
Vec_WecForEachLevel( p, vLevel, i ) {
for ( int k = 0; k < nLutSize; k++, Pos++ )
if ( pPermStr[Pos] != '_' )
Vec_IntPush( vLevel, pPermStr[Pos] == '*' ? -1 : (int)(pPermStr[Pos]-'a') );
}
return p;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static Vec_Wrd_t * Exa8_ManTruthTables( Exa8_Man_t * p )
{
Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs+1) ); int i;
for ( i = 0; i < p->nVars; i++ )
Abc_TtIthVar( Exa8_ManTruth(p, i), i, p->nVars );
//Dau_DsdPrintFromTruth( Exa8_ManTruth(p, p->nObjs), p->nVars );
return vInfo;
}
static int Exa8_ManVarReserve( Exa8_Man_t * p )
{
int nMintMax = 1 << p->nVars;
int nVarsPerMint = p->pPars->fUseIncr ? p->nNodes : (p->nLutSize + 1) * p->nNodes;
int64_t nTotal = (int64_t)p->iVar + (int64_t)nVarsPerMint * nMintMax;
if ( nTotal > INT_MAX )
nTotal = INT_MAX;
return (int)nTotal;
}
static int Exa8_ManMarkup( Exa8_Man_t * p )
{
int i, k, j;
assert( p->nObjs <= MAJ_NOBJS );
// assign functionality variables
p->iVar = 1 + p->LutMask * p->nNodes;
// assign connectivity variables
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( p->pPars->fLutCascade )
{
if ( i > p->nVars )
{
Vec_WecPush( p->vOutLits, i-1, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][0][i-1] = p->iVar++;
}
for ( k = (int)(i > p->nVars); k < p->nLutSize; k++ )
{
for ( j = 0; j < p->nVars - k + (int)(i > p->nVars); j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
}
}
continue;
}
for ( k = 0; k < p->nLutSize; k++ )
{
if ( p->pPars->fFewerVars && i == p->nObjs - 1 && k == 0 )
{
j = p->nObjs - 2;
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
continue;
}
for ( j = p->pPars->fFewerVars ? p->nLutSize - 1 - k : 0; j < i - k; j++ )
{
Vec_WecPush( p->vOutLits, j, Abc_Var2Lit(p->iVar, 0) );
p->VarMarks[i][k][j] = p->iVar++;
}
}
}
if ( !p->pPars->fSilent ) printf( "The number of parameter variables = %d.\n", p->iVar );
if ( p->pPars->fLutCascade && (p->pPars->fLutInFixed || p->pPars->pPermStr) ) {
if ( p->pPars->pPermStr )
p->vInVars = Exa8_ChooseInputVars2( p->nVars, p->nNodes, p->nLutSize, p->pPars->pPermStr );
else
p->vInVars = Exa8_ChooseInputVars( p->nVars, p->nNodes, p->nLutSize );
if ( !p->pPars->fSilent ) {
Vec_Int_t * vLevel; int i, Var;
printf( "Using fixed input assignment %s%s:\n",
p->pPars->pPermStr ? "provided by the user " : "generated randomly", p->pPars->pPermStr ? p->pPars->pPermStr : "" );
Vec_WecForEachLevelReverse( p->vInVars, vLevel, i ) {
printf( "%c : ", 'A'+p->nVars+i-p->nVars );
Vec_IntForEachEntry( vLevel, Var, k )
printf( "%c ", Var < 0 ? '*' : 'a'+Var );
printf( "\n" );
}
}
}
return p->iVar;
// printout
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
printf( " Node %2d\n", i );
for ( j = 0; j < p->nObjs; j++ )
{
printf( "Fanin %2d : ", j );
for ( k = 0; k < p->nLutSize; k++ )
printf( "%3d ", p->VarMarks[i][k][j] );
printf( "\n" );
}
}
return p->iVar;
}
static Exa8_Man_t * Exa8_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
{
Exa8_Man_t * p = ABC_CALLOC( Exa8_Man_t, 1 );
p->pPars = pPars;
p->nVars = pPars->nVars;
p->nNodes = pPars->nNodes;
p->nLutSize = pPars->nLutSize;
p->LutMask = (1 << pPars->nLutSize) - 1;
p->nObjs = pPars->nVars + pPars->nNodes;
p->nWords = Abc_TtWordNum(pPars->nVars);
p->pTruth = pTruth;
p->vOutLits = Vec_WecStart( p->nObjs );
p->iVar = Exa8_ManMarkup( p );
p->vInfo = Exa8_ManTruthTables( p );
if ( p->pPars->nLutSize == 2 )
p->vUsed2 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
else if ( p->pPars->nLutSize == 3 )
p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
p->pSat = kissat_init();
p->nVarAlloc = Exa8_ManVarReserve( p );
assert( p->nVarAlloc >= p->iVar );
kissat_reserve( p->pSat, p->nVarAlloc );
p->timeStop = 0;
return p;
}
static void Exa8_ManFree( Exa8_Man_t * p )
{
kissat_release( p->pSat );
Vec_WrdFree( p->vInfo );
Vec_BitFreeP( &p->vUsed2 );
Vec_BitFreeP( &p->vUsed3 );
Vec_WecFree( p->vOutLits );
Vec_WecFreeP( &p->vInVars );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Exa8_ManFindFanin( Exa8_Man_t * p, int i, int k )
{
int j, Count = 0, iVar = -1;
for ( j = 0; j < p->nObjs; j++ )
if ( p->VarMarks[i][k][j] && Exa8_KissatVarValue(p, p->VarMarks[i][k][j]) )
{
iVar = j;
Count++;
}
assert( Count == 1 );
return iVar;
}
static inline int Exa8_ManEval( Exa8_Man_t * p )
{
static int Flag = 0;
int i, k, j, iMint; word * pFanins[6];
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
pFanins[k] = Exa8_ManTruth( p, Exa8_ManFindFanin(p, i, k) );
Abc_TtConst0( Exa8_ManTruth(p, i), p->nWords );
for ( k = 1; k <= p->LutMask; k++ )
{
if ( !Exa8_KissatVarValue(p, iVarStart+k-1) )
continue;
// Abc_TtAndCompl( Exa8_ManTruth(p, p->nObjs), pFanins[0], !(k&1), pFanins[1], !(k>>1), p->nWords );
Abc_TtConst1( Exa8_ManTruth(p, p->nObjs), p->nWords );
for ( j = 0; j < p->nLutSize; j++ )
Abc_TtAndCompl( Exa8_ManTruth(p, p->nObjs), Exa8_ManTruth(p, p->nObjs), 0, pFanins[j], !((k >> j) & 1), p->nWords );
Abc_TtOr( Exa8_ManTruth(p, i), Exa8_ManTruth(p, i), Exa8_ManTruth(p, p->nObjs), p->nWords );
}
}
if ( Flag && p->nVars >= 6 )
iMint = Abc_TtFindLastDiffBit( Exa8_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
else
iMint = Abc_TtFindFirstDiffBit( Exa8_ManTruth(p, p->nObjs-1), p->pTruth, p->nVars );
if ( iMint == -1 )
return -1;
//Flag ^= 1;
assert( iMint < (1 << p->nVars) );
return iMint;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa8_ManPrintSolution( Exa8_Man_t * p, int fCompl )
{
int i, k, iVar;
printf( "Realization of given %d-input function using %d %d-input LUTs:\n", p->nVars, p->nNodes, p->nLutSize );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
int Val, iVarStart = 1 + p->LutMask*(i - p->nVars);
printf( "%c = %d\'b", 'A'+i-p->nVars, 1 << p->nLutSize );
for ( k = p->LutMask - 1; k >= 0; k-- )
{
Val = Exa8_KissatVarValue(p, iVarStart+k);
if ( i == p->nObjs - 1 && fCompl )
printf( "%d", !Val );
else
printf( "%d", Val );
}
if ( i == p->nObjs - 1 && fCompl )
printf( "1(" );
else
printf( "0(" );
for ( k = p->nLutSize - 1; k >= 0; k-- )
{
iVar = Exa8_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( " %c", 'a'+iVar );
else
printf( " %c", 'A'+iVar-p->nVars );
}
printf( " )\n" );
}
}
static void Exa8_ManPrintPerm( Exa8_Man_t * p )
{
int i, k, iVar;
for ( i = p->nVars; i < p->nObjs; i++ )
{
if ( i > p->nVars )
printf( "_" );
for ( k = p->nLutSize - 1; k >= 0; k-- )
{
iVar = Exa8_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
printf( "%c", 'a'+iVar );
}
}
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static void Exa8_ManDumpBlif( Exa8_Man_t * p, int fCompl )
{
int i, k, b, iVar;
char pFileName[1000];
char * pStr = Abc_UtilStrsav(p->pPars->pSymStr ? p->pPars->pSymStr : p->pPars->pTtStr);
if ( strlen(pStr) > 16 ) {
pStr[16] = '_';
pStr[17] = '\0';
}
sprintf( pFileName, "%s.blif", pStr );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) return;
fprintf( pFile, "# Realization of given %d-input function using %d %d-input LUTs synthesized by ABC on %s\n", p->nVars, p->nNodes, p->nLutSize, Extra_TimeStamp() );
fprintf( pFile, ".model %s\n", pStr );
fprintf( pFile, ".inputs" );
for ( k = 0; k < p->nVars; k++ )
fprintf( pFile, " %c", 'a'+k );
fprintf( pFile, "\n.outputs F\n" );
for ( i = p->nObjs - 1; i >= p->nVars; i-- )
{
fprintf( pFile, ".names" );
for ( k = 0; k < p->nLutSize; k++ )
{
iVar = Exa8_ManFindFanin( p, i, k );
if ( iVar >= 0 && iVar < p->nVars )
fprintf( pFile, " %c", 'a'+iVar );
else
fprintf( pFile, " %02d", iVar );
}
if ( i == p->nObjs - 1 )
fprintf( pFile, " F\n" );
else
fprintf( pFile, " %02d\n", i );
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
int Val = Exa8_KissatVarValue(p, iVarStart+k);
if ( Val == 0 )
continue;
for ( b = 0; b < p->nLutSize; b++ )
fprintf( pFile, "%d", ((k+1) >> b) & 1 );
fprintf( pFile, " %d\n", i != p->nObjs - 1 || !fCompl );
}
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
if ( !p->pPars->fSilent ) printf( "Finished dumping the resulting LUT network into file \"%s\".\n", pFileName );
ABC_FREE( pStr );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static int Exa8_ManAddCnfStart( Exa8_Man_t * p, int fOnlyAnd )
{
int pLits[MAJ_NOBJS], pLits2[2], i, j, k, n, m;
// input constraints
for ( i = p->nVars; i < p->nObjs; i++ )
{
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
{
int nLits = 0;
for ( j = 0; j < p->nObjs; j++ )
if ( p->VarMarks[i][k][j] )
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 0 );
assert( nLits > 0 );
// input uniqueness
if ( !Exa8_KissatAddClause( p, pLits, nLits ) )
return 0;
for ( n = 0; n < nLits; n++ )
for ( m = n+1; m < nLits; m++ )
{
pLits2[0] = Abc_LitNot(pLits[n]);
pLits2[1] = Abc_LitNot(pLits[m]);
if ( !Exa8_KissatAddClause( p, pLits2, 2 ) )
return 0;
}
if ( k == p->nLutSize - 1 )
break;
// symmetry breaking
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
for ( n = j; n < p->nObjs; n++ ) if ( p->VarMarks[i][k+1][n] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[i][k+1][n], 1 );
if ( !Exa8_KissatAddClause( p, pLits2, 2 ) )
return 0;
}
}
//#ifdef USE_NODE_ORDER
// node ordering
if ( p->pPars->fOrderNodes )
{
for ( j = p->nVars; j < i; j++ )
for ( n = 0; n < p->nObjs; n++ ) if ( p->VarMarks[i][0][n] )
for ( m = n+1; m < p->nObjs; m++ ) if ( p->VarMarks[j][0][m] )
{
pLits2[0] = Abc_Var2Lit( p->VarMarks[i][0][n], 1 );
pLits2[1] = Abc_Var2Lit( p->VarMarks[j][0][m], 1 );
if ( !Exa8_KissatAddClause( p, pLits2, 2 ) )
return 0;
}
}
//#endif
if ( p->nLutSize != 2 )
continue;
// two-input functions
for ( k = 0; k < 3; k++ )
{
pLits[0] = Abc_Var2Lit( iVarStart, k==1 );
pLits[1] = Abc_Var2Lit( iVarStart+1, k==2 );
pLits[2] = Abc_Var2Lit( iVarStart+2, k!=0 );
if ( !Exa8_KissatAddClause( p, pLits, 3 ) )
return 0;
}
if ( fOnlyAnd )
{
pLits[0] = Abc_Var2Lit( iVarStart, 1 );
pLits[1] = Abc_Var2Lit( iVarStart+1, 1 );
pLits[2] = Abc_Var2Lit( iVarStart+2, 0 );
if ( !Exa8_KissatAddClause( p, pLits, 3 ) )
return 0;
}
}
// outputs should be used
for ( i = 0; i < p->nObjs - 1; i++ )
{
Vec_Int_t * vArray = Vec_WecEntry(p->vOutLits, i);
int * pArray = Vec_IntArray( vArray );
int nArrayLits = Vec_IntSize( vArray );
assert( nArrayLits > 0 );
if ( !Exa8_KissatAddClause( p, pArray, nArrayLits ) )
return 0;
}
if ( p->vInVars ) {
Vec_Int_t * vLevel; int Var;
//Vec_WecPrint( p->vInVars, 0 );
Vec_WecForEachLevel( p->vInVars, vLevel, i )
{
assert( Vec_IntSize(vLevel) > 0 );
Vec_IntForEachEntry( vLevel, Var, k ) {
if ( Var < 0 ) continue;
if ( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var] == 0 ) {
printf( "Skipping variable %d in place %d because it cannot be constrained.\n", Var, k );
continue;
}
pLits[0] = Abc_Var2Lit( p->VarMarks[p->nVars+i][p->nLutSize-1-k][Var], 0 ); assert(pLits[0]);
if ( !Exa8_KissatAddClause( p, pLits, 1 ) )
return 0;
}
}
}
return 1;
}
static int Exa8_ManAddCnf( Exa8_Man_t * p, int iMint )
{
// save minterm values
int i, k, n, j, Value = Abc_TtGetBit(p->pTruth, iMint);
for ( i = 0; i < p->nVars; i++ )
p->VarVals[i] = (iMint >> i) & 1;
//printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
for ( i = p->nVars; i < p->nObjs; i++ )
{
// fanin connectivity
int iVarStart = 1 + p->LutMask*(i - p->nVars);
int iBaseSatVarI = p->iVar + (p->nLutSize+1)*(i - p->nVars);
for ( k = 0; k < p->nLutSize; k++ )
{
for ( j = 0; j < p->nObjs; j++ ) if ( p->VarMarks[i][k][j] )
{
int iBaseSatVarJ = p->iVar + (p->nLutSize+1)*(j - p->nVars);
for ( n = 0; n < 2; n++ )
{
int pLits[3], nLits = 0;
pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k][j], 1 );
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + k, n );
if ( j >= p->nVars )
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarJ + p->nLutSize, !n );
else if ( p->VarVals[j] == n )
continue;
if ( !Exa8_KissatAddClause( p, pLits, nLits ) )
return 0;
}
}
}
// node functionality
for ( n = 0; n < 2; n++ )
{
if ( i == p->nObjs - 1 && n == Value )
continue;
for ( k = 0; k <= p->LutMask; k++ )
{
int pLits[16], nLits = 0;
if ( k == 0 && n == 1 )
continue;
//pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 0, (k&1) );
//pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 1, (k>>1) );
//if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + 2, !n );
for ( j = 0; j < p->nLutSize; j++ )
pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, (k >> j) & 1 );
if ( i != p->nObjs - 1 ) pLits[nLits++] = Abc_Var2Lit( iBaseSatVarI + j, !n );
if ( k > 0 ) pLits[nLits++] = Abc_Var2Lit( iVarStart + k-1, n );
assert( nLits <= p->nLutSize+2 );
if ( !Exa8_KissatAddClause( p, pLits, nLits ) )
return 0;
}
}
}
p->iVar += (p->nLutSize+1)*p->nNodes;
assert( p->iVar <= p->nVarAlloc );
return 1;
}
int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
{
extern int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
if ( pPars->fMinNodes )
return Exa8_ManExactSynthesisIter( pPars );
int status = KISSAT_UNDEC;
int Res = 0;
abctime clkTotal = Abc_Clock();
Exa8_Man_t * p;
int fCompl = 0;
word pTruth[64];
if ( pPars->pSymStr ) {
word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
ABC_FREE( pFun );
}
if ( pPars->pTtStr )
Abc_TtReadHex( pTruth, pPars->pTtStr );
else assert( 0 );
assert( pPars->nVars <= 12 );
assert( pPars->nLutSize <= 6 );
if ( pPars->fUseIncr && !pPars->fSilent )
printf( "Warning: Ignoring incremental option when using Kissat.\n" );
pPars->fUseIncr = 0;
p = Exa8_ManAlloc( pPars, pTruth );
if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, p->nWords ); }
if ( !pPars->fSilent )
printf( "Running exact synthesis for %d-input function with %d %d-input LUTs...\n", p->nVars, p->nNodes, p->nLutSize );
if ( Exa8_ManAddCnfStart( p, pPars->fOnlyAnd ) )
{
int nMints = 1 << p->nVars;
int iMint;
status = KISSAT_UNSAT;
for ( iMint = 0; iMint < nMints; iMint++ )
{
if ( !Exa8_ManAddCnf( p, iMint ) )
break;
}
if ( iMint == nMints )
{
if ( pPars->RuntimeLim )
{
p->timeStop = Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC;
kissat_set_terminate( p->pSat, p, Exa8_KissatTerminate );
}
else
{
p->timeStop = 0;
kissat_set_terminate( p->pSat, NULL, NULL );
}
status = kissat_solve( p->pSat );
}
}
else
status = KISSAT_UNSAT;
if ( status == KISSAT_SAT )
{
int DiffMint = Exa8_ManEval( p );
if ( DiffMint != -1 )
printf( "Warning: Verification detected a mismatch at minterm %d.\n", DiffMint );
Exa8_ManPrintSolution( p, fCompl );
printf( "The variable permutation is \"" );
Exa8_ManPrintPerm(p);
printf( "\".\n" );
if ( pPars->fDumpBlif )
Exa8_ManDumpBlif( p, fCompl );
Res = 1;
}
else if ( status == KISSAT_UNSAT )
{
if ( !p->pPars->fSilent )
printf( "The problem has no solution.\n" );
Res = 2;
}
else
{
Res = 0;
if ( pPars->RuntimeLim )
printf( "The solver timed out after %d sec.\n", pPars->RuntimeLim );
}
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 ( pPars->pSymStr )
ABC_FREE( pPars->pTtStr );
Exa8_ManFree( p );
return Res;
}
int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
{
pPars->fMinNodes = 0;
int nNodeMin = (pPars->nVars-2)/(pPars->nLutSize-1) + 1;
int nNodeMax = pPars->nNodes, Result = 0;
int fGenPerm = pPars->pPermStr == NULL;
for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
printf( "\nTrying M = %d:\n", n );
pPars->nNodes = n;
if ( fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
int nDupVars = Abc_MaxInt(0, (pPars->nLutSize-1) - (pPars->nVars-pPars->nLutSize));
Vec_StrPush( vStr, '_' );
for ( int v = 0; v < nDupVars; v++ )
Vec_StrPush( vStr, 'a'+v );
for ( int v = 0; v < pPars->nLutSize-1-nDupVars; v++ )
Vec_StrPush( vStr, '*' );
for ( int m = 2; m < pPars->nNodes; m++ ) {
Vec_StrPush( vStr, '_' );
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, '*' );
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
if ( 0 && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
for ( int m = 1; m < pPars->nNodes; m++ ) {
Vec_StrPush( vStr, '_' );
if ( m & 1 )
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, 'a'+(pPars->nVars-(pPars->nLutSize-1-v)) );
else
for ( int v = 0; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, 'a'+v );
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
if ( 0 && fGenPerm ) {
Vec_Str_t * vStr = Vec_StrAlloc( 100 );
for ( int v = 0; v < pPars->nLutSize; v++ )
Vec_StrPush( vStr, 'a'+v );
for ( int m = 1; m < pPars->nNodes; m++ ) {
Vec_StrPush( vStr, '_' );
if ( m & 1 ) {
Vec_StrPush( vStr, '*' );
Vec_StrPush( vStr, '*' );
for ( int v = 2; v < pPars->nLutSize-1; v++ )
Vec_StrPush( vStr, 'a'+(pPars->nVars-(pPars->nLutSize-1-v)) );
}
else {
for ( int v = 0; v < pPars->nLutSize-3; v++ )
Vec_StrPush( vStr, 'a'+v );
Vec_StrPush( vStr, '*' );
Vec_StrPush( vStr, '*' );
}
}
Vec_StrPush( vStr, '\0' );
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = Vec_StrReleaseArray(vStr);
Vec_StrFree( vStr );
}
Result = Exa8_ManExactSynthesis(pPars);
fflush( stdout );
if ( Result == 1 )
break;
}
return Result;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

2
src/sat/bmc/module.make
View File

@ -25,6 +25,8 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcMaj.c \
src/sat/bmc/bmcMaj2.c \
src/sat/bmc/bmcMaj3.c \
src/sat/bmc/bmcMaj7.c \
src/sat/bmc/bmcMaj8.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMesh.c \
src/sat/bmc/bmcMesh2.c \

4
src/sat/cadical/cadical.hpp
View File

@ -982,6 +982,10 @@ public:
//
static void build (FILE *file, const char *prefix = "c ");
// Extra APIs
int clauses ();
int conflicts ();
private:
//==== start of state ====================================================

39
src/sat/cadical/cadicalSolver.c
View File

@ -239,10 +239,15 @@ int cadical_solver_addvar(cadical_solver* s) {
***********************************************************************/
void cadical_solver_setnvars(cadical_solver* s,int n) {
s->nVars = n;
if(ccadical_vars((CCaDiCaL*)s->p) == 0) {
if ( n <= s->nVars )
return;
if ( s->nVars == 0 )
ccadical_reserve((CCaDiCaL*)s->p, n);
else {
assert( 0 );
ccadical_reserve_difference((CCaDiCaL*)s->p, n - s->nVars);
}
s->nVars = n;
}
/**Function*************************************************************
@ -261,6 +266,36 @@ int cadical_solver_get_var_value(cadical_solver* s, int v) {
return ccadical_val((CCaDiCaL*)s->p, v + 1) > 0;
}
/**Function*************************************************************
Synopsis [get number of clauses]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int cadical_solver_nclauses(cadical_solver* s) {
return ccadical_clauses((CCaDiCaL*)s->p);
}
/**Function*************************************************************
Synopsis [get number of conflicts]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int cadical_solver_nconflicts(cadical_solver* s) {
return ccadical_conflicts((CCaDiCaL*)s->p);
}
/**Function*************************************************************

2
src/sat/cadical/cadicalSolver.h
View File

@ -65,6 +65,8 @@ extern int cadical_solver_nvars(cadical_solver* s);
extern int cadical_solver_addvar(cadical_solver* s);
extern void cadical_solver_setnvars(cadical_solver* s,int n);
extern int cadical_solver_get_var_value(cadical_solver* s, int v);
extern int cadical_solver_nclauses(cadical_solver* s);
extern int cadical_solver_nconflicts(cadical_solver* s);
extern Vec_Int_t * cadical_solve_cnf( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose );
ABC_NAMESPACE_HEADER_END

8
src/sat/cadical/cadical_ccadical.cpp
View File

@ -208,4 +208,12 @@ int ccadical_is_inconsistent(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->inconsistent ();
}
int ccadical_clauses(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->clauses ();
}
int ccadical_conflicts(CCaDiCaL *ptr) {
return ((Wrapper *) ptr)->solver->conflicts ();
}
ABC_NAMESPACE_IMPL_END

8
src/sat/cadical/cadical_restart.cpp
View File

@ -35,12 +35,12 @@ bool Internal::stabilizing () {
STOP (stable);
else
STOP (unstable);
const int64_t delta_conflicts =
stats.conflicts - last.stabilize.conflicts;
//const int64_t delta_conflicts =
// stats.conflicts - last.stabilize.conflicts;
const int64_t delta_ticks =
stats.ticks.search[stable] - last.stabilize.ticks;
const char *current_mode = stable ? "stable" : "unstable";
const char *next_mode = stable ? "unstable" : "stable";
//const char *current_mode = stable ? "stable" : "unstable";
//const char *next_mode = stable ? "unstable" : "stable";
PHASE ("stabilizing", stats.stabphases,
"reached %s stabilization limit %" PRId64 " after %" PRId64
" conflicts and %" PRId64 " ticks at %" PRId64

10
src/sat/cadical/cadical_solver.cpp
View File

@ -1759,6 +1759,16 @@ void Solver::error (const char *fmt, ...) {
va_end (ap);
}
/*------------------------------------------------------------------------*/
int Solver::clauses () {
return internal->stats.added.total;
}
int Solver::conflicts () {
return internal->stats.conflicts;
}
} // namespace CaDiCaL
ABC_NAMESPACE_IMPL_END

2
src/sat/cadical/ccadical.h
View File

@ -58,6 +58,8 @@ int ccadical_reserve_difference (CCaDiCaL *, int number_of_vars);
void ccadical_reserve(CCaDiCaL *, int min_max_var);
int ccadical_is_inconsistent(CCaDiCaL *);
int ccadical_clauses(CCaDiCaL *);
int ccadical_conflicts(CCaDiCaL *);
/*------------------------------------------------------------------------*/

15
src/sat/kissat/terminate.h
View File

@ -16,6 +16,21 @@ static inline bool kissat_terminated (kissat *solver, int bit,
const char *name, const char *file,
long lineno, const char *fun) {
KISSAT_assert (0 <= bit), KISSAT_assert (bit < 64);
#if defined(COVERAGE)
if (!solver->termination.flagged) {
int (*terminate) (void *) = solver->termination.terminate;
void *state = (void *) solver->termination.state;
if (terminate && terminate (state))
solver->termination.flagged = ~(uint64_t) 0;
}
#else
if (!solver->termination.flagged) {
int (*terminate) (void *) = solver->termination.terminate;
void *state = (void *) solver->termination.state;
if (terminate && terminate (state))
solver->termination.flagged = true;
}
#endif
#ifdef COVERAGE
const uint64_t mask = (uint64_t) 1 << bit;
if (!(solver->termination.flagged & mask))