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

Command "topoexact".

This commit is contained in:
Alan Mishchenko 2025-12-05 20:44:46 -08:00
parent b7f8df0941
commit e58a28b73b
5 changed files with 463 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -174,6 +174,7 @@ static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandLutExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAndExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAllExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTopoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOrchestrate ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -994,8 +995,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "varmin", Abc_CommandVarMin, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "faultclasses", Abc_CommandFaultClasses, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "exact", Abc_CommandExact, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "orchestrate", Abc_CommandOrchestrate, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "aigaug", Abc_CommandAIGAugmentation, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "orchestrate", Abc_CommandOrchestrate, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "aigaug", Abc_CommandAIGAugmentation, 1 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_start", Abc_CommandBmsStart, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "bms_stop", Abc_CommandBmsStop, 0 );
@ -1005,6 +1006,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "lutexact", Abc_CommandLutExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "andexact", Abc_CommandAndExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "allexact", Abc_CommandAllExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "topoexact", Abc_CommandTopoExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "testexact", Abc_CommandTestExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 );
@ -11387,6 +11389,126 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
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 );
Abc_Ntk_t * pNtkRes = NULL;
Abc_Ntk_t * pTopo = NULL;
int nTimeOut = 0;
int nSeed = 0;
char * pFileName = NULL;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "TSvh" ) ) != EOF )
{
switch ( c )
{
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut < 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;
}
nSeed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nSeed < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pNtkCur == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsStrash(pAbc->pNtkCur) )
{
Abc_Print( -1, "This command expect an AIG as the current network and BLIF file on the command line.\n" );
return 1;
}
if ( argc == globalUtilOptind + 1 )
pFileName = argv[globalUtilOptind];
if ( pFileName == NULL )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
}
pTopo = Io_Read( pFileName, Io_ReadFileType(pFileName), 1, 0 );
if ( pTopo == NULL )
{
Abc_Print( -1, "The topology file is not specified on the command line.\n" );
return 1;
}
if ( Abc_NtkGetFaninMax(pTopo) > 6 )
{
Abc_NtkDelete( pTopo );
Abc_Print( -1, "The topology network has nodes with more than 6 inputs.\n" );
return 1;
}
if ( Abc_NtkCiNum(pAbc->pNtkCur) != Abc_NtkCiNum(pTopo) )
{
Abc_NtkDelete( pTopo );
Abc_Print( -1, "The number of combinational inputs of the networks does not match.\n" );
return 1;
}
if ( Abc_NtkCoNum(pAbc->pNtkCur) != Abc_NtkCoNum(pTopo) )
{
Abc_NtkDelete( pTopo );
Abc_Print( -1, "The number of combinational outputs of the networks does not match.\n" );
return 1;
}
pTopo = Abc_NtkDupDfs( pNtkRes = pTopo );
Abc_NtkDelete( pNtkRes );
pNtkRes = Abc_NtkTopoExact( pAbc->pNtkCur, pTopo, nTimeOut, nSeed, fVerbose );
Abc_NtkDelete( pTopo );
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Command has failed.\n" );
return 0;
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: topoexact [-TS num] <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-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" );
return 1;
}
/**Function*************************************************************
Synopsis []
@ -49804,9 +49926,9 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
Vec_Int_t * vPos;
int c, nRegs = 0, iOutNum = -1, nOutRange = 1, iPartNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fExtractAll = 0, fComb = 0, fVerbose = 0;
int c, nRegs = 0, iOutNum = -1, nOutRange = 1, iPartNum = -1, iConeNum = -1, nLevelMax = 0, nTimeWindow = 0, fUseAllCis = 0, fExtractAll = 0, fComb = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWaecvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ORPLWCaecvh" ) ) != EOF )
{
switch ( c )
{
@ -49865,6 +49987,17 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nTimeWindow < 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;
}
iConeNum = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iConeNum < 1 )
goto usage;
break;
case 'a':
fUseAllCis ^= 1;
break;
@ -49917,6 +50050,17 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
}
if ( iConeNum > 0 )
{
if ( iConeNum >= Gia_ManObjNum(pAbc->pGia) || !Gia_ObjIsAnd(Gia_ManObj(pAbc->pGia, iConeNum)) )
{
Abc_Print( -1, "Abc_CommandAbc9Cone(): Object with Id %d is not a node.\n", iConeNum );
return 1;
}
pTemp = Gia_ManDupDfsNode( pAbc->pGia, Gia_ManObj(pAbc->pGia, iConeNum) );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
}
if ( iPartNum >= 0 )
{
Vec_Int_t * vClass;
@ -49957,13 +50101,14 @@ int Abc_CommandAbc9Cone( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &cone [-ORPLW num] [-aecvh]\n" );
Abc_Print( -2, "usage: &cone [-ORPLWC num] [-aecvh]\n" );
Abc_Print( -2, "\t extracting multi-output sequential logic cones\n" );
Abc_Print( -2, "\t-O num : the index of first PO to extract [default = %d]\n", iOutNum );
Abc_Print( -2, "\t-R num : (optional) the number of outputs to extract [default = %d]\n", nOutRange );
Abc_Print( -2, "\t-P num : (optional) the partition number to extract [default = %d]\n", iPartNum );
Abc_Print( -2, "\t-L num : (optional) extract cones with higher level [default = %d]\n", nLevelMax );
Abc_Print( -2, "\t-W num : (optional) extract cones falling into this window [default = %d]\n", nTimeWindow );
Abc_Print( -2, "\t-C num : (optional) extract cone of one node with ID equal to <num> [default = unused]\n" );
Abc_Print( -2, "\t-a : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" );
Abc_Print( -2, "\t-e : toggle writing all outputs into individual files [default = %s]\n", fExtractAll? "yes": "no" );
Abc_Print( -2, "\t-c : toggle performing cone extraction combinationally [default = %s]\n", fComb? "yes": "no" );

220
src/base/abci/abcTopo.c Normal file
View File

@ -0,0 +1,220 @@
/**CFile****************************************************************
FileName [abcTopo.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Network and node package.]
Synopsis [Topologically constrained exact synthesis.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: abcTopo.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "base/abc/abc.h"
#include "misc/util/utilTruth.h"
#include "sat/kissat/kissat.h"
#define KISSAT_UNSAT 20
#define KISSAT_SAT 10
#define KISSAT_UNDEC 0
static int AbcTopo_KissatTerminate( void * pData )
{
abctime * pTimeStop = (abctime *)pData;
return pTimeStop && *pTimeStop && Abc_Clock() > *pTimeStop;
}
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Exact synthesis of the MO function into a fixed-topology network.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkTopoDup( Abc_Ntk_t * pTopo, Vec_Wrd_t * vTruths )
{
Abc_Ntk_t * pNew = Abc_NtkDup(pTopo);
Abc_Obj_t * pObj; int i;
Abc_NtkForEachNode( pTopo, pObj, i ) {
extern char * Bbl_ManTruthToSop( unsigned * pTruth, int nVars );
char * pSop = Bbl_ManTruthToSop( (unsigned *)Vec_WrdEntryP(vTruths, i), Abc_ObjFaninNum(pObj) );
pObj->pData = Abc_SopRegister( (Mem_Flex_t *)pNew->pManFunc, pSop );
ABC_FREE( pSop );
}
return pNew;
}
Abc_Ntk_t * Abc_NtkTopoExact( Abc_Ntk_t * pFunc, Abc_Ntk_t * pTopo, int nTimeOut, int nSeed, 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_NtkForEachNode( pTopo, pObj, i ) {
assert( Abc_ObjFaninNum(pObj) <= 6 );
nMints += 1 << Abc_ObjFaninNum(pObj);
nNodeClausesPerMint += 2 * (1 << Abc_ObjFaninNum(pObj)); // two clauses per minterm
}
// derive input/output mapping of the original function, which will be synthesized
Gia_Man_t * pGia = Abc_NtkClpGia( pFunc );
Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pGia) );
Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( pGia, vSimsPi, 1 );
int nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(pGia);
assert( Abc_NtkCiNum(pTopo) == Gia_ManCiNum(pGia) );
assert( Abc_NtkPoNum(pTopo) == Gia_ManPoNum(pGia) );
assert( Vec_WrdSize(vSims) == Gia_ManPoNum(pGia) * nWords );
// map network objects to compact variable IDs (PIs first, then internal nodes)
Vec_Int_t * vObj2Var = Vec_IntStart( Abc_NtkObjNumMax(pTopo) );
int iMap = 0;
Abc_NtkForEachCi( pTopo, pObj, i )
Vec_IntWriteEntry( vObj2Var, Abc_ObjId(pObj), iMap++ );
Abc_NtkForEachNode( pTopo, pObj, i )
Vec_IntWriteEntry( vObj2Var, Abc_ObjId(pObj), iMap++ );
assert( iMap == Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo) );
// create Kissat SAT solver with as many variables as there are minterms
// plus additionally allocate vars to represent values of each node under each input minterm
kissat * pSat = kissat_init();
int nVarsAlloc = nMints + (1 << Abc_NtkCiNum(pTopo)) * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo));
kissat_reserve( pSat, nVarsAlloc );
if ( nSeed > 0 )
kissat_set_option( pSat, "seed", nSeed );
if ( fVerbose )
printf( "Running fixed-topology exact synthesis: PI = %d Nodes = %d PO = %d\n",
Abc_NtkCiNum(pTopo), Abc_NtkNodeNum(pTopo), Abc_NtkPoNum(pTopo) );
// for each minterm, iterate through each PI, each internal node, and each outputs
// 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);
for ( m = 0; m < nTopoMints; m++ ) {
int iVarBase = nMints + m * (Abc_NtkCiNum(pTopo) + Abc_NtkNodeNum(pTopo));
// set PI values for this minterm
Abc_NtkForEachCi( pTopo, pObj, k ) {
int fPiVal = Abc_TtGetBit( Vec_WrdArray(vSimsPi) + k * nWords, m );
int iPiVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pObj) );
int Lit = Abc_Var2Lit( iPiVar, !fPiVal );
kissat_add( pSat, Abc_LitIsCompl(Lit) ? -(Abc_Lit2Var(Lit) + 1) : (Abc_Lit2Var(Lit) + 1) );
kissat_add( pSat, 0 );
}
// for each internal node
int iMint = 0;
Abc_NtkForEachNode( pTopo, pObj, n ) {
int nFanins = Abc_ObjFaninNum(pObj);
int iNodeMintBase = iMint;
int iNodeVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pObj) );
// for each configuration of fanin values
for ( k = 0; k < (1 << nFanins); k++ ) {
// add clauses for both polarities of the node output
for ( int v = 0; v < 2; v++ ) {
int pLits[8], nLits = 0;
// add literal for the truth table variable (minterm k of this node)
pLits[nLits++] = Abc_Var2Lit( iNodeMintBase + k, v );
// add literal for the node output value
pLits[nLits++] = Abc_Var2Lit( iNodeVar, !v );
// check fanin values match minterm k
Abc_Obj_t * pFanin;
Abc_ObjForEachFanin( pObj, pFanin, f ) {
int iFaninVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pFanin) );
int fFaninVal = (k >> f) & 1;
pLits[nLits++] = Abc_Var2Lit( iFaninVar, !fFaninVal );
}
// add clause
for ( i = 0; i < nLits; i++ )
kissat_add( pSat, Abc_LitIsCompl(pLits[i]) ? -(Abc_Lit2Var(pLits[i]) + 1) : (Abc_Lit2Var(pLits[i]) + 1) );
kissat_add( pSat, 0 );
}
}
iMint += 1 << nFanins;
}
assert( iMint == nMints );
// constrain primary outputs to match the target function
Abc_NtkForEachPo( pTopo, pObj, n ) {
Abc_Obj_t * pDriver = Abc_ObjFanin0(pObj);
int iDriverVar = iVarBase + Vec_IntEntry( vObj2Var, Abc_ObjId(pDriver) );
// get expected output value from simulation and add unit clause
int fExpected = Abc_TtGetBit( Vec_WrdArray(vSims) + n * nWords, m );
int Lit = Abc_Var2Lit( iDriverVar, !fExpected );
kissat_add( pSat, Abc_LitIsCompl(Lit) ? -(Abc_Lit2Var(Lit) + 1) : (Abc_Lit2Var(Lit) + 1) );
kissat_add( pSat, 0 );
}
}
if ( fVerbose )
printf( "Minterm variables = %d. Internal variables = %d. Clauses = %d.\n", nMints, nVarsAlloc - nMints, nClauses );
abctime timeStop = 0;
if ( nTimeOut )
{
timeStop = Abc_Clock() + (abctime)nTimeOut * CLOCKS_PER_SEC;
kissat_set_terminate( pSat, &timeStop, AbcTopo_KissatTerminate );
}
else
kissat_set_terminate( pSat, NULL, NULL );
int status = kissat_solve( pSat );
if ( status == KISSAT_SAT )
{
// if it is satisfiable, collect the satisfying assignment into the array
Vec_Wrd_t * vTruths = Vec_WrdStart( Abc_NtkObjNumMax(pTopo) );
int iMint = 0;
Abc_NtkForEachNode( pTopo, pObj, i ) {
// iMint shows the first SAT variable of this node
// collect values into Truth
word TruthSmall = 0;
for ( int v = 0; v < (1 << Abc_ObjFaninNum(pObj)); v++ )
if ( kissat_value( pSat, iMint + v + 1 ) > 0 )
TruthSmall |= (word)1 << v;
// increment the minterm counter
iMint += 1 << Abc_ObjFaninNum(pObj);
// save the result into the array of truth tables
Vec_WrdWriteEntry( vTruths, i, Abc_Tt6Stretch( TruthSmall, Abc_ObjFaninNum(pObj) ) );
if ( fVerbose ) {
int nDigits = 1 << (Abc_ObjFaninNum(pObj)-2);
printf( "Node %2d (fanins = %d) 0x%0*lx\n", i, Abc_ObjFaninNum(pObj), nDigits, TruthSmall );
}
}
assert( iMint == nMints );
// create network with the corresponding truth tables
pRes = Abc_NtkTopoDup( pTopo, vTruths );
Vec_WrdFree( vTruths );
if ( fVerbose )
printf( "The problem has a solution.\n" );
}
else if ( status == KISSAT_UNSAT && fVerbose )
printf( "The problem has no solution.\n" );
else if ( status == KISSAT_UNDEC && fVerbose )
printf( "The solver returned unknown.\n" );
kissat_release( pSat );
Vec_WrdFree( vSims );
Vec_WrdFree( vSimsPi );
Vec_IntFree( vObj2Var );
Gia_ManStop( pGia );
if ( fVerbose )
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/base/abci/module.make
View File

@ -71,6 +71,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcSymm.c \
src/base/abci/abcTim.c \
src/base/abci/abcTiming.c \
src/base/abci/abcTopo.c \
src/base/abci/abcUnate.c \
src/base/abci/abcUnreach.c \
src/base/abci/abcVerify.c \

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

@ -75,12 +75,14 @@ struct Bmc_EsPar_t_
int Seed;
int n1HotAlgo;
int fDumpBlif;
int fGenTruths;
int fVerbose;
int fSilent;
char * pTtStr;
char * pSymStr;
char * pPermStr;
char * pGuide;
Vec_Wrd_t* vTruths;
};
static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )

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

@ -389,6 +389,50 @@ static inline int Exa8_ManEval( Exa8_Man_t * p )
SeeAlso []
***********************************************************************/
static Vec_Wrd_t * Exa8_ManSaveTruthTables( Exa8_Man_t * p, int fCompl )
{
int i, k, nWordsNode, nMintsNode;
assert( p->nLutSize <= 8 );
nMintsNode = 1 << p->nLutSize;
nWordsNode = (p->nLutSize <= 6) ? 1 : (p->nLutSize == 7 ? 2 : 4);
Vec_Wrd_t * vTruths = Vec_WrdStart( p->nObjs * nWordsNode );
for ( i = p->nVars; i < p->nObjs; i++ )
{
word Truth[4] = {0, 0, 0, 0};
int iVarStart = 1 + p->LutMask*(i - p->nVars);
for ( k = 0; k < p->LutMask; k++ )
{
if ( Exa8_KissatVarValue( p, iVarStart + k ) )
{
int bit = k + 1; // minterm index (minterm 0 is fixed to 0)
int w = bit >> 6;
int b = bit & 63;
Truth[w] |= ((word)1 << b);
}
}
// complement the output fully if needed (including minterm 0)
if ( i == p->nObjs - 1 && fCompl )
{
for ( int w = 0; w < nWordsNode; w++ )
{
word Mask;
int rem = nMintsNode - w * 64;
if ( rem <= 0 )
Mask = 0;
else if ( rem >= 64 )
Mask = ~(word)0;
else
Mask = (((word)1) << rem) - 1;
Truth[w] = (~Truth[w]) & Mask;
}
}
if ( p->nLutSize < 6 )
Truth[0] = Abc_Tt6Stretch( Truth[0], p->nLutSize );
for ( int w = 0; w < nWordsNode; w++ )
Vec_WrdWriteEntry( vTruths, i * nWordsNode + w, Truth[w] );
}
return vTruths;
}
static void Exa8_ManPrintSolution( Exa8_Man_t * p, int fCompl )
{
int i, k, iVar;
@ -692,7 +736,7 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
ABC_FREE( pFun );
}
if ( pPars->pTtStr )
if ( pPars->pTtStr && pPars->nVars <= 7 )
Abc_TtReadHex( pTruth, pPars->pTtStr );
else assert( 0 );
if ( pPars->fUseIncr && !pPars->fSilent )
@ -741,6 +785,11 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
printf( "\".\n" );
if ( pPars->fDumpBlif )
Exa8_ManDumpBlif( p, fCompl );
if ( p->pPars->fGenTruths ) {
if ( p->pPars->vTruths )
Vec_WrdFreeP( &p->pPars->vTruths );
p->pPars->vTruths = Exa8_ManSaveTruthTables( p, fCompl );
}
Res = 1;
}
else if ( status == KISSAT_UNSAT )
@ -845,6 +894,46 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
return Result;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars )
{
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
pPars->fKissat = 1;
pPars->fLutCascade = 1;
pPars->fMinNodes = 1;
pPars->fUsePerm = 1;
pPars->fGenTruths = 1;
pPars->nLutSize = 6;
int v, o, nOuts = Abc_Base2Log(nVars+1);
Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts );
for ( o = 0; o < nOuts; o++ ) {
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 );
if ( status != 1 ) {
printf( "Synthesis failed for output %d.\n", o );
break;
}
Vec_PtrPush( vRes, pPars->vTruths );
pPars->vTruths = NULL;
}
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////