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

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

This commit is contained in:
Miodrag Milanovic 2025-12-22 11:46:52 +01:00
parent bd05a6454e 64637b8395
commit c6966aa907
20 changed files with 917 additions and 46 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/giaDecGraph.cpp
View File

@ -38,6 +38,7 @@
#include <unordered_map>
#include <algorithm>
#include <functional>
#include <iterator>
#include "gia.h"
#include "misc/vec/vecHash.h"

66
src/aig/gia/giaTruth.c
View File

@ -22,6 +22,7 @@
#include "misc/vec/vecMem.h"
#include "misc/vec/vecWec.h"
#include "misc/util/utilTruth.h"
#include "bool/lucky/lucky.h"
#include "opt/dau/dau.h"
ABC_NAMESPACE_IMPL_START
@ -809,10 +810,73 @@ Gia_Man_t * Gia_ManIsoNpnReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int fV
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManNodeFunctionProfile( Gia_Man_t * p, int nVars )
{
int fCanonicize = 1;
Gia_Obj_t * pObj;
Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
int nWords = Abc_Truth6WordNum( nVars );
Vec_Mem_t * pTtMem = Vec_MemAlloc( nWords, 12 ); // supports up to nVars words
Vec_MemHashAlloc( pTtMem, 1000 );
Vec_Int_t * vCounts = Vec_IntAlloc( 100 );
permInfo * pi = setPermInfoPtr( nVars );
word pAuxWord[DAU_MAX_WORD], pAuxWord1[DAU_MAX_WORD], Truth[DAU_MAX_WORD], * pTruth; int i;
assert( nVars <= 7 );
Gia_ObjComputeTruthTableStart( p, nVars );
Gia_ManForEachAnd( p, pObj, i ) {
if ( Gia_ManSuppSize(p, &i, 1) != nVars )
continue;
Gia_ManCollectCis( p, &i, 1, vLeaves );
assert( Vec_IntSize(vLeaves) == nVars );
pTruth = Gia_ObjComputeTruthTableCut( p, pObj, vLeaves );
if ( fCanonicize ) {
memcpy( Truth, pTruth, sizeof(word) * nWords );
simpleMinimal( Truth, pAuxWord, pAuxWord1, pi, nVars ); // NPN canonical form
}
else {
memcpy( Truth, pTruth, sizeof(word) * nWords );
}
{
int nEntries = Vec_MemEntryNum( pTtMem );
int Value = Vec_MemHashInsert( pTtMem, Truth );
if ( Vec_MemEntryNum( pTtMem ) == nEntries )
Vec_IntAddToEntry( vCounts, Value, 1 );
else
{
assert( Value == nEntries );
Vec_IntPush( vCounts, 1 );
}
}
}
for ( i = 0; i < Vec_MemEntryNum(pTtMem); i++ ) {
word * pCanon = Vec_MemReadEntry( pTtMem, i );
int Count = Vec_IntEntry( vCounts, i );
Abc_TtPrintHexRev( stdout, pCanon, nVars );
printf( " %d\n", Count );
}
Gia_ObjComputeTruthTableStop( p );
Vec_IntFree( vLeaves );
Vec_IntFree( vCounts );
Vec_MemHashFree( pTtMem );
Vec_MemFree( pTtMem );
freePermInfoPtr( pi );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -229,6 +229,7 @@ static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGenTF ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGenAT ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGenPop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandGenFsm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCover ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1060,6 +1061,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 );
Cmd_CommandAdd( pAbc, "Various", "gentf", Abc_CommandGenTF, 0 );
Cmd_CommandAdd( pAbc, "Various", "genat", Abc_CommandGenAT, 0 );
Cmd_CommandAdd( pAbc, "Various", "genpop", Abc_CommandGenPop, 0 );
Cmd_CommandAdd( pAbc, "Various", "genfsm", Abc_CommandGenFsm, 0 );
Cmd_CommandAdd( pAbc, "Various", "cover", Abc_CommandCover, 1 );
Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 );
@ -11404,15 +11406,15 @@ usage:
***********************************************************************/
int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose );
extern Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose );
Abc_Ntk_t * pNtkRes = NULL;
Abc_Ntk_t * pTopo = NULL;
int nTimeOut = 0;
int nSeed = 0;
char * pFileName = NULL;
int c, fVerbose = 0;
int c, fAndGates = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "TSvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TSavh" ) ) != EOF )
{
switch ( c )
{
@ -11438,6 +11440,9 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nSeed < 0 )
goto usage;
break;
case 'a':
fAndGates ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -11490,7 +11495,7 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pTopo = Abc_NtkDupDfs( pNtkRes = pTopo );
Abc_NtkDelete( pNtkRes );
pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fVerbose );
pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fAndGates, fVerbose );
Abc_NtkDelete( pTopo );
if ( pNtkRes == NULL )
{
@ -11501,10 +11506,11 @@ int Abc_CommandTopoExact( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: topoexact [-TS num] <file>\n" );
Abc_Print( -2, "usage: topoexact [-TS num] [-avh] <file>\n" );
Abc_Print( -2, "\t exact synthesis solution for the fixed topology\n" );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-S <num> : the random seed to randomize the SAT solver [default = %d]\n", nSeed );
Abc_Print( -2, "\t-a : toggle using only and-gates (not xor-gates) [default = %s]\n", fAndGates ? "yes" : "no" );
Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose ? "yes" : "no" );
Abc_Print( -2, "\t-h : print the command usage\n" );
Abc_Print( -2, "\t<file> : BLIF file name with the topology\n" );
@ -16031,6 +16037,81 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandGenPop( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Abc_NtkLutCascadeFromPopcountLuts( int nVars, int nLutSize, int fVerbose, char * pFileName );
char * pFileName = NULL;
Abc_Ntk_t * pNtk = NULL;
int c, nVars = 10, nLutSize = 6, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NKvh" ) ) != 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 'K':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
goto usage;
}
nLutSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nLutSize < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc == globalUtilOptind + 1 )
pFileName = argv[globalUtilOptind];
pNtk = Abc_NtkLutCascadeFromPopcountLuts( nVars, nLutSize, fVerbose, pFileName );
if ( pNtk == NULL )
{
fprintf( pAbc->Err, "Deriving the network has failed.\n" );
return 1;
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
return 0;
usage:
Abc_Print( -2, "usage: genpop [-NK num] [-vh] <file.v>\n" );
Abc_Print( -2, "\t generates the adder tree\n" );
Abc_Print( -2, "\t-N <num> : the number of support variables [default = %d]\n", nVars );
Abc_Print( -2, "\t-K <num> : the number of LUT inputs [default = %d]\n", nLutSize );
Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "\t-<file.v> : (optional) Verilog file name\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -34771,10 +34852,7 @@ int Abc_CommandAbc9SaveAig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( fClear && pAbc->pGiaSaved != NULL )
{
Gia_ManStopP( &pAbc->pGiaSaved );
return 0;
}
if ( fArea && pAbc->pGiaSaved != NULL && Gia_ManAndNum(pAbc->pGiaSaved) <= Gia_ManAndNum(pAbc->pGia) )
return 0;
if ( !fArea && pAbc->pGiaSaved != NULL && !(Gia_ManLevelNum(pAbc->pGiaSaved) > Gia_ManLevelNum(pAbc->pGia) || (Gia_ManLevelNum(pAbc->pGiaSaved) == Gia_ManLevelNum(pAbc->pGia) && Gia_ManAndNum(pAbc->pGiaSaved) > Gia_ManAndNum(pAbc->pGia))) )
@ -42209,10 +42287,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
FILE * pFile;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
char ** pArgvNew;
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0;
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
Cec_ManCecSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxytvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdbasxytvwh" ) ) != EOF )
{
switch ( c )
{
@ -42247,6 +42325,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'd':
fDualOutput ^= 1;
break;
case 'b':
fSavedSpec ^= 1;
break;
case 'a':
fDumpMiter ^= 1;
break;
@ -42377,6 +42458,16 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
}
else if ( fSavedSpec )
{
if ( pAbc->pGiaSaved == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no saved specification.\n" );
return 1;
}
pGias[0] = pAbc->pGia;
pGias[1] = pAbc->pGiaSaved;
}
else
{
char * FileName, * pTemp;
@ -42498,17 +42589,19 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pGias[0] != pAbc->pGia )
Gia_ManStop( pGias[0] );
Gia_ManStop( pGias[1] );
if ( pGias[1] != pAbc->pGiaSaved )
Gia_ManStop( pGias[1] );
return 0;
usage:
Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxytvwh]\n" );
Abc_Print( -2, "usage: &cec [-CT num] [-nmdbasxytvwh]\n" );
Abc_Print( -2, "\t new combinational equivalence checker\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
Abc_Print( -2, "\t-b : toggle using saved specification [default = %s]\n", fSavedSpec? "yes":"no");
Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no");
Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no");
Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNewX? "yes":"no");

261
src/base/abci/abcCas.c
View File

@ -1703,10 +1703,269 @@ void Abc_NtkRandFile( char * pFileName, int nVars, int nFuncs, int nMints )
Vec_WrdFree( vTruths );
}
/**Function*************************************************************
Synopsis [Dump popcount LUT cascades into a Verilog file.]
Description [Emits one LUT6CY per LUT with placement attributes and
preserves cascade ordering via RLOC/BEL tags.]
SideEffects []
SeeAlso []
***********************************************************************/
static void Abc_LutCascadeDumpName( FILE * pFile, int Obj, int iCas, int nVars )
{
if ( Obj < nVars )
fprintf( pFile, "pi%d", Obj );
else
fprintf( pFile, "w%d_%d", iCas, Obj );
}
static void Abc_LutCascadeDumpOneVerilog( FILE * pFile, word * pLuts, int nVars, int iCas )
{
static const char * pBels[6] = { "A5LUT", "B5LUT", "C5LUT", "D5LUT", "E5LUT", "F5LUT" };
Vec_Int_t * vWires = Vec_IntAlloc( 32 );
word n, i;
for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] )
{
word nIns = pLuts[i+1];
word * pIns = pLuts+i+2;
int OutId = (int)pIns[nIns];
if ( OutId >= nVars )
Vec_IntPushUnique( vWires, OutId );
}
if ( Vec_IntSize(vWires) )
{
fprintf( pFile, " // cascade %d wires\n", iCas );
int Id; int k;
Vec_IntForEachEntry( vWires, Id, k )
fprintf( pFile, " wire w%d_%d;\n", iCas, Id );
fprintf( pFile, "\n" );
}
Vec_IntClear( vWires );
int iLastLut = -1;
for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] )
{
word nIns = pLuts[i+1];
word * pIns = pLuts+i+2;
word * pT = pLuts+i+2+nIns+1;
iLastLut = (int)pIns[nIns];
fprintf( pFile, " (* HU_SET = \"hu_set_%d\", RLOC = \"X%dY%u\", BEL = \"%s\", DONT_TOUCH = \"yes\", IS_BEL_FIXED = \"yes\" *)\n",
iCas, iCas, (unsigned)n, pBels[n % 6] );
fprintf( pFile, " LUT6CY #(.INIT(64'h" );
Abc_TtPrintHexRev( pFile, pT, 6 );
fprintf( pFile, ")) lut_%d_%u (\n", iCas, (unsigned)n );
int k;
for ( k = 0; k < 6; k++ )
{
fprintf( pFile, " .I%d(", k );
if ( k < (int)nIns )
Abc_LutCascadeDumpName( pFile, (int)pIns[k], iCas, nVars );
else
fprintf( pFile, "1'b0" );
fprintf( pFile, "),\n" );
}
fprintf( pFile, " .O(" );
Abc_LutCascadeDumpName( pFile, iLastLut, iCas, nVars );
fprintf( pFile, ")\n );\n\n" );
}
assert( iLastLut >= 0 );
fprintf( pFile, " assign pc%d = ", iCas );
Abc_LutCascadeDumpName( pFile, iLastLut, iCas, nVars );
fprintf( pFile, ";\n\n" );
Vec_IntFree( vWires );
}
void Abc_LutCascadeDumpVerilog( Vec_Ptr_t * vLuts, int nVars, const char * pFileName )
{
if ( vLuts == NULL || pFileName == NULL )
{
printf( "Abc_LutCascadeDumpVerilog(): Null input.\n" );
return;
}
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Abc_LutCascadeDumpVerilog(): Cannot open \"%s\" for writing.\n", pFileName );
return;
}
int nOuts = Vec_PtrSize( vLuts );
fprintf( pFile, "// Auto-generated LUT cascade\n" );
fprintf( pFile, "module lut_cascade_%d (\n", nVars );
int i;
fprintf( pFile, " input " );
for ( i = 0; i < nVars; i++ )
{
if ( i ) fprintf( pFile, ", " );
fprintf( pFile, "pi%d", i );
}
fprintf( pFile, ",\n output " );
for ( i = 0; i < nOuts; i++ )
{
if ( i ) fprintf( pFile, ", " );
fprintf( pFile, "pc%d", i );
}
fprintf( pFile, "\n);\n\n" );
word * pLuts;
Vec_PtrForEachEntry( word *, vLuts, pLuts, i )
{
if ( pLuts == NULL )
continue;
fprintf( pFile, " // cascade %d\n", i );
Abc_LutCascadeDumpOneVerilog( pFile, pLuts, nVars, i );
}
fprintf( pFile, "endmodule\n" );
fclose( pFile );
}
/**Function*************************************************************
Synopsis [Generates popcount as a set of LUT cascades.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Exa8_ManExactSynthesisPopcountAsLuts( int nVars, int nLutSize, int fVerbose )
{
extern Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int nLutSize, int fVerbose );
Vec_Ptr_t * vTruthSets = Exa8_ManExactSynthesisPopcount( nVars, nLutSize, fVerbose );
if ( vTruthSets == NULL )
return NULL;
int nWordsNode = Abc_TtWordNum( nLutSize );
int nOuts = Abc_Base2Log( nVars + 1 );
if ( Vec_PtrSize(vTruthSets) != nOuts && fVerbose )
printf( "Exa8_ManExactSynthesisPopcountAsLuts(): Expecting %d outputs, got %d.\n", nOuts, Vec_PtrSize(vTruthSets) );
Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_PtrSize(vTruthSets) );
Vec_Wrd_t * vTruths; int o;
Vec_PtrForEachEntry( Vec_Wrd_t *, vTruthSets, vTruths, o )
{
if ( vTruths == NULL )
continue;
int nObjs = Vec_WrdSize( vTruths ) / nWordsNode;
int nNodes = nObjs - nVars;
if ( nNodes <= 0 )
{
Vec_WrdFree( vTruths );
continue;
}
Vec_Wrd_t * vLutVec = Vec_WrdStart( 1 );
int pIns[6]; int i, k;
for ( i = 0; i < nNodes; i++ )
{
word * pTruth = Vec_WrdEntryP( vTruths, (nVars + i) * nWordsNode );
if ( i == 0 )
{
for ( k = 0; k < nLutSize; k++ )
pIns[k] = nLutSize-1-k;
}
else
{
pIns[0] = nVars + i - 1;
if ( i & 1 )
for ( k = 0; k < nLutSize-1; k++ )
pIns[k+1] = nVars - 1 - k;
else
for ( k = 0; k < nLutSize-1; k++ )
pIns[k+1] = nLutSize - 2 - k;
}
Abc_LutCascadeGenOne( vLutVec, nLutSize, pIns, nVars + i, pTruth );
}
if ( fVerbose )
Abc_LutCascadePrint( Vec_WrdArray(vLutVec), nLutSize );
Vec_PtrPush( vRes, Vec_WrdReleaseArray(vLutVec) );
Vec_WrdFree( vLutVec );
Vec_WrdFree( vTruths );
}
Vec_PtrFree( vTruthSets );
return vRes;
}
/**Function*************************************************************
Synopsis [Builds network for popcount cascades.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkLutCascadeFromPopcountLuts( int nVars, int nLutSize, int fVerbose, char * pFileName )
{
Vec_Ptr_t * vLuts = Exa8_ManExactSynthesisPopcountAsLuts( nVars, nLutSize, fVerbose );
if ( vLuts == NULL )
return NULL;
if ( pFileName && nLutSize == 6 ) {
Abc_LutCascadeDumpVerilog( vLuts, nVars, pFileName );
printf( "Wrote the resulting network into a Verilog file \"%s\".\n", pFileName );
}
Abc_Ntk_t * pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 0 );
Abc_Obj_t * pObj; int Id; char pName[32];
pNtkNew->pName = Extra_UtilStrsav( "pop" );
Vec_PtrPush( pNtkNew->vObjs, NULL );
for ( Id = 0; Id < nVars; Id++ )
{
pObj = Abc_NtkCreatePi( pNtkNew );
pName[0] = 'a' + Id;
pName[1] = 0;
Abc_ObjAssignName( pObj, pName, NULL );
}
Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
if ( Vec_PtrSize(vLuts) != Abc_Base2Log(nVars + 1) )
printf( "Abc_NtkLutCascadeFromPopcountLuts(): Expecting %d outputs, got %d.\n", Abc_Base2Log(nVars + 1), Vec_PtrSize(vLuts) );
word * pLuts; int o;
Vec_PtrForEachEntry( word *, vLuts, pLuts, o )
{
if ( pLuts == NULL )
continue;
Vec_Ptr_t * vCopy = Vec_PtrStart( nVars + pLuts[0] + 100 );
Abc_NtkForEachCi( pNtkNew, pObj, Id )
Vec_PtrWriteEntry( vCopy, Id, pObj );
word n, i, k; int iLastLut = -1;
for ( n = 0, i = 1; n < pLuts[0]; n++, i += pLuts[i] )
{
word nIns = pLuts[i+1];
word * pIns = pLuts+i+2;
word * pT = pLuts+i+2+nIns+1;
Abc_Obj_t * pNodeNew = Abc_NtkCreateNode( pNtkNew );
for ( k = 0; k < nIns; k++ )
Abc_ObjAddFanin( pNodeNew, (Abc_Obj_t *)Vec_PtrEntry(vCopy, pIns[k]) );
Abc_Obj_t * pObjNew = Abc_NtkLutCascadeDeriveSop( pNtkNew, pNodeNew, pT, nIns, vCover );
Vec_PtrWriteEntry( vCopy, pIns[nIns], pObjNew );
iLastLut = pIns[nIns];
}
if ( iLastLut == -1 )
{
Vec_PtrFree( vCopy );
continue;
}
Abc_Obj_t * pPo = Abc_NtkCreatePo( pNtkNew );
Abc_ObjAddFanin( pPo, (Abc_Obj_t *)Vec_PtrEntry(vCopy, iLastLut) );
snprintf( pName, sizeof(pName), "pc%d", o );
Abc_ObjAssignName( pPo, pName, NULL );
Vec_PtrFree( vCopy );
}
Vec_IntFree( vCover );
Vec_PtrFreeFree( vLuts );
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkLutCascadeFromPopcountLuts: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

38
src/base/abci/abcTopo.c
View File

@ -65,17 +65,18 @@ Abc_Ntk_t * Abc_NtkTopoDup( Abc_Ntk_t * pTopo, Vec_Wrd_t * vTruths )
}
return pNew;
}
Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fVerbose )
Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, int fAndGates, int fVerbose )
{
Abc_Ntk_t * pRes = NULL;
abctime clkTotal = Abc_Clock();
assert( Abc_NtkIsSopLogic(pTopo) );
// count how many variables we need to encode minterms of each node
Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0;
Abc_Obj_t * pObj; int i, nMints = 0, nNodeClausesPerMint = 0, nTwoFaninNodes = 0;
Abc_NtkForEachNode( pTopo, pObj, i ) {
assert( Abc_ObjFaninNum(pObj) <= 6 );
nMints += 1 << Abc_ObjFaninNum(pObj);
nNodeClausesPerMint += 2 * (1 << Abc_ObjFaninNum(pObj)); // two clauses per minterm
nTwoFaninNodes += (Abc_ObjFaninNum(pObj) == 2);
}
// derive input/output mapping of the original function, which will be synthesized
Gia_Man_t * pGia = Abc_NtkClpGia( pFunc );
@ -107,7 +108,38 @@ Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut
// and add constraints that tell us that the value of the node's output agrees with the values of its fanins
// while the value of the primary outputs is realized correctly by those internal nodes that drive the outputs
int m, n, k, f, nTopoMints = 1 << Abc_NtkCiNum(pTopo);
int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint);
int nClauses = nTopoMints * (Abc_NtkCiNum(pTopo) + Abc_NtkPoNum(pTopo) + nNodeClausesPerMint) +
(fAndGates ? 2 * nTwoFaninNodes : 0);
if ( fAndGates && nTwoFaninNodes )
{
// block XOR/XNOR truth tables for two-input nodes
int iMint = 0;
Abc_NtkForEachNode( pTopo, pObj, i )
{
int nFanins = Abc_ObjFaninNum(pObj);
if ( nFanins == 2 )
{
int pLits[4], j;
// forbid 0110
pLits[0] = Abc_Var2Lit( iMint + 0, 0 );
pLits[1] = Abc_Var2Lit( iMint + 1, 1 );
pLits[2] = Abc_Var2Lit( iMint + 2, 1 );
pLits[3] = Abc_Var2Lit( iMint + 3, 0 );
for ( j = 0; j < 4; j++ )
kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) );
kissat_add( pSat, 0 );
// forbid 1001
pLits[0] = Abc_Var2Lit( iMint + 0, 1 );
pLits[1] = Abc_Var2Lit( iMint + 1, 0 );
pLits[2] = Abc_Var2Lit( iMint + 2, 0 );
pLits[3] = Abc_Var2Lit( iMint + 3, 1 );
for ( j = 0; j < 4; j++ )
kissat_add( pSat, Abc_LitIsCompl(pLits[j]) ? -(Abc_Lit2Var(pLits[j]) + 1) : (Abc_Lit2Var(pLits[j]) + 1) );
kissat_add( pSat, 0 );
}
iMint += 1 << nFanins;
}
}
for ( m = 0; m < nTopoMints; m++ ) {
int iVarBase = nMints + m * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo));
// set PI values for this minterm

121
src/base/cmd/cmd.c
View File

@ -66,6 +66,7 @@ static int CmdCommandMvsis ( Abc_Frame_t * pAbc, int argc, char ** argv
static int CmdCommandCapo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandStarter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandAutoTuner ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int CmdCommandSolver ( Abc_Frame_t * pAbc, int argc, char ** argv );
extern int Cmd_CommandAbcLoadPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -121,6 +122,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "capo", CmdCommandCapo, 0 );
Cmd_CommandAdd( pAbc, "Various", "starter", CmdCommandStarter, 0 );
Cmd_CommandAdd( pAbc, "Various", "autotuner", CmdCommandAutoTuner, 0 );
Cmd_CommandAdd( pAbc, "Various", "&solver", CmdCommandSolver, 0 );
Cmd_CommandAdd( pAbc, "Various", "load_plugin", Cmd_CommandAbcLoadPlugIn, 0 );
}
@ -2806,6 +2808,125 @@ usage:
return 1;
}
/**Function********************************************************************
Synopsis [Calls Capo internally.]
Description []
SideEffects []
SeeAlso []
******************************************************************************/
int CmdCommandSolver( Abc_Frame_t * pAbc, int argc, char **argv )
{
extern void Gia_AigerWrite( Gia_Man_t * p, char * pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine );
FILE * pFile;
char Command[1000];
char TempFileName[100];
unsigned int RandomNum;
int i;
// Check for help flags
if ( argc > 1 )
{
if ( strcmp( argv[1], "-h" ) == 0 )
goto usage;
if ( strcmp( argv[1], "-?" ) == 0 )
goto usage;
}
// Check if AIG is available
if ( pAbc->pGia == NULL )
{
fprintf( pAbc->Err, "The current AIG is not available.\n" );
goto usage;
}
// Check if solver binary exists in current directory or PATH
char * pSolverName;
if ( (pFile = fopen( "./solver", "r" )) != NULL )
{
pSolverName = "./solver";
fclose( pFile );
}
else
{
// Check if solver exists in PATH
char CheckCommand[100];
sprintf( CheckCommand, "which solver > /dev/null 2>&1" );
if ( system( CheckCommand ) == 0 )
{
pSolverName = "solver";
}
else
{
fprintf( pAbc->Err, "Cannot find \"solver\" binary in the current directory or in PATH.\n" );
goto usage;
}
}
// Generate random 8-hex-character temporary filename
RandomNum = (unsigned int)(ABC_PTRUINT_T)pAbc ^
(unsigned int)(ABC_PTRUINT_T)pAbc->pGia ^
(unsigned int)time(NULL) ^
(unsigned int)getpid();
sprintf( TempFileName, "%08X.aig", RandomNum );
// Write the current AIG to the temporary file
Gia_AigerWrite( pAbc->pGia, TempFileName, 0, 0, 1 );
// Verify the file was created successfully
if ( (pFile = fopen( TempFileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Failed to create temporary AIG file \"%s\".\n", TempFileName );
return 1;
}
fclose( pFile );
// Build the command string
sprintf( Command, "%s", pSolverName );
// Add all user arguments
for ( i = 1; i < argc; i++ )
{
strcat( Command, " " );
strcat( Command, argv[i] );
}
// Add the AIG filename at the end
strcat( Command, " " );
strcat( Command, TempFileName );
// Debug: Show what command is being executed
fprintf( pAbc->Out, "Executing command: %s\n", Command );
// Execute the solver command
if ( system( Command ) == -1 )
{
fprintf( pAbc->Err, "The following command has failed:\n" );
fprintf( pAbc->Err, "\"%s\"\n", Command );
unlink( TempFileName );
return 1;
}
// Clean up the temporary file
unlink( TempFileName );
return 0;
usage:
fprintf( pAbc->Err, "\tusage: &solver <args>\n");
fprintf( pAbc->Err, "\t run the external solver binary on the current AIG\n" );
fprintf( pAbc->Err, "\t-h : print the command usage\n" );
fprintf( pAbc->Err, "\t<args> : arguments to pass to the solver\n" );
fprintf( pAbc->Err, "\t The current AIG will be written to a temporary file\n" );
fprintf( pAbc->Err, "\t and passed as the last argument to the solver.\n" );
fprintf( pAbc->Err, "\t Example: solver -h\n" );
return 1;
}
/**Function********************************************************************
Synopsis [Print the version string.]

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

@ -93,6 +93,7 @@ static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteSmv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteJson ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteJsonC ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteResub ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteMM ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandWriteMMGia ( Abc_Frame_t * pAbc, int argc, char **argv );
@ -176,6 +177,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "write_status", IoCommandWriteStatus, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_smv", IoCommandWriteSmv, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_json", IoCommandWriteJson, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_jsonc", IoCommandWriteJsonC, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&write_resub", IoCommandWriteResub, 0 );
Cmd_CommandAdd( pAbc, "I/O", "write_mm", IoCommandWriteMM, 0 );
Cmd_CommandAdd( pAbc, "I/O", "&write_mm", IoCommandWriteMMGia, 0 );
@ -4395,6 +4397,54 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandWriteJsonC( Abc_Frame_t * pAbc, int argc, char **argv )
{
extern void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL || !Abc_NtkHasMapping(pNtk) )
{
fprintf( pAbc->Out, "No curent network or network is not mapped.\n" );
return 0;
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFileName = argv[globalUtilOptind];
Jsonc_WriteTest( pNtk, pFileName );
return 0;
usage:
fprintf( pAbc->Err, "usage: write_jsonc [-ch] <file>\n" );
fprintf( pAbc->Err, "\t write the network in JSONC format\n" );
fprintf( pAbc->Err, "\t-h : print the help message\n" );
fprintf( pAbc->Err, "\tfile : the name of the file to write (extension .jsonc)\n" );
return 1;
}
/**Function*************************************************************
Synopsis []

145
src/base/io/ioJsonc.c
View File

@ -23,8 +23,10 @@
#include <string.h>
#include <stdint.h>
#include <stdbool.h>
#include <assert.h>
#include "ioAbc.h"
#include "map/mio/mio.h"
ABC_NAMESPACE_IMPL_START
@ -605,9 +607,150 @@ int Jsonc_ReadTest( char * pFileName )
return 0;
}
static int Jsonc_ParseNameBit( const char * pName, char * pBase, int nBase )
{
const char * pOpen;
const char * pClose;
int nCopy;
if ( pBase && nBase > 0 )
pBase[0] = '\0';
if ( pName == NULL || pBase == NULL || nBase <= 1 )
return 0;
pOpen = strrchr( pName, '[' );
pClose = pOpen ? strchr( pOpen, ']' ) : NULL;
if ( pOpen && pClose && pClose > pOpen + 1 )
{
nCopy = (int)(pOpen - pName);
if ( nCopy > nBase - 1 )
nCopy = nBase - 1;
memcpy( pBase, pName, nCopy );
pBase[nCopy] = '\0';
return atoi( pOpen + 1 );
}
strncpy( pBase, pName, nBase - 1 );
pBase[nBase - 1] = '\0';
return 0;
}
static const char * Jsonc_GetPortName( Abc_Obj_t * pObj )
{
if ( Abc_ObjIsCi(pObj) && Abc_NtkIsNetlist(pObj->pNtk) && Abc_ObjFanoutNum(pObj) )
return Abc_ObjName( Abc_ObjFanout0(pObj) );
if ( Abc_ObjIsCo(pObj) && Abc_NtkIsNetlist(pObj->pNtk) && Abc_ObjFaninNum(pObj) )
return Abc_ObjName( Abc_ObjFanin0(pObj) );
return Abc_ObjName(pObj);
}
static const char * Jsonc_GetNodeOutName( Abc_Obj_t * pObj )
{
static char Buffer[1024];
if ( Abc_ObjFanoutNum(pObj) )
{
Abc_Obj_t * pFan0 = Abc_ObjFanout0(pObj);
if ( Abc_ObjIsNet(pFan0) || Abc_ObjIsCo(pFan0) )
return Abc_ObjName(pFan0);
}
if ( Abc_ObjName(pObj) )
return Abc_ObjName(pObj);
snprintf( Buffer, sizeof(Buffer), "n%d", Abc_ObjId(pObj) );
return Buffer;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Jsonc_WriteTest( Abc_Ntk_t * p, char * pFileName )
{
Vec_Ptr_t * vNodes;
Vec_Int_t * vObj2Num;
Abc_Obj_t * pObj;
FILE * pFile;
int i, Counter, Total;
assert( Abc_NtkHasMapping(p) );
vNodes = Abc_NtkDfs2( p );
vObj2Num = Vec_IntStartFull( Abc_NtkObjNumMax(p) );
Total = Abc_NtkPiNum(p) + Vec_PtrSize(vNodes) + Abc_NtkPoNum(p);
pFile = fopen( pFileName, "wb" );
if ( pFile == NULL )
{
printf( "Jsonc_WriteTest(): Cannot open output file \"%s\" for writing.\n", pFileName );
Vec_IntFree( vObj2Num );
Vec_PtrFree( vNodes );
return;
}
fprintf( pFile, "{\n" );
fprintf( pFile, " \"name\": \"%s\",\n", Abc_NtkName(p) ? Abc_NtkName(p) : "" );
fprintf( pFile, " \"nodes\": [\n" );
Counter = 0;
Abc_NtkForEachPi( p, pObj, i )
{
char Name[1024];
int Bit = Jsonc_ParseNameBit( Jsonc_GetPortName(pObj), Name, sizeof(Name) );
Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter );
fprintf( pFile, " {\n" );
fprintf( pFile, " \"type\": \"pi\",\n" );
fprintf( pFile, " \"name\": \"%s\",\n", Name );
fprintf( pFile, " \"bit\": %d\n", Bit );
fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," );
}
Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
{
Mio_Gate_t * pGate = (Mio_Gate_t *)pObj->pData;
Mio_Pin_t * pPin;
int k;
assert( pGate != NULL );
Vec_IntWriteEntry( vObj2Num, Abc_ObjId(pObj), Counter );
fprintf( pFile, " {\n" );
fprintf( pFile, " \"type\": \"%s\",\n", "instance" );
fprintf( pFile, " \"name\": \"%s\",\n", Mio_GateReadName(pGate) );
fprintf( pFile, " \"fanins\":\n" );
fprintf( pFile, " {\n" );
for ( pPin = Mio_GateReadPins(pGate), k = 0; pPin; pPin = Mio_PinReadNext(pPin), k++ )
{
Abc_Obj_t * pFanin = Abc_ObjFanin0Ntk( Abc_ObjFanin(pObj, k) );
int FanId = Vec_IntEntry( vObj2Num, Abc_ObjId(pFanin) );
assert( FanId >= 0 );
fprintf( pFile, " \"%s\": { \"node\": %d", Mio_PinReadName(pPin), FanId );
if ( Abc_ObjIsNode(pFanin) && pFanin->pData != NULL )
fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pFanin->pData) );
fprintf( pFile, " }%s\n", Mio_PinReadNext(pPin) ? "," : "" );
}
fprintf( pFile, " }\n" );
//fprintf( pFile, " ]\n" );
fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," );
}
Abc_NtkForEachPo( p, pObj, i )
{
Abc_Obj_t * pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
char Name[1024];
int Bit = Jsonc_ParseNameBit( Jsonc_GetPortName(pObj), Name, sizeof(Name) );
int FanId = Vec_IntEntry( vObj2Num, Abc_ObjId(pDriver) );
assert( FanId >= 0 );
fprintf( pFile, " {\n" );
fprintf( pFile, " \"type\": \"PO\",\n" );
fprintf( pFile, " \"name\": \"%s\",\n", Name );
fprintf( pFile, " \"bit\": %d,\n", Bit );
fprintf( pFile, " \"fanin\": { \"node\": %d", FanId );
if ( Abc_ObjIsNode(pDriver) && pDriver->pData != NULL )
fprintf( pFile, ", \"pin\": \"%s\"", Mio_GateReadOutName((Mio_Gate_t *)pDriver->pData) );
fprintf( pFile, " }\n" );
fprintf( pFile, " }%s\n", ++Counter == Total ? "" : "," );
}
fprintf( pFile, " ]\n" );
fprintf( pFile, "}\n" );
fclose( pFile );
Vec_IntFree( vObj2Num );
Vec_PtrFree( vNodes );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

2
src/base/wln/wlnRtl.c
View File

@ -178,7 +178,7 @@ Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char *
char * pFileTemp = "_temp_.aig";
int fRtlil = strstr(pFileName, ".rtl") != NULL;
int fSVlog = strstr(pFileName, ".sv") != NULL;
sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; %saigmap; write_aiger %s\"",
sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; %saigmap; write_aiger -symbols %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? "-D" : "",

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

@ -49,12 +49,52 @@ ABC_NAMESPACE_IMPL_START
extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars );
extern int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars );
typedef struct Par_Share_t_ Par_Share_t;
typedef struct Par_ThData_t_ Par_ThData_t;
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
#ifndef ABC_USE_PTHREADS
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
#else // pthreads are used
#define PAR_THR_MAX 8
struct Par_Share_t_
{
volatile int fSolved;
volatile unsigned Result;
volatile int iEngine;
};
typedef struct Par_ThData_t_
{
Gia_Man_t * p;
int iEngine;
int fWorking;
int nTimeOut;
int Result;
int fVerbose;
Par_Share_t * pShare;
} Par_ThData_t;
static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result )
{
Par_ThData_t * pThData = (Par_ThData_t *)pUser;
Par_Share_t * pShare = pThData ? pThData->pShare : NULL;
if ( pShare == NULL )
return 0;
if ( fSolved )
{
if ( pShare->fSolved == 0 )
{
pShare->fSolved = 1;
pShare->Result = Result;
pShare->iEngine = pThData->iEngine;
}
return 0;
}
return pShare->fSolved != 0;
}
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -70,7 +110,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
SeeAlso []
***********************************************************************/
int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par_ThData_t * pThData )
{
abctime clk = Abc_Clock();
int RetValue = -1;
@ -84,6 +124,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
Ssw_RarSetDefaultParams( pPars );
pPars->TimeOut = nTimeOut;
pPars->fSilent = 1;
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
RetValue = Ssw_RarSimulateGia( p, pPars );
}
else if ( iEngine == 1 )
@ -92,6 +137,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
Saig_ParBmcSetDefaultParams( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@ -103,6 +153,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
Pdr_ManSetDefaultParams( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@ -115,6 +170,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
pPars->fUseGlucose = 1;
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@ -127,6 +187,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
pPars->fUseAbs = 1;
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@ -140,10 +205,17 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
pPars->nFramesAdd = 1; // the number of additional frames
pPars->fNotVerbose = 1; // silent
pPars->nTimeOut = nTimeOut; // timeout in seconds
if ( pThData && pThData->pShare )
{
pPars->pFuncProgress = Cec_SProveCallback;
pPars->pProgress = (void *)pThData;
}
RetValue = Bmcg_ManPerform( p, pPars );
}
else assert( 0 );
//while ( Abc_Clock() < clkStop );
if ( pThData && pThData->pShare && RetValue != -1 )
Cec_SProveCallback( (void *)pThData, 1, (unsigned)RetValue );
if ( fVerbose ) {
printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
@ -183,16 +255,6 @@ Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
#define PAR_THR_MAX 8
typedef struct Par_ThData_t_
{
Gia_Man_t * p;
int iEngine;
int fWorking;
int nTimeOut;
int Result;
int fVerbose;
} Par_ThData_t;
void * Cec_GiaProveWorkerThread( void * pArg )
{
Par_ThData_t * pThData = (Par_ThData_t *)pArg;
@ -207,13 +269,13 @@ void * Cec_GiaProveWorkerThread( void * pArg )
assert( 0 );
return NULL;
}
pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose );
pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose, pThData );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread )
void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare )
{
int i, status;
assert( nProcs <= PAR_THR_MAX );
@ -225,6 +287,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int n
ThData[i].fWorking = 0;
ThData[i].Result = -1;
ThData[i].fVerbose = fVerbose;
ThData[i].pShare = pShare;
if ( !WorkerThread )
continue;
status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
@ -254,7 +317,9 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
abctime clkScorr = 0, clkTotal = Abc_Clock();
Par_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
Par_Share_t Share;
int i, RetValue = -1, RetEngine = -2;
memset( &Share, 0, sizeof(Par_Share_t) );
Abc_CexFreeP( &p->pCexComb );
Abc_CexFreeP( &p->pCexSeq );
if ( !fSilent && fVerbose )
@ -264,7 +329,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
fflush( stdout );
assert( nProcs == 3 || nProcs == 5 );
Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread );
Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread, &Share );
// meanwhile, perform scorr
Gia_Man_t * pScorr = Cec_GiaScorrNew( p );
@ -280,7 +345,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(p), Gia_ManAndNum(pScorr) );
Abc_PrintTime( 1, "Time", clkScorr );
}
Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL );
Cec_GiaInitThreads( ThData, nProcs, pScorr, nTimeOut2, fVerbose, NULL, &Share );
// meanwhile, perform scorr
if ( Gia_ManAndNum(pScorr) < 100000 )
@ -297,7 +362,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
printf( "Reduced the miter from %d to %d nodes. ", Gia_ManAndNum(pScorr), Gia_ManAndNum(pScorr2) );
Abc_PrintTime( 1, "Time", clkScorr2 );
}
Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL );
Cec_GiaInitThreads( ThData, nProcs, pScorr2, nTimeOut3, fVerbose, NULL, &Share );
RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine );
// do something else
@ -338,4 +403,3 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
ABC_NAMESPACE_IMPL_END

3
src/proof/pdr/pdr.h
View File

@ -82,6 +82,8 @@ struct Pdr_Par_t_
int RunId; // PDR id in this run
int(*pFuncStop)(int); // callback to terminate
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback
void * pProgress; // progress callback data
abctime timeLastSolved; // the time when the last output was solved
Vec_Int_t * vOutMap; // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
char * pInvFileName; // invariable file name
@ -111,4 +113,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

4
src/proof/pdr/pdrCore.c
View File

@ -82,6 +82,8 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
pPars->pInvFileName = NULL; // invariant file name
pPars->pCexFilePrefix = NULL; // CEX output prefix
pPars->fBlocking = 0; // clause pushing with blocking
pPars->pFuncProgress = NULL; // progress/termination callback
pPars->pProgress = NULL; // progress callback data
}
/**Function*************************************************************
@ -2126,6 +2128,8 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
for ( k = 0; k < Saig_ManPoNum(pAig); k++ )
if ( Vec_IntEntry(pPars->vOutMap, k) == -2 ) // unknown
Vec_IntWriteEntry( pPars->vOutMap, k, -1 ); // undec
if ( pPars->pFuncProgress && (RetValue == 0 || RetValue == 1) )
pPars->pFuncProgress( pPars->pProgress, 1, (unsigned)RetValue );
if ( pPars->fUseBridge )
Gia_ManToBridgeAbort( stdout, 7, (unsigned char *)"timeout" );
return RetValue;

5
src/proof/pdr/pdrSat.c
View File

@ -307,6 +307,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
sat_solver_set_runtime_limit( pSat, Limit );
if ( RetValue == l_Undef )
return -1;
if ( p->pPars->pFuncProgress && p->pPars->pFuncProgress( p->pPars->pProgress, 0, (unsigned)k ) )
return -1;
}
else // check relative containment in terms of next states
{
@ -343,6 +345,8 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
else
return -1;
}
if ( p->pPars->pFuncProgress && p->pPars->pFuncProgress( p->pPars->pProgress, 0, (unsigned)k ) )
return -1;
}
clk = Abc_Clock() - clk;
p->tSat += clk;
@ -393,4 +397,3 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
ABC_NAMESPACE_IMPL_END

2
src/proof/ssw/ssw.h
View File

@ -115,6 +115,8 @@ struct Ssw_RarPars_t_
int nSolved;
Abc_Cex_t * pCex;
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback
void * pProgress; // progress callback data
};
typedef struct Ssw_Sml_t_ Ssw_Sml_t; // sequential simulation manager

6
src/proof/ssw/sswRarity.c
View File

@ -115,6 +115,8 @@ void Ssw_RarSetDefaultParams( Ssw_RarPars_t * p )
p->fSetLastState = 0;
p->fVerbose = 0;
p->fNotVerbose = 0;
p->pFuncProgress = NULL;
p->pProgress = NULL;
}
/**Function*************************************************************
@ -1007,6 +1009,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
timeLastSolved = Abc_Clock();
for ( r = 0; !pPars->nRounds || (nNumRestart * pPars->nRestart + r < pPars->nRounds); r++ )
{
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)r ) )
goto finish;
clk = Abc_Clock();
if ( fTryBmc )
{
@ -1019,6 +1023,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, Ssw_RarPars_t * pPars )
// simulate
for ( f = 0; f < pPars->nFrames; f++ )
{
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)(r * pPars->nFrames + f) ) )
goto finish;
Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
if ( fMiter )
{

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

@ -148,6 +148,8 @@ struct Saig_ParBmc_t_
int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
int RunId; // BMC id in this run
int(*pFuncStop)(int); // callback to terminate
int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback
void * pProgress; // progress callback data
};
@ -173,7 +175,9 @@ struct Bmc_AndPar_t_
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
int(*pFuncProgress)(void *, int, unsigned); // progress/termination callback
void * pProgress; // progress callback data
void (*pFuncOnFrameDone)(int, int, int); // callback on each frame status (frame, po, statuss)
};

9
src/sat/bmc/bmcBmc3.c
View File

@ -1353,6 +1353,8 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
p->nFailOuts = 0; // the number of failed outputs
p->nDropOuts = 0; // the number of timed out outputs
p->timeLastSolved = 0; // time when the last one was solved
p->pFuncProgress = NULL; // progress/termination callback
p->pProgress = NULL; // progress callback data
}
/**Function*************************************************************
@ -1528,6 +1530,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
pPars->timeLastSolved = Abc_Clock();
for ( f = 0; f < pPars->nFramesMax; f++ )
{
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)f ) )
goto finish;
// stop BMC after exploring all reachable states
if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
{
@ -1632,6 +1636,8 @@ clkOther += Abc_Clock() - clk2;
Abc_Print( 1, "Bmc3 got callbacks.\n" );
goto finish;
}
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)((f<<16) | i) ) )
goto finish;
// skip solved outputs
if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
continue;
@ -1663,6 +1669,8 @@ clkSatRun = Abc_Clock() - clk2;
fprintf( pLogFile, "Frame %5d Output %5d Time(ms) %8d %8d\n", f, i,
Lit < 2 ? 0 : (int)(clkSatRun * 1000 / CLOCKS_PER_SEC),
Lit < 2 ? 0 : Abc_MaxInt(0, Abc_MinInt(pPars->nTimeOutOne, pPars->nTimeOutOne - (int)((p->pTime4Outs[i] - clkSatRun) * 1000 / CLOCKS_PER_SEC))) );
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)((f<<16) | i) ) )
goto finish;
if ( p->pTime4Outs )
{
abctime timeSince = Abc_Clock() - clkOne;
@ -1894,4 +1902,3 @@ finish:
ABC_NAMESPACE_IMPL_END

13
src/sat/bmc/bmcBmcAnd.c
View File

@ -960,6 +960,8 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_Man_t * pTemp;
int nFramesMax, f, i=0, Lit = 1, status, RetValue = -2;
abctime clk = Abc_Clock();
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
return -1;
p = Bmc_MnaAlloc();
sat_solver_set_runtime_limit( p->pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose, &p->vPiMap );
@ -993,6 +995,11 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
for ( f = 0; f < nFramesMax; f++ )
{
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)f ) )
{
RetValue = -1;
break;
}
if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) )
{
// create another slice
@ -1000,6 +1007,11 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// try solving the outputs
for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ )
{
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, (unsigned)i ) )
{
RetValue = -1;
break;
}
Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i);
if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) )
continue;
@ -1097,4 +1109,3 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
ABC_NAMESPACE_IMPL_END

3
src/sat/bmc/bmcBmcG.c
View File

@ -445,6 +445,8 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
pPars->nProcs = 1;
if ( pPars->pFuncProgress && pPars->pFuncProgress( pPars->pProgress, 0, 0 ) )
return -1;
return Bmcg_ManPerformOne( pGia, pPars );
}
@ -454,4 +456,3 @@ int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
ABC_NAMESPACE_IMPL_END

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

@ -905,26 +905,30 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose )
Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int nLutSize, int fVerbose )
{
assert( nVars > nLutSize );
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
pPars->nVars = nVars;
pPars->nLutSize = nLutSize;
pPars->fKissat = 1;
pPars->fLutCascade = 1;
pPars->fMinNodes = 1;
pPars->fUsePerm = 1;
pPars->fGenTruths = 1;
pPars->fSilent = !fVerbose;
pPars->nLutSize = 6;
int v, o, nOuts = Abc_Base2Log(nVars+1);
Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts );
for ( o = 0; o < nOuts; o++ ) {
pPars->nNodes = 10;
ABC_FREE( pPars->pPermStr );
pPars->pPermStr = NULL;
char pBuffer[100];
for ( v = 0; v <= nVars; v++ )
pBuffer[v] = '0' + ((v >> o) & 1);
pBuffer[nVars+1] = '\0';
pPars->pSymStr = pBuffer;
int status = Exa8_ManExactSynthesis( pPars );
int status = Exa8_ManExactSynthesisIter( pPars );
if ( status != 1 ) {
printf( "Synthesis failed for output %d.\n", o );
break;
@ -932,6 +936,7 @@ Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose )
Vec_PtrPush( vRes, pPars->vTruths );
pPars->vTruths = NULL;
}
ABC_FREE( pPars->pPermStr );
return vRes;
}