mirror of https://github.com/YosysHQ/abc.git
Merge remote-tracking branch 'upstream/master' into yosys-experimental
This commit is contained in:
Miodrag Milanovic
commit
2a9e9c2a00
|
|
@ -6685,6 +6685,14 @@ SOURCE=.\src\proof\cec\cecCorr.c
|
|||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\proof\cec\cecCorr2.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\proof\cec\cecCorrCert.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
||||
SOURCE=.\src\proof\cec\cecCorrDyn.c
|
||||
# End Source File
|
||||
# Begin Source File
|
||||
|
|
|
|||
|
|
@ -1836,6 +1836,9 @@ extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p );
|
|||
extern void Tas_ManSatPrintStats( Tas_Man_t * p );
|
||||
extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
|
||||
extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
|
||||
extern void Tas_ManSetConflictNum( Tas_Man_t * p, int Num );
|
||||
extern void Tas_ManSyncCore( Tas_Man_t * p );
|
||||
extern Vec_Int_t * Tas_ManSolveRoots( Tas_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose );
|
||||
|
||||
/*=== giaDecGraph.c ===========================================================*/
|
||||
extern Gia_Man_t* Gia_ManDecGraph( Gia_Man_t* p );
|
||||
|
|
@ -1884,4 +1887,3 @@ ABC_NAMESPACE_HEADER_END
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -83,6 +83,7 @@ struct Tas_Man_t_
|
|||
{
|
||||
Tas_Par_t Pars; // parameters
|
||||
Gia_Man_t * pAig; // AIG manager
|
||||
int nSyncedObjs; // pAig objects already prepped (Value/marks/refs) for resident reuse
|
||||
Tas_Que_t pProp; // propagation queue
|
||||
Tas_Que_t pJust; // justification queue
|
||||
Tas_Que_t pClauses; // clause queue
|
||||
|
|
@ -90,6 +91,9 @@ struct Tas_Man_t_
|
|||
Vec_Int_t * vLevReas; // levels and decisions
|
||||
Vec_Int_t * vModel; // satisfying assignment
|
||||
Vec_Ptr_t * vTemp; // temporary storage
|
||||
Vec_Int_t * vOutLits; // optional endpoint literals to sample before cancel
|
||||
Vec_Int_t * vOutVals; // optional endpoint values by output
|
||||
int iOutVal; // current output whose endpoints are sampled
|
||||
// watched clauses
|
||||
Tas_Sto_t pStore; // storage for watched clauses
|
||||
int * pWatches; // watched lists for each literal
|
||||
|
|
@ -308,6 +312,29 @@ static inline void Tas_ManSaveModel( Tas_Man_t * p, Vec_Int_t * vCex )
|
|||
}
|
||||
}
|
||||
|
||||
static inline int Tas_ManLitValue( Tas_Man_t * p, int iLit )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
if ( iLit < 0 )
|
||||
return -1;
|
||||
if ( Abc_Lit2Var(iLit) == 0 )
|
||||
return Abc_LitIsCompl(iLit);
|
||||
pObj = Gia_ManObj( p->pAig, Abc_Lit2Var(iLit) );
|
||||
if ( !Tas_VarIsAssigned(pObj) )
|
||||
return -1;
|
||||
return Tas_VarValue(pObj) ^ Abc_LitIsCompl(iLit);
|
||||
}
|
||||
|
||||
static inline void Tas_ManSaveOutVals( Tas_Man_t * p, Vec_Int_t * vOutLits, Vec_Int_t * vOutVals, int Out )
|
||||
{
|
||||
if ( vOutLits == NULL || vOutVals == NULL )
|
||||
return;
|
||||
if ( 2*Out + 1 >= Vec_IntSize(vOutLits) )
|
||||
return;
|
||||
Vec_IntWriteEntry( vOutVals, 2*Out, Tas_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out) ) );
|
||||
Vec_IntWriteEntry( vOutVals, 2*Out + 1, Tas_ManLitValue( p, Vec_IntEntry(vOutLits, 2*Out + 1) ) );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -1380,7 +1407,10 @@ int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 )
|
|||
if ( pObj2 && !Tas_VarIsAssigned(Gia_Regular(pObj2)) )
|
||||
Tas_ManAssign( p, pObj2, 0, NULL, NULL );
|
||||
if ( !Tas_ManSolve_rec(p, 0) && !Tas_ManCheckLimits(p) )
|
||||
{
|
||||
Tas_ManSaveModel( p, p->vModel );
|
||||
Tas_ManSaveOutVals( p, p->vOutLits, p->vOutVals, p->iOutVal );
|
||||
}
|
||||
else
|
||||
RetValue = 1;
|
||||
Tas_ManCancelUntil( p, 0 );
|
||||
|
|
@ -1514,14 +1544,14 @@ void Tas_ManSatPrintStats( Tas_Man_t * p )
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
|
||||
Vec_Int_t * Tas_ManSolveMiterNcOutVals( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose, Vec_Int_t * vOutLits, Vec_Int_t ** pvOutVals )
|
||||
{
|
||||
extern void Gia_ManCollectTest( Gia_Man_t * pAig );
|
||||
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
|
||||
Tas_Man_t * p;
|
||||
Vec_Int_t * vCex, * vVisit, * vCexStore;
|
||||
Tas_Man_t * p;
|
||||
Vec_Int_t * vCex, * vVisit, * vCexStore, * vOutVals = NULL;
|
||||
Vec_Str_t * vStatus;
|
||||
Gia_Obj_t * pRoot;//, * pRootCopy;
|
||||
Gia_Obj_t * pRoot;//, * pRootCopy;
|
||||
// Gia_Man_t * pAigCopy = Gia_ManDup( pAig ), * pAigTemp;
|
||||
|
||||
int i, status;
|
||||
|
|
@ -1540,6 +1570,12 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
|
|||
// create resulting data-structures
|
||||
vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
|
||||
vCexStore = Vec_IntAlloc( 10000 );
|
||||
if ( pvOutVals )
|
||||
{
|
||||
*pvOutVals = NULL;
|
||||
if ( vOutLits )
|
||||
vOutVals = Vec_IntStartFull( 2 * Gia_ManPoNum(pAig) );
|
||||
}
|
||||
vVisit = Vec_IntAlloc( 100 );
|
||||
vCex = Tas_ReadModel( p );
|
||||
// solve for each output
|
||||
|
|
@ -1567,7 +1603,13 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
|
|||
// p->Pars.fUseActive = 1;
|
||||
p->Pars.fUseHighest = 1;
|
||||
p->Pars.fUseLowest = 0;
|
||||
p->vOutLits = vOutLits;
|
||||
p->vOutVals = vOutVals;
|
||||
p->iOutVal = i;
|
||||
status = Tas_ManSolve( p, Gia_ObjChild0(pRoot), NULL );
|
||||
p->vOutLits = NULL;
|
||||
p->vOutVals = NULL;
|
||||
p->iOutVal = -1;
|
||||
// printf( "\n" );
|
||||
/*
|
||||
if ( status == -1 )
|
||||
|
|
@ -1621,6 +1663,10 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
|
|||
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
|
||||
Tas_ManStop( p );
|
||||
*pvStatus = vStatus;
|
||||
if ( pvOutVals )
|
||||
*pvOutVals = vOutVals;
|
||||
else
|
||||
Vec_IntFreeP( &vOutVals );
|
||||
|
||||
// printf( "Total number of cex literals = %d. (Ave = %d)\n",
|
||||
// Vec_IntSize(vCexStore)-2*p->nSatUndec-2*p->nSatSat,
|
||||
|
|
@ -1628,6 +1674,11 @@ Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
|
|||
return vCexStore;
|
||||
}
|
||||
|
||||
Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose )
|
||||
{
|
||||
return Tas_ManSolveMiterNcOutVals( pAig, nConfs, pvStatus, fVerbose, NULL, NULL );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Packs patterns into array of simulation info.]
|
||||
|
|
@ -1782,10 +1833,144 @@ void Tas_ManSolveMiterNc2( Gia_Man_t * pAig, int nConfs, Gia_Man_t * pAigOld, Ve
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Sets the conflict limit.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Tas_ManSetConflictNum( Tas_Man_t * p, int Num )
|
||||
{
|
||||
p->Pars.nBTLimit = Num;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Syncs newly appended pAig objects for resident reuse.]
|
||||
|
||||
Description [Prepares objects appended since the last sync so the
|
||||
persistent solver can reuse the same manager across rounds. Mirrors
|
||||
Cbs_ManSyncCore but also resizes the TAS-specific watched-literal and
|
||||
activity arrays.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
void Tas_ManSyncCore( Tas_Man_t * p )
|
||||
{
|
||||
Gia_Man_t * pAig = p->pAig;
|
||||
Gia_Obj_t * pObj;
|
||||
int i, nObjs = Gia_ManObjNum( pAig );
|
||||
assert( p->nSyncedObjs <= nObjs );
|
||||
if ( p->nSyncedObjs == nObjs )
|
||||
return;
|
||||
pAig->pRefs = ABC_REALLOC( int, pAig->pRefs, nObjs );
|
||||
memset( pAig->pRefs + p->nSyncedObjs, 0, sizeof(int) * (nObjs - p->nSyncedObjs) );
|
||||
p->pWatches = ABC_REALLOC( int, p->pWatches, 2 * nObjs );
|
||||
memset( p->pWatches + 2 * p->nSyncedObjs, 0, sizeof(int) * 2 * (nObjs - p->nSyncedObjs) );
|
||||
p->pActivity = ABC_REALLOC( float, p->pActivity, nObjs );
|
||||
memset( p->pActivity + p->nSyncedObjs, 0, sizeof(float) * (nObjs - p->nSyncedObjs) );
|
||||
for ( i = p->nSyncedObjs; i < nObjs; i++ )
|
||||
{
|
||||
pObj = Gia_ManObj( pAig, i );
|
||||
pObj->fMark0 = pObj->fMark1 = 0;
|
||||
pObj->Value = ~0;
|
||||
pObj->fPhase = 0;
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
pAig->pRefs[Gia_ObjFaninId0(pObj, i)]++;
|
||||
pAig->pRefs[Gia_ObjFaninId1(pObj, i)]++;
|
||||
}
|
||||
}
|
||||
p->nSyncedObjs = nObjs;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Solves a set of root literals directly on a persistent AIG.]
|
||||
|
||||
Description [Same prover as Tas_ManSolveMiterNc, but each problem is a root
|
||||
literal of p->pAig (no CO needed) instead of a CO of a freshly built view, and
|
||||
the manager is resident: it is allocated once on the persistent COless pCore
|
||||
and reused across rounds, only Tas_ManSyncCore-ing the objects appended since
|
||||
the last call. Output index i corresponds to vRootLits[i]; vCexStore / vStatus
|
||||
format matches Tas_ManSolveMiterNc. CEX is saved by CioId, which on pCore
|
||||
equals the view's CI numbering.]
|
||||
|
||||
SideEffects [Prepares newly appended objects via Tas_ManSyncCore.]
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Tas_ManSolveRoots( Tas_Man_t * p, Vec_Int_t * vRootLits, Vec_Str_t ** pvStatus, int fVerbose )
|
||||
{
|
||||
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
|
||||
Gia_Man_t * pAig = p->pAig;
|
||||
Vec_Int_t * vCex, * vCexStore;
|
||||
Vec_Str_t * vStatus;
|
||||
int i, iLit, status;
|
||||
abctime clk, clkTotal = Abc_Clock();
|
||||
assert( Gia_ManRegNum(pAig) == 0 );
|
||||
Tas_ManSyncCore( p ); // prep only objects appended since the last solve
|
||||
vStatus = Vec_StrAlloc( Vec_IntSize(vRootLits) );
|
||||
vCexStore = Vec_IntAlloc( 10000 );
|
||||
vCex = Tas_ReadModel( p );
|
||||
Vec_IntForEachEntry( vRootLits, iLit, i )
|
||||
{
|
||||
Vec_IntClear( vCex );
|
||||
if ( Abc_Lit2Var(iLit) == 0 ) // structural constant root
|
||||
{
|
||||
if ( Abc_LitIsCompl(iLit) ) // const 1: trivial counter-example
|
||||
{
|
||||
Cec_ManSatAddToStore( vCexStore, vCex, i );
|
||||
Vec_StrPush( vStatus, 0 );
|
||||
}
|
||||
else // const 0: proved
|
||||
Vec_StrPush( vStatus, 1 );
|
||||
continue;
|
||||
}
|
||||
clk = Abc_Clock();
|
||||
p->Pars.fUseHighest = 1;
|
||||
p->Pars.fUseLowest = 0;
|
||||
status = Tas_ManSolve( p, Gia_ObjFromLit(pAig, iLit), NULL );
|
||||
Vec_StrPush( vStatus, (char)status );
|
||||
if ( status == -1 )
|
||||
{
|
||||
p->nSatUndec++;
|
||||
p->nConfUndec += p->Pars.nBTThis;
|
||||
Cec_ManSatAddToStore( vCexStore, NULL, i ); // timeout
|
||||
p->timeSatUndec += Abc_Clock() - clk;
|
||||
continue;
|
||||
}
|
||||
if ( status == 0 )
|
||||
{
|
||||
p->nSatSat++;
|
||||
p->nConfSat += p->Pars.nBTThis;
|
||||
Cec_ManSatAddToStore( vCexStore, vCex, i );
|
||||
p->timeSatSat += Abc_Clock() - clk;
|
||||
continue;
|
||||
}
|
||||
assert( status == 1 );
|
||||
p->nSatUnsat++;
|
||||
p->nConfUnsat += p->Pars.nBTThis;
|
||||
p->timeSatUnsat += Abc_Clock() - clk;
|
||||
}
|
||||
p->nSatTotal += Vec_IntSize(vRootLits);
|
||||
p->timeTotal += Abc_Clock() - clkTotal;
|
||||
*pvStatus = vStatus;
|
||||
return vCexStore;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
|
|||
|
|
@ -3564,10 +3564,435 @@ void Gia_ManFindMutualEquivsTest()
|
|||
}
|
||||
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Prints longest combinational paths between seq endpoints.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static char * Gia_ManPrintPathNameFallback( Gia_Man_t * p, int fCi, int iTerm, char * pBuffer )
|
||||
{
|
||||
if ( fCi )
|
||||
{
|
||||
if ( iTerm < Gia_ManPiNum(p) )
|
||||
sprintf( pBuffer, "pi%d", iTerm );
|
||||
else
|
||||
sprintf( pBuffer, "ro%d", iTerm - Gia_ManPiNum(p) );
|
||||
}
|
||||
else
|
||||
{
|
||||
if ( iTerm < Gia_ManPoNum(p) )
|
||||
sprintf( pBuffer, "po%d", iTerm );
|
||||
else
|
||||
sprintf( pBuffer, "ri%d", iTerm - Gia_ManPoNum(p) );
|
||||
}
|
||||
return pBuffer;
|
||||
}
|
||||
static int Gia_ManPrintPathNameBufferSize( Gia_Man_t * p )
|
||||
{
|
||||
Vec_Ptr_t * vNames;
|
||||
char * pName;
|
||||
int i, nSize = 64;
|
||||
vNames = p->vNamesIn;
|
||||
if ( vNames )
|
||||
Vec_PtrForEachEntry( char *, vNames, pName, i )
|
||||
if ( pName )
|
||||
nSize = Abc_MaxInt( nSize, (int)strlen(pName) + 64 );
|
||||
vNames = p->vNamesOut;
|
||||
if ( vNames )
|
||||
Vec_PtrForEachEntry( char *, vNames, pName, i )
|
||||
if ( pName )
|
||||
nSize = Abc_MaxInt( nSize, (int)strlen(pName) + 64 );
|
||||
return nSize;
|
||||
}
|
||||
static void Gia_ManPrintPathCopyToken( char * pBuffer, char * pBeg, char * pEnd )
|
||||
{
|
||||
int nChars = pEnd ? (int)(pEnd - pBeg) : (int)strlen(pBeg);
|
||||
memcpy( pBuffer, pBeg, nChars );
|
||||
pBuffer[nChars] = 0;
|
||||
}
|
||||
static char * Gia_ManPrintPathName( Gia_Man_t * p, int fCi, int iTerm, char * pBuffer, int fFull, int fLeaf )
|
||||
{
|
||||
Vec_Ptr_t * vNames = fCi ? p->vNamesIn : p->vNamesOut;
|
||||
char * pName = vNames && iTerm < Vec_PtrSize(vNames) ? (char *)Vec_PtrEntry(vNames, iTerm) : NULL;
|
||||
char * pBeg, * pEnd, * pFirst, * pFirstEnd;
|
||||
if ( pName == NULL )
|
||||
return Gia_ManPrintPathNameFallback( p, fCi, iTerm, pBuffer );
|
||||
if ( fFull )
|
||||
return pName;
|
||||
if ( fLeaf )
|
||||
{
|
||||
pBeg = strrchr( pName, ' ' );
|
||||
return pBeg ? pBeg + 1 : pName;
|
||||
}
|
||||
pFirst = pName;
|
||||
pFirstEnd = strchr( pFirst, ' ' );
|
||||
for ( pBeg = pName; pBeg && *pBeg; pBeg = pEnd ? pEnd + 1 : NULL )
|
||||
{
|
||||
pEnd = strchr( pBeg, ' ' );
|
||||
if ( strstr( pBeg, "reg_" ) && (pEnd == NULL || pEnd > strstr( pBeg, "reg_" )) )
|
||||
{
|
||||
Gia_ManPrintPathCopyToken( pBuffer, pBeg, pEnd );
|
||||
return pBuffer;
|
||||
}
|
||||
}
|
||||
Gia_ManPrintPathCopyToken( pBuffer, pFirst, pFirstEnd );
|
||||
return pBuffer;
|
||||
}
|
||||
static char * Gia_ManPrintPathKind( Gia_Man_t * p, int fCi, int iTerm )
|
||||
{
|
||||
if ( fCi )
|
||||
return iTerm < Gia_ManPiNum(p) ? (char *)"PI" : (char *)"RO";
|
||||
return iTerm < Gia_ManPoNum(p) ? (char *)"PO" : (char *)"RI";
|
||||
}
|
||||
static int Gia_ManPrintPathTermIndex( Gia_Man_t * p, int fCi, int iTerm )
|
||||
{
|
||||
if ( fCi )
|
||||
return iTerm < Gia_ManPiNum(p) ? iTerm : iTerm - Gia_ManPiNum(p);
|
||||
return iTerm < Gia_ManPoNum(p) ? iTerm : iTerm - Gia_ManPoNum(p);
|
||||
}
|
||||
static int Gia_ManPrintPathParseBit( char * pName, char * pBase, int * pBit, char * pSuffix )
|
||||
{
|
||||
char * pLeft = strrchr( pName, '[' );
|
||||
char * pRight = pLeft ? strchr( pLeft, ']' ) : NULL;
|
||||
char * pTemp;
|
||||
if ( pLeft == NULL || pRight == NULL )
|
||||
return 0;
|
||||
for ( pTemp = pLeft + 1; pTemp < pRight; pTemp++ )
|
||||
if ( *pTemp < '0' || *pTemp > '9' )
|
||||
return 0;
|
||||
Gia_ManPrintPathCopyToken( pBase, pName, pLeft );
|
||||
Gia_ManPrintPathCopyToken( pSuffix, pRight + 1, NULL );
|
||||
*pBit = atoi( pLeft + 1 );
|
||||
return 1;
|
||||
}
|
||||
static void Gia_ManPrintPathFormatTermRange( char * pBuffer, char * pKind, int iBeg, int iEnd )
|
||||
{
|
||||
if ( iBeg == iEnd )
|
||||
sprintf( pBuffer, "%s[%d]", pKind, iBeg );
|
||||
else
|
||||
sprintf( pBuffer, "%s[%d..%d]", pKind, iBeg, iEnd );
|
||||
}
|
||||
static void Gia_ManPrintPathFormatNameRange( char * pBuffer, char * pNameBeg, char * pNameEnd, int nNameSize )
|
||||
{
|
||||
char * BaseBeg, * BaseEnd, * SuffixBeg, * SuffixEnd;
|
||||
int BitBeg, BitEnd;
|
||||
if ( !strcmp(pNameBeg, pNameEnd) )
|
||||
{
|
||||
sprintf( pBuffer, "%s", pNameBeg );
|
||||
return;
|
||||
}
|
||||
BaseBeg = ABC_ALLOC( char, nNameSize );
|
||||
BaseEnd = ABC_ALLOC( char, nNameSize );
|
||||
SuffixBeg = ABC_ALLOC( char, nNameSize );
|
||||
SuffixEnd = ABC_ALLOC( char, nNameSize );
|
||||
if ( Gia_ManPrintPathParseBit(pNameBeg, BaseBeg, &BitBeg, SuffixBeg) &&
|
||||
Gia_ManPrintPathParseBit(pNameEnd, BaseEnd, &BitEnd, SuffixEnd) &&
|
||||
!strcmp(BaseBeg, BaseEnd) && !strcmp(SuffixBeg, SuffixEnd) )
|
||||
sprintf( pBuffer, "%s[%d..%d]%s", BaseBeg, BitBeg, BitEnd, SuffixBeg );
|
||||
else
|
||||
sprintf( pBuffer, "%s..%s", pNameBeg, pNameEnd );
|
||||
ABC_FREE( BaseBeg );
|
||||
ABC_FREE( BaseEnd );
|
||||
ABC_FREE( SuffixBeg );
|
||||
ABC_FREE( SuffixEnd );
|
||||
}
|
||||
static int Gia_ManPrintPathCanGroup( Gia_Man_t * p, int Level0, int Source0, int Sink0, int Level1, int Source1, int Sink1, int nNameSize )
|
||||
{
|
||||
char * pStore, * Buffer0, * Buffer1, * Buffer2, * Buffer3, * Base0, * Base1, * Suffix0, * Suffix1;
|
||||
int Bit0, Bit1;
|
||||
int RetValue;
|
||||
if ( Level0 != Level1 || Source0 != Source1 )
|
||||
return 0;
|
||||
if ( (Sink0 < Gia_ManPoNum(p)) != (Sink1 < Gia_ManPoNum(p)) )
|
||||
return 0;
|
||||
if ( Gia_ManPrintPathTermIndex(p, 0, Sink1) != Gia_ManPrintPathTermIndex(p, 0, Sink0) + 1 )
|
||||
return 0;
|
||||
pStore = ABC_ALLOC( char, 8 * nNameSize );
|
||||
Buffer0 = pStore + 0 * nNameSize;
|
||||
Buffer1 = pStore + 1 * nNameSize;
|
||||
Buffer2 = pStore + 2 * nNameSize;
|
||||
Buffer3 = pStore + 3 * nNameSize;
|
||||
Base0 = pStore + 4 * nNameSize;
|
||||
Base1 = pStore + 5 * nNameSize;
|
||||
Suffix0 = pStore + 6 * nNameSize;
|
||||
Suffix1 = pStore + 7 * nNameSize;
|
||||
Gia_ManPrintPathName( p, 1, Source0, Buffer0, 0, 0 );
|
||||
Gia_ManPrintPathName( p, 1, Source1, Buffer1, 0, 0 );
|
||||
if ( strcmp(Buffer0, Buffer1) )
|
||||
{
|
||||
ABC_FREE( pStore );
|
||||
return 0;
|
||||
}
|
||||
Gia_ManPrintPathName( p, 1, Source0, Buffer0, 0, 1 );
|
||||
Gia_ManPrintPathName( p, 1, Source1, Buffer1, 0, 1 );
|
||||
if ( strcmp(Buffer0, Buffer1) )
|
||||
{
|
||||
ABC_FREE( pStore );
|
||||
return 0;
|
||||
}
|
||||
Gia_ManPrintPathName( p, 0, Sink0, Buffer2, 0, 0 );
|
||||
Gia_ManPrintPathName( p, 0, Sink1, Buffer3, 0, 0 );
|
||||
if ( !Gia_ManPrintPathParseBit(Buffer2, Base0, &Bit0, Suffix0) ||
|
||||
!Gia_ManPrintPathParseBit(Buffer3, Base1, &Bit1, Suffix1) )
|
||||
{
|
||||
ABC_FREE( pStore );
|
||||
return 0;
|
||||
}
|
||||
RetValue = !strcmp(Base0, Base1) && !strcmp(Suffix0, Suffix1) && Bit1 == Bit0 + 1;
|
||||
ABC_FREE( pStore );
|
||||
return RetValue;
|
||||
}
|
||||
static int Gia_ManPrintPathCandBetter( int Level0, int Source0, int Sink0, int Level1, int Source1, int Sink1 )
|
||||
{
|
||||
if ( Level0 != Level1 )
|
||||
return Level0 > Level1;
|
||||
if ( Source0 != Source1 )
|
||||
return Source0 < Source1;
|
||||
return Sink0 < Sink1;
|
||||
}
|
||||
static int Gia_ManPrintPathFaninBetter( int Level0, int Source0, int Level1, int Source1 )
|
||||
{
|
||||
if ( Source0 < 0 )
|
||||
return 0;
|
||||
if ( Source1 < 0 )
|
||||
return 1;
|
||||
if ( Level0 != Level1 )
|
||||
return Level0 > Level1;
|
||||
return Source0 < Source1;
|
||||
}
|
||||
static void Gia_ManPrintPathInsert( int * pLevels, int * pSources, int * pSinks, int * pDrivers, int * pnPaths, int nPathsMax, int Level, int Source, int Sink, int Driver )
|
||||
{
|
||||
int i, k, nPaths = *pnPaths;
|
||||
if ( Source < 0 )
|
||||
return;
|
||||
for ( i = 0; i < nPaths; i++ )
|
||||
if ( Gia_ManPrintPathCandBetter(Level, Source, Sink, pLevels[i], pSources[i], pSinks[i]) )
|
||||
break;
|
||||
if ( i == nPathsMax )
|
||||
return;
|
||||
if ( nPaths < nPathsMax )
|
||||
nPaths++;
|
||||
for ( k = nPaths - 1; k > i; k-- )
|
||||
{
|
||||
pLevels[k] = pLevels[k-1];
|
||||
pSources[k] = pSources[k-1];
|
||||
pSinks[k] = pSinks[k-1];
|
||||
pDrivers[k] = pDrivers[k-1];
|
||||
}
|
||||
pLevels[i] = Level;
|
||||
pSources[i] = Source;
|
||||
pSinks[i] = Sink;
|
||||
pDrivers[i] = Driver;
|
||||
*pnPaths = nPaths;
|
||||
}
|
||||
static void Gia_ManPrintPathOne( Gia_Man_t * p, Vec_Int_t * vPreds, int Source, int Sink, int Driver, int nNameSize )
|
||||
{
|
||||
Vec_Int_t * vPath = Vec_IntAlloc( 100 );
|
||||
char * pBuffer = ABC_ALLOC( char, 2 * nNameSize );
|
||||
char * pBuffer0 = pBuffer;
|
||||
char * pBuffer1 = pBuffer + nNameSize;
|
||||
int i, Id;
|
||||
for ( Id = Driver; Id > 0 && !Gia_ObjIsCi(Gia_ManObj(p, Id)); Id = Vec_IntEntry(vPreds, Id) )
|
||||
{
|
||||
Vec_IntPush( vPath, Id );
|
||||
if ( Vec_IntEntry(vPreds, Id) < 0 )
|
||||
break;
|
||||
}
|
||||
printf( " %s[%d] %s", Gia_ManPrintPathKind(p, 1, Source), Gia_ManPrintPathTermIndex(p, 1, Source), Gia_ManPrintPathName(p, 1, Source, pBuffer0, 1, 0) );
|
||||
Vec_IntForEachEntryReverse( vPath, Id, i )
|
||||
printf( " -> AND %d", Id );
|
||||
printf( " -> %s[%d] %s\n", Gia_ManPrintPathKind(p, 0, Sink), Gia_ManPrintPathTermIndex(p, 0, Sink), Gia_ManPrintPathName(p, 0, Sink, pBuffer1, 1, 0) );
|
||||
ABC_FREE( pBuffer );
|
||||
Vec_IntFree( vPath );
|
||||
}
|
||||
void Gia_ManPrintPath( Gia_Man_t * p, int nPathsMax, int fVerbose, int fSummary )
|
||||
{
|
||||
Vec_Int_t * vLevels, * vSources, * vPreds;
|
||||
Vec_Int_t * vGroupStarts, * vGroupEnds;
|
||||
Gia_Obj_t * pObj;
|
||||
int * pLevels, * pSources, * pSinks, * pDrivers;
|
||||
int nGroupsMax = nPathsMax;
|
||||
int nPathsAlloc, nNameSize, nLineSize, nSourceTermW, nSourceNameW, nSinkTermW;
|
||||
int nPaths = 0, Counts[4] = {0}, MaxLevels[4] = {0};
|
||||
int i, k, Id, FanId, Level, Source, Sink, Driver, Cost, LevelBest, SourceBest, FanBest, nGroups, iBeg, iEnd;
|
||||
char * Buffer0, * Buffer1, * Buffer2, * Buffer3, * Buffer4, * Buffer5, * Buffer6, * Buffer7, * Buffer8, * Buffer9, * Buffer10;
|
||||
if ( nPathsMax < 1 )
|
||||
nPathsMax = 1;
|
||||
nGroupsMax = nPathsMax;
|
||||
nPathsAlloc = Abc_MinInt( Gia_ManCoNum(p), Abc_MaxInt(32 * nGroupsMax, nGroupsMax) );
|
||||
nNameSize = Gia_ManPrintPathNameBufferSize( p );
|
||||
nLineSize = 4 * nNameSize + 100;
|
||||
Buffer0 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer1 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer2 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer3 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer4 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer5 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer6 = ABC_ALLOC( char, nNameSize );
|
||||
Buffer7 = ABC_ALLOC( char, nLineSize );
|
||||
Buffer8 = ABC_ALLOC( char, nLineSize );
|
||||
Buffer9 = ABC_ALLOC( char, nLineSize );
|
||||
Buffer10 = ABC_ALLOC( char, nLineSize );
|
||||
vGroupStarts = Vec_IntAlloc( nGroupsMax );
|
||||
vGroupEnds = Vec_IntAlloc( nGroupsMax );
|
||||
vLevels = Vec_IntStart( Gia_ManObjNum(p) );
|
||||
vSources = Vec_IntStartFull( Gia_ManObjNum(p) );
|
||||
vPreds = Vec_IntStartFull( Gia_ManObjNum(p) );
|
||||
Gia_ManForEachObj( p, pObj, i )
|
||||
{
|
||||
Id = Gia_ObjId( p, pObj );
|
||||
if ( Gia_ObjIsCi(pObj) )
|
||||
{
|
||||
Vec_IntWriteEntry( vLevels, Id, 0 );
|
||||
Vec_IntWriteEntry( vSources, Id, Gia_ObjCioId(pObj) );
|
||||
continue;
|
||||
}
|
||||
if ( !Gia_ObjIsAnd(pObj) )
|
||||
continue;
|
||||
Cost = (!p->fGiaSimple && Gia_ObjIsBuf(pObj)) ? 0 : (Gia_ObjIsMux(p, pObj) || Gia_ObjIsXor(pObj) ? 2 : 1);
|
||||
LevelBest = SourceBest = FanBest = -1;
|
||||
for ( k = 0; k < Gia_ObjFaninNum(p, pObj); k++ )
|
||||
{
|
||||
FanId = k == 2 ? Gia_ObjFaninId2(p, Id) : Gia_ObjFaninId(pObj, Id, k);
|
||||
Level = Vec_IntEntry( vLevels, FanId );
|
||||
Source = Vec_IntEntry( vSources, FanId );
|
||||
if ( Gia_ManPrintPathFaninBetter(Level, Source, LevelBest, SourceBest) )
|
||||
LevelBest = Level, SourceBest = Source, FanBest = FanId;
|
||||
}
|
||||
Vec_IntWriteEntry( vLevels, Id, LevelBest + Cost );
|
||||
Vec_IntWriteEntry( vSources, Id, SourceBest );
|
||||
Vec_IntWriteEntry( vPreds, Id, FanBest );
|
||||
}
|
||||
pLevels = ABC_ALLOC( int, nPathsAlloc );
|
||||
pSources = ABC_ALLOC( int, nPathsAlloc );
|
||||
pSinks = ABC_ALLOC( int, nPathsAlloc );
|
||||
pDrivers = ABC_ALLOC( int, nPathsAlloc );
|
||||
Gia_ManForEachCo( p, pObj, i )
|
||||
{
|
||||
Driver = Gia_ObjFaninId0p( p, pObj );
|
||||
Level = Vec_IntEntry( vLevels, Driver );
|
||||
Source = Vec_IntEntry( vSources, Driver );
|
||||
Sink = Gia_ObjCioId( pObj );
|
||||
if ( Source >= 0 )
|
||||
{
|
||||
k = (Source >= Gia_ManPiNum(p) ? 2 : 0) + (Sink >= Gia_ManPoNum(p) ? 1 : 0);
|
||||
Counts[k]++;
|
||||
MaxLevels[k] = Abc_MaxInt( MaxLevels[k], Level );
|
||||
}
|
||||
Gia_ManPrintPathInsert( pLevels, pSources, pSinks, pDrivers, &nPaths, nPathsAlloc, Level, Source, Sink, Driver );
|
||||
}
|
||||
for ( i = 0, nGroups = 0; i < nPaths && nGroups < nGroupsMax; i = iEnd + 1, nGroups++ )
|
||||
{
|
||||
iBeg = iEnd = i;
|
||||
while ( iEnd + 1 < nPaths && Gia_ManPrintPathCanGroup(p, pLevels[iEnd], pSources[iEnd], pSinks[iEnd], pLevels[iEnd+1], pSources[iEnd+1], pSinks[iEnd+1], nNameSize) )
|
||||
iEnd++;
|
||||
Vec_IntPush( vGroupStarts, iBeg );
|
||||
Vec_IntPush( vGroupEnds, iEnd );
|
||||
}
|
||||
nSourceTermW = (int)strlen( "source" );
|
||||
nSourceNameW = 0;
|
||||
nSinkTermW = (int)strlen( "sink" );
|
||||
Vec_IntForEachEntry( vGroupStarts, iBeg, i )
|
||||
{
|
||||
char * pSourceName, * pSourceLeaf, * pSinkNameBeg, * pSinkNameEnd, * pSinkLeafBeg, * pSinkLeafEnd;
|
||||
iEnd = Vec_IntEntry( vGroupEnds, i );
|
||||
pSourceName = Gia_ManPrintPathName(p, 1, pSources[iBeg], Buffer0, 0, 0);
|
||||
pSourceLeaf = Gia_ManPrintPathName(p, 1, pSources[iBeg], Buffer1, 0, 1);
|
||||
pSinkNameBeg = Gia_ManPrintPathName(p, 0, pSinks[iBeg], Buffer2, 0, 0);
|
||||
pSinkNameEnd = Gia_ManPrintPathName(p, 0, pSinks[iEnd], Buffer3, 0, 0);
|
||||
pSinkLeafBeg = Gia_ManPrintPathName(p, 0, pSinks[iBeg], Buffer4, 0, 1);
|
||||
pSinkLeafEnd = Gia_ManPrintPathName(p, 0, pSinks[iEnd], Buffer5, 0, 1);
|
||||
Gia_ManPrintPathFormatTermRange( Buffer6, Gia_ManPrintPathKind(p, 1, pSources[iBeg]), Gia_ManPrintPathTermIndex(p, 1, pSources[iBeg]), Gia_ManPrintPathTermIndex(p, 1, pSources[iBeg]) );
|
||||
sprintf( Buffer7, "%s", pSourceName );
|
||||
if ( strcmp(pSourceName, pSourceLeaf) )
|
||||
sprintf( Buffer7 + strlen(Buffer7), "->%s", pSourceLeaf );
|
||||
Gia_ManPrintPathFormatTermRange( Buffer8, Gia_ManPrintPathKind(p, 0, pSinks[iBeg]), Gia_ManPrintPathTermIndex(p, 0, pSinks[iBeg]), Gia_ManPrintPathTermIndex(p, 0, pSinks[iEnd]) );
|
||||
Gia_ManPrintPathFormatNameRange( Buffer9, pSinkNameBeg, pSinkNameEnd, nNameSize );
|
||||
if ( strcmp(pSinkLeafBeg, pSinkLeafEnd) )
|
||||
Gia_ManPrintPathFormatNameRange( Buffer10, pSinkLeafBeg, pSinkLeafEnd, nNameSize );
|
||||
else
|
||||
sprintf( Buffer10, "%s", pSinkLeafBeg );
|
||||
if ( strcmp(Buffer9, Buffer10) )
|
||||
sprintf( Buffer9 + strlen(Buffer9), "<-%s", Buffer10 );
|
||||
nSourceTermW = Abc_MaxInt( nSourceTermW, (int)strlen(Buffer6) );
|
||||
nSourceNameW = Abc_MaxInt( nSourceNameW, (int)strlen(Buffer7) );
|
||||
nSinkTermW = Abc_MaxInt( nSinkTermW, (int)strlen(Buffer8) );
|
||||
}
|
||||
printf( "Grouped critical combinational paths:\n" );
|
||||
printf( " rank paths lev %-*s %-*s %-*s %s\n", nSourceTermW, "source", nSourceNameW, "", nSinkTermW, "sink", "" );
|
||||
Vec_IntForEachEntry( vGroupStarts, iBeg, i )
|
||||
{
|
||||
char * pSourceName, * pSourceLeaf, * pSinkNameBeg, * pSinkNameEnd, * pSinkLeafBeg, * pSinkLeafEnd;
|
||||
iEnd = Vec_IntEntry( vGroupEnds, i );
|
||||
pSourceName = Gia_ManPrintPathName(p, 1, pSources[iBeg], Buffer0, 0, 0);
|
||||
pSourceLeaf = Gia_ManPrintPathName(p, 1, pSources[iBeg], Buffer1, 0, 1);
|
||||
pSinkNameBeg = Gia_ManPrintPathName(p, 0, pSinks[iBeg], Buffer2, 0, 0);
|
||||
pSinkNameEnd = Gia_ManPrintPathName(p, 0, pSinks[iEnd], Buffer3, 0, 0);
|
||||
pSinkLeafBeg = Gia_ManPrintPathName(p, 0, pSinks[iBeg], Buffer4, 0, 1);
|
||||
pSinkLeafEnd = Gia_ManPrintPathName(p, 0, pSinks[iEnd], Buffer5, 0, 1);
|
||||
Gia_ManPrintPathFormatTermRange( Buffer6, Gia_ManPrintPathKind(p, 1, pSources[iBeg]), Gia_ManPrintPathTermIndex(p, 1, pSources[iBeg]), Gia_ManPrintPathTermIndex(p, 1, pSources[iBeg]) );
|
||||
sprintf( Buffer7, "%s", pSourceName );
|
||||
if ( strcmp(pSourceName, pSourceLeaf) )
|
||||
sprintf( Buffer7 + strlen(Buffer7), "->%s", pSourceLeaf );
|
||||
Gia_ManPrintPathFormatTermRange( Buffer8, Gia_ManPrintPathKind(p, 0, pSinks[iBeg]), Gia_ManPrintPathTermIndex(p, 0, pSinks[iBeg]), Gia_ManPrintPathTermIndex(p, 0, pSinks[iEnd]) );
|
||||
Gia_ManPrintPathFormatNameRange( Buffer9, pSinkNameBeg, pSinkNameEnd, nNameSize );
|
||||
if ( strcmp(pSinkLeafBeg, pSinkLeafEnd) )
|
||||
Gia_ManPrintPathFormatNameRange( Buffer10, pSinkLeafBeg, pSinkLeafEnd, nNameSize );
|
||||
else
|
||||
sprintf( Buffer10, "%s", pSinkLeafBeg );
|
||||
if ( strcmp(Buffer9, Buffer10) )
|
||||
sprintf( Buffer9 + strlen(Buffer9), "<-%s", Buffer10 );
|
||||
if ( iBeg == iEnd )
|
||||
sprintf( Buffer4, "%d", iBeg + 1 );
|
||||
else
|
||||
sprintf( Buffer4, "%d..%d", iBeg + 1, iEnd + 1 );
|
||||
printf( "%5d %-7s %3d %-*s %-*s %-*s %s\n", i + 1, Buffer4, pLevels[iBeg], nSourceTermW, Buffer6, nSourceNameW, Buffer7, nSinkTermW, Buffer8, Buffer9 );
|
||||
}
|
||||
if ( fVerbose )
|
||||
{
|
||||
printf( "\nAIG paths:\n" );
|
||||
Vec_IntForEachEntry( vGroupStarts, iBeg, i )
|
||||
Gia_ManPrintPathOne( p, vPreds, pSources[iBeg], pSinks[iBeg], pDrivers[iBeg], nNameSize );
|
||||
}
|
||||
if ( fSummary )
|
||||
{
|
||||
printf( "\nEndpoint summary:\n" );
|
||||
printf( " PI->PO : paths = %7d max levels = %6d\n", Counts[0], MaxLevels[0] );
|
||||
printf( " PI->RI : paths = %7d max levels = %6d\n", Counts[1], MaxLevels[1] );
|
||||
printf( " RO->PO : paths = %7d max levels = %6d\n", Counts[2], MaxLevels[2] );
|
||||
printf( " RO->RI : paths = %7d max levels = %6d\n", Counts[3], MaxLevels[3] );
|
||||
}
|
||||
ABC_FREE( pLevels );
|
||||
ABC_FREE( pSources );
|
||||
ABC_FREE( pSinks );
|
||||
ABC_FREE( pDrivers );
|
||||
ABC_FREE( Buffer0 );
|
||||
ABC_FREE( Buffer1 );
|
||||
ABC_FREE( Buffer2 );
|
||||
ABC_FREE( Buffer3 );
|
||||
ABC_FREE( Buffer4 );
|
||||
ABC_FREE( Buffer5 );
|
||||
ABC_FREE( Buffer6 );
|
||||
ABC_FREE( Buffer7 );
|
||||
ABC_FREE( Buffer8 );
|
||||
ABC_FREE( Buffer9 );
|
||||
ABC_FREE( Buffer10 );
|
||||
Vec_IntFree( vLevels );
|
||||
Vec_IntFree( vSources );
|
||||
Vec_IntFree( vPreds );
|
||||
Vec_IntFreeP( &vGroupStarts );
|
||||
Vec_IntFreeP( &vGroupEnds );
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
|
|||
|
|
@ -65,6 +65,7 @@
|
|||
#include "opt/fret/fretime.h"
|
||||
#include "opt/nwk/nwkMerge.h"
|
||||
#include "base/acb/acbPar.h"
|
||||
#include "base/wln/wln.h"
|
||||
#include "misc/extra/extra.h"
|
||||
#include "opt/eslim/eSLIM.h"
|
||||
|
||||
|
|
@ -494,6 +495,7 @@ static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandAbc9Scl ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Lcorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Scorr ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Scorr2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Choice ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9SatEnum ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
|
@ -666,6 +668,7 @@ static int Abc_CommandAbc9Divide ( Abc_Frame_t * pAbc, int argc, cha
|
|||
static int Abc_CommandAbc9Pipeline ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Unpipeline ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9Regio ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
static int Abc_CommandAbc9PrintPath ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv );
|
||||
|
||||
|
|
@ -1345,6 +1348,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "ABC9", "&scl", Abc_CommandAbc9Scl, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&lcorr", Abc_CommandAbc9Lcorr, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&scorr", Abc_CommandAbc9Scorr, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&scorr2", Abc_CommandAbc9Scorr2, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&choice", Abc_CommandAbc9Choice, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&sat", Abc_CommandAbc9Sat, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&satenum", Abc_CommandAbc9SatEnum, 0 );
|
||||
|
|
@ -1524,6 +1528,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "ABC9", "&unpipe", Abc_CommandAbc9Unpipeline, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "®io", Abc_CommandAbc9Regio, 0 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&print_path", Abc_CommandAbc9PrintPath, 0 );
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 );
|
||||
|
||||
Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 );
|
||||
|
|
@ -35114,9 +35119,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Aig_Man_t * pAig;
|
||||
Gia_Man_t * pGia, * pTemp;
|
||||
char * pInits;
|
||||
int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fReuseNames = 0, fVerbose = 0;
|
||||
int c, fGiaSimple = 0, fMapped = 0, fNames = 0, fReuseNames = 0, fSibls = 0, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "cmnrvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "cmnrvsh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -35135,6 +35140,9 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 's':
|
||||
fSibls ^= 1;
|
||||
break;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
|
|
@ -35170,10 +35178,15 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
else
|
||||
{
|
||||
if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
|
||||
{
|
||||
pAig = Abc_NtkToDarChoices( pAbc->pNtkCur );
|
||||
pGia = fSibls ? Gia_ManFromAigChoices( pAig ) : Gia_ManFromAig( pAig );
|
||||
}
|
||||
else
|
||||
{
|
||||
pAig = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
|
||||
pGia = Gia_ManFromAig( pAig );
|
||||
pGia = Gia_ManFromAig( pAig );
|
||||
}
|
||||
Aig_ManStop( pAig );
|
||||
}
|
||||
// copy names
|
||||
|
|
@ -35218,7 +35231,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &get [-cmnrvh] <file>\n" );
|
||||
Abc_Print( -2, "usage: &get [-cmnrvsh] <file>\n" );
|
||||
Abc_Print( -2, "\t converts the current network into GIA and moves it to the &-space\n" );
|
||||
Abc_Print( -2, "\t (if the network is a sequential logic network, normalizes the flops\n" );
|
||||
Abc_Print( -2, "\t to have const-0 initial values, equivalent to \"undc; st; zero\")\n" );
|
||||
|
|
@ -35227,6 +35240,7 @@ usage:
|
|||
Abc_Print( -2, "\t-n : toggles saving CI/CO names of the AIG [default = %s]\n", fNames? "yes": "no" );
|
||||
Abc_Print( -2, "\t-r : toggles reusing CI/CO names of the current AIG [default = %s]\n", fReuseNames? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggles additional verbose output [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-s : toggles exporting choice nodes as GIA siblings (pSibls) for &if-based mapping [default = %s]\n", fSibls? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Abc_Print( -2, "\t<file> : the file name\n");
|
||||
return 1;
|
||||
|
|
@ -41824,7 +41838,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Cec_ManCorSetDefaultParams( pPars );
|
||||
pPars->nProcs = 1;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqiowvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZpkrecqowvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -41923,9 +41937,6 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
case 'q':
|
||||
pPars->fStopWhenGone ^= 1;
|
||||
break;
|
||||
case 'i':
|
||||
pPars->fIncremental ^= 1;
|
||||
break;
|
||||
case 'o':
|
||||
fUseOld ^= 1;
|
||||
break;
|
||||
|
|
@ -41939,13 +41950,6 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pPars->fIncremental )
|
||||
{
|
||||
//preserve for incremental mode, maybe should be a separate command
|
||||
pPars->fDynSrm = 1; //dynamic SRM
|
||||
pPars->fIncrSim = 1; //incremental simulation
|
||||
pPars->fSkipFailResim = 1; //skip resimulation of failed flops
|
||||
}
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Scorr(): There is no AIG.\n" );
|
||||
|
|
@ -42006,7 +42010,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &scorr [-FCGXPSZ num] [-pkrecqiowvh]\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 );
|
||||
|
|
@ -42021,7 +42025,6 @@ usage:
|
|||
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
|
||||
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
|
||||
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
|
||||
Abc_Print( -2, "\t-i : toggle integrated incremental SRM/re-proof/resimulation [default = %s]\n", pPars->fIncremental? "yes": "no" );
|
||||
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
|
||||
Abc_Print( -2, "\t-w : toggle printing verbose info about equivalent flops [default = %s]\n", pPars->fVerboseFlops? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
|
|
@ -42029,6 +42032,267 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandAbc9Scorr2( 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 * Cec_ManLSCorrespondence2( 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 nFlopIncFreq = 0;
|
||||
int fUseOld = 0, c;
|
||||
Cec_ManCorSetDefaultParams( pPars );
|
||||
pPars->nProcs = 1;
|
||||
pPars->fIncremental = 1;
|
||||
pPars->fDynSrm = 1;
|
||||
pPars->fIncrSim = 1;
|
||||
pPars->fSkipFailResim = 1;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSZKYDpkrecqiIosvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'F':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nFrames = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nFrames < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'C':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nBTLimit = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nBTLimit < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'G':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nPrefix = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( pPars->nPrefix < 0 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'X':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pPars->nLimitMax = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
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 '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;
|
||||
case 'k':
|
||||
pPars->fConstCorr ^= 1;
|
||||
break;
|
||||
case 'r':
|
||||
pPars->fUseRings ^= 1;
|
||||
break;
|
||||
case 'e':
|
||||
pPars->fMakeChoices ^= 1;
|
||||
break;
|
||||
case 'c':
|
||||
pPars->fUseCSat ^= 1;
|
||||
break;
|
||||
case 'q':
|
||||
pPars->fStopWhenGone ^= 1;
|
||||
break;
|
||||
case 'i':
|
||||
pPars->fIncremental ^= 1;
|
||||
break;
|
||||
case 'D':
|
||||
pPars->fDynSrm ^= 1;
|
||||
break;
|
||||
case 'I':
|
||||
pPars->fIncrSim ^= 1;
|
||||
break;
|
||||
case 's':
|
||||
pPars->fSkipFailResim ^= 1;
|
||||
break;
|
||||
case 'Y':
|
||||
pPars->fBmcTasAdaptive ^= 1;
|
||||
break;
|
||||
case 'K':
|
||||
pPars->fKissatCert ^= 1;
|
||||
break;
|
||||
case 'o':
|
||||
fUseOld ^= 1;
|
||||
break;
|
||||
case 'v':
|
||||
pPars->fVerbose ^= 1;
|
||||
break;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pPars->fDynSrm && !pPars->fIncremental )
|
||||
{
|
||||
Abc_Print( -1, "The dynamic SRM manager (-D) requires -i.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( pPars->fBmcTasAdaptive && !pPars->fDynSrm )
|
||||
{
|
||||
Abc_Print( -1, "The adaptive BMC solver policy (-Y) requires -D.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( pPars->fKissatCert &&
|
||||
(fUseOld || fPartition || pPars->nPartSize > 0 ||
|
||||
nFlopIncFreq > 0 || pPars->nPrefix > 0) )
|
||||
{
|
||||
Abc_Print( -1, "The strict fixed-point oracle (-K) supports the direct engine with -G 0 only.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "&scorr2: There is no AIG.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( Gia_ManBoxNum(pAbc->pGia) && Gia_ManRegBoxNum(pAbc->pGia) )
|
||||
{
|
||||
if ( pAbc->pGia->pAigExtra == NULL )
|
||||
{
|
||||
printf( "Timing manager is given but there is no GIA of boxes.\n" );
|
||||
return 0;
|
||||
}
|
||||
pTemp = Gia_ManSweepWithBoxes( pAbc->pGia, NULL, pPars, 0, 0, pPars->fVerbose, pPars->fVerboseFlops );
|
||||
Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
return 0;
|
||||
}
|
||||
if ( Gia_ManRegNum(pAbc->pGia) == 0 )
|
||||
{
|
||||
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 )
|
||||
{
|
||||
extern void Gia_ManTransferEquivs2( Gia_Man_t * p, Gia_Man_t * pNew );
|
||||
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_ManLSCorrespondence2( pUsed, pPars );
|
||||
Gia_ManTransferEquivs2( pUsed, pAbc->pGia );
|
||||
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 )
|
||||
pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars );
|
||||
else if ( fPartition )
|
||||
pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
|
||||
else
|
||||
pTemp = Cec_ManLSCorrespondence2( pAbc->pGia, pPars );
|
||||
Abc_FrameUpdateGia( pAbc, pTemp );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &scorr2 [-FCGXPSZ num] [-pkrecqiDIsYKovh]\n" );
|
||||
Abc_Print( -2, "\t performs signal correpondence computation using the incremental scorr2 engine\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-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-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" );
|
||||
Abc_Print( -2, "\t-e : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
|
||||
Abc_Print( -2, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
|
||||
Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" );
|
||||
Abc_Print( -2, "\t-i : toggle incremental TFO-triggered re-proof [default = %s]\n", pPars->fIncremental? "yes": "no" );
|
||||
Abc_Print( -2, "\t-D : toggle persistent dynamic SRM construction [default = %s]\n", pPars->fDynSrm? "yes": "no" );
|
||||
Abc_Print( -2, "\t-I : toggle persistent event-driven resimulation [default = %s]\n", pPars->fIncrSim? "yes": "no" );
|
||||
Abc_Print( -2, "\t-s : toggle skipping resimulation without a real CEX [default = %s]\n", pPars->fSkipFailResim? "yes": "no" );
|
||||
Abc_Print( -2, "\t-Y : toggle guarded CBS-first/TAS-rescue BMC policy [default = %s]\n", pPars->fBmcTasAdaptive? "yes": "no" );
|
||||
Abc_Print( -2, "\t-K : toggle strict final fixed-point Kissat audit [default = %s]\n", pPars->fKissatCert? "yes": "no" );
|
||||
Abc_Print( -2, "\t-o : toggle calling old engine [default = %s]\n", fUseOld? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Abc_Print( -2, "\t This command was contributed by Xiran Zhao from University of Chinese Academy of Sciences (UCAS).\n" );
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
@ -43464,13 +43728,17 @@ static void Abc_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus )
|
||||
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int * pAbc_ReadAigerOrVerilogFileStatus )
|
||||
{
|
||||
FILE * pFile;
|
||||
Gia_Man_t * pGia;
|
||||
char * pTemp;
|
||||
char * pOrigFileName = NULL;
|
||||
char * pFileTemp = NULL;
|
||||
char * pDefines = NULL;
|
||||
char * pBoxes = NULL;
|
||||
char * pExposes = NULL;
|
||||
char * pInsts = NULL;
|
||||
int fVerilog, fSystemVerilog;
|
||||
|
||||
*pAbc_ReadAigerOrVerilogFileStatus = 0;
|
||||
|
|
@ -43498,8 +43766,9 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
|
|||
{
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
Aig_Man_t * pAig = NULL;
|
||||
char pCommand[2000];
|
||||
char * pCommand;
|
||||
char * pFileBase;
|
||||
int nCommand;
|
||||
int RetValue;
|
||||
int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL );
|
||||
// Save the original filename before changing it
|
||||
|
|
@ -43509,14 +43778,35 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
|
|||
pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 );
|
||||
sprintf( pFileTemp, "%s.aig", pFileBase );
|
||||
ABC_FREE( pFileBase );
|
||||
snprintf( pCommand, sizeof(pCommand),
|
||||
"yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
|
||||
pDefines ? "-D" : "", pDefines ? pDefines : "",
|
||||
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
|
||||
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
|
||||
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
|
||||
pFileName2 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
pDefines = Wln_YosysBuildDefines( vDefines );
|
||||
pBoxes = Wln_YosysBuildBoxCommands( vBoxes, 0 );
|
||||
pExposes = Wln_YosysBuildBoxCommands( vBoxes, 1 );
|
||||
pInsts = Wln_YosysBuildInstCommands( vInsts );
|
||||
nCommand = strlen("yosys") + (pDefines ? strlen(pDefines) : 0) + (pBoxes ? strlen(pBoxes) : 0) + (pExposes ? strlen(pExposes) : 0) + 2 * (pInsts ? strlen(pInsts) : 0) + strlen(pFileName) + (pFileName2 ? strlen(pFileName2) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 700;
|
||||
pCommand = ABC_ALLOC( char, nCommand );
|
||||
if ( pBoxes || pInsts )
|
||||
snprintf( pCommand, nCommand,
|
||||
"yosys -qp \"read_verilog %s %s%s%s%s; hierarchy -check %s%s; %s%shierarchy -check %s%s; proc; memory -nomap; %smemory_map; opt; async2sync; opt; setundef -undriven -expose; setundef -zero; dffunmap; techmap; opt; dffunmap; flatten; %s%sopt_clean; opt_expr; setundef -undriven -expose; setundef -zero; aigmap; write_aiger -symbols %s\"",
|
||||
pDefines ? pDefines : "",
|
||||
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
|
||||
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
|
||||
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
|
||||
pBoxes ? pBoxes : "",
|
||||
pInsts ? pInsts : "",
|
||||
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
|
||||
pInsts ? pInsts : "",
|
||||
pExposes ? pExposes : "",
|
||||
pFileName2 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
else
|
||||
snprintf( pCommand, nCommand,
|
||||
"yosys -qp \"read_verilog %s %s%s%s%s; hierarchy -check %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
|
||||
pDefines ? pDefines : "",
|
||||
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
|
||||
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
|
||||
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
|
||||
pFileName2 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
#if defined(__wasm)
|
||||
RetValue = 1;
|
||||
#else
|
||||
|
|
@ -43525,9 +43815,23 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
|
|||
if ( RetValue != 0 )
|
||||
{
|
||||
Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand );
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pBoxes );
|
||||
ABC_FREE( pExposes );
|
||||
ABC_FREE( pInsts );
|
||||
ABC_FREE( pFileTemp );
|
||||
return NULL;
|
||||
}
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pBoxes );
|
||||
ABC_FREE( pExposes );
|
||||
ABC_FREE( pInsts );
|
||||
pDefines = NULL;
|
||||
pBoxes = NULL;
|
||||
pExposes = NULL;
|
||||
pInsts = NULL;
|
||||
if ( pFileName2 )
|
||||
{
|
||||
Gia_Man_t * pGiaNames = NULL;
|
||||
|
|
@ -43596,12 +43900,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
|
||||
FILE * pFile;
|
||||
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
|
||||
char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL, * pFileName2 = NULL;
|
||||
char ** pArgvNew, * pTopModule = NULL, * pFileName2 = NULL;
|
||||
Vec_Ptr_t * vDefines = Vec_PtrAlloc( 0 );
|
||||
Vec_Ptr_t * vBoxes = Vec_PtrAlloc( 0 );
|
||||
Vec_Ptr_t * vInsts = Vec_PtrAlloc( 0 );
|
||||
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
|
||||
int Abc_ReadAigerOrVerilogFileStatus = 0;
|
||||
Cec_ManCecSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDFnmdbasxytvwh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDIBFnmdbasxytvwh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -43642,7 +43949,25 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pDefines = argv[globalUtilOptind];
|
||||
Vec_PtrPush( vDefines, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'B':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-B\" should be followed by a module pattern.\n" );
|
||||
goto usage;
|
||||
}
|
||||
Vec_PtrPush( vBoxes, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'I':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-I\" should be followed by an instance pattern.\n" );
|
||||
goto usage;
|
||||
}
|
||||
Vec_PtrPush( vInsts, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'F':
|
||||
|
|
@ -43696,6 +44021,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pAbc->pGia && pAbc->pGia->nXors )
|
||||
{
|
||||
Abc_Print( 0, "It looks like the current AIG is derived by &st -m. Such AIG contains XOR gates and cannot be verified before &st is applied.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
if ( pFileName2 )
|
||||
|
|
@ -43703,6 +44031,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( (pFile = fopen( pFileName2, "r" )) == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Cannot open input file \"%s\".\n", pFileName2 );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
fclose( pFile );
|
||||
|
|
@ -43714,6 +44045,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pAbc->pGia == NULL || nArgcNew != 0 )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Cec(): A miter cannot be given as an argument of command &cec and should be entered using &r.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
if ( fDualOutput )
|
||||
|
|
@ -43721,6 +44055,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( Gia_ManPoNum(pAbc->pGia) & 1 )
|
||||
{
|
||||
Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
if ( !pPars->fSilent )
|
||||
|
|
@ -43745,6 +44082,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
else
|
||||
Abc_Print( 1, "Networks are UNDECIDED. " );
|
||||
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
// handle the case when the output is disproved by an all-0 primary input pattern
|
||||
|
|
@ -43771,11 +44111,17 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
}
|
||||
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
if ( nArgcNew > 2 )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
if ( nArgcNew == 2 )
|
||||
|
|
@ -43784,9 +44130,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int n;
|
||||
for ( n = 0; n < 2; n++ )
|
||||
{
|
||||
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pFileName2, pTopModule, vDefines, vBoxes, vInsts, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
if ( pGias[n] == NULL )
|
||||
{
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return Abc_ReadAigerOrVerilogFileStatus;
|
||||
}
|
||||
}
|
||||
}
|
||||
else if ( fSavedSpec )
|
||||
|
|
@ -43794,6 +44145,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pAbc->pGiaSaved == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no saved specification.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
pGias[0] = pAbc->pGia;
|
||||
|
|
@ -43805,6 +44159,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
pGias[0] = pAbc->pGia;
|
||||
|
|
@ -43816,13 +44173,21 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( pAbc->pGia->pSpec == NULL )
|
||||
{
|
||||
Abc_Print( -1, "File name is not given on the command line.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
FileName = pAbc->pGia->pSpec;
|
||||
}
|
||||
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, vDefines, vBoxes, vInsts, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
if ( pGias[1] == NULL )
|
||||
{
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return Abc_ReadAigerOrVerilogFileStatus;
|
||||
}
|
||||
}
|
||||
if ( pGias[0] && pGias[1] )
|
||||
{
|
||||
|
|
@ -43880,6 +44245,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( fUseSim && Gia_ManCiNum(pMiter) > 40 )
|
||||
{
|
||||
Abc_Print( -1, "This type of CEC can only be applied to AIGs with no more than 40 inputs.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
if ( fUseSim )
|
||||
|
|
@ -43950,15 +44318,20 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Gia_ManStop( pGias[0] );
|
||||
if ( pGias[1] != pAbc->pGiaSaved )
|
||||
Gia_ManStop( pGias[1] );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-F str] [-nmdbasxytvwh]\n" );
|
||||
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-B str] [-I str] [-F str] [-nmdbasxytvwh]\n" );
|
||||
Abc_Print( -2, "\t new combinational equivalence checker\n" );
|
||||
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
|
||||
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
|
||||
Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-D str : defines to be used by Yosys for Verilog files [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-D str : possibly repeated defines used by Yosys for Verilog files [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-B str : possibly repeated module patterns to box in Verilog AIG output [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-I str : possibly repeated instance/cell patterns to box in Verilog AIG output [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-F str : second Verilog/SystemVerilog file read together with each Verilog input [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
|
||||
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
|
||||
|
|
@ -43972,6 +44345,9 @@ usage:
|
|||
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
|
||||
Abc_Print( -2, "\t-w : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no");
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
@ -60907,6 +61283,67 @@ usage:
|
|||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Abc_CommandAbc9PrintPath( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern void Gia_ManPrintPath( Gia_Man_t * p, int nPaths, int fVerbose, int fSummary );
|
||||
int c, nPaths = 10, fVerbose = 0, fSummary = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "Nvsh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'N':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
|
||||
goto usage;
|
||||
}
|
||||
nPaths = atoi(argv[globalUtilOptind]);
|
||||
globalUtilOptind++;
|
||||
if ( nPaths < 1 )
|
||||
goto usage;
|
||||
break;
|
||||
case 'v':
|
||||
fVerbose ^= 1;
|
||||
break;
|
||||
case 's':
|
||||
fSummary ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( pAbc->pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Abc_CommandAbc9PrintPath(): There is no AIG.\n" );
|
||||
return 0;
|
||||
}
|
||||
Gia_ManPrintPath( pAbc->pGia, nPaths, fVerbose, fSummary );
|
||||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &print_path [-N num] [-vsh]\n" );
|
||||
Abc_Print( -2, "\t prints longest combinational paths between sequential endpoints\n" );
|
||||
Abc_Print( -2, "\t-N num : number of path groups to print [default = %d]\n", nPaths );
|
||||
Abc_Print( -2, "\t-v : toggle printing one AIG path for each path group [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-s : toggle printing endpoint category summary [default = %s]\n", fSummary? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
return 1;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
|
|
|||
|
|
@ -4172,20 +4172,44 @@ usage:
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int IoCommandWriteTruthsPlaDigits( int nObjs )
|
||||
{
|
||||
int nDigits = 2;
|
||||
for ( nObjs--; nObjs >= 100; nObjs /= 10 )
|
||||
nDigits++;
|
||||
return nDigits;
|
||||
}
|
||||
static void IoCommandWriteTruthsPlaNames( FILE * pFile, Gia_Man_t * pGia, int fOuts )
|
||||
{
|
||||
int i, nObjs = fOuts ? Gia_ManCoNum(pGia) : Gia_ManPiNum(pGia);
|
||||
int nDigits = IoCommandWriteTruthsPlaDigits( nObjs );
|
||||
fprintf( pFile, "%s", fOuts ? ".ob" : ".ilb" );
|
||||
for ( i = 0; i < nObjs; i++ )
|
||||
{
|
||||
char * pName = fOuts ? Gia_ObjCoName(pGia, i) : Gia_ObjCiName(pGia, i);
|
||||
if ( pName )
|
||||
fprintf( pFile, " %s", pName );
|
||||
else
|
||||
fprintf( pFile, " %s%0*d", fOuts ? "po" : "pi", nDigits, i );
|
||||
}
|
||||
fprintf( pFile, "\n" );
|
||||
}
|
||||
int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
char * pFileName;
|
||||
FILE * pFile;
|
||||
word * pTruth;
|
||||
Vec_Wrd_t * vTruths = NULL;
|
||||
int nBytes;
|
||||
int fReverse = 0;
|
||||
int fHex = 1;
|
||||
int fBinaryFile = 0;
|
||||
int c, i;
|
||||
int fPla = 0;
|
||||
int c, i, k, m, Mint;
|
||||
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "rxbh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "rxbph" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -4198,6 +4222,9 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
case 'b':
|
||||
fBinaryFile ^= 1;
|
||||
break;
|
||||
case 'p':
|
||||
fPla ^= 1;
|
||||
break;
|
||||
case 'h':
|
||||
goto usage;
|
||||
default:
|
||||
|
|
@ -4221,6 +4248,11 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
}
|
||||
if ( argc != globalUtilOptind + 1 )
|
||||
goto usage;
|
||||
if ( fPla && fBinaryFile )
|
||||
{
|
||||
Abc_Print( -1, "IoCommandWriteTruths(): Options \"-p\" and \"-b\" cannot be used together.\n" );
|
||||
return 0;
|
||||
}
|
||||
// get the input file name
|
||||
pFileName = argv[globalUtilOptind];
|
||||
// convert to logic
|
||||
|
|
@ -4231,7 +4263,38 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
return 0;
|
||||
}
|
||||
nBytes = 8 * Abc_Truth6WordNum( Gia_ManPiNum(pAbc->pGia) );
|
||||
Gia_ManForEachCo( pAbc->pGia, pObj, i )
|
||||
if ( fPla )
|
||||
{
|
||||
vTruths = Vec_WrdAlloc( Gia_ManCoNum(pAbc->pGia) * Abc_Truth6WordNum(Gia_ManPiNum(pAbc->pGia)) );
|
||||
Gia_ManForEachCo( pAbc->pGia, pObj, i )
|
||||
{
|
||||
pTruth = Gia_ObjComputeTruthTable( pAbc->pGia, pObj );
|
||||
Vec_WrdPushArray( vTruths, pTruth, Abc_Truth6WordNum(Gia_ManPiNum(pAbc->pGia)) );
|
||||
}
|
||||
fprintf( pFile, ".i %d\n", Gia_ManPiNum(pAbc->pGia) );
|
||||
fprintf( pFile, ".o %d\n", Gia_ManCoNum(pAbc->pGia) );
|
||||
fprintf( pFile, ".type fr\n" );
|
||||
IoCommandWriteTruthsPlaNames( pFile, pAbc->pGia, 0 );
|
||||
IoCommandWriteTruthsPlaNames( pFile, pAbc->pGia, 1 );
|
||||
fprintf( pFile, ".p %d\n", 1 << Gia_ManPiNum(pAbc->pGia) );
|
||||
for ( m = 0; m < (1 << Gia_ManPiNum(pAbc->pGia)); m++ )
|
||||
{
|
||||
Mint = 0;
|
||||
for ( k = Gia_ManPiNum(pAbc->pGia) - 1; k >= 0; k-- )
|
||||
{
|
||||
fprintf( pFile, "%d", (m >> k) & 1 );
|
||||
if ( (m >> k) & 1 )
|
||||
Mint |= 1 << (Gia_ManPiNum(pAbc->pGia) - 1 - k);
|
||||
}
|
||||
fprintf( pFile, " " );
|
||||
for ( i = 0; i < Gia_ManCoNum(pAbc->pGia); i++ )
|
||||
fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vTruths, i * Abc_Truth6WordNum(Gia_ManPiNum(pAbc->pGia))), Mint) );
|
||||
fprintf( pFile, "\n" );
|
||||
}
|
||||
fprintf( pFile, ".e\n" );
|
||||
Vec_WrdFree( vTruths );
|
||||
}
|
||||
else Gia_ManForEachCo( pAbc->pGia, pObj, i )
|
||||
{
|
||||
pTruth = Gia_ObjComputeTruthTable( pAbc->pGia, pObj );
|
||||
if ( fBinaryFile )
|
||||
|
|
@ -4245,11 +4308,12 @@ int IoCommandWriteTruths( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
fprintf( pAbc->Err, "usage: &write_truth [-rxbh] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t writes truth tables of each PO of GIA manager into a file\n" );
|
||||
fprintf( pAbc->Err, "usage: &write_truth [-rxbph] <file>\n" );
|
||||
fprintf( pAbc->Err, "\t writes truth tables of GIA manager into a file\n" );
|
||||
fprintf( pAbc->Err, "\t-r : toggle reversing bits in the truth table [default = %s]\n", fReverse? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-x : toggle writing in the hex notation [default = %s]\n", fHex? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-b : toggle using binary file format [default = %s]\n", fBinaryFile? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-p : toggle writing PLA format with .type fr [default = %s]\n", fPla? "yes":"no" );
|
||||
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
|
||||
fprintf( pAbc->Err, "\tfile : the name of the file to write\n" );
|
||||
return 1;
|
||||
|
|
|
|||
|
|
@ -250,6 +250,10 @@ extern Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * p, int fIgnoreIO, int fSkipSimp
|
|||
extern void Wln_NtkRetimeCreateDelayInfo( Wln_Ntk_t * pNtk );
|
||||
/*=== wlcWriteVer.c ========================================================*/
|
||||
extern void Wln_WriteVer( Wln_Ntk_t * p, char * pFileName );
|
||||
/*=== wlnRtl.c ========================================================*/
|
||||
extern char * Wln_YosysBuildDefines( Vec_Ptr_t * vDefines );
|
||||
extern char * Wln_YosysBuildBoxCommands( Vec_Ptr_t * vBoxes, int fExpose );
|
||||
extern char * Wln_YosysBuildInstCommands( Vec_Ptr_t * vInsts );
|
||||
|
||||
/*=== wlcRead.c ========================================================*/
|
||||
typedef struct Rtl_Lib_t_ Rtl_Lib_t;
|
||||
|
|
@ -263,4 +267,3 @@ ABC_NAMESPACE_HEADER_END
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -92,9 +92,9 @@ void Wln_End( Abc_Frame_t * pAbc )
|
|||
******************************************************************************/
|
||||
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
|
||||
extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
|
||||
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
|
||||
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, char * pLibrary, int fVerbose );
|
||||
extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
|
||||
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, int fCollapse, int fVerbose );
|
||||
|
||||
FILE * pFile;
|
||||
char * pFileName = NULL;
|
||||
|
|
@ -103,7 +103,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int nFileNames = 0;
|
||||
int fFileNamesAlloc = 0;
|
||||
char * pTopModule= NULL;
|
||||
char * pDefines = NULL;
|
||||
Vec_Ptr_t * vDefines = Vec_PtrAlloc( 0 );
|
||||
Vec_Ptr_t * vBoxes = Vec_PtrAlloc( 0 );
|
||||
Vec_Ptr_t * vInsts = Vec_PtrAlloc( 0 );
|
||||
char * pLibrary = NULL;
|
||||
int fBlast = 0;
|
||||
int fDontBlast = 0;
|
||||
|
|
@ -115,7 +117,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int fSetUndef = 0;
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLFbdisumlcvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "TMDIBLFbdisumlcvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -140,10 +142,28 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
case 'D':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
|
||||
Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pDefines = argv[globalUtilOptind];
|
||||
Vec_PtrPush( vDefines, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'B':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-B\" should be followed by a module pattern.\n" );
|
||||
goto usage;
|
||||
}
|
||||
Vec_PtrPush( vBoxes, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'I':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-I\" should be followed by an instance pattern.\n" );
|
||||
goto usage;
|
||||
}
|
||||
Vec_PtrPush( vInsts, argv[globalUtilOptind] );
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'L':
|
||||
|
|
@ -201,6 +221,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
if ( nFileNames < 1 )
|
||||
{
|
||||
printf( "Abc_CommandReadWlc(): Input file name(s) should be given on the command line.\n" );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
ppFileNames = pFileName2 ? ABC_ALLOC( char *, nFileNames + 1 ) : argv + globalUtilOptind;
|
||||
|
|
@ -223,6 +246,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 1, "\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
fclose( pFile );
|
||||
|
|
@ -238,23 +264,39 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
}
|
||||
if ( (Vec_PtrSize(vBoxes) > 0 || Vec_PtrSize(vInsts) > 0) && (pLibrary || fDontBlast) )
|
||||
{
|
||||
Abc_Print( -1, "Command line switches \"-B\" and \"-I\" are only supported when bit-blasting into an AIG.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
|
||||
// perform reading
|
||||
if ( pLibrary )
|
||||
{
|
||||
Abc_Ntk_t * pNtk = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
|
||||
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, pLibrary, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
|
||||
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
|
||||
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, pLibrary, fVerbose );
|
||||
else
|
||||
{
|
||||
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
|
||||
|
|
@ -263,9 +305,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
Gia_Man_t * pNew = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
|
||||
{
|
||||
if ( nFileNames > 1 )
|
||||
|
|
@ -273,15 +315,21 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
Abc_FrameUpdateGia( pAbc, pNew );
|
||||
|
|
@ -290,9 +338,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
Rtl_Lib_t * pLib = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
|
||||
{
|
||||
if ( nFileNames > 1 )
|
||||
|
|
@ -300,28 +348,39 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
|
||||
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
}
|
||||
Wln_AbcUpdateRtl( pAbc, pLib );
|
||||
}
|
||||
if ( fFileNamesAlloc )
|
||||
ABC_FREE( ppFileNames );
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name> [file_name...]\n" );
|
||||
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-B <module_pattern>] [-I <instance_pattern>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name> [file_name...]\n" );
|
||||
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
|
||||
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" );
|
||||
Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" );
|
||||
Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-D : specify possibly repeated defines to be used by Yosys (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-B : specify possibly repeated module patterns to box in AIG output (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-I : specify possibly repeated instance/cell patterns to box in AIG output (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-F : specify an additional Verilog/SystemVerilog file (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" );
|
||||
|
|
@ -334,6 +393,9 @@ usage:
|
|||
Abc_Print( -2, "\t-u : toggle replacing undefined/reset-X with zero using Yosys setundef [default = %s]\n", fSetUndef? "yes": "no" );
|
||||
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
|
||||
Abc_Print( -2, "\t-h : print the command usage\n");
|
||||
Vec_PtrFree( vDefines );
|
||||
Vec_PtrFree( vBoxes );
|
||||
Vec_PtrFree( vInsts );
|
||||
return 1;
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -146,6 +146,63 @@ static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames )
|
|||
return 1;
|
||||
return 0;
|
||||
}
|
||||
char * Wln_YosysBuildDefines( Vec_Ptr_t * vDefines )
|
||||
{
|
||||
char * pDefine, * pDefines;
|
||||
int i, nChars = 1;
|
||||
if ( vDefines == NULL || Vec_PtrSize(vDefines) == 0 )
|
||||
return NULL;
|
||||
Vec_PtrForEachEntry( char *, vDefines, pDefine, i )
|
||||
nChars += strlen(pDefine) + 4;
|
||||
pDefines = ABC_ALLOC( char, nChars );
|
||||
pDefines[0] = 0;
|
||||
Vec_PtrForEachEntry( char *, vDefines, pDefine, i )
|
||||
{
|
||||
if ( i )
|
||||
strcat( pDefines, " " );
|
||||
strcat( pDefines, "-D" );
|
||||
strcat( pDefines, pDefine );
|
||||
}
|
||||
return pDefines;
|
||||
}
|
||||
char * Wln_YosysBuildBoxCommands( Vec_Ptr_t * vBoxes, int fExpose )
|
||||
{
|
||||
char * pBox, * pBoxes;
|
||||
const char * pPrefix = fExpose ? "expose -evert t:" : "blackbox ";
|
||||
int i, nChars = 1;
|
||||
if ( vBoxes == NULL || Vec_PtrSize(vBoxes) == 0 )
|
||||
return NULL;
|
||||
Vec_PtrForEachEntry( char *, vBoxes, pBox, i )
|
||||
nChars += strlen(pPrefix) + strlen(pBox) + 2;
|
||||
pBoxes = ABC_ALLOC( char, nChars );
|
||||
pBoxes[0] = 0;
|
||||
Vec_PtrForEachEntry( char *, vBoxes, pBox, i )
|
||||
{
|
||||
strcat( pBoxes, pPrefix );
|
||||
strcat( pBoxes, pBox );
|
||||
strcat( pBoxes, "; " );
|
||||
}
|
||||
return pBoxes;
|
||||
}
|
||||
char * Wln_YosysBuildInstCommands( Vec_Ptr_t * vInsts )
|
||||
{
|
||||
char * pInst, * pInsts;
|
||||
const char * pPrefix = "expose -evert c:";
|
||||
int i, nChars = 1;
|
||||
if ( vInsts == NULL || Vec_PtrSize(vInsts) == 0 )
|
||||
return NULL;
|
||||
Vec_PtrForEachEntry( char *, vInsts, pInst, i )
|
||||
nChars += strlen(pPrefix) + strlen(pInst) + 2;
|
||||
pInsts = ABC_ALLOC( char, nChars );
|
||||
pInsts[0] = 0;
|
||||
Vec_PtrForEachEntry( char *, vInsts, pInst, i )
|
||||
{
|
||||
strcat( pInsts, pPrefix );
|
||||
strcat( pInsts, pInst );
|
||||
strcat( pInsts, "; " );
|
||||
}
|
||||
return pInsts;
|
||||
}
|
||||
int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
|
||||
{
|
||||
#if defined(__wasm)
|
||||
|
|
@ -166,21 +223,21 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
|
|||
return 1;
|
||||
#endif
|
||||
}
|
||||
Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
|
||||
Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, int fCollapse, int fVerbose )
|
||||
{
|
||||
Rtl_Lib_t * pNtk = NULL;
|
||||
char * pFileNames, * pCommand;
|
||||
char * pFileNames, * pCommand, * pDefines;
|
||||
char * pFileTemp = "_temp_.rtlil";
|
||||
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
|
||||
int nCommand;
|
||||
if ( nFileNames == 1 && strstr(ppFileNames[0], ".rtl") )
|
||||
return Rtl_LibReadFile( ppFileNames[0], ppFileNames[0] );
|
||||
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
|
||||
pDefines = Wln_YosysBuildDefines( vDefines );
|
||||
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 200;
|
||||
pCommand = ABC_ALLOC( char, nCommand );
|
||||
sprintf( pCommand, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
|
||||
sprintf( pCommand, "%s -qp \"read_verilog %s %s%s; hierarchy -check %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
|
||||
Wln_GetYosysName(),
|
||||
pDefines ? "-D" : "",
|
||||
pDefines ? pDefines : "",
|
||||
fSVlog ? "-sv " : "",
|
||||
pFileNames,
|
||||
|
|
@ -193,10 +250,12 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * p
|
|||
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
|
||||
{
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pFileNames );
|
||||
return NULL;
|
||||
}
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pFileNames );
|
||||
pNtk = Rtl_LibReadFile( pFileTemp, ppFileNames[0] );
|
||||
if ( pNtk == NULL )
|
||||
|
|
@ -208,10 +267,10 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * p
|
|||
unlink( pFileTemp );
|
||||
return pNtk;
|
||||
}
|
||||
Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
|
||||
Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
|
||||
{
|
||||
Gia_Man_t * pGia = NULL;
|
||||
char * pFileNames, * pCommand;
|
||||
char * pFileNames, * pCommand, * pDefines, * pBoxes, * pExposes, * pInsts;
|
||||
char * pFileTemp, * pFileBase;
|
||||
int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL;
|
||||
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
|
||||
|
|
@ -222,31 +281,62 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char *
|
|||
sprintf( pFileTemp, "%s.aig", pFileBase );
|
||||
ABC_FREE( pFileBase );
|
||||
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
|
||||
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500;
|
||||
pDefines = Wln_YosysBuildDefines( vDefines );
|
||||
pBoxes = Wln_YosysBuildBoxCommands( vBoxes, 0 );
|
||||
pExposes = Wln_YosysBuildBoxCommands( vBoxes, 1 );
|
||||
pInsts = Wln_YosysBuildInstCommands( vInsts );
|
||||
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pBoxes ? strlen(pBoxes) : 0) + (pExposes ? strlen(pExposes) : 0) + 2 * (pInsts ? strlen(pInsts) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 700;
|
||||
pCommand = ABC_ALLOC( char, nCommand );
|
||||
sprintf( pCommand, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
|
||||
Wln_GetYosysName(),
|
||||
fRtlil ? "read_rtlil" : "read_verilog",
|
||||
pDefines ? "-D" : "",
|
||||
pDefines ? pDefines : "",
|
||||
fSVlog ? "-sv " : "",
|
||||
pFileNames,
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
pTopModule ? pTopModule : "",
|
||||
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
|
||||
fSetUndef ? "setundef -init -zero; " : "",
|
||||
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
if ( pBoxes || pInsts )
|
||||
sprintf( pCommand, "%s -qp \"%s %s %s%s; hierarchy -check %s%s; %s%shierarchy -check %s%s; proc; memory -nomap; %smemory_map; opt; async2sync; opt; setundef -undriven -expose; setundef -zero; %sdffunmap; %sopt; dffunmap; flatten; %s%sopt_clean; opt_expr; setundef -undriven -expose; setundef -zero; aigmap; write_aiger -symbols %s\"",
|
||||
Wln_GetYosysName(),
|
||||
fRtlil ? "read_rtlil" : "read_verilog",
|
||||
pDefines ? pDefines : "",
|
||||
fSVlog ? "-sv " : "",
|
||||
pFileNames,
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
pTopModule ? pTopModule : "",
|
||||
pBoxes ? pBoxes : "",
|
||||
pInsts ? pInsts : "",
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
pTopModule ? pTopModule : "",
|
||||
pInsts ? pInsts : "",
|
||||
fSetUndef ? "setundef -init -zero; " : "",
|
||||
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
|
||||
pExposes ? pExposes : "",
|
||||
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
else
|
||||
sprintf( pCommand, "%s -qp \"%s %s %s%s; hierarchy -check %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
|
||||
Wln_GetYosysName(),
|
||||
fRtlil ? "read_rtlil" : "read_verilog",
|
||||
pDefines ? pDefines : "",
|
||||
fSVlog ? "-sv " : "",
|
||||
pFileNames,
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
pTopModule ? pTopModule : "",
|
||||
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
|
||||
fSetUndef ? "setundef -init -zero; " : "",
|
||||
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
if ( fVerbose )
|
||||
printf( "%s\n", pCommand );
|
||||
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
|
||||
{
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pBoxes );
|
||||
ABC_FREE( pExposes );
|
||||
ABC_FREE( pInsts );
|
||||
ABC_FREE( pFileNames );
|
||||
ABC_FREE( pFileTemp );
|
||||
return NULL;
|
||||
}
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pBoxes );
|
||||
ABC_FREE( pExposes );
|
||||
ABC_FREE( pInsts );
|
||||
ABC_FREE( pFileNames );
|
||||
pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 );
|
||||
if ( pGia == NULL )
|
||||
|
|
@ -269,21 +359,21 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char *
|
|||
}
|
||||
return pGia;
|
||||
}
|
||||
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose )
|
||||
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, char * pLibrary, int fVerbose )
|
||||
{
|
||||
Abc_Ntk_t * pNtk = NULL;
|
||||
char * pFileNames, * pCommand;
|
||||
char * pFileNames, * pCommand, * pDefines;
|
||||
char * pFileTemp = "_temp_.blif";
|
||||
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
|
||||
int nCommand;
|
||||
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
|
||||
pDefines = Wln_YosysBuildDefines( vDefines );
|
||||
nCommand = strlen(Wln_GetYosysName()) + strlen(pLibrary) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 300;
|
||||
pCommand = ABC_ALLOC( char, nCommand );
|
||||
sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
|
||||
sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s %s; hierarchy -check %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
|
||||
Wln_GetYosysName(),
|
||||
pLibrary,
|
||||
fSVlog ? "-sv " : "-vlog95",
|
||||
pDefines ? "-D" : "",
|
||||
pDefines ? pDefines : "",
|
||||
pFileNames,
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
|
|
@ -296,10 +386,12 @@ Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, ch
|
|||
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
|
||||
{
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pFileNames );
|
||||
return NULL;
|
||||
}
|
||||
ABC_FREE( pCommand );
|
||||
ABC_FREE( pDefines );
|
||||
ABC_FREE( pFileNames );
|
||||
pCommand = ABC_ALLOC( char, strlen(pLibrary) + 20 );
|
||||
sprintf( pCommand, "read_lib %s", pLibrary );
|
||||
|
|
|
|||
|
|
@ -351,6 +351,19 @@ static inline abctime Abc_Clock()
|
|||
return (abctime) clock();
|
||||
#endif
|
||||
}
|
||||
// Returns monotonic wall-clock time in nanoseconds. The dynamic SRM
|
||||
// heuristics use this to compare rebuild and reuse costs.
|
||||
static inline abctime Abc_ClockHr()
|
||||
{
|
||||
#if defined(CLOCK_MONOTONIC)
|
||||
struct timespec ts;
|
||||
if ( clock_gettime( CLOCK_MONOTONIC, &ts ) < 0 )
|
||||
return (abctime)-1;
|
||||
return ((abctime) ts.tv_sec) * 1000000000 + (abctime) ts.tv_nsec;
|
||||
#else
|
||||
return (abctime)( (double)Abc_Clock() * 1.0e9 / CLOCKS_PER_SEC );
|
||||
#endif
|
||||
}
|
||||
// counting thread time
|
||||
static inline abctime Abc_ThreadClock()
|
||||
{
|
||||
|
|
|
|||
|
|
@ -159,6 +159,9 @@ struct Cec_ParCor_t_
|
|||
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
|
||||
int nIncrFallbackPct; // (-i) fall back to full SRM when active pairs exceed this percent
|
||||
int nDynSrmRebuildPct; // (-D) cold-rebuild when active pairs exceed this percent
|
||||
int nDynSrmCompactMult; // (-D) cold-compact when core exceeds this multiple of reset size
|
||||
int fLatchCorr; // consider only latch outputs
|
||||
int fConstCorr; // consider only constants
|
||||
int fUseRings; // use rings
|
||||
|
|
@ -167,10 +170,16 @@ struct Cec_ParCor_t_
|
|||
// int fFirstStop; // stop on the first sat output
|
||||
int fUseSmartCnf; // use smart CNF computation
|
||||
int fStopWhenGone; // quit when PO is not a candidate constant
|
||||
int fIncremental; // integrated incremental mode for &scorr
|
||||
int fIncremental; // active-list/TFO-triggered reproof in main loop
|
||||
int fIncrOracle; // internal unbounded shadow SAT for pairs skipped by -i
|
||||
int fIncrSim; // persistent CEX-TFO-only resimulation after SAT
|
||||
int fDynSrm; // persistent dynamic SRM and true-unroll resimulation
|
||||
int fDynSrmNoAdapt;// disable adaptive cold-rebuilds in DynSRM
|
||||
int fUseTas; // use TAS (vs CBS) for persistent solving (-D)
|
||||
int fBmcTasAdaptive;// use guarded CBS-first/TAS-rescue policy in BMC
|
||||
int fKissatCert; // strictly audit final base+step obligations with Kissat
|
||||
int fSkipFailResim;// skip resim in rounds with no real CEX (only timeout/fail)
|
||||
int fVerifyResim; // internal oracle: check incremental resim values vs full sweep
|
||||
int fVerboseFlops; // verbose stats
|
||||
int fVeryVerbose; // verbose stats
|
||||
int fVerbose; // verbose stats
|
||||
|
|
|
|||
|
|
@ -192,10 +192,18 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
|
|||
p->nBTLimit = 100; // conflict limit at a node
|
||||
p->nLevelMax = -1; // (scorr only) the max number of levels
|
||||
p->nStepsMax = -1; // (scorr only) the max number of induction steps
|
||||
p->nIncrFallbackPct = 100; // (-i) fall back to full SRM when active pairs exceed this percent
|
||||
p->nDynSrmRebuildPct = 20; // (-D) cold-rebuild when active pairs exceed this percent
|
||||
p->nDynSrmCompactMult = 4; // (-D) cold-compact when core exceeds this multiple of reset size
|
||||
p->fLatchCorr = 0; // consider only latch outputs
|
||||
p->fConstCorr = 0; // consider only constants
|
||||
p->fUseRings = 1; // combine classes into rings
|
||||
p->fIncrOracle = 0; // internal unbounded shadow SAT for pairs skipped by -i
|
||||
p->fSkipFailResim = 0; // skip resim when a round has no real CEX (only timeout/fail)
|
||||
p->fDynSrmNoAdapt = 1; // timing-guided DynSRM rebuild heuristic is opt-in
|
||||
p->fUseTas = 0; // use CBS by default for persistent solving
|
||||
p->fBmcTasAdaptive = 0; // guarded BMC TAS rescue is opt-in (-Y)
|
||||
p->fKissatCert = 0; // strict final base+step Kissat audit is opt-in
|
||||
p->fUseCSat = 1; // use circuit-based solver
|
||||
// p->fFirstStop = 0; // stop on the first sat output
|
||||
p->fUseSmartCnf = 0; // use smart CNF computation
|
||||
|
|
|
|||
|
|
@ -34,9 +34,7 @@ static inline int Cec_ParCorShouldStop( Cec_ParCor_t * pPars )
|
|||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// Shared with cecCorrIncr.c (declared in cecInt.h).
|
||||
extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
|
|
@ -47,13 +45,13 @@ extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pO
|
|||
Synopsis [Computes the real value of the literal w/o spec reduction.]
|
||||
|
||||
Description []
|
||||
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
|
||||
static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
|
||||
{
|
||||
if ( Gia_ObjIsAnd(pObj) )
|
||||
{
|
||||
|
|
@ -77,7 +75,7 @@ int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int
|
|||
Synopsis [Recursively performs speculative reduction for the object.]
|
||||
|
||||
Description []
|
||||
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
|
@ -106,7 +104,7 @@ void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pOb
|
|||
Synopsis [Derives SRM for signal correspondence.]
|
||||
|
||||
Description []
|
||||
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
|
@ -223,7 +221,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
|
|||
Synopsis [Derives SRM for signal correspondence.]
|
||||
|
||||
Description []
|
||||
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
|
@ -292,7 +290,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix,
|
|||
Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]
|
||||
|
||||
Description []
|
||||
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
|
@ -499,53 +497,6 @@ int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iS
|
|||
return iStart;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs bitpacking of counter-examples and records bit lanes.]
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
int Cec_ManLoadCounterExamplesMapped( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vOutBits )
|
||||
{
|
||||
Vec_Int_t * vPat;
|
||||
Vec_Ptr_t * vPres;
|
||||
int nWords = Vec_PtrReadWordsSimInfo(vInfo);
|
||||
int nBits = 32 * nWords;
|
||||
int k, nSize, Out;
|
||||
Vec_IntClear( vOutBits );
|
||||
vPat = Vec_IntAlloc( 100 );
|
||||
vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
|
||||
Vec_PtrCleanSimInfo( vPres, 0, nWords );
|
||||
while ( iStart < Vec_IntSize(vCexStore) )
|
||||
{
|
||||
Out = Vec_IntEntry( vCexStore, iStart++ );
|
||||
nSize = Vec_IntEntry( vCexStore, iStart++ );
|
||||
if ( nSize <= 0 )
|
||||
continue;
|
||||
Vec_IntClear( vPat );
|
||||
for ( k = 0; k < nSize; k++ )
|
||||
Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
|
||||
for ( k = 1; k < nBits; k++ )
|
||||
if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
|
||||
break;
|
||||
if ( k < nBits )
|
||||
{
|
||||
Vec_IntPush( vOutBits, Out );
|
||||
Vec_IntPush( vOutBits, k );
|
||||
}
|
||||
if ( k == nBits-1 )
|
||||
break;
|
||||
}
|
||||
Vec_PtrFree( vPres );
|
||||
Vec_IntFree( vPat );
|
||||
return iStart;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Performs bitpacking of counter-examples.]
|
||||
|
|
@ -587,53 +538,6 @@ int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int i
|
|||
return iStart;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Classifies vCexStore entries by SAT outcome.]
|
||||
|
||||
Description [Each entry is (Out, nLits[, lit0, ..., lit{nLits-1}]).
|
||||
nLits > 0 -> real SAT CEX with usable literals;
|
||||
nLits == 0 -> trivial SAT (e.g. SRM PO became const 1);
|
||||
nLits == -1 -> timeout/fail, no CEX.
|
||||
Counts are written via the out-pointers (any may be NULL).
|
||||
Returns 1 iff there is at least one entry usable for resim
|
||||
(real or trivial), preserving the prior skip-failed-resim
|
||||
semantics where only timeout-only stores get skipped.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int Cec_ManCexStoreClassify( Vec_Int_t * vCexStore, int * pnReal, int * pnTriv, int * pnFail )
|
||||
{
|
||||
int iStart = 0, nSize, nReal = 0, nTriv = 0, nFail = 0;
|
||||
while ( iStart < Vec_IntSize(vCexStore) )
|
||||
{
|
||||
iStart++; // output number
|
||||
assert( iStart < Vec_IntSize(vCexStore) );
|
||||
nSize = Vec_IntEntry( vCexStore, iStart++ );
|
||||
if ( nSize > 0 )
|
||||
{
|
||||
nReal++;
|
||||
iStart += nSize;
|
||||
}
|
||||
else if ( nSize == 0 )
|
||||
{
|
||||
nTriv++;
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( nSize == -1 );
|
||||
nFail++;
|
||||
}
|
||||
}
|
||||
if ( pnReal ) *pnReal = nReal;
|
||||
if ( pnTriv ) *pnTriv = nTriv;
|
||||
if ( pnFail ) *pnFail = nFail;
|
||||
return (nReal + nTriv) > 0;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Resimulates counter-examples derived by the SAT solver.]
|
||||
|
|
@ -645,104 +549,33 @@ static int Cec_ManCexStoreClassify( Vec_Int_t * vCexStore, int * pnReal, int * p
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int Cec_ManResimulateCounterExamplesSeed( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, Cec_SeedSim_t * pSeed, Vec_Int_t * vOutputs )
|
||||
{
|
||||
Vec_Int_t * vPairs = NULL;
|
||||
Vec_Int_t * vOutBits = NULL;
|
||||
Vec_Ptr_t * vSimInfo = NULL;
|
||||
int RetValue = 0, iStart = 0, fValueRefs = 0;
|
||||
if ( pSeed )
|
||||
Cec_SeedSimBeginCall( pSeed ); // reset per-call local/full/maxdirty counters
|
||||
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
|
||||
{
|
||||
Vec_Int_t * vPairs;
|
||||
Vec_Ptr_t * vSimInfo;
|
||||
int RetValue = 0, iStart = 0;
|
||||
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
|
||||
Gia_ManCreateValueRefs( pSim->pAig );
|
||||
// pSim->pPars->nWords = 63;
|
||||
pSim->pPars->nFrames = nFrames;
|
||||
if ( pSeed )
|
||||
{
|
||||
Cec_SeedSimEnsurePersistent( pSeed, pSim );
|
||||
// Defer the (possibly full-unroll-sized) class cone: it is built lazily
|
||||
// inside Cec_SeedSimTryBatch() only once a batch passes the density gate,
|
||||
// so rounds that fall back to full resim never pay for it.
|
||||
pSeed->fUseCone = 0;
|
||||
vSimInfo = pSeed->vSimInfo;
|
||||
vOutBits = Vec_IntAlloc( 1000 );
|
||||
}
|
||||
else
|
||||
{
|
||||
Gia_ManCreateValueRefs( pSim->pAig );
|
||||
fValueRefs = 1;
|
||||
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
|
||||
}
|
||||
vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
|
||||
vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
|
||||
while ( iStart < Vec_IntSize(vCexStore) )
|
||||
{
|
||||
if ( pSeed )
|
||||
{
|
||||
int LocalStatus;
|
||||
iStart = Cec_SeedSimLoadPersistentBatch(
|
||||
pSeed, vCexStore, iStart, vPairs, vOutBits );
|
||||
if ( pSeed->nFallbackCooldown > 0 )
|
||||
{
|
||||
Cec_SeedSimBypassBatch( pSeed, Vec_IntSize(vOutBits) / 2 );
|
||||
pSeed->nFallbackCooldown--;
|
||||
}
|
||||
else if ( (LocalStatus = Cec_SeedSimTryBatch(
|
||||
pSeed, pSim, vSimInfo, vOutputs, vOutBits, nFrames )) ==
|
||||
CEC_SEEDSIM_RESULT_LOCAL )
|
||||
{
|
||||
pSeed->nFallbackStreak = 0;
|
||||
pSeed->nFallbackCooldown = 0;
|
||||
continue;
|
||||
}
|
||||
else if ( LocalStatus == CEC_SEEDSIM_RESULT_FULL_WIDE )
|
||||
{
|
||||
int Shift;
|
||||
pSeed->nFallbackStreak++;
|
||||
Shift = Abc_MinInt( pSeed->nFallbackStreak - 1, 3 );
|
||||
pSeed->nFallbackCooldown =
|
||||
Abc_MinInt( (1 << Shift) - 1,
|
||||
CEC_SEEDSIM_MAX_FALLBACK_BACKOFF );
|
||||
}
|
||||
else
|
||||
{
|
||||
pSeed->nFallbackStreak = 0;
|
||||
pSeed->nFallbackCooldown = 0;
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
|
||||
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
|
||||
Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
|
||||
}
|
||||
// The local path returned above. Reaching here means standard full
|
||||
// resimulation, either outside incremental mode or as a fallback.
|
||||
if ( pSeed )
|
||||
{
|
||||
if ( !fValueRefs )
|
||||
{
|
||||
Gia_ManCreateValueRefs( pSim->pAig );
|
||||
fValueRefs = 1;
|
||||
}
|
||||
RetValue |= Cec_ManSeqResimulateSeed( pSim, vSimInfo, pSeed );
|
||||
Cec_SeedSimRestorePersistentInputs( pSeed );
|
||||
}
|
||||
else
|
||||
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
|
||||
Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
|
||||
iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
|
||||
// iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
|
||||
// Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
|
||||
Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
|
||||
RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
|
||||
// Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
|
||||
}
|
||||
//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
|
||||
assert( iStart == Vec_IntSize(vCexStore) );
|
||||
Vec_IntFreeP( &vOutBits );
|
||||
if ( !pSeed )
|
||||
Vec_PtrFree( vSimInfo );
|
||||
Vec_IntFreeP( &vPairs );
|
||||
Vec_PtrFree( vSimInfo );
|
||||
Vec_IntFree( vPairs );
|
||||
return RetValue;
|
||||
}
|
||||
|
||||
int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames )
|
||||
{
|
||||
return Cec_ManResimulateCounterExamplesSeed( pSim, vCexStore, nFrames, NULL, NULL );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Resimulates counter-examples derived by the SAT solver.]
|
||||
|
|
@ -772,102 +605,12 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
|
|||
return RetValue;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Checks whether two endpoints are still in the same class.]
|
||||
|
||||
Description [Ring mode needs special handling for the closing edge
|
||||
tail -> head because Gia_ObjHasSameRepr() compares raw
|
||||
representatives and the head stores GIA_VOID.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int Cec_ManObjsStillMerged( Gia_Man_t * p, int iRepr, int iObj, int fRings )
|
||||
{
|
||||
int iReprRoot, iObjRoot;
|
||||
if ( !fRings )
|
||||
return Gia_ObjHasSameRepr( p, iRepr, iObj );
|
||||
if ( iRepr == 0 )
|
||||
return Gia_ObjIsConst( p, iObj );
|
||||
if ( iObj == 0 )
|
||||
return Gia_ObjIsConst( p, iRepr );
|
||||
if ( !Gia_ObjIsClass( p, iRepr ) || !Gia_ObjIsClass( p, iObj ) )
|
||||
return 0;
|
||||
iReprRoot = Gia_ObjIsHead( p, iRepr ) ? iRepr : Gia_ObjRepr( p, iRepr );
|
||||
iObjRoot = Gia_ObjIsHead( p, iObj ) ? iObj : Gia_ObjRepr( p, iObj );
|
||||
return iReprRoot == iObjRoot && iReprRoot != GIA_VOID;
|
||||
}
|
||||
|
||||
static int Cec_ManObjToSplit( Gia_Man_t * p, int iRepr, int iObj, int fRings )
|
||||
{
|
||||
// For the ring closing edge (tail, head), split the tail. Splitting the
|
||||
// head is also correct, but it changes the representative of the whole
|
||||
// remaining class and creates a much larger incremental seed set.
|
||||
if ( fRings && iObj > 0 && Gia_ObjIsHead( p, iObj ) && Gia_ObjIsClass( p, iRepr ) )
|
||||
return iRepr;
|
||||
return iObj;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Directly splits pairs whose SAT result was trivial (nLits==0).]
|
||||
|
||||
Description [A trivial SAT (e.g. SRM PO became const 1) is a real
|
||||
disproval but carries no CEX literals, so Cec_ManResimulateCounterExamples
|
||||
cannot break the pair -- only random filler can, and usually does not.
|
||||
Splitting these pairs directly is sound (SAT proved disequivalence) and
|
||||
recovers work that the standard resim path leaves on the table.
|
||||
|
||||
Only nLits==0 entries are touched; nLits>0 entries are left for resim to
|
||||
refine, matching the established behaviour in Gia_ManCheckRefinements
|
||||
that avoids force-splitting CEX-bearing SAT pairs (token_ring regression).
|
||||
|
||||
Returns the number of pairs actually split this call.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static int Cec_ManTrivialSatSplit( Gia_Man_t * pAig, Cec_ManSim_t * pSim,
|
||||
Vec_Int_t * vCexStore, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, int fRings )
|
||||
{
|
||||
int iStart = 0, Out, nSize, iRepr, iObj, iSplit, Count = 0;
|
||||
while ( iStart < Vec_IntSize(vCexStore) )
|
||||
{
|
||||
Out = Vec_IntEntry( vCexStore, iStart++ );
|
||||
assert( iStart < Vec_IntSize(vCexStore) );
|
||||
nSize = Vec_IntEntry( vCexStore, iStart++ );
|
||||
if ( nSize > 0 )
|
||||
{
|
||||
iStart += nSize;
|
||||
continue;
|
||||
}
|
||||
if ( nSize < 0 )
|
||||
continue;
|
||||
// nSize == 0 -> trivial SAT, no CEX literals.
|
||||
assert( Out < Vec_StrSize(vStatus) );
|
||||
assert( Vec_StrEntry(vStatus, Out) == 0 );
|
||||
iRepr = Vec_IntEntry( vOutputs, 2*Out );
|
||||
iObj = Vec_IntEntry( vOutputs, 2*Out + 1 );
|
||||
if ( !Cec_ManObjsStillMerged( pAig, iRepr, iObj, fRings ) )
|
||||
continue;
|
||||
iSplit = Cec_ManObjToSplit( pAig, iRepr, iObj, fRings );
|
||||
if ( Cec_ManSimClassRemoveOne( pSim, iSplit ) )
|
||||
Count++;
|
||||
}
|
||||
return Count;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Updates equivalence classes by marking those that timed out.]
|
||||
|
||||
Description [Returns 1 if all nodes are proved.]
|
||||
|
||||
Description [Returns 1 if all ndoes are proved.]
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
|
@ -1049,7 +792,7 @@ int Cec_ManCountLits( Gia_Man_t * p )
|
|||
|
||||
***********************************************************************/
|
||||
void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
|
||||
{
|
||||
{
|
||||
Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
|
||||
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
|
||||
Vec_Str_t * vStatus;
|
||||
|
|
@ -1057,16 +800,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
|
|||
Vec_Int_t * vCexStore;
|
||||
Cec_ManSim_t * pSim;
|
||||
Gia_Man_t * pSrm;
|
||||
int fChanges, i;
|
||||
int nBmcResimFrames = pPars->nFrames + 1 + nPrefs;
|
||||
int fBmcPersist = 0;
|
||||
// BMC SRM is keyed only on pReprs (Gia_ManCorrSpecReduceInit ignores
|
||||
// its fRings flag). So the incremental filter only needs pReprs-based
|
||||
// seeds; pNexts changes cannot affect this SRM and there are no ring
|
||||
// closing edges to reprove -- BMC is structurally simpler than the
|
||||
// main inductive loop.
|
||||
Cec_IncrMgr_t * pBmcMgr = NULL;
|
||||
Cec_DynSrm_t * pBmcDynSrm = NULL;
|
||||
int fChanges, RetValue, i;
|
||||
// prepare simulation manager
|
||||
Cec_ManSimSetDefaultParams( pParsSim );
|
||||
pParsSim->nWords = pPars->nWords;
|
||||
|
|
@ -1079,102 +813,29 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
|
|||
Cec_ManSatSetDefaultParams( pParsSat );
|
||||
pParsSat->nBTLimit = pPars->nBTLimit;
|
||||
pParsSat->fVerbose = pPars->fVerbose;
|
||||
if ( pPars->fIncremental )
|
||||
{
|
||||
pBmcMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames + nPrefs );
|
||||
Cec_IncrMgrSnapshotClasses( pBmcMgr );
|
||||
}
|
||||
if ( pPars->fDynSrm && pBmcMgr )
|
||||
pBmcDynSrm = Cec_DynSrmAlloc( pAig, pBmcMgr );
|
||||
fBmcPersist = ( pBmcDynSrm != NULL && pPars->fUseCSat );
|
||||
fChanges = 1;
|
||||
for ( i = 0; fChanges && (!pPars->nLimitMax || i < pPars->nLimitMax); i++ )
|
||||
{
|
||||
int * pTfoMask = NULL;
|
||||
int nReprSeeds = 0, nTotalPairs = 0, nActivePairs = 0;
|
||||
int nBmcPos = 0;
|
||||
if ( Cec_ParCorShouldStop( pPars ) )
|
||||
break;
|
||||
abctime clkBmc = Abc_Clock();
|
||||
fChanges = 0;
|
||||
// BMC SRM is non-ring (Gia_ManCorrSpecReduceInit ignores fRings);
|
||||
// the incremental mask filters on pReprs-derived endpoints only.
|
||||
if ( pBmcMgr && i > 0 )
|
||||
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
|
||||
if ( Gia_ManPoNum(pSrm) == 0 )
|
||||
{
|
||||
nReprSeeds = Cec_IncrMgrComputeSeeds( pBmcMgr );
|
||||
if ( nReprSeeds == 0 )
|
||||
{
|
||||
// No pReprs change. BMC SRM topology is unchanged.
|
||||
break;
|
||||
}
|
||||
Cec_IncrMgrComputeTfo( pBmcMgr );
|
||||
// BMC SRM is non-ring; pass fRings=0 so we count (head, member)
|
||||
// pairs only and skip any ring-edge bookkeeping.
|
||||
if ( pBmcDynSrm )
|
||||
Cec_DynSrmCountActivePairs( pBmcDynSrm, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs );
|
||||
else
|
||||
Cec_IncrMgrCountActivePairs( pBmcMgr, 0, pBmcMgr->pTfoMark, &nTotalPairs, &nActivePairs );
|
||||
if ( nActivePairs == 0 )
|
||||
break;
|
||||
// Same fallback heuristic as the main loop: above ~70% active,
|
||||
// the mask plus emission filter costs more than just rebuilding
|
||||
// the full SRM.
|
||||
if ( !( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs ) )
|
||||
pTfoMask = pBmcMgr->pTfoMark;
|
||||
}
|
||||
pSrm = NULL;
|
||||
if ( fBmcPersist )
|
||||
Cec_DynSrmBuildCoreInit( pBmcDynSrm, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
|
||||
else if ( pBmcDynSrm )
|
||||
pSrm = Cec_DynSrmBuildInit( pBmcDynSrm, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
|
||||
else if ( pTfoMask )
|
||||
pSrm = Gia_ManCorrSpecReduceInit_Active( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pTfoMask );
|
||||
else
|
||||
pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
|
||||
nBmcPos = fBmcPersist ? Vec_IntSize(Cec_DynSrmOutLits(pBmcDynSrm)) : Gia_ManCoNum(pSrm);
|
||||
if ( pTfoMask && pPars->fVeryVerbose )
|
||||
Abc_Print( 1, " [bmc-incr i=%d repr=%d active=%d/%d POs=%d]\n",
|
||||
i, nReprSeeds, nActivePairs, nTotalPairs, nBmcPos );
|
||||
// Snapshot after SRM construction, before SAT/refine: this is the
|
||||
// class state whose pairs were just emitted. The next iteration's
|
||||
// diff vs this snapshot tells us which pairs are stale.
|
||||
if ( pBmcMgr )
|
||||
Cec_IncrMgrSnapshotClasses( pBmcMgr );
|
||||
if ( nBmcPos == 0 )
|
||||
{
|
||||
if ( pSrm )
|
||||
Gia_ManStop( pSrm );
|
||||
Gia_ManStop( pSrm );
|
||||
Vec_IntFree( vOutputs );
|
||||
break;
|
||||
}
|
||||
}
|
||||
pParsSat->nBTLimit *= 10;
|
||||
if ( fBmcPersist )
|
||||
vCexStore = Cec_DynSrmSolve( pBmcDynSrm, pPars->nBTLimit, &vStatus );
|
||||
else if ( pPars->fUseCSat )
|
||||
if ( pPars->fUseCSat )
|
||||
vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
|
||||
else
|
||||
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
|
||||
// refine classes with these counter-examples
|
||||
if ( Vec_IntSize(vCexStore) )
|
||||
{
|
||||
int nCexReal = 0, nCexTriv = 0;
|
||||
// classify CEX entries: real (nLits>0) / trivial (==0) / fail (==-1)
|
||||
Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL );
|
||||
// only invoke resim when there is a real CEX (nLits>0). Trivial
|
||||
// (nLits==0) and fail (==-1) entries carry no literals; trivial
|
||||
// pairs are handled by direct split below, fail pairs by chk.
|
||||
if ( nCexReal > 0 || !pPars->fSkipFailResim )
|
||||
{
|
||||
// Keep BMC/init CEX resimulation on the canonical full path even
|
||||
// in incremental mode. BMC counterexamples are partial models
|
||||
// of frame/prefix-specific SAT obligations; retaining them as a
|
||||
// persistent simulation background over-refines classes and can
|
||||
// significantly hurt gate QoR. The main correspondence loop
|
||||
// below still uses event resim for ordinary refinement batches.
|
||||
Cec_ManResimulateCounterExamples( pSim, vCexStore, nBmcResimFrames );
|
||||
}
|
||||
if ( nCexTriv > 0 )
|
||||
Cec_ManTrivialSatSplit( pAig, pSim, vCexStore, vStatus, vOutputs, pPars->fUseRings );
|
||||
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
|
||||
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
|
||||
fChanges = 1;
|
||||
}
|
||||
|
|
@ -1183,14 +844,11 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
|
|||
// recycle
|
||||
Vec_IntFree( vCexStore );
|
||||
Vec_StrFree( vStatus );
|
||||
if ( pSrm )
|
||||
Gia_ManStop( pSrm );
|
||||
Gia_ManStop( pSrm );
|
||||
Vec_IntFree( vOutputs );
|
||||
if ( Cec_ParCorShouldStop( pPars ) )
|
||||
break;
|
||||
}
|
||||
Cec_DynSrmFree( pBmcDynSrm );
|
||||
Cec_IncrMgrFree( pBmcMgr );
|
||||
Cec_ManSimStop( pSim );
|
||||
}
|
||||
|
||||
|
|
@ -1287,19 +945,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
|
||||
Cec_ManSim_t * pSim;
|
||||
Gia_Man_t * pSrm;
|
||||
int r, nPrev[4] = {0};
|
||||
int r, RetValue, nPrev[4] = {0};
|
||||
abctime clkTotal = Abc_Clock();
|
||||
abctime clkSat = 0, clkSim = 0, clkSrm = 0;
|
||||
abctime clk2, clk = Abc_Clock();
|
||||
// Incremental active-list manager (NULL if -i not set)
|
||||
Cec_IncrMgr_t * pMgr = NULL;
|
||||
// Persistent dynamic SRM construction manager (NULL outside incremental mode).
|
||||
Cec_DynSrm_t * pDynSrm = NULL;
|
||||
int fPersist = 0; // incremental + circuit-SAT: solve persistent pCore directly
|
||||
// Unified CEX event-resimulation manager (NULL outside incremental mode).
|
||||
Cec_SeedSim_t * pSeedSim = NULL;
|
||||
abctime clkIncr = 0;
|
||||
int nIncrSkipped = 0, nIncrFallback = 0;
|
||||
if ( Gia_ManRegNum(pAig) == 0 )
|
||||
{
|
||||
Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
|
||||
|
|
@ -1330,9 +979,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
|
||||
if ( pPars->fVerbose )
|
||||
{
|
||||
Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d. Incr = %d. Dyn = %d.\n",
|
||||
Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
|
||||
Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
|
||||
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat, pPars->fIncremental, pPars->fDynSrm );
|
||||
pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
|
||||
Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
|
||||
}
|
||||
// check the base case
|
||||
|
|
@ -1350,136 +999,41 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
Cec_ManSimStop( pSim );
|
||||
return 1;
|
||||
}
|
||||
if ( pPars->fIncremental )
|
||||
{
|
||||
pMgr = Cec_IncrMgrAlloc( pAig, pPars->nFrames );
|
||||
Cec_IncrMgrSnapshotClasses( pMgr );
|
||||
}
|
||||
if ( pPars->fDynSrm && pMgr )
|
||||
pDynSrm = Cec_DynSrmAlloc( pAig, pMgr );
|
||||
// Incremental persistence path: solve the persistent COless pCore directly (circuit
|
||||
// SAT only), skipping the per-round throwaway view that BuildView copies.
|
||||
fPersist = ( pDynSrm != NULL && pPars->fUseCSat );
|
||||
// Resident local-sim manager sized for the main-loop resim depth.
|
||||
if ( pPars->fIncrSim )
|
||||
pSeedSim = Cec_SeedSimAlloc( pAig, pPars->nFrames + 1 + nAddFrames, pPars->nFrames, pParsSim->nWords );
|
||||
// perform refinement of equivalence classes
|
||||
for ( r = 0; r < nIterMax; r++ )
|
||||
{
|
||||
{
|
||||
if ( Cec_ParCorShouldStop( pPars ) )
|
||||
{
|
||||
Cec_ManSimStop( pSim );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
return 1;
|
||||
}
|
||||
if ( pPars->nStepsMax == r )
|
||||
{
|
||||
Cec_ManSimStop( pSim );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
|
||||
fflush( stdout );
|
||||
return 1;
|
||||
}
|
||||
clk = Abc_Clock();
|
||||
// perform speculative reduction (with optional active-list filter)
|
||||
// perform speculative reduction
|
||||
clk2 = Abc_Clock();
|
||||
{
|
||||
int * pTfoMask = NULL;
|
||||
int nReprSeeds = 0, nNextChanges = 0;
|
||||
int nTotalPairs = 0, nActivePairs = 0;
|
||||
// Decide whether to apply incremental TFO mask this iteration.
|
||||
// Skip on r==0 because the first full SRM establishes the cache.
|
||||
if ( pMgr && r > 0 )
|
||||
{
|
||||
abctime clkI = Abc_Clock();
|
||||
nReprSeeds = Cec_IncrMgrComputeSeeds( pMgr );
|
||||
nNextChanges = pPars->fUseRings ? Cec_IncrMgrCountNextChanges( pMgr ) : 0;
|
||||
if ( nReprSeeds == 0 && nNextChanges == 0 )
|
||||
{
|
||||
// No class-state change since the full/active SRM just
|
||||
// proved these pairs; this is true convergence.
|
||||
clkIncr += Abc_Clock() - clkI;
|
||||
clkSrm += Abc_Clock() - clk2;
|
||||
break;
|
||||
}
|
||||
else
|
||||
{
|
||||
Cec_IncrMgrComputeTfo( pMgr );
|
||||
if ( pDynSrm )
|
||||
Cec_DynSrmCountActivePairs( pDynSrm, pPars->fUseRings, pMgr->pTfoMark, &nTotalPairs, &nActivePairs );
|
||||
else
|
||||
Cec_IncrMgrCountActivePairs( pMgr, pPars->fUseRings, pMgr->pTfoMark, &nTotalPairs, &nActivePairs );
|
||||
if ( nActivePairs == 0 )
|
||||
{
|
||||
// Classes changed, but no remaining candidate pair
|
||||
// depends on the changes and no new ring edge exists.
|
||||
clkIncr += Abc_Clock() - clkI;
|
||||
clkSrm += Abc_Clock() - clk2;
|
||||
break;
|
||||
}
|
||||
// Fallback is based on emitted candidate pairs, not seed count.
|
||||
// Above ~70% active pairs, full SRM is usually cheaper.
|
||||
else if ( nTotalPairs > 0 && (ABC_INT64_T)10 * nActivePairs > (ABC_INT64_T)7 * nTotalPairs )
|
||||
{
|
||||
nIncrFallback++;
|
||||
}
|
||||
else
|
||||
{
|
||||
pTfoMask = pMgr->pTfoMark;
|
||||
nIncrSkipped += nTotalPairs - nActivePairs;
|
||||
}
|
||||
}
|
||||
clkIncr += Abc_Clock() - clkI;
|
||||
}
|
||||
|
||||
// Incremental persistence under circuit-SAT: build the COless pCore and solve
|
||||
// its root literals directly below; skip the per-round throwaway view.
|
||||
if ( fPersist )
|
||||
{
|
||||
Cec_DynSrmBuildCore( pDynSrm, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
|
||||
pSrm = NULL;
|
||||
}
|
||||
else if ( pDynSrm )
|
||||
pSrm = Cec_DynSrmBuild( pDynSrm, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pTfoMask ? CEC_EMIT_ACTIVE : CEC_EMIT_ALL );
|
||||
else if ( pTfoMask )
|
||||
pSrm = Gia_ManCorrSpecReduce_Emit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings, pTfoMask, pMgr, CEC_EMIT_ACTIVE, NULL );
|
||||
else
|
||||
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
|
||||
if ( pTfoMask && pPars->fVeryVerbose )
|
||||
Abc_Print( 1, " [incr r=%d repr=%d next=%d tfo=%d active=%d/%d POs=%d]\n",
|
||||
r, nReprSeeds, nNextChanges,
|
||||
Vec_IntSize(pMgr->vTfoNodes), nActivePairs, nTotalPairs,
|
||||
fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm) );
|
||||
// Snapshot after SRM construction: the active builder still needs
|
||||
// the old pNexts snapshot to recognize newly-created ring edges.
|
||||
// SAT/sim refinement below is what creates the next iteration's diff.
|
||||
if ( pMgr )
|
||||
Cec_IncrMgrSnapshotClasses( pMgr );
|
||||
}
|
||||
assert( fPersist || (Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig)) );
|
||||
pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
|
||||
assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
|
||||
clkSrm += Abc_Clock() - clk2;
|
||||
if ( (fPersist ? Vec_IntSize(Cec_DynSrmOutLits(pDynSrm)) : Gia_ManCoNum(pSrm)) == 0 )
|
||||
if ( Gia_ManCoNum(pSrm) == 0 )
|
||||
{
|
||||
Vec_IntFree( vOutputs );
|
||||
if ( pSrm )
|
||||
Gia_ManStop( pSrm );
|
||||
Gia_ManStop( pSrm );
|
||||
break;
|
||||
}
|
||||
//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
|
||||
// found counter-examples to speculation
|
||||
clk2 = Abc_Clock();
|
||||
if ( fPersist )
|
||||
vCexStore = Cec_DynSrmSolve( pDynSrm, pPars->nBTLimit, &vStatus );
|
||||
else if ( pPars->fUseCSat )
|
||||
if ( pPars->fUseCSat )
|
||||
vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 );
|
||||
else
|
||||
vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
|
||||
if ( pSrm )
|
||||
Gia_ManStop( pSrm );
|
||||
Gia_ManStop( pSrm );
|
||||
clkSat += Abc_Clock() - clk2;
|
||||
if ( Vec_IntSize(vCexStore) == 0 )
|
||||
{
|
||||
|
|
@ -1492,21 +1046,10 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
|
||||
// refine classes with these counter-examples
|
||||
clk2 = Abc_Clock();
|
||||
{
|
||||
int nCexReal = 0, nCexTriv = 0;
|
||||
Cec_ManCexStoreClassify( vCexStore, &nCexReal, &nCexTriv, NULL );
|
||||
if ( nCexReal > 0 || !pPars->fSkipFailResim )
|
||||
{
|
||||
Cec_ManResimulateCounterExamplesSeed( pSim,
|
||||
vCexStore, pPars->nFrames + 1 + nAddFrames,
|
||||
pSeedSim, vOutputs );
|
||||
}
|
||||
if ( nCexTriv > 0 )
|
||||
Cec_ManTrivialSatSplit( pAig, pSim, vCexStore, vStatus, vOutputs, pPars->fUseRings );
|
||||
Vec_IntFree( vCexStore );
|
||||
clkSim += Abc_Clock() - clk2;
|
||||
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
|
||||
}
|
||||
RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
|
||||
Vec_IntFree( vCexStore );
|
||||
clkSim += Abc_Clock() - clk2;
|
||||
Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
|
||||
if ( pPars->fVerbose )
|
||||
Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
|
||||
Vec_StrFree( vStatus );
|
||||
|
|
@ -1515,9 +1058,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
if ( Cec_ParCorShouldStop( pPars ) )
|
||||
{
|
||||
Cec_ManSimStop( pSim );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
return 1;
|
||||
}
|
||||
// quit if const is no longer there
|
||||
|
|
@ -1527,9 +1067,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
printf( "because the property output is no longer a candidate constant.\n" );
|
||||
fflush( stdout );
|
||||
Cec_ManSimStop( pSim );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
return 0;
|
||||
}
|
||||
if ( pPars->nLimitMax )
|
||||
|
|
@ -1541,9 +1078,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
printf( "because refinement does not proceed quickly.\n" );
|
||||
fflush( stdout );
|
||||
Cec_ManSimStop( pSim );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
ABC_FREE( pAig->pReprs );
|
||||
ABC_FREE( pAig->pNexts );
|
||||
return 0;
|
||||
|
|
@ -1571,21 +1105,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
|
|||
ABC_PRTP( "Sat ", clkSat, clkTotal );
|
||||
ABC_PRTP( "Sim ", clkSim, clkTotal );
|
||||
ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
|
||||
if ( pMgr )
|
||||
{
|
||||
ABC_PRTP( "Incr ", clkIncr, clkTotal );
|
||||
Abc_Print( 1, "Incr: fallback rounds = %d, skipped candidate pairs = %d\n", nIncrFallback, nIncrSkipped );
|
||||
}
|
||||
if ( pDynSrm )
|
||||
Cec_DynSrmPrintStats( pDynSrm );
|
||||
Abc_PrintTime( 1, "TOTAL", clkTotal );
|
||||
fflush( stdout );
|
||||
}
|
||||
Cec_IncrMgrFree( pMgr );
|
||||
Cec_DynSrmFree( pDynSrm );
|
||||
Cec_SeedSimFree( pSeedSim );
|
||||
return 1;
|
||||
}
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -0,0 +1,155 @@
|
|||
/**CFile****************************************************************
|
||||
|
||||
FileName [cecCorrCert.c]
|
||||
|
||||
SystemName [ABC: Logic synthesis and verification system.]
|
||||
|
||||
PackageName [Combinational equivalence checking.]
|
||||
|
||||
Synopsis [Kissat certificate for the final &scorr2 fixed point.]
|
||||
|
||||
Author [Xiran Zhao]
|
||||
|
||||
Affiliation [University of Chinese Academy of Sciences (UCAS)]
|
||||
|
||||
Date [Ver. 1.0. Started - Jun 2026.]
|
||||
|
||||
***********************************************************************/
|
||||
|
||||
#include "cecInt.h"
|
||||
#include "sat/cnf/cnf.h"
|
||||
#include "sat/kissat/kissatSolver.h"
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
extern void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out );
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [Certifies all SRM mismatch outputs in one Kissat call.]
|
||||
|
||||
Description [The generated CNF contains one OR clause over all SRM
|
||||
outputs. UNSAT therefore proves every candidate pair simultaneously.
|
||||
On SAT, one full CI assignment and one violated output are returned in
|
||||
the same format used by the ordinary correspondence refinement loop.
|
||||
|
||||
Return values are 1 (all outputs UNSAT), 0 (SAT counterexample), and
|
||||
-1 (UNKNOWN or an inconsistent model/API result).]
|
||||
|
||||
SideEffects [None on pSrm or the host correspondence classes.]
|
||||
|
||||
***********************************************************************/
|
||||
int Cec_ManCorrKissatCertify( Gia_Man_t * pSrm, Vec_Int_t * vOutputs,
|
||||
Vec_Int_t ** pvCexStore, Vec_Str_t ** pvStatus, int * piOut, int fVerbose )
|
||||
{
|
||||
Cnf_Dat_t * pCnf;
|
||||
kissat_solver * pSat;
|
||||
Vec_Int_t * vCexStore = Vec_IntAlloc( 16 );
|
||||
Vec_Str_t * vStatus = Vec_StrAlloc( Gia_ManCoNum(pSrm) );
|
||||
Gia_Obj_t * pObj;
|
||||
unsigned char * pValues = NULL;
|
||||
abctime clk = Abc_Clock();
|
||||
int i, iVar, * pBeg, * pEnd, Status = -1, iOut = -1;
|
||||
|
||||
assert( Vec_IntSize(vOutputs) == 2 * Gia_ManCoNum(pSrm) );
|
||||
*pvCexStore = NULL;
|
||||
*pvStatus = NULL;
|
||||
*piOut = -1;
|
||||
for ( i = 0; i < Gia_ManCoNum(pSrm); i++ )
|
||||
Vec_StrPush( vStatus, 1 );
|
||||
if ( Gia_ManCoNum(pSrm) == 0 )
|
||||
{
|
||||
if ( fVerbose )
|
||||
Abc_Print( 1, "[scorr2-audit] result=pass pairs=0 reason=structural time_sec=0.00\n" );
|
||||
*pvCexStore = vCexStore;
|
||||
*pvStatus = vStatus;
|
||||
return 1;
|
||||
}
|
||||
|
||||
// fAddOrCla=1 asserts that at least one mismatch output is true.
|
||||
pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pSrm, 8, 0, 1, 0, 0 );
|
||||
pSat = kissat_solver_new();
|
||||
kissat_solver_setnvars( pSat, pCnf->nVars );
|
||||
Cnf_CnfForClause( pCnf, pBeg, pEnd, i )
|
||||
if ( !kissat_solver_addclause(pSat, pBeg, pEnd) )
|
||||
{
|
||||
// Contradiction during clause loading is already an UNSAT proof.
|
||||
Status = -1;
|
||||
goto finish;
|
||||
}
|
||||
Status = kissat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
|
||||
if ( Status == -1 )
|
||||
goto finish;
|
||||
if ( Status == 0 )
|
||||
goto finish;
|
||||
|
||||
// Evaluate the GIA under the Kissat model to identify a violated pair.
|
||||
pValues = ABC_CALLOC( unsigned char, Gia_ManObjNum(pSrm) );
|
||||
Gia_ManForEachCi( pSrm, pObj, i )
|
||||
{
|
||||
iVar = pCnf->pVarNums[Gia_ObjId(pSrm, pObj)];
|
||||
pValues[Gia_ObjId(pSrm, pObj)] = iVar >= 0 ? kissat_solver_get_var_value(pSat, iVar) : 0;
|
||||
}
|
||||
Gia_ManForEachAnd( pSrm, pObj, i )
|
||||
pValues[Gia_ObjId(pSrm, pObj)] =
|
||||
(pValues[Gia_ObjFaninId0p(pSrm, pObj)] ^ Gia_ObjFaninC0(pObj)) &
|
||||
(pValues[Gia_ObjFaninId1p(pSrm, pObj)] ^ Gia_ObjFaninC1(pObj));
|
||||
Gia_ManForEachCo( pSrm, pObj, i )
|
||||
if ( pValues[Gia_ObjFaninId0p(pSrm, pObj)] ^ Gia_ObjFaninC0(pObj) )
|
||||
{
|
||||
iOut = i;
|
||||
break;
|
||||
}
|
||||
if ( iOut < 0 )
|
||||
{
|
||||
Status = 0;
|
||||
goto finish;
|
||||
}
|
||||
{
|
||||
Vec_Int_t * vCex = Vec_IntAlloc( Gia_ManCiNum(pSrm) );
|
||||
Gia_ManForEachCi( pSrm, pObj, i )
|
||||
Vec_IntPush( vCex, Abc_Var2Lit(Gia_ObjCioId(pObj), !pValues[Gia_ObjId(pSrm, pObj)]) );
|
||||
Vec_StrWriteEntry( vStatus, iOut, 0 );
|
||||
Cec_ManSatAddToStore( vCexStore, vCex, iOut );
|
||||
Vec_IntFree( vCex );
|
||||
}
|
||||
|
||||
finish:
|
||||
if ( fVerbose )
|
||||
{
|
||||
if ( Status == -1 )
|
||||
Abc_Print( 1, "[scorr2-audit] result=pass pairs=%d vars=%d clauses=%d ", Gia_ManCoNum(pSrm), pCnf->nVars, pCnf->nClauses );
|
||||
else if ( Status == 1 && iOut >= 0 )
|
||||
Abc_Print( 1, "[scorr2-audit] result=counterexample pair=%d/%d nodes=%d/%d ", iOut, Gia_ManCoNum(pSrm), Vec_IntEntry(vOutputs, 2*iOut), Vec_IntEntry(vOutputs, 2*iOut+1) );
|
||||
else
|
||||
Abc_Print( -1, "[scorr2-audit] result=unknown pairs=%d ", Gia_ManCoNum(pSrm) );
|
||||
Abc_PrintTime( 1, "Kissat", Abc_Clock() - clk );
|
||||
if ( Status == 1 && iOut >= 0 && pValues != NULL )
|
||||
{
|
||||
Abc_Print( -1, "[scorr2-audit] model" );
|
||||
Gia_ManForEachCi( pSrm, pObj, i )
|
||||
{
|
||||
if ( i == 16 )
|
||||
{
|
||||
Abc_Print( -1, " ..." );
|
||||
break;
|
||||
}
|
||||
Abc_Print( -1, " ci%d=%d", Gia_ObjCioId(pObj), pValues[Gia_ObjId(pSrm, pObj)] );
|
||||
}
|
||||
Abc_Print( -1, "\n" );
|
||||
}
|
||||
}
|
||||
ABC_FREE( pValues );
|
||||
kissat_solver_delete( pSat );
|
||||
Cnf_DataFree( pCnf );
|
||||
*pvCexStore = vCexStore;
|
||||
*pvStatus = vStatus;
|
||||
*piOut = iOut;
|
||||
if ( Status == -1 )
|
||||
return 1;
|
||||
if ( Status == 1 && iOut >= 0 )
|
||||
return 0;
|
||||
return -1;
|
||||
}
|
||||
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
|
@ -6,11 +6,11 @@
|
|||
|
||||
PackageName [Combinational equivalence checking.]
|
||||
|
||||
Synopsis [Dynamic SRM manager for &scorr.]
|
||||
Synopsis [Dynamic SRM manager for &scorr2.]
|
||||
|
||||
Author [Xiran Zhao]
|
||||
|
||||
Affiliation [University of Chinese Academy of Sciences]
|
||||
Affiliation [University of Chinese Academy of Sciences (UCAS)]
|
||||
|
||||
Date [Ver. 1.0. Started - Jun 2026.]
|
||||
|
||||
|
|
@ -20,6 +20,13 @@
|
|||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
|
||||
#define CEC_BMC_TAS_PROBE_ROOTS 8
|
||||
#define CEC_BMC_TAS_PROBE_SUCCESS_PCT 75
|
||||
#define CEC_BMC_TAS_CORE_NORM_MAX 25000
|
||||
#define CEC_BMC_TAS_CORE_ABS_MAX 200000
|
||||
#define CEC_BMC_TAS_RETRY_ROOTS_MAX 8192
|
||||
#define CEC_BMC_TAS_STRUCT_WORK_MAX 64000000LL
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
@ -29,8 +36,12 @@ struct Cec_DynSrm_t_
|
|||
Gia_Man_t * pAig; // host AIG; owned by caller
|
||||
Cec_IncrMgr_t * pIncr; // active-list manager; owned by caller
|
||||
Gia_Man_t * pCore; // persistent SRM core without COs
|
||||
Cbs_Man_t * pCbs; // resident circuit-SAT manager on pCore
|
||||
Cbs_Man_t * pCbs; // resident circuit-SAT manager on pCore (-D direct solving)
|
||||
Tas_Man_t * pTas; // resident TAS manager on pCore (-D direct solving)
|
||||
int nCoreObjsAtReset; // real post-build pCore size after the last cold (re)build, for compaction (0 until that build finishes)
|
||||
int fUseAdaptive; // use timing-guided cold rebuilds in addition to the hard bloat guard
|
||||
int nCompactMult;
|
||||
int fForceRebuild;
|
||||
Vec_Int_t * vSpecLits; // cached core literals, indexed by frame/object
|
||||
Vec_Int_t * vOutLits; // core literals selected as current SAT outputs
|
||||
Vec_Int_t * vCopyTouched; // core ANDs copied into the current view
|
||||
|
|
@ -38,8 +49,6 @@ struct Cec_DynSrm_t_
|
|||
Vec_Int_t * vRoMap; // host obj id -> RO index
|
||||
// Phase-2 measurement (behavior-preserving): per-key stamp used to count the
|
||||
// union of true-value (no repr substitution) cones of the active pairs.
|
||||
int * pTrueMark; // size = nFramesTotal * nObjs; 0 = unvisited
|
||||
int nTrueStamp; // current visit stamp
|
||||
int nObjs;
|
||||
int nPis;
|
||||
int nRegs;
|
||||
|
|
@ -47,8 +56,21 @@ struct Cec_DynSrm_t_
|
|||
int nCoreCiNum;
|
||||
int nBuilds;
|
||||
int nBuildsActive;
|
||||
int nBuildsFull;
|
||||
int nCoreResets;
|
||||
int nCoreCompactions;
|
||||
int nIncrFallbackResets;
|
||||
int nDynActiveResets;
|
||||
int nAdaptiveResets;
|
||||
int nAdaptiveBurstResets;
|
||||
int nAdaptiveBurstLeft;
|
||||
int nBuildsSinceReset;
|
||||
int nLastBuildReset;
|
||||
int nLastResetReason;
|
||||
int nForceResetReason;
|
||||
int nLastResetSpan;
|
||||
int nAdaptResetSamples;
|
||||
int nAdaptReuseSamples;
|
||||
int nCoreBuilds;
|
||||
int nViewBuilds;
|
||||
int nCacheFullClears;
|
||||
|
|
@ -60,18 +82,66 @@ struct Cec_DynSrm_t_
|
|||
int nCoreObjsMax;
|
||||
int nViewObjsLast;
|
||||
int nViewObjsMax;
|
||||
int nCoreDeltaLast;
|
||||
int nCoreDeltaMax;
|
||||
int nCoreBloatLastPermil;
|
||||
int nCoreBloatMaxPermil;
|
||||
ABC_INT64_T nOutLitsActiveSum;
|
||||
ABC_INT64_T nOutLitsFullSum;
|
||||
ABC_INT64_T nCoreObjsActiveSum;
|
||||
ABC_INT64_T nCoreObjsFullSum;
|
||||
ABC_INT64_T nSolveIters;
|
||||
ABC_INT64_T nSolveCalls;
|
||||
ABC_INT64_T nSolveReal;
|
||||
ABC_INT64_T nSolveTriv;
|
||||
ABC_INT64_T nSolveFail;
|
||||
ABC_INT64_T nSolveFailIters;
|
||||
ABC_INT64_T nFailCoreObjSum;
|
||||
ABC_INT64_T nFailOutLitSum;
|
||||
int nFailCoreObjMax;
|
||||
int nFailOutLitMax;
|
||||
double dAdaptResetCost;
|
||||
double dAdaptReuseCost;
|
||||
double dAdaptLastCost;
|
||||
abctime tBuildLast;
|
||||
abctime tBuildEnsureLast;
|
||||
abctime tBuildInvalidateLast;
|
||||
abctime tBuildEmitLast;
|
||||
abctime tBuildTotal;
|
||||
abctime tBuildResetTotal;
|
||||
abctime tBuildReuseTotal;
|
||||
abctime tBuildEnsureTotal;
|
||||
abctime tBuildInvalidateTotal;
|
||||
abctime tBuildEmitTotal;
|
||||
abctime tViewLast;
|
||||
abctime tViewTotal;
|
||||
abctime tSolveLast;
|
||||
ABC_INT64_T nBmcAdaptiveRounds;
|
||||
ABC_INT64_T nBmcCbsRoots;
|
||||
ABC_INT64_T nBmcCbsUnknown;
|
||||
ABC_INT64_T nBmcTasProbeRoots;
|
||||
ABC_INT64_T nBmcTasRetryRoots;
|
||||
ABC_INT64_T nBmcTasResolved;
|
||||
ABC_INT64_T nBmcTasUnknown;
|
||||
ABC_INT64_T nBmcTasEnabledRounds;
|
||||
ABC_INT64_T nBmcTasSkippedLarge;
|
||||
ABC_INT64_T nBmcTasSkippedWork;
|
||||
ABC_INT64_T nBmcTasSkippedBudget;
|
||||
ABC_INT64_T nBmcTasStructWork;
|
||||
abctime tBmcCbs;
|
||||
abctime tBmcTas;
|
||||
};
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// FUNCTION DEFINITIONS ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
// Active-pair selection mirrors incremental mode: a pair is active iff an endpoint is
|
||||
// Active-pair selection mirrors -i exactly: a pair is active iff an endpoint is
|
||||
// in the alias-aware TFO (or, in ring mode, the ring edge itself changed). The
|
||||
// earlier "pending" set that force-re-emitted still-merged SAT pairs has been
|
||||
// removed: per md/scorr_i_correctness_bug_report.md the alias-aware TFO is the
|
||||
// real fix, and the retry/pending protection was shown to be both unnecessary
|
||||
// and incomplete.
|
||||
// (alias-only passes -d) and incomplete. -d (incr-oracle) certifies soundness.
|
||||
static int Cec_DynSrmActiveConst( Cec_DynSrm_t * p, int * pTfoMark, int ObjId )
|
||||
{
|
||||
(void)p;
|
||||
|
|
@ -134,6 +204,9 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
|
|||
if ( p->pCbs ) // stop resident solver before its pCore is freed
|
||||
Cbs_ManStop( p->pCbs );
|
||||
p->pCbs = NULL;
|
||||
if ( p->pTas )
|
||||
Tas_ManStop( p->pTas );
|
||||
p->pTas = NULL;
|
||||
if ( p->pCore )
|
||||
Gia_ManStop( p->pCore );
|
||||
p->pCore = NULL;
|
||||
|
|
@ -143,8 +216,6 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
|
|||
Vec_IntFreeP( &p->vCopyTouched );
|
||||
Vec_IntFreeP( &p->vPiMap );
|
||||
Vec_IntFreeP( &p->vRoMap );
|
||||
ABC_FREE( p->pTrueMark );
|
||||
p->nTrueStamp = 0;
|
||||
p->nObjs = p->nPis = p->nRegs = p->nFramesTotal = p->nCoreCiNum = 0;
|
||||
}
|
||||
|
||||
|
|
@ -153,30 +224,104 @@ static void Cec_DynSrmResetCore( Cec_DynSrm_t * p )
|
|||
// solver's per-round sync/solve walks an ever-larger graph. At a quiescent
|
||||
// point (start of a build) cold-rebuild once it exceeds a multiple of its
|
||||
// post-build size; the rebuilt core re-materializes only the live active cones.
|
||||
#define CEC_DYN_COMPACT_MULT 4
|
||||
#define CEC_DYN_COMPACT_MULT 4
|
||||
#define CEC_DYN_ADAPT_BLOAT_PERMIL 3000
|
||||
#define CEC_DYN_ADAPT_WORSE_PERMIL 1500
|
||||
#define CEC_DYN_ADAPT_RESET_BETTER_PERMIL 750
|
||||
#define CEC_DYN_ADAPT_MIN_REUSE_SAMPLES 8
|
||||
#define CEC_DYN_ADAPT_MIN_CALLS 16
|
||||
#define CEC_DYN_ADAPT_MIN_BUILDS_SINCE_RESET 2
|
||||
#define CEC_DYN_ADAPT_FAST_GROW_SPAN 4
|
||||
#define CEC_DYN_ADAPT_BURST_ROUNDS 2
|
||||
#define CEC_DYN_ADAPT_FAST_COMPACT_SPAN 2
|
||||
|
||||
enum {
|
||||
CEC_DYN_RESET_NONE = 0,
|
||||
CEC_DYN_RESET_SHAPE = 1,
|
||||
CEC_DYN_RESET_COMPACT = 2,
|
||||
CEC_DYN_RESET_ADAPT = 3,
|
||||
CEC_DYN_RESET_BURST = 4,
|
||||
CEC_DYN_RESET_IFALLBACK = 5,
|
||||
CEC_DYN_RESET_DACTIVE = 6
|
||||
};
|
||||
|
||||
static int Cec_DynSrmCurrentBloatPermil( Cec_DynSrm_t * p )
|
||||
{
|
||||
if ( p->nCoreObjsAtReset <= 0 || p->pCore == NULL )
|
||||
return 1000;
|
||||
return (int)((ABC_INT64_T)1000 * Gia_ManObjNum(p->pCore) / p->nCoreObjsAtReset);
|
||||
}
|
||||
|
||||
static int Cec_DynSrmShouldCompact( Cec_DynSrm_t * p )
|
||||
{
|
||||
// 64-bit multiply: nCoreObjsAtReset can reach tens of millions (the growth
|
||||
// case this guards), so CEC_DYN_COMPACT_MULT * it must not overflow int.
|
||||
// case this guards), so nCompactMult * it must not overflow int.
|
||||
return p->nCoreObjsAtReset > 0 &&
|
||||
Gia_ManObjNum(p->pCore) > (ABC_INT64_T)CEC_DYN_COMPACT_MULT * p->nCoreObjsAtReset;
|
||||
Gia_ManObjNum(p->pCore) > (ABC_INT64_T)p->nCompactMult * p->nCoreObjsAtReset;
|
||||
}
|
||||
|
||||
static int Cec_DynSrmShouldAdaptiveReset( Cec_DynSrm_t * p )
|
||||
{
|
||||
int nBloat;
|
||||
if ( !p->fUseAdaptive )
|
||||
return CEC_DYN_RESET_NONE;
|
||||
if ( p->nAdaptiveBurstLeft > 0 )
|
||||
{
|
||||
p->nAdaptiveBurstLeft--;
|
||||
p->nAdaptiveBurstResets++;
|
||||
return CEC_DYN_RESET_BURST;
|
||||
}
|
||||
if ( p->nBuildsSinceReset < CEC_DYN_ADAPT_MIN_BUILDS_SINCE_RESET )
|
||||
return CEC_DYN_RESET_NONE;
|
||||
if ( p->nBuildsSinceReset > CEC_DYN_ADAPT_FAST_GROW_SPAN )
|
||||
return CEC_DYN_RESET_NONE;
|
||||
if ( p->nAdaptResetSamples == 0 || p->nAdaptReuseSamples < CEC_DYN_ADAPT_MIN_REUSE_SAMPLES )
|
||||
return CEC_DYN_RESET_NONE;
|
||||
nBloat = Cec_DynSrmCurrentBloatPermil( p );
|
||||
if ( nBloat < CEC_DYN_ADAPT_BLOAT_PERMIL )
|
||||
return CEC_DYN_RESET_NONE;
|
||||
if ( 1000.0 * p->dAdaptReuseCost > (double)CEC_DYN_ADAPT_WORSE_PERMIL * p->dAdaptResetCost )
|
||||
return CEC_DYN_RESET_ADAPT;
|
||||
return CEC_DYN_RESET_NONE;
|
||||
}
|
||||
|
||||
static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr )
|
||||
{
|
||||
Gia_Obj_t * pObj;
|
||||
int f, i, nFramesTotal = nFrames + fScorr;
|
||||
int ResetReason = CEC_DYN_RESET_NONE;
|
||||
int fSameShape = ( p->pCore != NULL &&
|
||||
p->nObjs == Gia_ManObjNum(p->pAig) &&
|
||||
p->nPis == Gia_ManPiNum(p->pAig) &&
|
||||
p->nRegs == Gia_ManRegNum(p->pAig) &&
|
||||
p->nFramesTotal == nFramesTotal );
|
||||
if ( fSameShape && !Cec_DynSrmShouldCompact(p) )
|
||||
p->nLastBuildReset = 0;
|
||||
p->nLastResetReason = CEC_DYN_RESET_NONE;
|
||||
if ( !fSameShape )
|
||||
ResetReason = CEC_DYN_RESET_SHAPE;
|
||||
else if ( p->fForceRebuild )
|
||||
ResetReason = p->nForceResetReason;
|
||||
else if ( Cec_DynSrmShouldCompact(p) )
|
||||
ResetReason = CEC_DYN_RESET_COMPACT;
|
||||
else
|
||||
ResetReason = Cec_DynSrmShouldAdaptiveReset( p );
|
||||
if ( fSameShape && ResetReason == CEC_DYN_RESET_NONE )
|
||||
return;
|
||||
if ( fSameShape ) // reusable shape but bloated: cold-rebuild
|
||||
p->fForceRebuild = 0;
|
||||
p->nForceResetReason = CEC_DYN_RESET_NONE;
|
||||
if ( ResetReason == CEC_DYN_RESET_COMPACT ) // reusable shape but bloated: cold-rebuild
|
||||
p->nCoreCompactions++;
|
||||
if ( ResetReason == CEC_DYN_RESET_IFALLBACK )
|
||||
p->nIncrFallbackResets++;
|
||||
if ( ResetReason == CEC_DYN_RESET_DACTIVE )
|
||||
p->nDynActiveResets++;
|
||||
if ( ResetReason == CEC_DYN_RESET_ADAPT )
|
||||
p->nAdaptiveResets++;
|
||||
p->nLastResetSpan = p->nBuildsSinceReset;
|
||||
Cec_DynSrmResetCore( p );
|
||||
p->nLastBuildReset = 1;
|
||||
p->nLastResetReason = ResetReason;
|
||||
p->nBuildsSinceReset = 0;
|
||||
p->nObjs = Gia_ManObjNum( p->pAig );
|
||||
p->nPis = Gia_ManPiNum( p->pAig );
|
||||
p->nRegs = Gia_ManRegNum( p->pAig );
|
||||
|
|
@ -186,8 +331,6 @@ static void Cec_DynSrmEnsureCore( Cec_DynSrm_t * p, int nFrames, int fScorr )
|
|||
p->vCopyTouched = Vec_IntAlloc( 1000 );
|
||||
p->vPiMap = Vec_IntStartFull( p->nObjs );
|
||||
p->vRoMap = Vec_IntStartFull( p->nObjs );
|
||||
p->pTrueMark = ABC_CALLOC( int, p->nFramesTotal * p->nObjs );
|
||||
p->nTrueStamp = 0;
|
||||
p->pCore = Gia_ManStart( Abc_MaxInt( p->nFramesTotal * p->nObjs, 1000 ) );
|
||||
p->pCore->pName = Abc_UtilStrsav( p->pAig->pName );
|
||||
p->pCore->pSpec = Abc_UtilStrsav( p->pAig->pSpec );
|
||||
|
|
@ -411,14 +554,77 @@ static Gia_Man_t * Cec_DynSrmBuildView( Cec_DynSrm_t * p )
|
|||
return pView;
|
||||
}
|
||||
|
||||
Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr )
|
||||
static void Cec_DynSrmRecordBuildStats( Cec_DynSrm_t * p,
|
||||
Cec_IncrEmitMode_t Mode, int nCoreObjsBefore, int nCoreResetsBefore,
|
||||
abctime tBuild, abctime tEnsure, abctime tInvalidate, abctime tEmit )
|
||||
{
|
||||
int fReset = p->nCoreResets > nCoreResetsBefore;
|
||||
p->nBuildsSinceReset++;
|
||||
if ( Mode == CEC_EMIT_ACTIVE )
|
||||
{
|
||||
p->nOutLitsActiveSum += p->nOutLitsLast;
|
||||
p->nCoreObjsActiveSum += p->nCoreObjsLast;
|
||||
}
|
||||
else if ( Mode == CEC_EMIT_ALL )
|
||||
{
|
||||
p->nBuildsFull++;
|
||||
p->nOutLitsFullSum += p->nOutLitsLast;
|
||||
p->nCoreObjsFullSum += p->nCoreObjsLast;
|
||||
}
|
||||
p->nCoreDeltaLast = Abc_MaxInt( 0, p->nCoreObjsLast - nCoreObjsBefore );
|
||||
p->nCoreDeltaMax = Abc_MaxInt( p->nCoreDeltaMax, p->nCoreDeltaLast );
|
||||
if ( p->nCoreObjsAtReset > 0 )
|
||||
{
|
||||
p->nCoreBloatLastPermil =
|
||||
(int)((ABC_INT64_T)1000 * p->nCoreObjsLast / p->nCoreObjsAtReset);
|
||||
p->nCoreBloatMaxPermil =
|
||||
Abc_MaxInt( p->nCoreBloatMaxPermil, p->nCoreBloatLastPermil );
|
||||
}
|
||||
if ( tBuild )
|
||||
{
|
||||
p->tBuildLast = tBuild;
|
||||
p->tBuildEnsureLast = tEnsure;
|
||||
p->tBuildInvalidateLast = tInvalidate;
|
||||
p->tBuildEmitLast = tEmit;
|
||||
p->tBuildTotal += tBuild;
|
||||
if ( fReset )
|
||||
p->tBuildResetTotal += tBuild;
|
||||
else
|
||||
p->tBuildReuseTotal += tBuild;
|
||||
p->tBuildEnsureTotal += tEnsure;
|
||||
p->tBuildInvalidateTotal += tInvalidate;
|
||||
p->tBuildEmitTotal += tEmit;
|
||||
}
|
||||
}
|
||||
|
||||
Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr, int fUseAdaptive )
|
||||
{
|
||||
Cec_DynSrm_t * p = ABC_CALLOC( Cec_DynSrm_t, 1 );
|
||||
p->pAig = pAig;
|
||||
p->pIncr = pIncr;
|
||||
p->fUseAdaptive = fUseAdaptive;
|
||||
p->nCompactMult = CEC_DYN_COMPACT_MULT;
|
||||
return p;
|
||||
}
|
||||
|
||||
void Cec_DynSrmSetParams( Cec_DynSrm_t * p, Cec_ParCor_t * pPars )
|
||||
{
|
||||
if ( p == NULL || pPars == NULL )
|
||||
return;
|
||||
p->nCompactMult = Abc_MaxInt( 1, pPars->nDynSrmCompactMult );
|
||||
}
|
||||
|
||||
void Cec_DynSrmForceRebuild( Cec_DynSrm_t * p, int fIncrFallback )
|
||||
{
|
||||
if ( p == NULL )
|
||||
return;
|
||||
p->fForceRebuild = 1;
|
||||
if ( fIncrFallback )
|
||||
p->nForceResetReason = CEC_DYN_RESET_IFALLBACK;
|
||||
else if ( p->nForceResetReason != CEC_DYN_RESET_IFALLBACK )
|
||||
p->nForceResetReason = CEC_DYN_RESET_DACTIVE;
|
||||
}
|
||||
|
||||
void Cec_DynSrmFree( Cec_DynSrm_t * p )
|
||||
{
|
||||
if ( p == NULL )
|
||||
|
|
@ -427,19 +633,57 @@ void Cec_DynSrmFree( Cec_DynSrm_t * p )
|
|||
ABC_FREE( p );
|
||||
}
|
||||
|
||||
void Cec_DynSrmPrintStats( Cec_DynSrm_t * p )
|
||||
static void Cec_DynSrmUpdateAdaptCost( double * pCost, int * pSamples, double Value )
|
||||
{
|
||||
if ( *pSamples == 0 )
|
||||
*pCost = Value;
|
||||
else
|
||||
*pCost = 0.75 * *pCost + 0.25 * Value;
|
||||
(*pSamples)++;
|
||||
}
|
||||
|
||||
void Cec_DynSrmRecordSolveStats( Cec_DynSrm_t * p,
|
||||
int nCalls, int nReal, int nTriv, int nFail, abctime tSat )
|
||||
{
|
||||
int nDen;
|
||||
double dCost;
|
||||
if ( p == NULL )
|
||||
return;
|
||||
Abc_Print( 1, "DynSRM: builds = %d, active_builds = %d\n",
|
||||
p->nBuilds, p->nBuildsActive );
|
||||
Abc_Print( 1, "DynSRM: core_resets = %d, compactions = %d, core_builds = %d, view_builds = %d, out_lits_last/max = %d/%d, core_objs_last/max = %d/%d, view_objs_last/max = %d/%d\n",
|
||||
p->nCoreResets, p->nCoreCompactions, p->nCoreBuilds, p->nViewBuilds,
|
||||
p->nOutLitsLast, p->nOutLitsMax,
|
||||
p->nCoreObjsLast, p->nCoreObjsMax,
|
||||
p->nViewObjsLast, p->nViewObjsMax );
|
||||
Abc_Print( 1, "DynSRM: cache_full_clears = %d, cache_local_clears = %d, cache_local_entries = %d\n",
|
||||
p->nCacheFullClears, p->nCacheLocalClears, p->nCacheLocalEntries );
|
||||
p->nSolveIters++;
|
||||
p->nSolveCalls += nCalls;
|
||||
p->nSolveReal += nReal;
|
||||
p->nSolveTriv += nTriv;
|
||||
p->nSolveFail += nFail;
|
||||
if ( nFail > 0 )
|
||||
{
|
||||
p->nSolveFailIters++;
|
||||
p->nFailCoreObjSum += (ABC_INT64_T)nFail * p->nCoreObjsLast;
|
||||
p->nFailOutLitSum += (ABC_INT64_T)nFail * p->nOutLitsLast;
|
||||
p->nFailCoreObjMax = Abc_MaxInt( p->nFailCoreObjMax, p->nCoreObjsLast );
|
||||
p->nFailOutLitMax = Abc_MaxInt( p->nFailOutLitMax, p->nOutLitsLast );
|
||||
}
|
||||
p->tSolveLast = tSat;
|
||||
if ( !p->fUseAdaptive || p->tBuildLast == 0 )
|
||||
return;
|
||||
nDen = nCalls > 0 ? nCalls : p->nOutLitsLast;
|
||||
if ( nDen < CEC_DYN_ADAPT_MIN_CALLS )
|
||||
return;
|
||||
dCost = (double)(p->tBuildLast + tSat) / (double)nDen;
|
||||
p->dAdaptLastCost = dCost;
|
||||
if ( p->nLastBuildReset )
|
||||
{
|
||||
if ( p->nLastResetReason != CEC_DYN_RESET_SHAPE )
|
||||
{
|
||||
Cec_DynSrmUpdateAdaptCost( &p->dAdaptResetCost, &p->nAdaptResetSamples, dCost );
|
||||
if ( p->nAdaptReuseSamples >= CEC_DYN_ADAPT_MIN_REUSE_SAMPLES &&
|
||||
p->nLastResetReason == CEC_DYN_RESET_COMPACT &&
|
||||
p->nLastResetSpan <= CEC_DYN_ADAPT_FAST_COMPACT_SPAN &&
|
||||
1000.0 * dCost < (double)CEC_DYN_ADAPT_RESET_BETTER_PERMIL * p->dAdaptReuseCost )
|
||||
p->nAdaptiveBurstLeft = CEC_DYN_ADAPT_BURST_ROUNDS;
|
||||
}
|
||||
}
|
||||
else
|
||||
Cec_DynSrmUpdateAdaptCost( &p->dAdaptReuseCost, &p->nAdaptReuseSamples, dCost );
|
||||
}
|
||||
|
||||
void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark,
|
||||
|
|
@ -493,12 +737,16 @@ void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark,
|
|||
|
||||
// Builds (or extends) the persistent COless pCore and selects this round's
|
||||
// active-pair root literals into p->vOutLits / *pvOutputs. Shared by the view
|
||||
// path (Cec_DynSrmBuild) and the persistent path (solve pCore directly).
|
||||
// path (Cec_DynSrmBuild) and the -D persistence path (solve pCore directly).
|
||||
void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
|
||||
Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode )
|
||||
{
|
||||
Gia_Obj_t * pObj, * pRepr;
|
||||
int i, iPrev, iObj, iPrevNew, iObjNew, iPrevRaw, iObjRaw;
|
||||
int nCoreResetsBefore, nCoreObjsBefore;
|
||||
int fMeasure = p->fUseAdaptive;
|
||||
abctime tBuild = fMeasure ? Abc_ClockHr() : 0;
|
||||
abctime tStep, tEnsure = 0, tInvalidate = 0, tEmit = 0;
|
||||
assert( p != NULL );
|
||||
assert( nFrames > 0 );
|
||||
assert( Gia_ManRegNum(p->pAig) > 0 );
|
||||
|
|
@ -507,8 +755,15 @@ void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
|
|||
p->nBuilds++;
|
||||
if ( Mode == CEC_EMIT_ACTIVE )
|
||||
p->nBuildsActive++;
|
||||
nCoreResetsBefore = p->nCoreResets;
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Cec_DynSrmEnsureCore( p, nFrames, fScorr );
|
||||
if ( fMeasure ) tEnsure = Abc_ClockHr() - tStep;
|
||||
nCoreObjsBefore = Gia_ManObjNum( p->pCore );
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
|
||||
if ( fMeasure ) tInvalidate = Abc_ClockHr() - tStep;
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Gia_ManSetPhase( p->pAig );
|
||||
*pvOutputs = Vec_IntAlloc( 1000 );
|
||||
Vec_IntClear( p->vOutLits );
|
||||
|
|
@ -603,6 +858,10 @@ void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr,
|
|||
if ( p->nCoreObjsAtReset == 0 ) // first build after a cold (re)set: record the
|
||||
p->nCoreObjsAtReset = p->nCoreObjsLast; // real post-build size as the compaction baseline
|
||||
p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
|
||||
if ( fMeasure ) tEmit = Abc_ClockHr() - tStep;
|
||||
if ( fMeasure ) tBuild = Abc_ClockHr() - tBuild;
|
||||
Cec_DynSrmRecordBuildStats( p, Mode, nCoreObjsBefore, nCoreResetsBefore,
|
||||
tBuild, tEnsure, tInvalidate, tEmit );
|
||||
}
|
||||
|
||||
Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr,
|
||||
|
|
@ -621,6 +880,10 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
|
|||
{
|
||||
Gia_Obj_t * pObj, * pRepr;
|
||||
int f, i, iPrevNew, iObjNew;
|
||||
int nCoreResetsBefore, nCoreObjsBefore;
|
||||
int fMeasure = p->fUseAdaptive;
|
||||
abctime tBuild = fMeasure ? Abc_ClockHr() : 0;
|
||||
abctime tStep, tEnsure = 0, tInvalidate = 0, tEmit = 0;
|
||||
assert( p != NULL );
|
||||
assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
|
||||
assert( Gia_ManRegNum(p->pAig) > 0 );
|
||||
|
|
@ -629,8 +892,15 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
|
|||
p->nBuilds++;
|
||||
if ( Mode == CEC_EMIT_ACTIVE )
|
||||
p->nBuildsActive++;
|
||||
nCoreResetsBefore = p->nCoreResets;
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Cec_DynSrmEnsureCore( p, nFrames + nPrefix, fScorr );
|
||||
if ( fMeasure ) tEnsure = Abc_ClockHr() - tStep;
|
||||
nCoreObjsBefore = Gia_ManObjNum( p->pCore );
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Cec_DynSrmInvalidateCache( p, Mode == CEC_EMIT_SKIPPED ? NULL : pTfoMask );
|
||||
if ( fMeasure ) tInvalidate = Abc_ClockHr() - tStep;
|
||||
tStep = fMeasure ? Abc_ClockHr() : 0;
|
||||
Gia_ManSetPhase( p->pAig );
|
||||
*pvOutputs = Vec_IntAlloc( 1000 );
|
||||
Vec_IntClear( p->vOutLits );
|
||||
|
|
@ -665,6 +935,13 @@ void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fS
|
|||
if ( p->nCoreObjsAtReset == 0 )
|
||||
p->nCoreObjsAtReset = p->nCoreObjsLast;
|
||||
p->nCoreObjsMax = Abc_MaxInt( p->nCoreObjsMax, p->nCoreObjsLast );
|
||||
if ( fMeasure )
|
||||
{
|
||||
tEmit = Abc_ClockHr() - tStep;
|
||||
tBuild = Abc_ClockHr() - tBuild;
|
||||
}
|
||||
Cec_DynSrmRecordBuildStats( p, Mode, nCoreObjsBefore, nCoreResetsBefore,
|
||||
tBuild, tEnsure, tInvalidate, tEmit );
|
||||
}
|
||||
|
||||
Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr,
|
||||
|
|
@ -681,16 +958,254 @@ Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p ) { return p->vOutLits; }
|
|||
// circuit-SAT manager (allocated lazily; re-created after a core reset/compaction
|
||||
// since its pAig is freed there). The CI-layout assert guards the CEX CioId ->
|
||||
// resim-input contract that the discarded view used to enforce in the main loop.
|
||||
Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus )
|
||||
Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas )
|
||||
{
|
||||
assert( Gia_ManRegNum(p->pCore) == 0 );
|
||||
assert( Gia_ManCiNum(p->pCore) == p->nRegs + p->nFramesTotal * p->nPis );
|
||||
if ( fUseTas )
|
||||
{
|
||||
if ( p->pTas == NULL )
|
||||
p->pTas = Tas_ManAlloc( p->pCore, nConfs );
|
||||
Tas_ManSetConflictNum( p->pTas, nConfs );
|
||||
return Tas_ManSolveRoots( p->pTas, p->vOutLits, pvStatus, 0 );
|
||||
}
|
||||
if ( p->pCbs == NULL )
|
||||
p->pCbs = Cbs_ManAlloc( p->pCore );
|
||||
Cbs_ManSetConflictNum( p->pCbs, nConfs );
|
||||
return Cbs_ManSolveRoots( p->pCbs, p->vOutLits, pvStatus, 0 );
|
||||
}
|
||||
|
||||
static void Cec_DynSrmStoreCopyEntry( Vec_Int_t * vDest, Vec_Int_t * vSrc, int iStart, int iOut )
|
||||
{
|
||||
int k, nLits = Vec_IntEntry( vSrc, iStart + 1 );
|
||||
Vec_IntPush( vDest, iOut );
|
||||
Vec_IntPush( vDest, nLits );
|
||||
for ( k = 0; k < nLits; k++ )
|
||||
Vec_IntPush( vDest, Vec_IntEntry(vSrc, iStart + 2 + k) );
|
||||
}
|
||||
|
||||
static Vec_Int_t * Cec_DynSrmStoreIndex( Vec_Int_t * vStore, int nRoots )
|
||||
{
|
||||
Vec_Int_t * vStarts = Vec_IntStartFull( nRoots );
|
||||
int iStart = 0, iOut, nLits;
|
||||
while ( iStart < Vec_IntSize(vStore) )
|
||||
{
|
||||
iOut = Vec_IntEntry( vStore, iStart );
|
||||
nLits = Vec_IntEntry( vStore, iStart + 1 );
|
||||
assert( iOut >= 0 && iOut < nRoots );
|
||||
assert( nLits >= -1 );
|
||||
Vec_IntWriteEntry( vStarts, iOut, iStart );
|
||||
iStart += 2 + Abc_MaxInt( nLits, 0 );
|
||||
}
|
||||
assert( iStart == Vec_IntSize(vStore) );
|
||||
return vStarts;
|
||||
}
|
||||
|
||||
// Runs TAS on a subset of roots and merges its local output indices into the
|
||||
// original CBS status/store namespace. Returns the number of SAT/UNSAT roots.
|
||||
static int Cec_DynSrmTasRetryBatch( Cec_DynSrm_t * p, int nConfs,
|
||||
Vec_Int_t * vRoots, Vec_Int_t * vRootToOrig, Vec_Str_t * vFinalStatus,
|
||||
Vec_Int_t * vTasStore, Vec_Int_t * vTasStarts )
|
||||
{
|
||||
Vec_Str_t * vStatus = NULL;
|
||||
Vec_Int_t * vStore;
|
||||
abctime clk = Abc_ClockHr();
|
||||
int i, iStart = 0, iLocal, iOrig, nLits, Status, nResolved = 0;
|
||||
assert( Vec_IntSize(vRoots) == Vec_IntSize(vRootToOrig) );
|
||||
if ( p->pTas == NULL )
|
||||
p->pTas = Tas_ManAlloc( p->pCore, nConfs );
|
||||
Tas_ManSetConflictNum( p->pTas, nConfs );
|
||||
vStore = Tas_ManSolveRoots( p->pTas, vRoots, &vStatus, 0 );
|
||||
p->tBmcTas += Abc_ClockHr() - clk;
|
||||
Vec_StrForEachEntry( vStatus, Status, i )
|
||||
{
|
||||
iOrig = Vec_IntEntry( vRootToOrig, i );
|
||||
if ( Status != -1 )
|
||||
{
|
||||
Vec_StrWriteEntry( vFinalStatus, iOrig, (char)Status );
|
||||
nResolved++;
|
||||
}
|
||||
}
|
||||
while ( iStart < Vec_IntSize(vStore) )
|
||||
{
|
||||
iLocal = Vec_IntEntry( vStore, iStart );
|
||||
nLits = Vec_IntEntry( vStore, iStart + 1 );
|
||||
assert( iLocal >= 0 && iLocal < Vec_IntSize(vRootToOrig) );
|
||||
iOrig = Vec_IntEntry( vRootToOrig, iLocal );
|
||||
Vec_IntWriteEntry( vTasStarts, iOrig, Vec_IntSize(vTasStore) );
|
||||
Cec_DynSrmStoreCopyEntry( vTasStore, vStore, iStart, iOrig );
|
||||
iStart += 2 + Abc_MaxInt( nLits, 0 );
|
||||
}
|
||||
assert( iStart == Vec_IntSize(vStore) );
|
||||
Vec_IntFree( vStore );
|
||||
Vec_StrFree( vStatus );
|
||||
return nResolved;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis [CBS-first BMC solving with guarded TAS rescue.]
|
||||
|
||||
Description [Forced -T remains TAS-only. The default path solves every
|
||||
root with CBS, then considers only CBS UNKNOWN roots. Large cores are
|
||||
rejected using both absolute and frame-normalized size. Otherwise TAS is
|
||||
sampled on eight roots; only a 75% successful probe enables retrying the
|
||||
remainder. A deterministic node-root work budget and a retry-root cap bound
|
||||
TAS use without consulting machine-dependent wall time. The final status/CEX
|
||||
arrays preserve original root indices.]
|
||||
|
||||
***********************************************************************/
|
||||
Vec_Int_t * Cec_DynSrmSolveBmcAdaptive( Cec_DynSrm_t * p, int nConfs,
|
||||
Vec_Str_t ** pvStatus, int fUseTas )
|
||||
{
|
||||
Vec_Str_t * vStatus = NULL;
|
||||
Vec_Int_t * vCbsStore, * vCbsStarts, * vUnknown;
|
||||
Vec_Int_t * vProbeRoots, * vProbeMap, * vRetryRoots, * vRetryMap;
|
||||
Vec_Int_t * vTasStore, * vTasStarts, * vFinalStore;
|
||||
abctime clk;
|
||||
int i, Status, nRoots = Vec_IntSize(p->vOutLits), nProbe, nProbeResolved;
|
||||
int nFrames = Abc_MaxInt( 1, p->nFramesTotal );
|
||||
int nCore = Gia_ManObjNum( p->pCore );
|
||||
int nCoreNorm = (nCore + nFrames - 1) / nFrames;
|
||||
int fCoreEligible;
|
||||
|
||||
if ( fUseTas )
|
||||
return Cec_DynSrmSolve( p, nConfs, pvStatus, 1 );
|
||||
p->nBmcAdaptiveRounds++;
|
||||
p->nBmcCbsRoots += nRoots;
|
||||
clk = Abc_ClockHr();
|
||||
vCbsStore = Cec_DynSrmSolve( p, nConfs, &vStatus, 0 );
|
||||
p->tBmcCbs += Abc_ClockHr() - clk;
|
||||
vUnknown = Vec_IntAlloc( 64 );
|
||||
Vec_StrForEachEntry( vStatus, Status, i )
|
||||
if ( Status == -1 )
|
||||
Vec_IntPush( vUnknown, i );
|
||||
p->nBmcCbsUnknown += Vec_IntSize(vUnknown);
|
||||
if ( Vec_IntSize(vUnknown) == 0 )
|
||||
{
|
||||
Vec_IntFree( vUnknown );
|
||||
*pvStatus = vStatus;
|
||||
return vCbsStore;
|
||||
}
|
||||
|
||||
fCoreEligible = nCore <= CEC_BMC_TAS_CORE_ABS_MAX &&
|
||||
nCoreNorm <= CEC_BMC_TAS_CORE_NORM_MAX;
|
||||
if ( !fCoreEligible )
|
||||
{
|
||||
p->nBmcTasSkippedLarge += Vec_IntSize(vUnknown);
|
||||
Vec_IntFree( vUnknown );
|
||||
*pvStatus = vStatus;
|
||||
return vCbsStore;
|
||||
}
|
||||
|
||||
vCbsStarts = Cec_DynSrmStoreIndex( vCbsStore, nRoots );
|
||||
vTasStore = Vec_IntAlloc( 64 );
|
||||
vTasStarts = Vec_IntStartFull( nRoots );
|
||||
nProbe = Abc_MinInt( CEC_BMC_TAS_PROBE_ROOTS, Vec_IntSize(vUnknown) );
|
||||
if ( p->nBmcTasStructWork + (ABC_INT64_T)nCoreNorm * nProbe >
|
||||
CEC_BMC_TAS_STRUCT_WORK_MAX )
|
||||
{
|
||||
p->nBmcTasSkippedWork += Vec_IntSize(vUnknown);
|
||||
Vec_IntFree( vCbsStarts );
|
||||
Vec_IntFree( vTasStore );
|
||||
Vec_IntFree( vTasStarts );
|
||||
Vec_IntFree( vUnknown );
|
||||
*pvStatus = vStatus;
|
||||
return vCbsStore;
|
||||
}
|
||||
vProbeRoots = Vec_IntAlloc( nProbe );
|
||||
vProbeMap = Vec_IntAlloc( nProbe );
|
||||
for ( i = 0; i < nProbe; i++ )
|
||||
{
|
||||
int iOrig = Vec_IntEntry( vUnknown, i );
|
||||
Vec_IntPush( vProbeRoots, Vec_IntEntry(p->vOutLits, iOrig) );
|
||||
Vec_IntPush( vProbeMap, iOrig );
|
||||
}
|
||||
p->nBmcTasProbeRoots += nProbe;
|
||||
nProbeResolved = Cec_DynSrmTasRetryBatch( p, nConfs, vProbeRoots, vProbeMap,
|
||||
vStatus, vTasStore, vTasStarts );
|
||||
p->nBmcTasStructWork += (ABC_INT64_T)nCoreNorm * nProbe;
|
||||
p->nBmcTasResolved += nProbeResolved;
|
||||
p->nBmcTasUnknown += nProbe - nProbeResolved;
|
||||
Vec_IntFree( vProbeRoots );
|
||||
Vec_IntFree( vProbeMap );
|
||||
|
||||
if ( nProbeResolved * 100 >= CEC_BMC_TAS_PROBE_SUCCESS_PCT * nProbe &&
|
||||
Vec_IntSize(vUnknown) > nProbe )
|
||||
{
|
||||
int nRetryAvail = Vec_IntSize(vUnknown) - nProbe;
|
||||
int nRetryBudget = CEC_BMC_TAS_RETRY_ROOTS_MAX - (int)p->nBmcTasRetryRoots;
|
||||
ABC_INT64_T nWorkLeft = CEC_BMC_TAS_STRUCT_WORK_MAX - p->nBmcTasStructWork;
|
||||
int nRetryWork = nWorkLeft > 0 ? (int)(nWorkLeft / nCoreNorm) : 0;
|
||||
int nRetry = Abc_MinInt( nRetryAvail,
|
||||
Abc_MinInt( Abc_MaxInt(0, nRetryBudget), Abc_MaxInt(0, nRetryWork) ) );
|
||||
if ( nRetryBudget <= 0 )
|
||||
p->nBmcTasSkippedBudget += nRetryAvail;
|
||||
else if ( nRetryWork <= 0 )
|
||||
p->nBmcTasSkippedWork += nRetryAvail;
|
||||
else
|
||||
{
|
||||
vRetryRoots = Vec_IntAlloc( nRetry );
|
||||
vRetryMap = Vec_IntAlloc( nRetry );
|
||||
for ( i = nProbe; i < nProbe + nRetry; i++ )
|
||||
{
|
||||
int iOrig = Vec_IntEntry( vUnknown, i );
|
||||
Vec_IntPush( vRetryRoots, Vec_IntEntry(p->vOutLits, iOrig) );
|
||||
Vec_IntPush( vRetryMap, iOrig );
|
||||
}
|
||||
p->nBmcTasEnabledRounds++;
|
||||
p->nBmcTasRetryRoots += Vec_IntSize(vRetryRoots);
|
||||
i = Cec_DynSrmTasRetryBatch( p, nConfs, vRetryRoots, vRetryMap,
|
||||
vStatus, vTasStore, vTasStarts );
|
||||
p->nBmcTasResolved += i;
|
||||
p->nBmcTasUnknown += Vec_IntSize(vRetryRoots) - i;
|
||||
p->nBmcTasStructWork += (ABC_INT64_T)nCoreNorm * nRetry;
|
||||
if ( nRetry < nRetryAvail )
|
||||
{
|
||||
if ( nRetry == nRetryBudget )
|
||||
p->nBmcTasSkippedBudget += nRetryAvail - nRetry;
|
||||
else
|
||||
p->nBmcTasSkippedWork += nRetryAvail - nRetry;
|
||||
}
|
||||
Vec_IntFree( vRetryRoots );
|
||||
Vec_IntFree( vRetryMap );
|
||||
}
|
||||
}
|
||||
|
||||
// Rebuild the CEX store once so a TAS answer cleanly replaces the CBS
|
||||
// UNKNOWN entry instead of leaving both records for Gia_ManCheckRefinements.
|
||||
vFinalStore = Vec_IntAlloc( Vec_IntSize(vCbsStore) + Vec_IntSize(vTasStore) );
|
||||
Vec_StrForEachEntry( vStatus, Status, i )
|
||||
{
|
||||
int iStart;
|
||||
if ( Status == 1 )
|
||||
continue;
|
||||
if ( Status == -1 )
|
||||
{
|
||||
Vec_IntPush( vFinalStore, i );
|
||||
Vec_IntPush( vFinalStore, -1 );
|
||||
continue;
|
||||
}
|
||||
iStart = Vec_IntEntry( vCbsStarts, i );
|
||||
if ( iStart >= 0 && Vec_StrEntry(vStatus, i) == 0 &&
|
||||
Vec_IntEntry(vCbsStore, iStart + 1) >= 0 )
|
||||
Cec_DynSrmStoreCopyEntry( vFinalStore, vCbsStore, iStart, i );
|
||||
else
|
||||
{
|
||||
iStart = Vec_IntEntry( vTasStarts, i );
|
||||
assert( iStart >= 0 );
|
||||
Cec_DynSrmStoreCopyEntry( vFinalStore, vTasStore, iStart, i );
|
||||
}
|
||||
}
|
||||
Vec_IntFree( vCbsStore );
|
||||
Vec_IntFree( vCbsStarts );
|
||||
Vec_IntFree( vTasStore );
|
||||
Vec_IntFree( vTasStarts );
|
||||
Vec_IntFree( vUnknown );
|
||||
*pvStatus = vStatus;
|
||||
return vFinalStore;
|
||||
}
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -6,11 +6,11 @@
|
|||
|
||||
PackageName [Combinational equivalence checking.]
|
||||
|
||||
Synopsis [Incremental active-list / TFO filter for &scorr.]
|
||||
Synopsis [Incremental active-list / TFO filter for &scorr2.]
|
||||
|
||||
Author [Xiran Zhao]
|
||||
|
||||
Affiliation [University of Chinese Academy of Sciences]
|
||||
Affiliation [University of Chinese Academy of Sciences (UCAS)]
|
||||
|
||||
Date [Ver. 1.0. Started - May 2026.]
|
||||
|
||||
|
|
@ -477,7 +477,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
|
|||
(Mode == CEC_EMIT_SKIPPED && !fActive);
|
||||
if ( !fEmit )
|
||||
continue;
|
||||
iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorr2SpecReal( pNew, p, pObj, nFrames, 0 );
|
||||
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) );
|
||||
if ( iObjNew != 0 )
|
||||
{
|
||||
|
|
@ -507,8 +507,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
|
|||
(Mode == CEC_EMIT_SKIPPED && !fActive);
|
||||
if ( fEmit )
|
||||
{
|
||||
iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
|
||||
iPrevRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
|
||||
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
|
||||
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
|
||||
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
|
||||
|
|
@ -536,8 +536,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
|
|||
(Mode == CEC_EMIT_SKIPPED && !fActive);
|
||||
if ( fEmit )
|
||||
{
|
||||
iPrevRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
|
||||
iPrevRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorr2SpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
|
||||
iPrevNew = Abc_LitNotCond( iPrevRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
|
||||
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
|
||||
if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
|
||||
|
|
@ -572,8 +572,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr,
|
|||
if ( !fEmit )
|
||||
continue;
|
||||
}
|
||||
iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
|
||||
iPrevRaw = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorr2SpecReal( pNew, p, pRepr, nFrames, 0 );
|
||||
iObjRaw = Gia_ManCorr2SpecReal( pNew, p, pObj, nFrames, 0 );
|
||||
iPrevNew = iPrevRaw;
|
||||
iObjNew = Abc_LitNotCond( iObjRaw, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
|
||||
if ( iPrevNew != iObjNew )
|
||||
|
|
@ -662,8 +662,8 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nP
|
|||
if ( !pTfoMark[i] && !pTfoMark[idR] )
|
||||
continue;
|
||||
}
|
||||
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
|
||||
iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
|
||||
iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorr2SpecReal( pNew, p, pRepr, f, nPrefix );
|
||||
iObjNew = Gia_ManCorr2SpecReal( pNew, p, pObj, f, nPrefix );
|
||||
iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
|
||||
if ( iPrevNew != iObjNew )
|
||||
{
|
||||
|
|
|
|||
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
PackageName [Combinational equivalence checking.]
|
||||
|
||||
Synopsis [Persistent event-driven incremental simulation for &scorr.]
|
||||
Synopsis [Persistent event-driven incremental simulation for &scorr2.]
|
||||
|
||||
Description [Keeps packed CI patterns and host-AIG values across CEX batches.
|
||||
Only changed CI words are propagated through the frame-aware fanout graph.
|
||||
|
|
@ -15,7 +15,7 @@
|
|||
|
||||
Author [Xiran Zhao]
|
||||
|
||||
Affiliation [University of Chinese Academy of Sciences]
|
||||
Affiliation [University of Chinese Academy of Sciences (UCAS)]
|
||||
|
||||
Date [Ver. 1.0. Started - Jun 2026.]
|
||||
|
||||
|
|
@ -389,6 +389,8 @@ void Cec_SeedSimFree( Cec_SeedSim_t * p )
|
|||
ABC_FREE( p->pEventWords );
|
||||
ABC_FREE( p->pCone );
|
||||
ABC_FREE( p->pConeClose );
|
||||
ABC_FREE( p->pReprPre );
|
||||
ABC_FREE( p->pNextPre );
|
||||
ABC_FREE( p->pRootMark );
|
||||
ABC_FREE( p->pTxnMark );
|
||||
ABC_FREE( p->pPackPres );
|
||||
|
|
@ -1327,6 +1329,149 @@ static void Cec_SeedSimBuildPersistentValues( Cec_SeedSim_t * p )
|
|||
}
|
||||
}
|
||||
|
||||
// (-V) Oracle for incremental-resim correctness. The maintained pVal must equal
|
||||
// the true value of every IN-CONE key under the current persistent inputs. We
|
||||
// snapshot the under-test values, recompute the trusted values by a full sweep
|
||||
// from vSimInfo (no class side effects), compare on cone keys, then restore the
|
||||
// under-test values so the run trajectory is unchanged (purely observational).
|
||||
// Out-of-cone keys are intentionally stale and are not checked.
|
||||
int Cec_SeedSimVerifyValues( Cec_SeedSim_t * p )
|
||||
{
|
||||
size_t nKeys, nVals;
|
||||
unsigned * pTest;
|
||||
int Key, w, nBad = 0;
|
||||
if ( p->pVal == NULL )
|
||||
return 0;
|
||||
nKeys = (size_t)p->nFrames * p->nObjs;
|
||||
nVals = nKeys * (size_t)p->nWords;
|
||||
pTest = ABC_ALLOC( unsigned, nVals );
|
||||
memcpy( pTest, p->pVal, sizeof(unsigned) * nVals ); // maintained (under test)
|
||||
Cec_SeedSimBuildPersistentValues( p ); // p->pVal := true values
|
||||
for ( Key = 0; Key < (int)nKeys; Key++ )
|
||||
{
|
||||
if ( p->fUseCone && !Abc_InfoHasBit(p->pCone, Key) )
|
||||
continue;
|
||||
for ( w = 0; w < p->nWords; w++ )
|
||||
{
|
||||
size_t Flat = (size_t)Key * p->nWords + w;
|
||||
if ( pTest[Flat] != p->pVal[Flat] )
|
||||
{
|
||||
if ( nBad < 20 )
|
||||
Abc_Print( 1, " [resim-oracle] STALE key f=%d obj=%d w=%d "
|
||||
"maintained=%08x true=%08x\n",
|
||||
Key / p->nObjs, Key % p->nObjs, w,
|
||||
pTest[Flat], p->pVal[Flat] );
|
||||
nBad++;
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
if ( nBad )
|
||||
Abc_Print( 1, " [resim-oracle] %d in-cone keys STALE "
|
||||
"(maintained != true under persistent inputs)\n", nBad );
|
||||
memcpy( p->pVal, pTest, sizeof(unsigned) * nVals ); // restore: stay observational
|
||||
ABC_FREE( pTest );
|
||||
return nBad;
|
||||
}
|
||||
|
||||
// (-V) Capture the class partition (pReprs/pNexts) before a batch is resimulated.
|
||||
// Cec_SeedSimVerifyRefine() replays the trusted full resim from this snapshot.
|
||||
void Cec_SeedSimVerifySnapshot( Cec_SeedSim_t * p )
|
||||
{
|
||||
int nObjs = p->nObjs;
|
||||
if ( p->pAig->pReprs == NULL || p->pAig->pNexts == NULL )
|
||||
return;
|
||||
if ( p->pReprPre == NULL )
|
||||
{
|
||||
p->pReprPre = ABC_ALLOC( int, nObjs );
|
||||
p->pNextPre = ABC_ALLOC( int, nObjs );
|
||||
}
|
||||
memcpy( p->pReprPre, p->pAig->pReprs, sizeof(int) * nObjs );
|
||||
memcpy( p->pNextPre, p->pAig->pNexts, sizeof(int) * nObjs );
|
||||
}
|
||||
|
||||
static inline int Cec_SeedSimSavedRoot( int * pReprs, int ObjId )
|
||||
{
|
||||
return pReprs[ObjId] == GIA_VOID ? ObjId : pReprs[ObjId];
|
||||
}
|
||||
|
||||
// (-V) Oracle for class refinement (not just the value cache). The incremental
|
||||
// resim has just committed its splits for this batch (P_incr). We re-run the
|
||||
// TRUSTED full resim on the SAME packed CEX inputs starting from the pre-batch
|
||||
// partition (P0), giving the reference partition P_full.
|
||||
//
|
||||
// Both directions matter:
|
||||
// * P_incr merged, P_full split: missed split, a correctness risk.
|
||||
// * P_incr split, P_full merged: extra split, a QoR regression.
|
||||
//
|
||||
// The check reuses the production refinement code (correct phase/const handling),
|
||||
// then restores P_incr so the run stays observational. Returns #mismatches.
|
||||
int Cec_SeedSimVerifyRefine( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
|
||||
Vec_Ptr_t * vSimInfo, int nFrames )
|
||||
{
|
||||
Gia_Man_t * pAig = p->pAig;
|
||||
int nObjs = p->nObjs;
|
||||
int * pReprIncr, * pNextIncr;
|
||||
int i, nMissed = 0, nExtra = 0;
|
||||
if ( pAig->pReprs == NULL || p->pReprPre == NULL )
|
||||
return 0;
|
||||
pReprIncr = ABC_ALLOC( int, nObjs );
|
||||
pNextIncr = ABC_ALLOC( int, nObjs );
|
||||
memcpy( pReprIncr, pAig->pReprs, sizeof(int) * nObjs ); // P_incr (committed)
|
||||
memcpy( pNextIncr, pAig->pNexts, sizeof(int) * nObjs );
|
||||
// restore the pre-batch partition and run the trusted full resim
|
||||
memcpy( pAig->pReprs, p->pReprPre, sizeof(int) * nObjs );
|
||||
memcpy( pAig->pNexts, p->pNextPre, sizeof(int) * nObjs );
|
||||
Gia_ManCreateValueRefs( pAig );
|
||||
pSim->pPars->nFrames = nFrames;
|
||||
Cec_ManSeqResimulate( pSim, vSimInfo ); // pAig now holds P_full
|
||||
// a pair merged in P_incr but split in P_full is a missed (unsound) split
|
||||
for ( i = 1; i < nObjs; i++ )
|
||||
{
|
||||
int rIncr = pReprIncr[i], ci, cr;
|
||||
if ( rIncr == GIA_VOID )
|
||||
continue; // i was a head/none in P_incr
|
||||
ci = Gia_ObjRepr(pAig, i) == GIA_VOID ? i : Gia_ObjRepr(pAig, i);
|
||||
cr = Gia_ObjRepr(pAig, rIncr) == GIA_VOID ? rIncr : Gia_ObjRepr(pAig, rIncr);
|
||||
if ( ci != cr )
|
||||
{
|
||||
if ( nMissed < 20 )
|
||||
Abc_Print( 1, " [resim-oracle] MISSED SPLIT obj=%d repr=%d "
|
||||
"(merged by incremental, split by full resim)\n", i, rIncr );
|
||||
nMissed++;
|
||||
}
|
||||
}
|
||||
// a pair split in P_incr but merged in P_full is an extra split (QoR loss)
|
||||
for ( i = 1; i < nObjs; i++ )
|
||||
{
|
||||
int rFull = Gia_ObjRepr(pAig, i), ci, cr;
|
||||
if ( rFull == GIA_VOID )
|
||||
continue; // i was a head/none in P_full
|
||||
ci = Cec_SeedSimSavedRoot( pReprIncr, i );
|
||||
cr = Cec_SeedSimSavedRoot( pReprIncr, rFull );
|
||||
if ( ci != cr )
|
||||
{
|
||||
if ( nExtra < 20 )
|
||||
Abc_Print( 1, " [resim-oracle] EXTRA SPLIT obj=%d repr=%d "
|
||||
"(split by incremental roots %d/%d, merged by full resim)\n",
|
||||
i, rFull, ci, cr );
|
||||
nExtra++;
|
||||
}
|
||||
}
|
||||
// restore the committed (incremental) partition: stay observational
|
||||
memcpy( pAig->pReprs, pReprIncr, sizeof(int) * nObjs );
|
||||
memcpy( pAig->pNexts, pNextIncr, sizeof(int) * nObjs );
|
||||
ABC_FREE( pReprIncr );
|
||||
ABC_FREE( pNextIncr );
|
||||
if ( nMissed )
|
||||
Abc_Print( 1, " [resim-oracle] %d MISSED SPLITS this batch "
|
||||
"(incremental coarser than full resim)\n", nMissed );
|
||||
if ( nExtra )
|
||||
Abc_Print( 1, " [resim-oracle] %d EXTRA SPLITS this batch "
|
||||
"(incremental finer than full resim; QoR regression)\n", nExtra );
|
||||
return nMissed + nExtra;
|
||||
}
|
||||
|
||||
void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim )
|
||||
{
|
||||
int nInputs = p->nRegs + p->nPis * p->nFrames;
|
||||
|
|
@ -1928,6 +2073,11 @@ int Cec_SeedSimTryBatch( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
|
|||
Cec_SeedSimRecordBatch( p, Vec_IntSize(vOutBits) / 2 );
|
||||
p->nEventInputVarsMax = Abc_MaxInt( p->nEventInputVarsMax, nInputVars );
|
||||
p->nEventInputWordsMax = Abc_MaxInt( p->nEventInputWordsMax, nInputWords );
|
||||
// Up-front density gate. A batch whose changed-CI seed is a large fraction
|
||||
// of all unrolled inputs will dirty a near-full closure, so event
|
||||
// propagation cannot beat a bit-parallel full sweep. Reject it here before
|
||||
// mutating any persistent value, instead of propagating until a mid-flight
|
||||
// budget abort discards the work (and then still falling back to full).
|
||||
if ( (ABC_INT64_T)nInputVars * CEC_EVENT_INPUT_FRAC_DEN >
|
||||
(ABC_INT64_T)nTotalInputs * CEC_EVENT_INPUT_FRAC_NUM )
|
||||
{
|
||||
|
|
@ -1935,6 +2085,17 @@ int Cec_SeedSimTryBatch( Cec_SeedSim_t * p, Cec_ManSim_t * pSim,
|
|||
p->nBatchFull++;
|
||||
return CEC_SEEDSIM_RESULT_FULL_WIDE;
|
||||
}
|
||||
// No class-cone gate. Event propagation below follows the full forward TFO of
|
||||
// this batch's changed CIs (bounded only by the deterministic nNodeLimit /
|
||||
// nEdgeLimit work budget; exceeding it falls back to a full sweep without
|
||||
// committing). This keeps the persistent pVal globally consistent with the
|
||||
// committed inputs, so Cec_SeedSimEventRefine() never reads a stale value and
|
||||
// never misses a split. pSeed->fUseCone stays 0 (reset in
|
||||
// Cec_ManResimulateCounterExamples), so Cec_SeedSimConeHasKey() is always true.
|
||||
// The old per-call active-pair cone was too narrow -> stale values across calls
|
||||
// -> missed splits -> unsound merges; see md/I_resim_soundness_bug.md. The
|
||||
// cone scaffolding (Cec_SeedSimBuildClassCone / pCone / ...) is retained, unused,
|
||||
// for a future adaptive *full-candidate* cone on sparse-candidate designs.
|
||||
(void)vOutputs;
|
||||
Cec_SeedSimReset( p );
|
||||
Vec_IntClear( p->vValueUndo );
|
||||
|
|
@ -2023,7 +2184,8 @@ void Cec_SeedSimBeginCall( Cec_SeedSim_t * p )
|
|||
p->nEventLocal = p->nEventFallback = 0;
|
||||
p->nEventPopsMax = p->nEventEdgesMax = 0;
|
||||
p->nEventInputVarsMax = p->nEventInputWordsMax = 0;
|
||||
p->nEventFallbackWork = 0;
|
||||
p->nEventFallbackWork = p->nEventFallbackTime = 0;
|
||||
p->nAdaptTrips = 0;
|
||||
}
|
||||
|
||||
void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex )
|
||||
|
|
|
|||
|
|
@ -191,7 +191,7 @@ typedef enum Cec_IncrEmitMode_t_
|
|||
CEC_EMIT_SKIPPED
|
||||
} Cec_IncrEmitMode_t;
|
||||
|
||||
// Persistent event-driven simulation manager for &scorr incremental mode.
|
||||
// Persistent event-driven simulation manager for &scorr2 -I.
|
||||
// Packed input patterns and host-AIG values survive across CEX batches. A
|
||||
// batch records only the input words it changes; real value deltas propagate
|
||||
// through the frame-aware fanout graph and dirty classes are fully regrouped.
|
||||
|
|
@ -268,8 +268,14 @@ struct Cec_SeedSim_t_
|
|||
Vec_Int_t * vConeQueue; // newly marked keys used to class-close pCone
|
||||
int * pConeClose; // (frame,root) stamp: class already closed this build
|
||||
int nConeCloseVer; // version for pConeClose
|
||||
int fVerify; // (-V) check maintained values vs full sweep each batch
|
||||
int * pReprPre; // (-V) class-repr snapshot captured before a batch
|
||||
int * pNextPre; // (-V) class-next snapshot captured before a batch
|
||||
int nFallbackStreak; // persists across resimulation calls
|
||||
int nFallbackCooldown; // batches bypassed before next event probe
|
||||
int nAdaptLocal; // decaying window: recent successful event batches
|
||||
int nAdaptFail; // decaying window: recent event batches that fell back
|
||||
int nAdaptTrips; // per-call adaptive cooldown activations
|
||||
// Class-refinement scratch.
|
||||
int * pRootMark; // per-objId "root already queued" stamp
|
||||
int nRootVersion;
|
||||
|
|
@ -288,7 +294,7 @@ struct Cec_SeedSim_t_
|
|||
unsigned * pPhase0; // nWords of 0 (phase-0 vector, used by refine)
|
||||
unsigned * pPhase1; // nWords of ~0 (phase-1 vector)
|
||||
int fOwnsFanout; // 1 if we built static fanout (must free)
|
||||
// Profile counters (reset per resim call)
|
||||
// Per-call work state used by bounded fallback and adaptive control.
|
||||
int nBatchLocal; // rounds handled by local TFO sim
|
||||
int nBatchFull; // rounds that fell back to full sweep
|
||||
int nBatchTrunc; // local rounds that stopped optional TFO expansion
|
||||
|
|
@ -313,10 +319,12 @@ struct Cec_SeedSim_t_
|
|||
int nEventInputVarsMax; // largest changed-CI count in one batch
|
||||
int nEventInputWordsMax; // largest changed-CI-word count in one batch
|
||||
int nEventFallbackWork; // structural word-operation budget exceeded
|
||||
int nEventFallbackTime; // adaptive elapsed-time budget exceeded
|
||||
};
|
||||
|
||||
// Dynamic SRM construction manager for &scorr incremental mode. It keeps the
|
||||
// speculative SRM core used by SAT.
|
||||
// Dynamic SRM construction manager for &scorr2 -D. It keeps the speculative SRM
|
||||
// core used by SAT; counterexample resimulation is selected independently by
|
||||
// -I and otherwise uses the original host-AIG path.
|
||||
typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
|
||||
|
||||
// Recursive diagnosis has a much higher constant factor than a linear sweep.
|
||||
|
|
@ -337,6 +345,15 @@ typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
|
|||
// Consecutive wide cones use bounded exponential backoff. A successful local
|
||||
// batch clears both the streak and cooldown immediately.
|
||||
#define CEC_SEEDSIM_MAX_FALLBACK_BACKOFF 7
|
||||
// Adaptive event-resim circuit breaker. Logs showed good cases are strongly
|
||||
// local-heavy (400k: 161/0, fermat: 451/6) while bad cases are fallback-heavy
|
||||
// (RAV: 122/1335). Use a small decaying window to probe again after cooldown
|
||||
// without repeatedly paying the failed event propagation cost.
|
||||
#define CEC_SEEDSIM_ADAPT_WINDOW 16
|
||||
#define CEC_SEEDSIM_ADAPT_MIN_SAMPLES 8
|
||||
#define CEC_SEEDSIM_ADAPT_FAIL_MUL 2
|
||||
#define CEC_SEEDSIM_ADAPT_FAIL_EXTRA 4
|
||||
#define CEC_SEEDSIM_ADAPT_MAX_COOLDOWN 31
|
||||
#define CEC_EVENT_NODE_WORD_FRAC_NUM 1
|
||||
#define CEC_EVENT_NODE_WORD_FRAC_DEN 10
|
||||
#define CEC_EVENT_EDGE_WORD_FRAC_NUM 1
|
||||
|
|
@ -361,13 +378,13 @@ typedef struct Cec_DynSrm_t_ Cec_DynSrm_t;
|
|||
|
||||
/*=== cecCorr.c ============================================================*/
|
||||
extern void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, abctime Time );
|
||||
extern void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops );
|
||||
extern Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p );
|
||||
extern void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo );
|
||||
extern int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart );
|
||||
extern int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
extern void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
extern Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings );
|
||||
/*=== cecCorr2.c ===========================================================*/
|
||||
extern int Gia_ManCorr2SpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
extern void Gia_ManCorr2SpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
|
||||
extern Gia_Man_t * Gia_ManCorr2SpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, Vec_Int_t ** pvOutLits );
|
||||
extern Gia_Man_t * Cec_ManLSCorrespondence2( Gia_Man_t * pAig, Cec_ParCor_t * pPars );
|
||||
/*=== cecCorrCert.c =========================================================*/
|
||||
extern int Cec_ManCorrKissatCertify( Gia_Man_t * pSrm, Vec_Int_t * vOutputs, Vec_Int_t ** pvCexStore, Vec_Str_t ** pvStatus, int * piOut, int fVerbose );
|
||||
/*=== cecCorrIncr.c ============================================================*/
|
||||
extern Cec_IncrMgr_t * Cec_IncrMgrAlloc( Gia_Man_t * pAig, int nFrames );
|
||||
extern void Cec_IncrMgrFree( Cec_IncrMgr_t * p );
|
||||
|
|
@ -380,16 +397,19 @@ extern void Cec_IncrMgrComputeTfo( Cec_IncrMgr_t * p );
|
|||
extern Gia_Man_t * Gia_ManCorrSpecReduce_Emit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMark, Cec_IncrMgr_t * pIncr, Cec_IncrEmitMode_t Mode, Vec_Int_t ** pvOutLits );
|
||||
extern Gia_Man_t * Gia_ManCorrSpecReduceInit_Active( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMark );
|
||||
/*=== cecCorrDyn.c ============================================================*/
|
||||
extern Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr );
|
||||
extern Cec_DynSrm_t * Cec_DynSrmAlloc( Gia_Man_t * pAig, Cec_IncrMgr_t * pIncr, int fUseAdaptive );
|
||||
extern void Cec_DynSrmSetParams( Cec_DynSrm_t * p, Cec_ParCor_t * pPars );
|
||||
extern void Cec_DynSrmForceRebuild( Cec_DynSrm_t * p, int fIncrFallback );
|
||||
extern void Cec_DynSrmFree( Cec_DynSrm_t * p );
|
||||
extern void Cec_DynSrmPrintStats( Cec_DynSrm_t * p );
|
||||
extern void Cec_DynSrmRecordSolveStats( Cec_DynSrm_t * p, int nCalls, int nReal, int nTriv, int nFail, abctime tSat );
|
||||
extern void Cec_DynSrmCountActivePairs( Cec_DynSrm_t * p, int fRings, int * pTfoMark, int * pnTotal, int * pnActive );
|
||||
extern Gia_Man_t * Cec_DynSrmBuild( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode );
|
||||
extern void Cec_DynSrmBuildCore( Cec_DynSrm_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings, int * pTfoMask, Cec_IncrEmitMode_t Mode );
|
||||
extern Gia_Man_t * Cec_DynSrmBuildInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode );
|
||||
extern void Cec_DynSrmBuildCoreInit( Cec_DynSrm_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int * pTfoMask, Cec_IncrEmitMode_t Mode );
|
||||
extern Vec_Int_t * Cec_DynSrmOutLits( Cec_DynSrm_t * p );
|
||||
extern Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus );
|
||||
extern Vec_Int_t * Cec_DynSrmSolve( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas );
|
||||
extern Vec_Int_t * Cec_DynSrmSolveBmcAdaptive( Cec_DynSrm_t * p, int nConfs, Vec_Str_t ** pvStatus, int fUseTas );
|
||||
/*=== cecCorrIncrSim.c ============================================================*/
|
||||
extern Cec_SeedSim_t * Cec_SeedSimAlloc( Gia_Man_t * pAig, int nFrames, int iSeedFrame, int nWords );
|
||||
extern void Cec_SeedSimFree( Cec_SeedSim_t * p );
|
||||
|
|
@ -401,6 +421,9 @@ extern void Cec_SeedSimBeginCall( Cec_SeedSim_t * p );
|
|||
extern void Cec_SeedSimBypassBatch( Cec_SeedSim_t * p, int nCex );
|
||||
extern void Cec_SeedSimEnsurePersistent( Cec_SeedSim_t * p, Cec_ManSim_t * pSim );
|
||||
extern void Cec_SeedSimBuildClassCone( Cec_SeedSim_t * p, Vec_Int_t * vOutputs );
|
||||
extern int Cec_SeedSimVerifyValues( Cec_SeedSim_t * p );
|
||||
extern void Cec_SeedSimVerifySnapshot( Cec_SeedSim_t * p );
|
||||
extern int Cec_SeedSimVerifyRefine( Cec_SeedSim_t * p, Cec_ManSim_t * pSim, Vec_Ptr_t * vSimInfo, int nFrames );
|
||||
extern int Cec_SeedSimLoadPersistentBatch( Cec_SeedSim_t * p, Vec_Int_t * vCexStore, int iStart, Vec_Int_t * vPairs, Vec_Int_t * vOutBits );
|
||||
extern void Cec_SeedSimRestorePersistentInputs( Cec_SeedSim_t * p );
|
||||
/*=== cecClass.c ============================================================*/
|
||||
|
|
@ -466,4 +489,3 @@ ABC_NAMESPACE_HEADER_END
|
|||
////////////////////////////////////////////////////////////////////////
|
||||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
|
||||
|
|
|
|||
|
|
@ -3,6 +3,8 @@ SRC += src/proof/cec/cecCec.c \
|
|||
src/proof/cec/cecClass.c \
|
||||
src/proof/cec/cecCore.c \
|
||||
src/proof/cec/cecCorr.c \
|
||||
src/proof/cec/cecCorr2.c \
|
||||
src/proof/cec/cecCorrCert.c \
|
||||
src/proof/cec/cecCorrDyn.c \
|
||||
src/proof/cec/cecCorrIncr.c \
|
||||
src/proof/cec/cecCorrIncrSim.c \
|
||||
|
|
|
|||
Loading…
Reference in New Issue