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

Partitioned &scorr.

This commit is contained in:
Alan Mishchenko 2023-07-21 18:49:06 -07:00
parent 55ed1e6698
commit 3592078ddb
4 changed files with 323 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -37232,13 +37232,15 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
extern Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars );
Cec_ParCor_t Pars, * pPars = &Pars;
Gia_Man_t * pTemp;
int fPartition = 0;
int fUseOld = 0, c;
Cec_ManCorSetDefaultParams( pPars );
pPars->nProcs = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqowvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSpkrecqowvh" ) ) != EOF )
{
switch ( c )
{
@ -37264,7 +37266,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nBTLimit < 0 )
goto usage;
break;
case 'P':
case 'G':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
@ -37286,6 +37288,28 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nLimitMax < 0 )
goto usage;
break;
case 'P':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
goto usage;
}
pPars->nProcs = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nProcs < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
pPars->nPartSize = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nPartSize < 0 )
goto usage;
break;
case 'p':
fPartition ^= 1;
break;
@ -37338,7 +37362,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "The network is combinational.\n" );
return 0;
}
if ( fUseOld )
if ( pPars->nPartSize > 0 )
pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars );
else if ( fUseOld )
pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars );
else if ( fPartition )
pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
@ -37348,12 +37374,14 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqowvh]\n" );
Abc_Print( -2, "usage: &scorr [-FCGXPS num] [-pkrecqowvh]\n" );
Abc_Print( -2, "\t performs signal correpondence computation\n" );
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
Abc_Print( -2, "\t-G num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", pPars->nProcs );
Abc_Print( -2, "\t-S num : the number of flops in one partition [default = %d]\n", pPars->nPartSize );
Abc_Print( -2, "\t-p : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
Abc_Print( -2, "\t-k : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
Abc_Print( -2, "\t-r : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );

2
src/proof/cec/cec.h
View File

@ -147,6 +147,8 @@ struct Cec_ParCor_t_
int nFrames; // the number of time frames
int nPrefix; // the number of time frames in the prefix
int nBTLimit; // conflict limit at a node
int nProcs; // the number of processes
int nPartSize; // the partition size
int nLevelMax; // (scorr only) the max number of levels
int nStepsMax; // (scorr only) the max number of induction steps
int nLimitMax; // (scorr only) stop after this many iterations if little or no improvement

1
src/proof/ssw/ssw.h
View File

@ -42,6 +42,7 @@ struct Ssw_Pars_t_
{
int nPartSize; // size of the partition
int nOverSize; // size of the overlap between partitions
int nProcs; // the number of processors
int nFramesK; // the induction depth
int nFramesAddSim; // the number of additional frames to simulate
int fConstrs; // treat the last nConstrs POs as seq constraints

289
src/proof/ssw/sswPart.c
View File

@ -20,10 +20,23 @@
#include "sswInt.h"
#include "aig/ioa/ioa.h"
#include "aig/gia/giaAig.h"
#include "proof/cec/cec.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 ///
////////////////////////////////////////////////////////////////////////
@ -32,6 +45,141 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performing SAT sweeping for the array of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Ssw_SignalCorrespondenceArray1( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
Gia_Man_t * pGia; int i;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
pCorPars->nBTLimit = pPars->nBTLimit;
pCorPars->fVerbose = pPars->fVerbose;
pCorPars->fUseCSat = 1;
Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
if ( Gia_ManPiNum(pGia) > 0 )
Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
}
/**Function*************************************************************
Synopsis [Performing SAT sweeping for the array of AIGs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
#ifndef ABC_USE_PTHREADS
void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
Ssw_SignalCorrespondenceArray1( vGias, pPars );
}
#else // pthreads are used
#define PAR_THR_MAX 100
typedef struct Par_ScorrThData_t_
{
Cec_ParCor_t CorPars;
Gia_Man_t * p;
int * pMap;
int iThread;
int nTimeOut;
int fWorking;
} Par_ScorrThData_t;
void * Ssw_GiaWorkerThread( void * pArg )
{
Par_ScorrThData_t * pThData = (Par_ScorrThData_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;
}
Cec_ManLSCorrespondenceClasses( pThData->p, &pThData->CorPars );
pThData->fWorking = 0;
}
assert( 0 );
return NULL;
}
void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
{
//abctime clkTotal = Abc_Clock();
Par_ScorrThData_t ThData[PAR_THR_MAX];
pthread_t WorkerThread[PAR_THR_MAX];
int i, status, nProcs = pPars->nProcs;
Vec_Ptr_t * vStack;
Cec_ParCor_t CorPars, * pCorPars = &CorPars;
Cec_ManCorSetDefaultParams( pCorPars );
if ( pPars->fVerbose )
printf( "Running concurrent &scorr with %d processes.\n", nProcs );
fflush( stdout );
if ( pPars->nProcs < 2 )
return Ssw_SignalCorrespondenceArray1( vGias, pPars );
// subtract manager thread
nProcs--;
assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
// start threads
for ( i = 0; i < nProcs; i++ )
{
ThData[i].CorPars = *pCorPars;
ThData[i].iThread = i;
//ThData[i].nTimeOut = pPars->nTimeOut;
ThData[i].fWorking = 0;
status = pthread_create( WorkerThread + i, NULL, Ssw_GiaWorkerThread, (void *)(ThData + i) ); assert( status == 0 );
}
// look at the threads
vStack = Vec_PtrDup( vGias );
while ( Vec_PtrSize(vStack) > 0 )
{
for ( i = 0; i < nProcs; i++ )
{
if ( ThData[i].fWorking )
continue;
ThData[i].p = (Gia_Man_t*)Vec_PtrPop( vStack );
ThData[i].fWorking = 1;
break;
}
}
Vec_PtrFree( vStack );
// 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 );
// stop
ThData[i].p = NULL;
ThData[i].fWorking = 1;
}
}
#endif // pthreads are used
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweeping.]
@ -45,7 +193,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 0;
int fPrintParts = 1;
char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vResult;
@ -132,6 +280,143 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
}
/**Function*************************************************************
Synopsis [Performs partitioned sequential SAT sweeping.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_SignalCorrespondencePart2( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
{
int fPrintParts = 1;
//char Buffer[100];
Aig_Man_t * pTemp, * pNew;
Vec_Ptr_t * vAigs;
Vec_Ptr_t * vGias;
Vec_Ptr_t * vMaps;
Vec_Ptr_t * vResult;
Vec_Int_t * vPart;
int * pMapBack = NULL;
int i, nCountPis, nCountRegs;
int nClasses, nPartSize, fVerbose;
abctime clk = Abc_Clock();
if ( pPars->fConstrs )
{
Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
return NULL;
}
// save parameters
nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
// generate partitions
if ( pAig->vClockDoms )
{
// divide large clock domains into separate partitions
vResult = Vec_PtrAlloc( 100 );
Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
{
if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
else
Vec_PtrPush( vResult, Vec_IntDup(vPart) );
}
}
else
vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
// vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
// vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
// collect partitions
vAigs = Vec_PtrAlloc( 100 );
vGias = Vec_PtrAlloc( 100 );
vMaps = Vec_PtrAlloc( 100 );
if ( fPrintParts )
Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
Aig_ManSetRegNum( pTemp, pTemp->nRegs );
Vec_PtrPush( vAigs, pTemp );
Vec_PtrPush( vGias, Gia_ManFromAigSimple(pTemp) );
Vec_PtrPush( vMaps, pMapBack );
//sprintf( Buffer, "part%03d.aig", i );
//Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
if ( fPrintParts )
Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
}
// solve partitions
Ssw_SignalCorrespondenceArray( vGias, pPars );
// collect the results
Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
{
int * pMapBack = (int *)Vec_PtrEntry( vMaps, i );
Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry( vGias, i );
Aig_Man_t * pTemp2 = Gia_ManToAigSimple( pGia );
pTemp = (Aig_Man_t *)Vec_PtrEntry( vAigs, i );
Gia_ManReprToAigRepr2( pTemp2, pGia );
// remap back
nClasses = Aig_TransferMappedClasses( pAig, pTemp2, pMapBack );
if ( fVerbose )
Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), 0, 0, Aig_ManNodeNum(pTemp), 0, nClasses );
Aig_ManStop( pTemp );
Aig_ManStop( pTemp2 );
Gia_ManStop( pGia );
ABC_FREE( pMapBack );
}
Vec_PtrFree( vAigs );
Vec_PtrFree( vGias );
Vec_PtrFree( vMaps );
// remap the AIG
pNew = Aig_ManDupRepr( pAig, 0 );
Aig_ManSeqCleanup( pNew );
// Aig_ManPrintStats( pAig );
// Aig_ManPrintStats( pNew );
Vec_VecFree( (Vec_Vec_t *)vResult );
pPars->nPartSize = nPartSize;
pPars->fVerbose = fVerbose;
if ( fVerbose )
{
ABC_PRT( "Total time", Abc_Clock() - clk );
}
return pNew;
}
void Gia_ManRestoreNodeMapping( Aig_Man_t * pAig, Gia_Man_t * pGia )
{
Aig_Obj_t * pObjAig; int i;
assert( Gia_ManObjNum(pGia) == Aig_ManObjNum(pAig) );
Aig_ManForEachObj( pAig, pObjAig, i )
pObjAig->iData = Abc_Var2Lit(i, 0);
}
Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars )
{
Gia_Man_t * pRes = NULL;
Aig_Man_t * pNew = NULL;
Aig_Man_t * pAig = Gia_ManToAigSimple(p);
Ssw_Pars_t SswPars, * pSswPars = &SswPars;
assert( pPars->nProcs > 0 );
assert( pPars->nPartSize > 0 );
Ssw_ManSetDefaultParams( pSswPars );
pSswPars->nBTLimit = pPars->nBTLimit;
pSswPars->nProcs = pPars->nProcs;
pSswPars->nPartSize = pPars->nPartSize;
pSswPars->fVerbose = pPars->fVerbose;
pNew = Ssw_SignalCorrespondencePart2( pAig, pSswPars );
Gia_ManRestoreNodeMapping( pAig, p );
Gia_ManReprFromAigRepr2( pAig, p );
pRes = Gia_ManFromAigSimple(pNew);
Aig_ManStop( pNew );
Aig_ManStop( pAig );
return pRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////