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

Experimental features of &scorr.

This commit is contained in:
Alan Mishchenko 2024-07-28 13:00:32 -07:00
parent 93388c0d26
commit 3e1979f3c6
2 changed files with 205 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -38042,11 +38042,12 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ParCor_t Pars, * pPars = &Pars;
Gia_Man_t * pTemp;
int fPartition = 0;
int nFlopIncFreq = 0;
int fUseOld = 0, c;
Cec_ManCorSetDefaultParams( pPars );
pPars->nProcs = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSpkrecqowvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
{
switch ( c )
{
@ -38116,6 +38117,17 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nPartSize < 0 )
goto usage;
break;
case 'Z':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-Z\" should be followed by an integer.\n" );
goto usage;
}
nFlopIncFreq = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nFlopIncFreq < 0 )
goto usage;
break;
case 'p':
fPartition ^= 1;
break;
@ -38168,6 +38180,31 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 0, "The network is combinational.\n" );
return 0;
}
if ( nFlopIncFreq )
{
extern Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops );
extern Gia_Man_t * Gia_ManDupStopsRem( Gia_Man_t * p, Vec_Int_t * vStops );
extern Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose );
Vec_Int_t * vStops = Gia_ManFindStopFlops( pAbc->pGia, nFlopIncFreq, pPars->fVerbose );
if ( vStops )
{
Gia_Man_t * pUsed = Gia_ManDupStopsAdd( pAbc->pGia, vStops );
if ( pPars->nPartSize > 0 )
pTemp = Gia_SignalCorrespondencePart( pUsed, pPars );
else if ( fUseOld )
pTemp = Cec_ManScorrCorrespondence( pUsed, pPars );
else if ( fPartition )
pTemp = Gia_ManScorrDivideTest( pUsed, pPars );
else
pTemp = Cec_ManLSCorrespondence( pUsed, pPars );
Gia_ManStop( pUsed );
pTemp = Gia_ManDupStopsRem( pUsed = pTemp, vStops );
Gia_ManStop( pUsed );
Abc_FrameUpdateGia( pAbc, pTemp );
Vec_IntFree( vStops );
return 0;
}
}
if ( pPars->nPartSize > 0 )
pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars );
else if ( fUseOld )
@ -38180,7 +38217,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &scorr [-FCGXPS num] [-pkrecqowvh]\n" );
Abc_Print( -2, "usage: &scorr [-FCGXPSZ 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 );
@ -38188,6 +38225,7 @@ usage:
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-Z num : the average flop include frequency [default = %d]\n", nFlopIncFreq );
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" );

165
src/proof/cec/cecCorr.c
View File

@ -1269,6 +1269,171 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Wec_t * Gia_ManCreateRegSupps( Gia_Man_t * p, int fVerbose )
{
abctime clk = Abc_Clock();
Gia_Obj_t * pObj; int i, Id;
Vec_Wec_t * vSuppsR = Vec_WecStart( Gia_ManRegNum(p) );
Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
Gia_ManForEachRo( p, pObj, i )
Vec_IntPush( Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)), i );
Gia_ManForEachAnd( p, pObj, Id )
Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
Vec_WecEntry(vSupps, Id) );
Gia_ManForEachRi( p, pObj, i )
Vec_IntAppend( Vec_WecEntry(vSuppsR, i), Vec_WecEntry(vSupps, Gia_ObjFaninId0p(p, pObj)) );
Vec_WecFree( vSupps );
if ( fVerbose )
Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
return vSuppsR;
}
Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose )
{
Vec_Int_t * vRes = NULL, * vTemp; int i, k, Spot, Temp, nItems = 0;
Vec_Wec_t * vSupps = Gia_ManCreateRegSupps( p, fVerbose );
Vec_Int_t * vNexts = Vec_IntStartFull( Gia_ManRegNum(p) );
Vec_Int_t * vAvail = Vec_IntStart( Gia_ManRegNum(p) );
Vec_Int_t * vHeads = Vec_IntAlloc( 10 );
Vec_WecForEachLevel( vSupps, vTemp, i ) {
if ( Vec_IntSize(vTemp) > 2 )
continue;
if ( (Spot = Vec_IntFind(vTemp, i)) >= 0 )
Vec_IntDrop( vTemp, Spot );
if ( Vec_IntSize(vTemp) != 1 )
continue;
Vec_IntWriteEntry( vNexts, i, Vec_IntEntry(vTemp, 0) );
Vec_IntWriteEntry( vAvail, Vec_IntEntry(vTemp, 0), 1 );
}
Vec_IntForEachEntry( vNexts, Spot, i )
if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 )
Vec_IntPush( vHeads, i );
Vec_IntForEachEntry( vHeads, Spot, i ) {
for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
;
if ( k > 100 )
{
nItems++;
if ( vRes == NULL )
vRes = Vec_IntAlloc( 100 );
for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
if ( k % nFlopIncFreq == 0 )
Vec_IntPush( vRes, Temp );
}
while ( Vec_IntEntry(vNexts, Spot) >= 0 )
{
int Next = Vec_IntEntry(vNexts, Spot);
Vec_IntWriteEntry( vNexts, Spot, -1 );
Spot = Next;
}
}
if ( fVerbose && vRes )
printf( "Detected %d sequence%s containing %d flops.\n", nItems, nItems > 1 ? "s":"", Vec_IntSize(vRes) );
Vec_IntFree( vNexts );
Vec_IntFree( vAvail );
Vec_IntFree( vHeads );
Vec_WecFree( vSupps );
return vRes;
}
Gia_Man_t * Gia_ManDupStopsAdd( Gia_Man_t * p, Vec_Int_t * vStops )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj; int i, Stop;
Vec_Int_t * vExtras = Vec_IntAlloc( Vec_IntSize(vStops) );
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Vec_IntForEachEntry( vStops, Stop, i )
Vec_IntPush( vExtras, Gia_ManAppendCi(pNew) );
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Vec_IntForEachEntry( vStops, Stop, i )
{
int Lit = Gia_ManCi(p, Gia_ManPiNum(p)+Stop)->Value;
Gia_ManCi(p, Gia_ManPiNum(p)+Stop)->Value = Vec_IntEntry(vExtras, i);
Vec_IntWriteEntry( vExtras, i, Lit );
}
Gia_ManForEachAnd( p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachPo( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Vec_IntForEachEntry( vExtras, Stop, i )
Gia_ManAppendCo( pNew, Stop );
Gia_ManForEachRi( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Vec_IntFree( vExtras );
return pNew;
}
void Gia_ManDupStopsRem_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return;
assert( Gia_ObjIsAnd(pObj) );
Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin1(pObj) );
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_Man_t * Gia_ManDupStopsRem( Gia_Man_t * p, Vec_Int_t * vStops )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj; int i;
pNew = Gia_ManStart( Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManFillValue( p );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachPi( p, pObj, i )
if ( i < Gia_ManPiNum(p) - Vec_IntSize(vStops) )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachRo( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachPo( p, pObj, i )
if ( i >= Gia_ManPoNum(p) - Vec_IntSize(vStops) )
Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachPi( p, pObj, i )
if ( i >= Gia_ManPiNum(p) - Vec_IntSize(vStops) )
pObj->Value = Gia_ObjFanin0Copy( Gia_ManPo(p, i - Gia_ManPiNum(p) + Gia_ManPoNum(p)) );
Gia_ManForEachPo( p, pObj, i )
if ( i < Gia_ManPoNum(p) - Vec_IntSize(vStops) )
Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachRi( p, pObj, i )
Gia_ManDupStopsRem_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_ManForEachPo( p, pObj, i )
if ( i < Gia_ManPoNum(p) - Vec_IntSize(vStops) )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManForEachRi( p, pObj, i )
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
Gia_Man_t * Gia_ManDupStopsTest( Gia_Man_t * p )
{
Vec_Int_t * vStops = Gia_ManFindStopFlops( p, 1, 1 );
if ( vStops == NULL )
return Gia_ManDup(p);
Gia_Man_t * pNew1 = Gia_ManDupStopsAdd( p, vStops );
Gia_Man_t * pNew2 = Gia_ManDupStopsRem( pNew1, vStops );
Gia_ManStop( pNew1 );
Vec_IntFree( vStops );
return pNew2;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////