diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 12:11:46 -0400 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-11-01 12:11:46 -0400 |
| commit | 3b8095a6715f8d9befa450d61af5e8567c1f19ac (patch) | |
| tree | 2bc6eda79f5b3d40433bb69db14646d1fcfdf112 /src/aig/gia/giaSweeper.c | |
| parent | 57b51411813a7eab9943cc7b0efa884949156171 (diff) | |
| download | abc-3b8095a6715f8d9befa450d61af5e8567c1f19ac.tar.gz abc-3b8095a6715f8d9befa450d61af5e8567c1f19ac.tar.bz2 abc-3b8095a6715f8d9befa450d61af5e8567c1f19ac.zip | |
Sweeper condition complement bug-fix and code for internal verification.
Diffstat (limited to 'src/aig/gia/giaSweeper.c')
| -rw-r--r-- | src/aig/gia/giaSweeper.c | 25 |
1 files changed, 23 insertions, 2 deletions
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 4cad0bdc..838b9978 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -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) ); @@ -969,6 +969,27 @@ Vec_Int_t * Gia_SweeperGraft( Gia_Man_t * pDst, Vec_Int_t * vProbes, Gia_Man_t * /**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.] Description [Returns the result as a new GIA manager with as many inputs @@ -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 |