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

Experiments with recent ideas.

This commit is contained in:
Alan Mishchenko 2014-03-20 20:18:25 -07:00
parent b581e16f32
commit c86a13f0b5
7 changed files with 503 additions and 280 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
abclib.dsp
View File

@ -1419,6 +1419,10 @@ SOURCE=.\src\sat\bmc\bmcBmcAnd.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\bmc\bmcBmci.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcCexCut.c SOURCE=.\src\sat\bmc\bmcCexCut.c
# End Source File # End Source File
# Begin Source File # Begin Source File
@ -1447,7 +1451,7 @@ SOURCE=.\src\sat\bmc\bmcICheck.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\bmc\bmcLilac.c SOURCE=.\src\sat\bmc\bmcInse.c
# End Source File # End Source File
# Begin Source File # Begin Source File
@ -1455,11 +1459,11 @@ SOURCE=.\src\sat\bmc\bmcLoad.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\bmc\bmcMulti.c SOURCE=.\src\sat\bmc\bmcMaxi.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\sat\bmc\bmcTulip.c SOURCE=.\src\sat\bmc\bmcMulti.c
# End Source File # End Source File
# Begin Source File # Begin Source File

20
src/aig/gia/giaMan.c
View File

@ -305,12 +305,16 @@ void Gia_ManPrintTents( Gia_Man_t * p )
void Gia_ManPrintInitClasses( Vec_Int_t * vInits ) void Gia_ManPrintInitClasses( Vec_Int_t * vInits )
{ {
int i, Value; int i, Value;
int Counts[4] = {0}; int Counts[6] = {0};
Vec_IntForEachEntry( vInits, Value, i ) Vec_IntForEachEntry( vInits, Value, i )
Counts[Value]++; Counts[Value]++;
for ( i = 0; i < 4; i++ ) for ( i = 0; i < 6; i++ )
printf( "%d = %d ", i, Counts[i] ); if ( Counts[i] )
printf( "X = %d\n", Counts[2] + Counts[3] ); printf( "%d = %d ", i, Counts[i] );
printf( " " );
printf( "B = %d ", Counts[0] + Counts[1] );
printf( "X = %d ", Counts[2] + Counts[3] );
printf( "Q = %d\n", Counts[4] + Counts[5] );
Vec_IntForEachEntry( vInits, Value, i ) Vec_IntForEachEntry( vInits, Value, i )
{ {
Counts[Value]++; Counts[Value]++;
@ -319,9 +323,13 @@ void Gia_ManPrintInitClasses( Vec_Int_t * vInits )
else if ( Value == 1 ) else if ( Value == 1 )
printf( "1" ); printf( "1" );
else if ( Value == 2 ) else if ( Value == 2 )
printf( "x" ); printf( "2" );
else if ( Value == 3 ) else if ( Value == 3 )
printf( "X" ); printf( "3" );
else if ( Value == 4 )
printf( "4" );
else if ( Value == 5 )
printf( "5" );
else assert( 0 ); else assert( 0 );
} }
printf( "\n" ); printf( "\n" );

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

@ -399,8 +399,9 @@ static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Tulip ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Lilac ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9PoPart2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv ); //static int Abc_CommandAbc9CexMerge ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -964,8 +965,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&tulip", Abc_CommandAbc9Tulip, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&lilac", Abc_CommandAbc9Lilac, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 ); // Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
@ -32751,9 +32753,104 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Inse( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); extern Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
int c, nFrames = 10, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
{
switch ( c )
{
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
nFrames = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFrames < 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
goto usage;
}
nWords = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nWords < 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;
}
nTimeOut = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut < 0 )
goto usage;
break;
case 's':
fSim ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Inse(): There is no AIG.\n" );
return 0;
}
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{
Abc_Print( -1, "Abc_CommandAbc9Inse(): AIG is combinational.\n" );
return 0;
}
if ( pAbc->pGia->vInitClasses != NULL )
{
Abc_Print( 1, "Abc_CommandAbc9Inse(): All-0 initial state is assumed.\n" );
Vec_IntFreeP( &pAbc->pGia->vInitClasses );
}
pAbc->pGia->vInitClasses = Gia_ManInseTest( pAbc->pGia, NULL, nFrames, nWords, nTimeOut, fSim, fVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &inse [-FWT num] [-svh]\n" );
Abc_Print( -2, "\t experimental procedure\n" );
Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords );
Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-s : toggles using ternary simulation [default = %s]\n", fSim? "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 []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Maxi( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
Vec_Int_t * vTemp; Vec_Int_t * vTemp;
int c, nFrames = 5, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0; int c, nFrames = 5, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
@ -32808,20 +32905,20 @@ int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9Tulip(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Maxi(): There is no AIG.\n" );
return 0; return 0;
} }
if ( Gia_ManRegNum(pAbc->pGia) == 0 ) if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{ {
Abc_Print( -1, "Abc_CommandAbc9Tulip(): AIG is combinational.\n" ); Abc_Print( -1, "Abc_CommandAbc9Maxi(): AIG is combinational.\n" );
return 0; return 0;
} }
pAbc->pGia->vInitClasses = Gia_ManTulipTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); pAbc->pGia->vInitClasses = Gia_ManMaxiTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
Vec_IntFreeP( &vTemp ); Vec_IntFreeP( &vTemp );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &tulip [-FWT num] [-svh]\n" ); Abc_Print( -2, "usage: &maxi [-FWT num] [-svh]\n" );
Abc_Print( -2, "\t experimental procedure\n" ); Abc_Print( -2, "\t experimental procedure\n" );
Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords ); Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords );
@ -32843,9 +32940,9 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9Bmci( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ); extern int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0; int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
@ -32899,24 +32996,24 @@ int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( pAbc->pGia == NULL ) if ( pAbc->pGia == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9Lilac(): There is no AIG.\n" ); Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
return 0; return 0;
} }
if ( Gia_ManRegNum(pAbc->pGia) == 0 ) if ( Gia_ManRegNum(pAbc->pGia) == 0 )
{ {
Abc_Print( -1, "Abc_CommandAbc9Lilac(): AIG is combinational.\n" ); Abc_Print( -1, "Abc_CommandAbc9Bmci(): AIG is combinational.\n" );
return 0; return 0;
} }
if ( pAbc->pGia->vInitClasses == NULL ) if ( pAbc->pGia->vInitClasses == NULL )
{ {
Abc_Print( -1, "Abc_CommandAbc9Lilac(): Init array is not given.\n" ); Abc_Print( -1, "Abc_CommandAbc9Bmci(): Init array is not given.\n" );
return 0; return 0;
} }
Gia_ManLilacTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose ); Gia_ManBmciTest( pAbc->pGia, pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &lilac [-FWT num] [-svh]\n" ); Abc_Print( -2, "usage: &bmci [-FWT num] [-svh]\n" );
Abc_Print( -2, "\t experimental procedure\n" ); Abc_Print( -2, "\t experimental procedure\n" );
Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames ); Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames );
Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords ); Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n", nWords );

28
src/sat/bmc/bmcLilac.c → src/sat/bmc/bmcBmci.c
View File

@ -1,6 +1,6 @@
/**CFile**************************************************************** /**CFile****************************************************************
FileName [bmcLilac.c] FileName [bmcBmci.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.] Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcLilac.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: bmcBmci.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
@ -88,7 +88,7 @@ static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPl
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse ) void Bmc_BmciUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int fPiReuse )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i; int i;
@ -115,7 +115,7 @@ void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) int Bmc_BmciPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
{ {
Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew );
int iLitPart0, iLitPart1, iRes; int iLitPart0, iLitPart1, iRes;
@ -129,8 +129,8 @@ int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Ma
return iRes; return iRes;
} }
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies ); iLitPart0 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies ); iLitPart1 = Bmc_BmciPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) ); iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) );
iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) ); iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) );
Vec_IntPush( vPartMap, iIdNew ); Vec_IntPush( vPartMap, iIdNew );
@ -138,7 +138,7 @@ int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Ma
Vec_IntWriteEntry( vCopies, iIdNew, iRes ); Vec_IntWriteEntry( vCopies, iIdNew, iRes );
return iRes; return iRes;
} }
Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies ) Gia_Man_t * Bmc_BmciPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
{ {
Gia_Man_t * pPart; Gia_Man_t * pPart;
int i, iLit, iLitPart; int i, iLit, iLitPart;
@ -153,7 +153,7 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM
if ( iLit == -1 ) if ( iLit == -1 )
continue; continue;
assert( iLit >= 2 ); assert( iLit >= 2 );
iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies ); iLitPart = Bmc_BmciPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) ); Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) );
Vec_IntPush( vPartMap, -1 ); Vec_IntPush( vPartMap, -1 );
} }
@ -173,7 +173,7 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose ) int Bmc_BmciPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose )
{ {
int nSatVars = 1; int nSatVars = 1;
Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies; Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies;
@ -210,8 +210,8 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
for ( f = 0; f < nFrames; f++ ) for ( f = 0; f < nFrames; f++ )
{ {
abctime clk = Abc_Clock(); abctime clk = Abc_Clock();
Bmc_LilacUnfold( pNew, p, vLits0, 0 ); Bmc_BmciUnfold( pNew, p, vLits0, 0 );
Bmc_LilacUnfold( pNew, p, vLits1, 1 ); Bmc_BmciUnfold( pNew, p, vLits1, 1 );
assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) ); assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) );
nMiters = 0; nMiters = 0;
Vec_IntClear( vMiters ); Vec_IntClear( vMiters );
@ -228,7 +228,7 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
break; break;
} }
// create new part // create new part
pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies ); pPart = Bmc_BmciPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
pCnf = Cnf_DeriveGiaRemapped( pPart ); pCnf = Cnf_DeriveGiaRemapped( pPart );
Cnf_DataLiftGia( pCnf, pPart, nSatVars ); Cnf_DataLiftGia( pCnf, pPart, nSatVars );
nSatVars += pCnf->nVars; nSatVars += pCnf->nVars;
@ -327,10 +327,10 @@ cleanup:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose ) int Gia_ManBmciTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
{ {
Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) ); Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose ); Bmc_BmciPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
Vec_IntFree( vInit0 ); Vec_IntFree( vInit0 );
return 1; return 1;
} }

307
src/sat/bmc/bmcTulip.c → src/sat/bmc/bmcInse.c
View File

@ -1,6 +1,6 @@
/**CFile**************************************************************** /**CFile****************************************************************
FileName [bmcTulip.c] FileName [bmcInse.c]
SystemName [ABC: Logic synthesis and verification system.] SystemName [ABC: Logic synthesis and verification system.]
@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.] Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcTulip.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] Revision [$Id: bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/ ***********************************************************************/
@ -49,7 +49,7 @@ static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id ) { return (wor
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit ) void Gia_ManInseInit( Gia_Man_t * p, Vec_Int_t * vInit )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
word * pData1, * pData0; word * pData1, * pData0;
@ -69,7 +69,7 @@ void Gia_ManRoseInit( Gia_Man_t * p, Vec_Int_t * vInit )
pData0[i] = pData1[i] = 0; pData0[i] = pData1[i] = 0;
} }
} }
void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id ) void Gia_ManInseSimulateObj( Gia_Man_t * p, int Id )
{ {
Gia_Obj_t * pObj = Gia_ManObj( p, Id ); Gia_Obj_t * pObj = Gia_ManObj( p, Id );
word * pData0, * pDataA0, * pDataB0; word * pData0, * pDataA0, * pDataB0;
@ -170,7 +170,7 @@ void Gia_ManRoseSimulateObj( Gia_Man_t * p, int Id )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost ) int Gia_ManInseHighestScore( Gia_Man_t * p, int * pCost )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
word * pData0, * pData1; word * pData0, * pData1;
@ -195,7 +195,7 @@ int Gia_ManRoseHighestScore( Gia_Man_t * p, int * pCost )
ABC_FREE( pCounts ); ABC_FREE( pCounts );
return iPat; return iPat;
} }
void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat ) void Gia_ManInseFindStarting( Gia_Man_t * p, int iPat, Vec_Int_t * vInit, Vec_Int_t * vInputs )
{ {
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
word * pData0, * pData1; word * pData0, * pData1;
@ -214,6 +214,53 @@ void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
else else
Vec_IntPush( vInit, 2 ); Vec_IntPush( vInit, 2 );
} }
Gia_ManForEachPi( p, pObj, k )
{
pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
pData1 = pData0 + p->iData;
for ( i = 0; i < p->iData; i++ )
assert( (pData0[i] & pData1[i]) == 0 );
if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
Vec_IntPush( vInputs, 0 );
else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
Vec_IntPush( vInputs, 1 );
else
Vec_IntPush( vInputs, 2 );
}
}
Vec_Int_t * Gia_ManInseSimulate( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInputs, Vec_Int_t * vInit )
{
Vec_Int_t * vRes;
Gia_Obj_t * pObj, * pObjRo, * pObjRi;
int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
int i, f, iBit = 0;
assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
Gia_ManConst0(p)->fMark0 = 0;
Gia_ManForEachRi( p, pObj, i )
pObj->fMark0 = Vec_IntEntry(vInit0, i);
for ( f = 0; f < nFrames; f++ )
{
Gia_ManForEachPi( p, pObj, i )
pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
Gia_ManForEachAnd( p, pObj, i )
pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
Gia_ManForEachRi( p, pObj, i )
pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
pObjRo->fMark0 = pObjRi->fMark0;
}
assert( iBit == Vec_IntSize(vInputs) );
vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
Gia_ManForEachRo( p, pObj, i )
Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
Gia_ManForEachObj( p, pObj, i )
pObj->fMark0 = 0;
return vRes;
} }
/**Function************************************************************* /**Function*************************************************************
@ -227,18 +274,19 @@ void Gia_ManRoseFindStarting( Gia_Man_t * p, Vec_Int_t * vInit, int iPat )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose ) Vec_Int_t * Gia_ManInsePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int fVerbose )
{ {
Vec_Int_t * vInit; Vec_Int_t * vRes, * vInit, * vInputs;
Gia_Obj_t * pObj; Gia_Obj_t * pObj;
int i, f, iPat, Cost, Cost0; int i, f, iPat, Cost, Cost0;
abctime clk, clkTotal = Abc_Clock(); abctime clk, clkTotal = Abc_Clock();
Gia_ManRandomW( 1 ); Gia_ManRandomW( 1 );
if ( fVerbose ) if ( fVerbose )
printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " ); printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
vInit = Vec_IntDup(vInit0); vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
Gia_ParTestAlloc( p, nWords ); Gia_ParTestAlloc( p, nWords );
Gia_ManRoseInit( p, vInit ); Gia_ManInseInit( p, vInit );
Cost0 = 0; Cost0 = 0;
Vec_IntForEachEntry( vInit, iPat, i ) Vec_IntForEachEntry( vInit, iPat, i )
Cost0 += ((iPat >> 1) & 1); Cost0 += ((iPat >> 1) & 1);
@ -248,43 +296,22 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames,
{ {
clk = Abc_Clock(); clk = Abc_Clock();
Gia_ManForEachObj( p, pObj, i ) Gia_ManForEachObj( p, pObj, i )
Gia_ManRoseSimulateObj( p, i ); Gia_ManInseSimulateObj( p, i );
iPat = Gia_ManRoseHighestScore( p, &Cost ); iPat = Gia_ManInseHighestScore( p, &Cost );
Gia_ManRoseFindStarting( p, vInit, iPat ); Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
Gia_ManRoseInit( p, vInit ); Gia_ManInseInit( p, vInit );
if ( fVerbose ) if ( fVerbose )
printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 ); printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 );
if ( fVerbose ) if ( fVerbose )
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
} }
Gia_ParTestFree( p ); Gia_ParTestFree( p );
vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
Vec_IntFreeP( &vInit );
Vec_IntFreeP( &vInputs );
printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) ); printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal ); Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
// printf( "The resulting init state is invalid.\n" ); return vRes;
Vec_IntFreeP( &vInit );
return vInit;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
} }
/**Function************************************************************* /**Function*************************************************************
@ -298,207 +325,11 @@ static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Gia_Man_t * Gia_ManTulipUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit ) Vec_Int_t * Gia_ManInseTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, f;
pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
// control/data variables
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
// build timeframes
assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
{
if ( Vec_IntEntry(vInit, i) == 0 )
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 0;
else if ( Vec_IntEntry(vInit, i) == 1 )
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i)) : 1;
else if ( Vec_IntEntry(vInit, i) == 2 )
pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
else if ( Vec_IntEntry(vInit, i) == 3 )
pObj->Value = Gia_ManHashAnd(pNew, Gia_ManCiLit(pNew, i), Gia_ManCiLit(pNew, Gia_ManRegNum(p)+i));
else assert( 0 );
}
for ( f = 0; f < nFrames; f++ )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
}
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
{
int nIterMax = 1000000;
int i, iLit, Iter, status;
int nLits, * pLits;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
Vec_Int_t * vLits, * vMap;
sat_solver * pSat;
Gia_Obj_t * pObj;
Gia_Man_t * p0 = Gia_ManTulipUnfold( p, nFrames, 0, vInit );
Gia_Man_t * p1 = Gia_ManTulipUnfold( p, nFrames, 1, vInit );
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
Gia_ManStop( p0 );
Gia_ManStop( p1 );
assert( Gia_ManRegNum(p) > 0 );
if ( fVerbose )
printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// add one large OR clause
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( pM, pObj, i )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
// create assumptions
Vec_IntClear( vLits );
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( !(Vec_IntEntry(vInit, i) & 2) )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
if ( fVerbose )
{
printf( "Iter%6d : ", 0 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", Vec_IntSize(vLits) );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
for ( Iter = 0; Iter < nIterMax; Iter++ )
{
abctime clk = Abc_Clock();
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
clkSat += Abc_Clock() - clk;
if ( status == l_Undef )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
break;
}
if ( status == l_True )
{
// if ( fVerbose )
// printf( "\n" );
printf( "The problem is SAT after %d iterations. ", Iter );
break;
}
assert( status == l_False );
nLits = sat_solver_final( pSat, &pLits );
if ( fVerbose )
{
printf( "Iter%6d : ", Iter+1 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", nLits );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
if ( Vec_IntSize(vLits) == nLits )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
break;
}
// collect used literals
Vec_IntClear( vLits );
for ( i = 0; i < nLits; i++ )
Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
}
// create map
vMap = Vec_IntStart( pCnf->nVars );
Vec_IntForEachEntry( vLits, iLit, i )
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
// create output
Vec_IntFree( vLits );
vLits = Vec_IntDup(vInit);
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( !(Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
Vec_IntFree( vMap );
// cleanup
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pM );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return vLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
{ {
Vec_Int_t * vRes, * vInit; Vec_Int_t * vRes, * vInit;
if ( fSim ) vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
{ vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose );
}
else
{
vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose );
}
if ( vInit != vInit0 ) if ( vInit != vInit0 )
Vec_IntFree( vInit ); Vec_IntFree( vInit );
return vRes; return vRes;

282
src/sat/bmc/bmcMaxi.c Normal file
View File

@ -0,0 +1,282 @@
/**CFile****************************************************************
FileName [bmcMaxi.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based bounded model checking.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: bmcMaxi.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
{
Cnf_Dat_t * pCnf;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
pAig->nRegs = 0;
pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
Aig_ManStop( pAig );
return pCnf;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManMaxiUnfold( Gia_Man_t * p, int nFrames, int fUseVars, Vec_Int_t * vInit )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, f;
pNew = Gia_ManStart( fUseVars * 2 * Gia_ManRegNum(p) + nFrames * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
Gia_ManConst0(p)->Value = 0;
// control/data variables
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
Gia_ManForEachRo( p, pObj, i )
Gia_ManAppendCi( pNew );
// build timeframes
assert( !vInit || Vec_IntSize(vInit) == Gia_ManRegNum(p) );
Gia_ManForEachRo( p, pObj, i )
{
int Value = Vec_IntEntry( vInit, i );
int iCtrl = Gia_ManCiLit( pNew, i );
int iData = Gia_ManCiLit( pNew, Gia_ManRegNum(p)+i );
// decide based on Value
if ( Value == 0 )
pObj->Value = fUseVars ? Gia_ManHashAnd(pNew, iCtrl, iData) : 0;
else if ( Value == 1 )
pObj->Value = fUseVars ? Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData) : 1;
else if ( Value == 2 )
pObj->Value = Gia_ManHashAnd(pNew, iCtrl, iData);
else if ( Value == 3 )
pObj->Value = Gia_ManHashOr(pNew, Abc_LitNot(iCtrl), iData);
else if ( Value == 4 )
pObj->Value = 0;
else if ( Value == 5 )
pObj->Value = 1;
else assert( 0 );
}
for ( f = 0; f < nFrames; f++ )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ObjFanin0Copy(pObj);
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
}
Gia_ManForEachRi( p, pObj, i )
pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == 2 * Gia_ManRegNum(p) + nFrames * Gia_ManPiNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMaxiPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nTimeOut, int fVerbose )
{
int nIterMax = 1000000;
int i, iLit, Iter, status;
int nLits, * pLits;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
Vec_Int_t * vLits, * vMap;
sat_solver * pSat;
Gia_Obj_t * pObj;
Gia_Man_t * p0 = Gia_ManMaxiUnfold( p, nFrames, 0, vInit );
Gia_Man_t * p1 = Gia_ManMaxiUnfold( p, nFrames, 1, vInit );
Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM );
Gia_ManStop( p0 );
Gia_ManStop( p1 );
assert( Gia_ManRegNum(p) > 0 );
if ( fVerbose )
printf( "Running with %d frames and %sgiven init state.\n", nFrames, vInit ? "":"no " );
pSat = sat_solver_new();
sat_solver_setnvars( pSat, pCnf->nVars );
sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
assert( 0 );
// add one large OR clause
vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
Gia_ManForEachCo( pM, pObj, i )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
// create assumptions
Vec_IntClear( vLits );
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( Vec_IntEntry(vInit, i) == 0 || Vec_IntEntry(vInit, i) == 1 )
Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1) );
if ( fVerbose )
{
printf( "Iter%6d : ", 0 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", Vec_IntSize(vLits) );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
for ( Iter = 0; Iter < nIterMax; Iter++ )
{
abctime clk = Abc_Clock();
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
clkSat += Abc_Clock() - clk;
if ( status == l_Undef )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Timeout reached after %d seconds and %d iterations. ", nTimeOut, Iter );
break;
}
if ( status == l_True )
{
// if ( fVerbose )
// printf( "\n" );
printf( "The problem is SAT after %d iterations. ", Iter );
break;
}
assert( status == l_False );
nLits = sat_solver_final( pSat, &pLits );
if ( fVerbose )
{
printf( "Iter%6d : ", Iter+1 );
printf( "Var =%10d ", sat_solver_nvars(pSat) );
printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
printf( "Subset =%6d ", nLits );
Abc_PrintTime( 1, "Time", clkSat );
// ABC_PRTr( "Solver time", clkSat );
}
if ( Vec_IntSize(vLits) == nLits )
{
// if ( fVerbose )
// printf( "\n" );
printf( "Reached fixed point with %d entries after %d iterations. ", Vec_IntSize(vLits), Iter+1 );
break;
}
// collect used literals
Vec_IntClear( vLits );
for ( i = 0; i < nLits; i++ )
Vec_IntPush( vLits, Abc_LitNot(pLits[i]) );
}
// create map
vMap = Vec_IntStart( pCnf->nVars );
Vec_IntForEachEntry( vLits, iLit, i )
Vec_IntWriteEntry( vMap, Abc_Lit2Var(iLit), 1 );
// create output
Vec_IntFree( vLits );
vLits = Vec_IntDup(vInit);
Gia_ManForEachPi( pM, pObj, i )
if ( i == Gia_ManRegNum(p) )
break;
else if ( Vec_IntEntry(vLits, i) == 4 || Vec_IntEntry(vLits, i) == 5 )
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) );
else if ( (Vec_IntEntry(vLits, i) == 0 || Vec_IntEntry(vLits, i) == 1) && !Vec_IntEntry(vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) )
Vec_IntWriteEntry( vLits, i, Vec_IntEntry(vLits, i) | 2 );
Vec_IntFree( vMap );
// cleanup
sat_solver_delete( pSat );
Cnf_DataFree( pCnf );
Gia_ManStop( pM );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
return vLits;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ManMaxiTest( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
{
Vec_Int_t * vRes, * vInit;
vInit = vInit0 ? vInit0 : Vec_IntStart( Gia_ManRegNum(p) );
vRes = Gia_ManMaxiPerform( p, vInit, nFrames, nTimeOut, fVerbose );
if ( vInit != vInit0 )
Vec_IntFree( vInit );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

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

@ -2,6 +2,7 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcBmc2.c \ src/sat/bmc/bmcBmc2.c \
src/sat/bmc/bmcBmc3.c \ src/sat/bmc/bmcBmc3.c \
src/sat/bmc/bmcBmcAnd.c \ src/sat/bmc/bmcBmcAnd.c \
src/sat/bmc/bmcBmci.c \
src/sat/bmc/bmcCexCut.c \ src/sat/bmc/bmcCexCut.c \
src/sat/bmc/bmcCexDepth.c \ src/sat/bmc/bmcCexDepth.c \
src/sat/bmc/bmcCexMin1.c \ src/sat/bmc/bmcCexMin1.c \
@ -9,8 +10,8 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexTools.c \ src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcFault.c \ src/sat/bmc/bmcFault.c \
src/sat/bmc/bmcICheck.c \ src/sat/bmc/bmcICheck.c \
src/sat/bmc/bmcLilac.c \ src/sat/bmc/bmcInse.c \
src/sat/bmc/bmcLoad.c \ src/sat/bmc/bmcLoad.c \
src/sat/bmc/bmcMaxi.c \
src/sat/bmc/bmcMulti.c \ src/sat/bmc/bmcMulti.c \
src/sat/bmc/bmcTulip.c \
src/sat/bmc/bmcUnroll.c src/sat/bmc/bmcUnroll.c