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

Command "andexact".

This commit is contained in:
Alan Mishchenko 2025-12-03 13:39:13 -08:00
parent 5e58e34f6c
commit b7f8df0941
5 changed files with 1197 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
src/aig/gia/giaTim.c
View File

@ -953,20 +953,6 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v
***********************************************************************/
/*
› Please have a look at how name mapping is done in procedure Abc_FrameReadMiniLutNameMapping() in file "src/aig/gia/
giaMini.c". The main idea is to map the object IDs in the design after synthesis (pAbc->pGiaMiniLut) into the object IDs in
the design before synthesis (pAbc->pGiaMiniAig). The computation is divided into three steps: (1) computing object
equivalences using Gia_ManComputeGiaEquivs(), which annotates the input AIG (pGia) containing both designs before and after
synthesis with equivalence class information; this information contains equivalence classes of objects from both designs; (2)
creating a map (pRes) of the resulting object IDs (in pAbc->pGiaMiniLut) into the original object IDs (in pAbc->pGiaMiniAig)
using procedure Gia_ManMapMiniLut2MiniAig(); this map is enabled by having two arrays (one of them is pAbc->vCopyMiniAig
mapping objects of pAbc->pGiaMiniAig in the original object IDs; the other one is pAbc->vCopyMiniLut mapping objects of
pAbc->pGiaMiniLut into the IDs of pAbc->pGiaMiniLut); (3) verification procedure (commented out by default)
Gia_ManNameMapVerify() which checks that the resulting mapping computed by Gia_ManMapMiniLut2MiniAig() is correct. Please
let me know if this computation is clear.
*/
Vec_Int_t * Gia_ManVerifyFindNameMapping( Gia_Man_t * p, Gia_Man_t * p1, Gia_Man_t * p2, Vec_Int_t * vMap1, Vec_Int_t * vMap2 )
{
Vec_Int_t * vRes = Vec_IntStartFull(Vec_IntSize(vMap2));

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

@ -172,6 +172,7 @@ static int Abc_CommandBmsPs ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandMajExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTwoExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
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_CommandTestExact ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMajGen ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1002,6 +1003,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Exact synthesis", "majexact", Abc_CommandMajExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "twoexact", Abc_CommandTwoExact, 0 );
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", "testexact", Abc_CommandTestExact, 0 );
Cmd_CommandAdd( pAbc, "Exact synthesis", "majgen", Abc_CommandMajGen, 0 );
@ -10992,7 +10994,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv )
usage:
Abc_Print( -2, "usage: lutexact [-NMKTFUS <num>] [-Y string] [-P string] [-iaorfgckdsmpvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" );
Abc_Print( -2, "\t exact synthesis of N-input function using M K-input lookup-tables\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 );
Abc_Print( -2, "\t-K <num> : the number of node fanins [default = %d]\n", pPars->nLutSize );
@ -11020,6 +11022,186 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAndExact( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Exa9_ManExactSynthesis( Bmc_EsPar_t * pPars );
extern int Exa9_ManExactSynthesisIter( Bmc_EsPar_t * pPars );
extern char * Abc_NtkReadTruth( Abc_Ntk_t * pNtk );
int c;
Bmc_EsPar_t Pars, * pPars = &Pars;
Bmc_EsParSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NMTSHYiadsmvh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
pPars->nVars = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->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;
}
pPars->nNodes = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nNodes < 0 )
goto usage;
break;
case 'T':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
goto usage;
}
pPars->RuntimeLim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->RuntimeLim < 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;
}
pPars->Seed = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->Seed < 0 )
goto usage;
break;
case 'H':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-H\" should be followed by a string.\n" );
goto usage;
}
pPars->n1HotAlgo = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
break;
case 'Y':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" );
goto usage;
}
pPars->pSymStr = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'i':
pPars->fUseIncr ^= 1;
break;
case 'a':
pPars->fOnlyAnd ^= 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;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc == globalUtilOptind + 1 )
pPars->pTtStr = argv[globalUtilOptind];
else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
{
pPars->pTtStr = Abc_NtkReadTruth( Abc_FrameReadNtk(pAbc) );
if ( pPars->pTtStr )
pPars->nVars = Abc_NtkCiNum(Abc_FrameReadNtk(pAbc));
}
if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 )
{
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) );
return 1;
}
if ( pPars->nVars > pPars->nNodes + 1 )
{
Abc_Print( -1, "Function with %d variales cannot be implemented with %d two-input nodes.\n", pPars->nVars, pPars->nNodes );
return 1;
}
if ( pPars->nVars > 14 )
{
Abc_Print( -1, "Function should not have more than 14 inputs.\n" );
return 1;
}
if ( pPars->nNodes > 16 )
{
Abc_Print( -1, "Node count cannot be more than 16 inputs.\n" );
return 1;
}
if ( pPars->fMinNodes )
Exa9_ManExactSynthesisIter( pPars );
else
Exa9_ManExactSynthesis( pPars );
if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) )
ABC_FREE( pPars->pTtStr );
return 0;
usage:
Abc_Print( -2, "usage: andexact [-NMTSH <num>] [-Y str] [-iadmsvh] <hex>\n" );
Abc_Print( -2, "\t exact synthesis of N-input function using two-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 two-input nodes [default = %d]\n", pPars->nNodes );
Abc_Print( -2, "\t-T <num> : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim );
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-H <num> : the 1-hotness algorithm used (0 = naive; 1 = seq; 2 = bim; 3 = cmd) [default = %d]\n", pPars->n1HotAlgo );
Abc_Print( -2, "\t-Y <str> : charasteristic string of a symmetric function [default = %s]\n", pPars->pSymStr ? pPars->pSymStr : "unused" );
Abc_Print( -2, "\t-i : toggle using incremental SAT (CEGAR over minterms) [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-m : toggle minimum-node solution possibly smaller than \"-M <num>\" [default = %s]\n", pPars->fMinNodes ? "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-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" );
return 1;
}
/**Function*************************************************************
Synopsis []

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

@ -73,6 +73,7 @@ struct Bmc_EsPar_t_
int nRandFuncs;
int nMintNum;
int Seed;
int n1HotAlgo;
int fDumpBlif;
int fVerbose;
int fSilent;
@ -102,6 +103,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
pPars->fUniqFans = 0;
pPars->fLutCascade = 0;
pPars->RuntimeLim = 0;
pPars->n1HotAlgo = 1;
pPars->fVerbose = 0;
}
@ -274,4 +276,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1011
src/sat/bmc/bmcMaj9.c Normal file
View File

File diff suppressed because it is too large Load Diff

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

@ -27,6 +27,7 @@ SRC += src/sat/bmc/bmcBCore.c \
src/sat/bmc/bmcMaj3.c \
src/sat/bmc/bmcMaj7.c \
src/sat/bmc/bmcMaj8.c \
src/sat/bmc/bmcMaj9.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMesh.c \
src/sat/bmc/bmcMesh2.c \