From cc636a0d8390cb54ed2abad393c297d63e1ba52f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 28 Sep 2023 06:40:57 -0700 Subject: [PATCH] Experiments with verification. --- src/base/abci/abc.c | 85 ++++++++++++++++ src/proof/cec/cecProve.c | 205 ++++++++++++++++++++++++++++++++++++++ src/proof/cec/module.make | 1 + 3 files changed, 291 insertions(+) create mode 100644 src/proof/cec/cecProve.c diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4ee12db27..586ac2c57 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -541,6 +541,7 @@ static int Abc_CommandAbc9PoPart ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GroupProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9SProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SplitSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1314,6 +1315,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gprove", Abc_CommandAbc9GroupProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mprove", Abc_CommandAbc9MultiProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitprove", Abc_CommandAbc9SplitProve, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&sprove", Abc_CommandAbc9SProve, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&splitsat", Abc_CommandAbc9SplitSat, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmcs", Abc_CommandAbc9SBmc, 0 ); @@ -46278,6 +46280,89 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "PTsvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); + goto usage; + } + nProcs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nProcs <= 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" ); + goto usage; + } + nTimeOut = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nTimeOut <= 0 ) + goto usage; + break; + case 's': + fSilent ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" ); + return 1; + } + if ( Gia_ManRegNum(pAbc->pGia) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" ); + return 1; + } + pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, fVerbose, fVeryVerbose, fSilent ); + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); + return 0; + +usage: + Abc_Print( -2, "usage: &sprove [-PT 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-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" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c new file mode 100644 index 000000000..748f506f9 --- /dev/null +++ b/src/proof/cec/cecProve.c @@ -0,0 +1,205 @@ +/**CFile**************************************************************** + + FileName [cecSplit.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Combinational equivalence checking.] + + Synopsis [Cofactoring for combinational miters.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include +#include "aig/gia/gia.h" +#include "aig/gia/giaAig.h" + + +#ifdef ABC_USE_PTHREADS + +#ifdef _WIN32 +#include "../lib/pthread.h" +#else +#include +#include +#endif + +#endif + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifndef ABC_USE_PTHREADS + +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; } + +#else // pthreads are used + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCex ) +{ + abctime clk = Abc_Clock(); + //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock(); + printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut ); + if ( iEngine == 0 ) + { + } + else if ( iEngine == 1 ) + { + } + else if ( iEngine == 2 ) + { + } + else if ( iEngine == 3 ) + { + } + else assert( 0 ); + //while ( Abc_Clock() < clkStop ); + printf( "Engine %d finished. ", iEngine ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +#define PAR_THR_MAX 8 +typedef struct Par_ThData_t_ +{ + Gia_Man_t * p; + Abc_Cex_t * pCex; + int iEngine; + int fWorking; + int nTimeOut; + int Result; +} Par_ThData_t; +void * Cec_GiaProveWorkerThread( void * pArg ) +{ + Par_ThData_t * pThData = (Par_ThData_t *)pArg; + volatile int * pPlace = &pThData->fWorking; + while ( 1 ) + { + while ( *pPlace == 0 ); + assert( pThData->fWorking ); + if ( pThData->p == NULL ) + { + pthread_exit( NULL ); + assert( 0 ); + return NULL; + } + pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, &pThData->pCex ); + pThData->fWorking = 0; + } + assert( 0 ); + return NULL; +} +int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) +{ + 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 + 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; + 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 + for ( i = 0; i < nProcs; i++ ) + if ( ThData[i].fWorking ) + i = -1; + + // 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 " ); + else if ( RetValue == 1 ) + printf( "Problem is UNSAT " ); + else if ( RetValue == -1 ) + printf( "Problem is UNDECIDED " ); + else assert( 0 ); + printf( ". " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal ); + fflush( stdout ); + } + return RetValue; +} + +#endif // pthreads are used + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make index ed3dac110..ed8deba98 100644 --- a/src/proof/cec/module.make +++ b/src/proof/cec/module.make @@ -6,6 +6,7 @@ SRC += src/proof/cec/cecCec.c \ src/proof/cec/cecIso.c \ src/proof/cec/cecMan.c \ src/proof/cec/cecPat.c \ + src/proof/cec/cecProve.c \ src/proof/cec/cecSat.c \ src/proof/cec/cecSatG.c \ src/proof/cec/cecSatG2.c \