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-09-28 06:40:57 -07:00
parent 0f11580fce
commit cc636a0d83
3 changed files with 291 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -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 []

205
src/proof/cec/cecProve.c Normal file
View File

@ -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 <math.h>
#include "aig/gia/gia.h"
#include "aig/gia/giaAig.h"
#ifdef ABC_USE_PTHREADS
#ifdef _WIN32
#include "../lib/pthread.h"
#else
#include <pthread.h>
#include <unistd.h>
#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

1
src/proof/cec/module.make
View File

@ -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 \