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

Adding gla to sprove.

This commit is contained in:
Alan Mishchenko 2026-03-08 12:04:25 -07:00
parent a745d5ec81
commit 7ae0f4966a
5 changed files with 47 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -51398,7 +51398,7 @@ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL;
Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc;
int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
int c, nProcs = 6, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "PTUWusvwh" ) ) != EOF )
{

3
src/proof/abs/abs.h
View File

@ -74,6 +74,8 @@ struct Abs_Par_t_
char * pFileVabs; // dumps the abstracted model into this file
int fVerbose; // verbose flag
int fVeryVerbose; // print additional information
int RunId; // id in this run
int (*pFuncStop)(int); // callback to terminate
int iFrame; // the number of frames covered
int iFrameProved; // the number of frames proved
int nFramesNoChange; // the number of last frames without changes
@ -174,4 +176,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

10
src/proof/abs/absGla.c
View File

@ -1576,6 +1576,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
for ( i = f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; i++ )
{
int nAbsOld;
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
goto finish;
// remember the timeframe
p->pPars->iFrame = -1;
// create new SAT solver
@ -1585,6 +1587,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
// unroll the circuit
for ( f = 0; !pPars->nFramesMax || f < pPars->nFramesMax; f++ )
{
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
goto finish;
// remember current limits
int nConflsBeg = sat_solver2_nconflicts(p->pSat);
int nAbs = Vec_IntSize(p->vAbs);
@ -1618,6 +1622,11 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
nVarsOld = p->nSatVars;
for ( c = 0; ; c++ )
{
if ( pPars->pFuncStop && pPars->pFuncStop(pPars->RunId) )
{
Status = l_Undef;
goto finish;
}
// consider the special case when the target literal is implied false
// by implications which happened as a result of previous refinements
// note that incremental UNSAT core cannot be computed because there is no learned clauses
@ -1898,4 +1907,3 @@ finish:
ABC_NAMESPACE_IMPL_END

3
src/proof/abs/absUtil.c
View File

@ -59,6 +59,8 @@ void Abs_ParSetDefaults( Abs_Par_t * p )
p->fUseRollback = 0; // use rollback to the starting number of frames
p->fPropFanout = 1; // propagate fanouts during refinement
p->fVerbose = 0; // verbose flag
p->RunId = -1; // id in this run
p->pFuncStop = NULL; // callback to terminate
p->iFrame = -1; // the number of frames covered
p->iFrameProved = -1; // the number of frames proved
p->nFramesNoChangeLim = 2; // the number of frames without change to dump abstraction
@ -254,4 +256,3 @@ int Gia_GlaCountNodes( Gia_Man_t * p, Vec_Int_t * vGla )
ABC_NAMESPACE_IMPL_END

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

@ -26,6 +26,7 @@
#include "proof/pdr/pdr.h"
#include "proof/cec/cec.h"
#include "proof/ssw/ssw.h"
#include "proof/abs/abs.h"
#ifdef ABC_USE_PTHREADS
@ -66,6 +67,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
#define PAR_ENGINE_UFAR 6
#define PAR_ENGINE_SCORR1 7
#define PAR_ENGINE_SCORR2 8
#define PAR_ENGINE_GLA 9
struct Par_Share_t_
{
volatile int fSolved;
@ -90,6 +92,7 @@ typedef struct Cec_ScorrStop_t_
abctime TimeToStop;
} Cec_ScorrStop_t;
static volatile Par_Share_t * g_pUfarShare = NULL;
static volatile Par_Share_t * g_pGlaShare = NULL;
static inline const char * Cec_SolveEngineName( int iEngine )
{
if ( iEngine == 0 ) return "rar";
@ -101,6 +104,7 @@ static inline const char * Cec_SolveEngineName( int iEngine )
if ( iEngine == PAR_ENGINE_UFAR ) return "ufar";
if ( iEngine == PAR_ENGINE_SCORR1 ) return "scorr-new";
if ( iEngine == PAR_ENGINE_SCORR2 ) return "scorr-old";
if ( iEngine == PAR_ENGINE_GLA ) return "gla-q";
return "unknown";
}
static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
@ -128,6 +132,11 @@ static int Cec_SProveStopUfar( int RunId )
(void)RunId;
return g_pUfarShare && g_pUfarShare->fSolved != 0;
}
static int Cec_SProveStopGla( int RunId )
{
(void)RunId;
return g_pGlaShare && g_pGlaShare->fSolved != 0;
}
static int Cec_ScorrStop( void * pUser )
{
Cec_ScorrStop_t * p = (Cec_ScorrStop_t *)pUser;
@ -177,7 +186,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
{
abctime clk = Abc_Clock();
int RetValue = -1;
if ( iEngine != PAR_ENGINE_UFAR && Gia_ManRegNum(p) == 0 )
if ( iEngine != PAR_ENGINE_UFAR && iEngine != PAR_ENGINE_GLA && Gia_ManRegNum(p) == 0 )
{
if ( fVerbose )
printf( "Engine %d skipped because the current miter is combinational.\n", iEngine );
@ -294,6 +303,22 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
g_pUfarShare = NULL;
}
}
else if ( iEngine == PAR_ENGINE_GLA )
{
if ( Gia_ManPoNum(p) != 1 )
return -1;
Abs_Par_t Pars, * pPars = &Pars;
Abs_ParSetDefaults( pPars );
pPars->nTimeOut = nTimeOut;
pPars->fCallProver = 1; // emulate "&gla -q"
pPars->fVerbose = 0;
pPars->fVeryVerbose = 0;
pPars->RunId = 0;
pPars->pFuncStop = Cec_SProveStopGla;
g_pGlaShare = pThData ? pThData->pShare : NULL;
RetValue = Gia_ManPerformGla( p, pPars );
g_pGlaShare = NULL;
}
else assert( 0 );
//while ( Abc_Clock() < clkStop );
if ( pThData && pThData->pShare && RetValue != -1 )
@ -379,7 +404,12 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
{
ThData[i].p = Gia_ManDup(p);
Cec_CopyGiaName( p, ThData[i].p );
ThData[i].iEngine = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
if ( fUseUif && i == nWorkers - 1 )
ThData[i].iEngine = PAR_ENGINE_UFAR;
else if ( !fUseUif && nWorkers == 6 && i == 5 )
ThData[i].iEngine = PAR_ENGINE_GLA;
else
ThData[i].iEngine = i;
ThData[i].nTimeOut = nTimeOut;
ThData[i].fWorking = 0;
ThData[i].Result = -1;
@ -427,7 +457,7 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
printf( "Processes = %d TimeOut = %d sec Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
fflush( stdout );
assert( nProcs == 3 || nProcs == 5 );
assert( nProcs == 3 || nProcs == 5 || nProcs == 6 );
assert( nWorkers <= PAR_THR_MAX );
Cec_GiaInitThreads( ThData, nWorkers, p, nTimeOut, nTimeOut3, pWlc, fUseUif, fVerbose, WorkerThread, &Share );