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

Sweeper condition complement bug-fix and code for internal verification.

This commit is contained in:
Alan Mishchenko 2013-11-01 12:11:46 -04:00
parent 57b5141181
commit 3b8095a671
8 changed files with 60 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/aig/gia/gia.h
View File

@ -1007,7 +1007,8 @@ extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 )
extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits );
extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fVerbose );
extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose );
extern Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl );
extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose );
extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p );

30
src/aig/gia/giaDup.c
View File

@ -1880,7 +1880,7 @@ int Gia_ManMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fVerbose )
Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
@ -1951,7 +1951,12 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
}
else
else if ( fImplic )
{
iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
Gia_ManAppendCo( pNew, iLit );
}
else
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManPo(p1,i)) );
Gia_ManAppendCo( pNew, iLit );
@ -1990,6 +1995,11 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
}
else if ( fImplic )
{
iLit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Abc_LitNot(Gia_ObjFanin0Copy(Gia_ManPo(p1,i))) );
Gia_ManAppendCo( pNew, iLit );
}
else
{
iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(p1,i)) );
@ -2006,6 +2016,22 @@ Gia_Man_t * Gia_ManMiter( Gia_Man_t * p0, Gia_Man_t * p1, int nInsDup, int fDual
return pNew;
}
/**Function*************************************************************
Synopsis [Computes the AND of all POs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupAnd( Gia_Man_t * p, int fCompl )
{
return NULL;
}
/**Function*************************************************************
Synopsis [Transforms the circuit into a regular miter.]

4
src/aig/gia/giaEquiv.c
View File

@ -1882,7 +1882,7 @@ int Gia_ManFilterEquivsForSpeculation( Gia_Man_t * pGia, char * pName1, char * p
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );
@ -2021,7 +2021,7 @@ int Gia_ManFilterEquivsUsingParts( Gia_Man_t * pGia, char * pName1, char * pName
Abc_Print( 1, "Cannot read second file %s.\n", pName2 );
return 0;
}
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0 );
pMiter = Gia_ManMiter( pGia1, pGia2, 0, 0, 1, 0, 0 );
if ( pMiter == NULL )
{
Gia_ManStop( pGia1 );

25
src/aig/gia/giaSweeper.c
View File

@ -784,7 +784,7 @@ int Gia_SweeperCheckEquiv( Gia_Man_t * pGia, int Probe1, int Probe2 )
{
iLitAig = Gia_SweeperProbeLit( pGia, ProbeId );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitAig) );
Vec_IntPush( p->vCondAssump, Swp_ManLit2Lit(p, iLitAig) );
Vec_IntPush( p->vCondAssump, Abc_LitNot(Swp_ManLit2Lit(p, iLitAig)) );
}
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitOld) );
Gia_ManCnfNodeAddToSolver( p, Abc_Lit2Var(iLitNew) );
@ -967,6 +967,27 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t *
return vOutLits;
}
/**Function*************************************************************
Synopsis [Verification of the sweeper.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_SweeperVerify( Gia_Man_t * p0, Gia_Man_t * p1, Gia_Man_t * pC )
{
Gia_Man_t * pMiter = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
Gia_Man_t * pConstr = Gia_ManDupAnd( pC, 0 );
Gia_ManStop( pConstr );
Gia_ManStop( pMiter );
return 1;
}
/**Function*************************************************************
Synopsis [Performs conditional sweeping of the cone.]
@ -995,7 +1016,7 @@ Gia_Man_t * Gia_SweeperSweep( Gia_Man_t * p, Vec_Int_t * vProbeOuts, int nWords,
pGiaCond = Gia_SweeperExtractUserLogic( p, vProbeConds, NULL, NULL );
pGiaOuts = Gia_SweeperExtractUserLogic( p, vProbeOuts, NULL, NULL );
Gia_ManSetPhase( pGiaOuts );
// if there is no conditions, define constant true constrain (constant 0 output)
// if there is no conditions, define constant true constraint (constant 0 output)
if ( Gia_ManPoNum(pGiaCond) == 0 )
Gia_ManAppendCo( pGiaCond, Gia_ManConst0Lit() );
// perform sweeping under constraints

2
src/aig/gia/giaTim.c
View File

@ -554,7 +554,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit )
pGia1 = Gia_ManDupCollapse( pGia, pGia->pAigExtra, NULL );
Vec_IntFreeP( &vBoxPres );
// compute the miter
pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, fVerbose );
pMiter = Gia_ManMiter( pGia0, pGia1, 0, 1, 0, 0, fVerbose );
if ( pMiter )
{
Cec_ParCec_t ParsCec, * pPars = &ParsCec;

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

@ -27966,7 +27966,7 @@ int Abc_CommandAbc9Miter( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, fVerbose );
pAux = Gia_ManMiter( pAbc->pGia, pSecond, nInsDup, fDualOut, fSeq, 0, fVerbose );
Gia_ManStop( pSecond );
Abc_FrameUpdateGia( pAbc, pAux );
return 0;
@ -29352,7 +29352,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// compute the miter
pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, pPars->fVerbose );
pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, 0, pPars->fVerbose );
if ( pMiter )
{
if ( fDumpMiter )

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

@ -301,7 +301,7 @@ int Cec_ManVerifyTwo( Gia_Man_t * p0, Gia_Man_t * p1, int fVerbose )
int RetValue;
Cec_ManCecSetDefaultParams( pPars );
pPars->fVerbose = fVerbose;
pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, pPars->fVerbose );
pMiter = Gia_ManMiter( p0, p1, 0, 1, 0, 0, pPars->fVerbose );
if ( pMiter == NULL )
return -1;
RetValue = Cec_ManVerify( pMiter, pPars );

2
src/sat/bmc/bmcICheck.c
View File

@ -206,7 +206,7 @@ void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty,
// create miter
pTemp = Gia_ManDup( p );
pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0 );
pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
Gia_ManStop( pTemp );
assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );