summaryrefslogtreecommitdiff
path: root/src/sat/bmc
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc')
-rw-r--r--src/sat/bmc/bmc.h3
-rw-r--r--src/sat/bmc/bmcBmcAnd.c6
-rw-r--r--src/sat/bmc/bmcCexDepth.c4
-rw-r--r--src/sat/bmc/bmcCexMin2.c4
-rw-r--r--src/sat/bmc/bmcCexTools.c4
-rw-r--r--src/sat/bmc/bmcEco.c2
-rw-r--r--src/sat/bmc/bmcFault.c34
-rw-r--r--src/sat/bmc/bmcMaj.c73
-rw-r--r--src/sat/bmc/bmcUnroll.c4
9 files changed, 110 insertions, 24 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 71a3359..12439fa 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -58,6 +58,7 @@ struct Bmc_EsPar_t_
int fOrderNodes;
int fEnumSols;
int fFewerVars;
+ int RuntimeLim;
int fVerbose;
char * pTtStr;
};
@@ -76,6 +77,7 @@ static inline void Bmc_EsParSetDefault( Bmc_EsPar_t * pPars )
pPars->fOrderNodes = 0;
pPars->fEnumSols = 0;
pPars->fFewerVars = 0;
+ pPars->RuntimeLim = 0;
pPars->fVerbose = 1;
}
@@ -186,6 +188,7 @@ struct Bmc_ParFf_t_
int fNonStrict;
int fBasic;
int fFfOnly;
+ int fCheckUntest;
int fDump;
int fDumpDelay;
int fDumpUntest;
diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c
index 04d4435..b9c2db2 100644
--- a/src/sat/bmc/bmcBmcAnd.c
+++ b/src/sat/bmc/bmcBmcAnd.c
@@ -711,7 +711,7 @@ int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fDumpFrames )
{
p->pFrames = Gia_ManCleanup( p->pFrames );
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
Gia_ManStop( p->pFrames );
}
@@ -793,7 +793,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
for ( f = 0; f < nFramesMax; f++ )
@@ -977,7 +977,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
Gia_ManPrintStats( p->pFrames, NULL );
if ( pPars->fDumpFrames )
{
- Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 );
+ Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0, 0 );
printf( "Dumped unfolded frames into file \"frames.aig\".\n" );
}
if ( pPars->fUseOldCnf )
diff --git a/src/sat/bmc/bmcCexDepth.c b/src/sat/bmc/bmcCexDepth.c
index 38b57d5..f0883f9 100644
--- a/src/sat/bmc/bmcCexDepth.c
+++ b/src/sat/bmc/bmcCexDepth.c
@@ -110,7 +110,7 @@ Gia_Man_t * Bmc_CexTarget( Gia_Man_t * p, int nFrames )
Gia_ManPrintStats( pNew, NULL );
pTemp = Gia_ManDupAppendCones( p, &pNew, 1, 1 );
Gia_ManStop( pNew );
- Gia_AigerWrite( pTemp, "miter3.aig", 0, 0 );
+ Gia_AigerWrite( pTemp, "miter3.aig", 0, 0, 0 );
return pTemp;
}
@@ -308,7 +308,7 @@ Gia_Man_t * Bmc_CexBuildNetwork2Test( Gia_Man_t * p, Abc_Cex_t * pCex, int nFram
Vec_PtrPush( vCones, pNew );
}
pNew = Gia_ManDupAppendCones( p, (Gia_Man_t **)Vec_PtrArray(vCones), Vec_PtrSize(vCones), 1 );
- Gia_AigerWrite( pNew, "miter2.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "miter2.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Vec_PtrForEachEntry( Gia_Man_t *, vCones, pTemp, i )
Gia_ManStop( pTemp );
diff --git a/src/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
index b851460..b39b8ee 100644
--- a/src/sat/bmc/bmcCexMin2.c
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -334,7 +334,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
printf( "%3d : ", iFrameStart );
Gia_ManPrintStats( pNew, NULL );
if ( fVerbose )
- Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "temp.aig", 0, 0, 0 );
Gia_ManStop( pNew );
}
else // CEX min
@@ -345,7 +345,7 @@ Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int
printf( "%3d : ", f );
Gia_ManPrintStats( pNew, NULL );
if ( fVerbose )
- Gia_AigerWrite( pNew, "temp.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "temp.aig", 0, 0, 0 );
Gia_ManStop( pNew );
}
}
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 9c80b27..5a29c8b 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -173,7 +173,7 @@ void Bmc_CexPerformUnrollingTest( Gia_Man_t * p, Abc_Cex_t * pCex )
abctime clk = Abc_Clock();
pNew = Bmc_CexPerformUnrolling( p, pCex );
Gia_ManPrintStats( pNew, NULL );
- Gia_AigerWrite( pNew, "unroll.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "unroll.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unroll.aig\".\n" );
@@ -285,7 +285,7 @@ void Bmc_CexBuildNetworkTest( Gia_Man_t * p, Abc_Cex_t * pCex )
abctime clk = Abc_Clock();
pNew = Bmc_CexBuildNetwork( p, pCex );
Gia_ManPrintStats( pNew, NULL );
- Gia_AigerWrite( pNew, "unate.aig", 0, 0 );
+ Gia_AigerWrite( pNew, "unate.aig", 0, 0, 0 );
//Bmc_CexDumpAogStats( pNew, Abc_Clock() - clk );
Gia_ManStop( pNew );
printf( "CE-induced network is written into file \"unate.aig\".\n" );
diff --git a/src/sat/bmc/bmcEco.c b/src/sat/bmc/bmcEco.c
index 9d30fc0..b42d527 100644
--- a/src/sat/bmc/bmcEco.c
+++ b/src/sat/bmc/bmcEco.c
@@ -291,7 +291,7 @@ void Bmc_EcoMiterTest()
Vec_IntPush( vFans, Gia_ObjId(pOld, pObj) );
pMiter = Bmc_EcoMiter( pGold, pOld, vFans );
Vec_IntFree( vFans );
- Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0 );
+ Gia_AigerWrite( pMiter, "eco_miter.aig", 0, 0, 0 );
// find the patch
RetValue = Bmc_EcoPatch( pMiter, Gia_ManCiNum(pGold), Gia_ManCoNum(pGold) );
if ( RetValue == 1 )
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 0f63fa6..28d8a0c 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -22,6 +22,7 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"
+#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
@@ -58,6 +59,7 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
p->nIterCheck = 0;
p->fBasic = 0;
p->fFfOnly = 0;
+ p->fCheckUntest = 0;
p->fDump = 0;
p->fDumpUntest = 0;
p->fVerbose = 0;
@@ -476,6 +478,7 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
+ int VarLimit = 4 * Gia_ManAndNum(p);
pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
@@ -484,22 +487,22 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
- if ( Vec_IntEntry(vMap, iFuncVars++) )
+ if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl0 = Gia_ManAppendCi(pNew);
else
iCtrl0 = 0, Gia_ManAppendCi(pNew);
- if ( Vec_IntEntry(vMap, iFuncVars++) )
+ if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl1 = Gia_ManAppendCi(pNew);
else
iCtrl1 = 0, Gia_ManAppendCi(pNew);
- if ( Vec_IntEntry(vMap, iFuncVars++) )
+ if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl2 = Gia_ManAppendCi(pNew);
else
iCtrl2 = 0, Gia_ManAppendCi(pNew);
- if ( Vec_IntEntry(vMap, iFuncVars++) )
+ if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl3 = Gia_ManAppendCi(pNew);
else
iCtrl3 = 0, Gia_ManAppendCi(pNew);
@@ -751,7 +754,7 @@ Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
Gia_ManStop( pTemp );
assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * (fFfOnly ? Count : Gia_ManAndNum(p)) );
// if ( fUseFaults )
-// Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
+// Gia_AigerWrite( pNew, "newfault.aig", 0, 0, 0 );
return pNew;
}
@@ -1257,7 +1260,7 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int
p1 = Gia_ManFOFUnfold( p, vMap );
if ( pPars->Algo != 1 )
p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
-// Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
+// Gia_AigerWrite( p1, "newfault.aig", 0, 0, 0 );
// printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
// create miter
@@ -1441,6 +1444,19 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
return;
}
+ printf( "Options: " );
+ printf( "Untestable faults = %s. ", pPars->fCheckUntest || pPars->fDumpDelay ? "yes": "no" );
+ if ( pPars->nCardConstr )
+ printf( "Using %sstrict cardinality %d. ", pPars->fNonStrict ? "non-" : "", pPars->nCardConstr );
+ if ( pPars->fFfOnly )
+ printf( "Faults at FF outputs only = yes. " );
+ if ( pPars->nTimeOut )
+ printf( "Runtime limit = %d sec. ", pPars->nTimeOut );
+ if ( p != pG && pG->pSpec )
+ printf( "Golden model = %s. ", pG->pSpec );
+ printf( "Verbose = %s. ", pPars->fVerbose ? "yes": "no" );
+ printf( "\n" );
+
// select algorithm
if ( pPars->Algo == 0 )
nFuncVars = Gia_ManCiNum(p);
@@ -1565,7 +1581,7 @@ finish:
// dump the test suite
if ( pPars->fDump )
{
- char * pFileName = "tests.txt";
+ char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_tests.txt") : "tests.txt";
if ( pPars->fDumpDelay && pPars->Algo == 1 )
{
Gia_ManDumpTestsDelay( vTests, Iter, pFileName, p );
@@ -1579,7 +1595,7 @@ finish:
}
// compute untestable faults
- if ( Iter && (p != pG || pPars->fDumpUntest) )
+ if ( Iter && (p != pG || pPars->fDumpUntest || pPars->fCheckUntest) )
{
abctime clkTotal = Abc_Clock();
// restart the SAT solver
@@ -1680,7 +1696,7 @@ finish:
if ( pPars->fDumpUntest && status == l_True )
{
abctime clk = Abc_Clock();
- char * pFileName = "untest.txt";
+ char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_untest.txt") : "untest.txt";
int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
if ( p == pG )
printf( "Dumped %d untestable multiple faults into file \"%s\". ", nUntests, pFileName );
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 4f2c8db..08571a3 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -500,6 +500,8 @@ Exa_Man_t * Exa_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
p->vInfo = Exa_ManTruthTables( p );
p->pSat = bmcg_sat_solver_start();
bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+ if ( pPars->RuntimeLim )
+ bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
return p;
}
void Exa_ManFree( Exa_Man_t * p )
@@ -572,6 +574,59 @@ static inline int Exa_ManEval( Exa_Man_t * p )
SeeAlso []
***********************************************************************/
+void Exa_ManDumpBlif( Exa_Man_t * p, int fCompl )
+{
+ char Buffer[1000];
+ char FileName[1000];
+ FILE * pFile;
+ int i, k, iVar;
+ if ( fCompl )
+ Abc_TtNot( p->pTruth, p->nWords );
+ Extra_PrintHexadecimalString( Buffer, (unsigned *)p->pTruth, p->nVars );
+ if ( fCompl )
+ Abc_TtNot( p->pTruth, p->nWords );
+ sprintf( FileName, "%s_%d_%d.blif", Buffer, 2, p->nNodes );
+ pFile = fopen( FileName, "wb" );
+ fprintf( pFile, "# Realization of the %d-input function %s using %d two-input gates:\n", p->nVars, Buffer, p->nNodes );
+ fprintf( pFile, ".model %s_%d_%d\n", Buffer, 2, p->nNodes );
+ fprintf( pFile, ".inputs" );
+ for ( i = 0; i < p->nVars; i++ )
+ fprintf( pFile, " %c", 'a'+i );
+ fprintf( pFile, "\n" );
+ fprintf( pFile, ".outputs F\n" );
+ for ( i = p->nObjs - 1; i >= p->nVars; i-- )
+ {
+ int iVarStart = 1 + 3*(i - p->nVars);
+ int Val1 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart);
+ int Val2 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+1);
+ int Val3 = bmcg_sat_solver_read_cex_varvalue(p->pSat, iVarStart+2);
+
+ fprintf( pFile, ".names" );
+ for ( k = 1; k >= 0; k-- )
+ {
+ iVar = Exa_ManFindFanin( p, i, k );
+ if ( iVar >= 0 && iVar < p->nVars )
+ fprintf( pFile, " %c", 'a'+iVar );
+ else
+ fprintf( pFile, " %02d", iVar );
+ }
+ if ( i == p->nObjs - 1 )
+ fprintf( pFile, " F\n" );
+ else
+ fprintf( pFile, " %02d\n", i );
+ if ( i == p->nObjs - 1 && fCompl )
+ fprintf( pFile, "00 1\n" );
+ if ( (i == p->nObjs - 1 && fCompl) ^ Val1 )
+ fprintf( pFile, "01 1\n" );
+ if ( (i == p->nObjs - 1 && fCompl) ^ Val2 )
+ fprintf( pFile, "10 1\n" );
+ if ( (i == p->nObjs - 1 && fCompl) ^ Val3 )
+ fprintf( pFile, "11 1\n" );
+ }
+ fprintf( pFile, ".end\n\n" );
+ fclose( pFile );
+ printf( "Solution was dumped into file \"%s\".\n", FileName );
+}
void Exa_ManPrintSolution( Exa_Man_t * p, int fCompl )
{
int i, k, iVar;
@@ -775,10 +830,18 @@ void Exa_ManExactSynthesis( Bmc_EsPar_t * pPars )
printf( "The problem has no solution.\n" );
break;
}
+ if ( status == GLUCOSE_UNDEC )
+ {
+ printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+ break;
+ }
iMint = Exa_ManEval( p );
}
if ( iMint == -1 )
+ {
Exa_ManPrintSolution( p, fCompl );
+ Exa_ManDumpBlif( p, fCompl );
+ }
Exa_ManFree( p );
Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
}
@@ -915,6 +978,8 @@ static Exa3_Man_t * Exa3_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
p->vUsed3 = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
p->pSat = bmcg_sat_solver_start();
bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
+ if ( pPars->RuntimeLim )
+ bmcg_sat_solver_set_runtime_limit( p->pSat, Abc_Clock() + pPars->RuntimeLim * CLOCKS_PER_SEC );
return p;
}
static void Exa3_ManFree( Exa3_Man_t * p )
@@ -1267,15 +1332,17 @@ void Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars )
status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
if ( pPars->fVerbose && (!pPars->fUseIncr || i % 100 == 0) )
Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
- if ( status == GLUCOSE_UNSAT )
+ if ( status == GLUCOSE_UNSAT || status == GLUCOSE_UNDEC )
break;
iMint = Exa3_ManEval( p );
}
- if ( pPars->fVerbose )
+ if ( pPars->fVerbose && status != GLUCOSE_UNDEC )
Exa3_ManPrint( p, i, iMint, Abc_Clock() - clkTotal );
if ( iMint == -1 )
Exa3_ManPrintSolution( p, fCompl );
- else
+ else if ( status == GLUCOSE_UNDEC )
+ printf( "The problem timed out after %d sec.\n", pPars->RuntimeLim );
+ else
printf( "The problem has no solution.\n" );
printf( "Added = %d. Tried = %d. ", p->nUsed[1], p->nUsed[0] );
Exa3_ManFree( p );
diff --git a/src/sat/bmc/bmcUnroll.c b/src/sat/bmc/bmcUnroll.c
index 0ad9271..1051393 100644
--- a/src/sat/bmc/bmcUnroll.c
+++ b/src/sat/bmc/bmcUnroll.c
@@ -489,8 +489,8 @@ void Unr_ManTest( Gia_Man_t * pGia, int nFrames )
Gia_ManPrintStats( pFrames0, NULL );
Gia_ManPrintStats( pFrames1, NULL );
-Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0 );
-Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0 );
+Gia_AigerWrite( pFrames0, "frames0.aig", 0, 0, 0 );
+Gia_AigerWrite( pFrames1, "frames1.aig", 0, 0, 0 );
Gia_ManStop( pFrames0 );
Gia_ManStop( pFrames1 );
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-02 17:58:49 +0000