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

Bug fixes in &cec command.

This commit is contained in:
Alan Mishchenko 2012-02-10 00:07:31 -08:00
parent b186f362a7
commit 71891354b4
2 changed files with 87 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -24980,7 +24980,8 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
Cec_ManVerify( pAbc->pGia, pPars );
pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
return 0;
}
@ -25017,7 +25018,8 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 1, 0, pPars->fVerbose );
if ( pMiter )
{
Cec_ManVerify( pMiter, pPars );
pAbc->Status = Cec_ManVerify( pMiter, pPars );
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Gia_ManStop( pMiter );
}
Gia_ManStop( pSecond );

112
src/proof/cec/cecCec.c
View File

@ -48,13 +48,10 @@ void Cec_ManTransformPattern( Gia_Man_t * p, int iOut, int * pValues )
{
int i;
assert( p->pCexComb == NULL );
p->pCexComb = (Abc_Cex_t *)ABC_CALLOC( char,
sizeof(Abc_Cex_t) + sizeof(unsigned) * Abc_BitWordNum(Gia_ManCiNum(p)) );
p->pCexComb = Abc_CexAlloc( 0, Gia_ManCiNum(p), 1 );
p->pCexComb->iPo = iOut;
p->pCexComb->nPis = Gia_ManCiNum(p);
p->pCexComb->nBits = Gia_ManCiNum(p);
for ( i = 0; i < Gia_ManCiNum(p); i++ )
if ( pValues[i] )
if ( pValues && pValues[i] )
Abc_InfoSetBit( p->pCexComb->pData, i );
}
@ -122,6 +119,77 @@ Abc_PrintTime( 1, "Time", clock() - clkTotal );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
{
Gia_Obj_t * pObj1, * pObj2;
Gia_Obj_t * pDri1, * pDri2;
int i, clk = clock();
Gia_ManSetPhase( p );
Gia_ManForEachPo( p, pObj1, i )
{
pObj2 = Gia_ManPo( p, ++i );
// check if they different on all-0 pattern
// (for example, when they have the same driver but complemented)
if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 );
Abc_PrintTime( 1, "Time", clock() - clk );
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
return 0;
}
// get the drivers
pDri1 = Gia_ObjFanin0(pObj1);
pDri2 = Gia_ObjFanin0(pObj2);
// drivers are different PIs
if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 );
Abc_PrintTime( 1, "Time", clock() - clk );
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
// if their compl attributes are the same - one should be complemented
assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) );
Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) );
return 0;
}
// one of the drivers is a PI; another is a constant 0
if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) ||
(Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 );
Abc_PrintTime( 1, "Time", clock() - clk );
pPars->iOutFail = i/2;
Cec_ManTransformPattern( p, i/2, NULL );
// the compl attributes are the same - the PI should be complemented
assert( Gia_ObjFaninC0(pObj1) == Gia_ObjFaninC0(pObj2) );
if ( Gia_ObjIsPi(p, pDri1) )
Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri1) );
else
Abc_InfoSetBit( p->pCexComb->pData, Gia_ObjCioId(pDri2) );
return 0;
}
}
if ( Gia_ManAndNum(p) == 0 )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", clock() - clk );
return 1;
}
return -1;
}
/**Function*************************************************************
Synopsis [New CEC engine.]
@ -140,6 +208,13 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_Man_t * p, * pNew;
int RetValue, clk = clock();
double clkTotal = clock();
// consider special cases:
// 1) (SAT) a pair of POs have different value under all-0 pattern
// 2) (SAT) a pair of POs has different PI/Const drivers
// 3) (UNSAT) 1-2 do not hold and there is no nodes
RetValue = Cec_ManHandleSpecialCases( pInit, pPars );
if ( RetValue == 0 || RetValue == 1 )
return RetValue;
// preprocess
p = Gia_ManDup( pInit );
Gia_ManEquivFixOutputPairs( p );
@ -176,31 +251,10 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
Gia_ManStop( pNew );
pNew = p;
}
if ( Gia_ManAndNum(pNew) == 0 )
{
Gia_Obj_t * pObj1, * pObj2;
int i;
Gia_ManForEachPo( pNew, pObj1, i )
{
pObj2 = Gia_ManPo( pNew, ++i );
if ( Gia_ObjChild0(pObj1) != Gia_ObjChild0(pObj2) )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ. ", i/2 );
Abc_PrintTime( 1, "Time", clock() - clk );
Gia_ManStop( pNew );
pPars->iOutFail = i/2;
return 0;
}
}
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", clock() - clk );
Gia_ManStop( pNew );
return 1;
}
if ( pPars->fVerbose )
{
Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " );
Abc_PrintTime( 1, "Time", clock() - clk );
Abc_Print( 1, "Networks are UNDECIDED after the new CEC engine. " );
Abc_PrintTime( 1, "Time", clock() - clk );
}
if ( fDumpUndecided )
{
@ -216,7 +270,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
}
// call other solver
if ( pPars->fVerbose )
Abc_Print( 1, "Calling the old CEC engine.\n" );
Abc_Print( 1, "Calling the old CEC engine.\n" );
fflush( stdout );
RetValue = Cec_ManVerifyOld( pNew, pPars->fVerbose, &pPars->iOutFail );
p->pCexComb = pNew->pCexComb; pNew->pCexComb = NULL;