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

Experiments with verification.

This commit is contained in:
Alan Mishchenko 2023-10-23 09:38:08 -07:00
parent 8dbf8965fd
commit 01ad71b26f
3 changed files with 204 additions and 48 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -46383,10 +46383,10 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent );
int c, nProcs = 5, nTimeOut = 3, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent );
int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTsvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWsvwh" ) ) != EOF )
{
switch ( c )
{
@ -46412,6 +46412,28 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nTimeOut <= 0 )
goto usage;
break;
case 'U':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-U\" should be followed by a positive integer.\n" );
goto usage;
}
nTimeOut2 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut2 <= 0 )
goto usage;
break;
case 'W':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-W\" should be followed by a positive integer.\n" );
goto usage;
}
nTimeOut3 = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nTimeOut3 <= 0 )
goto usage;
break;
case 's':
fSilent ^= 1;
break;
@ -46437,15 +46459,17 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" );
return 1;
}
pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, fVerbose, fVeryVerbose, fSilent );
pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, nTimeOut2, nTimeOut3, fVerbose, fVeryVerbose, fSilent );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
return 0;
usage:
Abc_Print( -2, "usage: &sprove [-PT num] [-svwh]\n" );
Abc_Print( -2, "usage: &sprove [-PTUW num] [-svwh]\n" );
Abc_Print( -2, "\t proves CEC problem by case-splitting\n" );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", nProcs );
Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut );
Abc_Print( -2, "\t-U num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut2 );
Abc_Print( -2, "\t-W num : runtime limit in seconds per subproblem [default = %d]\n", nTimeOut3 );
Abc_Print( -2, "\t-s : enable silent computation (no reporting) [default = %s]\n", fSilent? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );

2
src/base/io/ioUtil.c
View File

@ -944,7 +944,7 @@ char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
Vec_IntForEachEntry( vLevel, Num, k )
pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num);
pCube[nVars+0] = ' ';
pCube[nVars+1] = '1';
pCube[nVars+1] = '0';
pCube[nVars+2] = '\n';
}
return pStr;

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

@ -22,6 +22,11 @@
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#include "sat/bmc/bmc.h"
#include "proof/pdr/pdr.h"
#include "proof/cec/cec.h"
#include "proof/ssw/ssw.h"
#ifdef ABC_USE_PTHREADS
@ -41,9 +46,12 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
extern int Ssw_RarSimulateGia( Gia_Man_t * p, Ssw_RarPars_t * pPars );
extern int Bmcg_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars );
#ifndef ABC_USE_PTHREADS
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
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
@ -62,28 +70,106 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int
SeeAlso []
***********************************************************************/
int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCex )
int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose )
{
abctime clk = Abc_Clock();
abctime clk = Abc_Clock();
int RetValue = -1;
//abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock();
if ( fVerbose )
printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut );
Abc_CexFreeP( &p->pCexSeq );
if ( iEngine == 0 )
{
Ssw_RarPars_t Pars, * pPars = &Pars;
Ssw_RarSetDefaultParams( pPars );
pPars->TimeOut = nTimeOut;
pPars->fSilent = 1;
RetValue = Ssw_RarSimulateGia( p, pPars );
}
else if ( iEngine == 1 )
{
}
Saig_ParBmc_t Pars, * pPars = &Pars;
Saig_ParBmcSetDefaultParams( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
}
else if ( iEngine == 2 )
{
}
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
}
else if ( iEngine == 3 )
{
Saig_ParBmc_t Pars, * pPars = &Pars;
Saig_ParBmcSetDefaultParams( pPars );
pPars->fUseGlucose = 1;
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Saig_ManBmcScalable( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
}
else if ( iEngine == 4 )
{
Pdr_Par_t Pars, * pPars = &Pars;
Pdr_ManSetDefaultParams( pPars );
pPars->fUseAbs = 1;
pPars->nTimeOut = nTimeOut;
pPars->fSilent = 1;
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
RetValue = Pdr_ManSolve( pAig, pPars );
p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
Aig_ManStop( pAig );
}
else if ( iEngine == 5 )
{
Bmc_AndPar_t Pars, * pPars = &Pars;
memset( pPars, 0, sizeof(Bmc_AndPar_t) );
pPars->nProcs = 1; // the number of parallel solvers
pPars->nFramesAdd = 1; // the number of additional frames
pPars->fNotVerbose = 1; // silent
pPars->nTimeOut = nTimeOut; // timeout in seconds
RetValue = Bmcg_ManPerform( p, pPars );
}
else assert( 0 );
//while ( Abc_Clock() < clkStop );
printf( "Engine %d finished. ", iEngine );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return 0;
if ( fVerbose ) {
printf( "Engine %d finished and %ssolved the problem. ", iEngine, RetValue != -1 ? " " : "not " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
}
return RetValue;
}
Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p )
{
Ssw_Pars_t Pars, * pPars = &Pars;
Ssw_ManSetDefaultParams( pPars );
Aig_Man_t * pAig = Gia_ManToAigSimple( p );
Aig_Man_t * pAig2 = Ssw_SignalCorrespondence( pAig, pPars );
Gia_Man_t * pGia2 = Gia_ManFromAigSimple( pAig2 );
Aig_ManStop( pAig2 );
Aig_ManStop( pAig );
return pGia2;
}
Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p )
{
Cec_ParCor_t Pars, * pPars = &Pars;
Cec_ManCorSetDefaultParams( pPars );
pPars->nBTLimit = 100;
pPars->nLevelMax = 100;
pPars->fVerbose = 0;
pPars->fUseCSat = 1;
return Cec_ManLSCorrespondence( p, pPars );
}
/**Function*************************************************************
@ -101,11 +187,11 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCe
typedef struct Par_ThData_t_
{
Gia_Man_t * p;
Abc_Cex_t * pCex;
int iEngine;
int fWorking;
int nTimeOut;
int Result;
int fVerbose;
} Par_ThData_t;
void * Cec_GiaProveWorkerThread( void * pArg )
{
@ -121,73 +207,119 @@ void * Cec_GiaProveWorkerThread( void * pArg )
assert( 0 );
return NULL;
}
pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, &pThData->pCex );
pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, pThData->fVerbose );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent )
void Cec_GiaInitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int nTimeOut, int fVerbose, pthread_t * WorkerThread )
{
abctime clkTotal = Abc_Clock();
Par_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, status, RetValue = -1;
Abc_CexFreeP( &p->pCexComb );
Abc_CexFreeP( &p->pCexSeq );
if ( fVerbose )
printf( "Solving verification problem with the following parameters:\n" );
if ( fVerbose )
printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
fflush( stdout );
if ( nProcs == 1 )
return -1;
// subtract manager thread
nProcs--;
assert( (nProcs == 4 || nProcs == 8) && nProcs <= PAR_THR_MAX );
// start threads
int i, status;
assert( nProcs <= PAR_THR_MAX );
for ( i = 0; i < nProcs; i++ )
{
ThData[i].p = Gia_ManDup(p);
ThData[i].pCex = NULL;
ThData[i].iEngine = i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
ThData[i].fVerbose = fVerbose;
if ( !WorkerThread )
continue;
status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
for ( i = 0; i < nProcs; i++ )
ThData[i].fWorking = 1;
// wait till threads finish
}
int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nProcs, Gia_Man_t * p, int RetValue, int * pRetEngine )
{
int i;
for ( i = 0; i < nProcs; i++ )
{
if ( RetValue == -1 && !ThData[i].fWorking && ThData[i].Result != -1 ) {
RetValue = ThData[i].Result;
*pRetEngine = i;
if ( !p->pCexSeq && ThData[i].p->pCexSeq )
p->pCexSeq = Abc_CexDup( ThData[i].p->pCexSeq, -1 );
}
if ( ThData[i].fWorking )
i = -1;
}
return RetValue;
}
int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fVerbose, int fVeryVerbose, int fSilent )
{
abctime clkScorr = 0, clkTotal = Abc_Clock();
Par_ThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, RetValue = -1, RetEngine = -2;
Abc_CexFreeP( &p->pCexComb );
Abc_CexFreeP( &p->pCexSeq );
if ( !fSilent && fVerbose )
printf( "Solving verification problem with the following parameters:\n" );
if ( !fSilent && fVerbose )
printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
fflush( stdout );
assert( nProcs == 3 || nProcs == 5 );
Cec_GiaInitThreads( ThData, nProcs, p, nTimeOut, fVerbose, WorkerThread );
// meanwhile, perform scorr
Gia_Man_t * pScorr = Cec_GiaScorrNew( p );
clkScorr = Abc_Clock() - clkTotal;
if ( Gia_ManAndNum(pScorr) == 0 )
RetValue = 1, RetEngine = -1;
RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine );
if ( RetValue == -1 )
{
abctime clkScorr2, clkStart = Abc_Clock();
if ( !fSilent && fVerbose ) {
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 );
// meanwhile, perform scorr
Gia_Man_t * pScorr2 = Cec_GiaScorrOld( pScorr );
clkScorr2 = Abc_Clock() - clkStart;
if ( Gia_ManAndNum(pScorr2) == 0 )
RetValue = 1;
RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine );
if ( RetValue == -1 )
{
if ( !fSilent && fVerbose ) {
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 );
RetValue = Cec_GiaWaitThreads( ThData, nProcs, p, RetValue, &RetEngine );
// do something else
}
Gia_ManStop( pScorr2 );
}
Gia_ManStop( pScorr );
// stop threads
for ( i = 0; i < nProcs; i++ )
{
assert( !ThData[i].fWorking );
// cleanup
Gia_ManStopP( &ThData[i].p );
if ( !p->pCexSeq && ThData[i].pCex )
p->pCexSeq = Abc_CexDup( ThData[i].pCex, -1 );
Abc_CexFreeP( &ThData[i].pCex );
// stop
ThData[i].p = NULL;
ThData[i].fWorking = 1;
}
if ( !fSilent )
{
if ( RetValue == 0 )
printf( "Problem is SAT " );
printf( "Problem is SAT (solved by %d) ", RetEngine );
else if ( RetValue == 1 )
printf( "Problem is UNSAT " );
printf( "Problem is UNSAT (solved by %d) ", RetEngine );
else if ( RetValue == -1 )
printf( "Problem is UNDECIDED " );
else assert( 0 );
printf( ". " );
printf( " " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
fflush( stdout );
}