diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-25 11:49:25 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-25 11:49:25 -0700 |
| commit | 94b26fe5a21199ddbd5c564331e7ee2848c8d498 (patch) | |
| tree | 3c59199ce64e9fe8e840e322dd9ddf6b149248e1 /src | |
| parent | b255c7693e0264974128de2b00e1a386fba0b239 (diff) | |
| download | abc-94b26fe5a21199ddbd5c564331e7ee2848c8d498.tar.gz abc-94b26fe5a21199ddbd5c564331e7ee2848c8d498.tar.bz2 abc-94b26fe5a21199ddbd5c564331e7ee2848c8d498.zip | |
Improving CEC (command 'dcec') by integrating XOR balancing.
Diffstat (limited to 'src')
| -rw-r--r-- | src/base/abci/abc.c | 6 | ||||
| -rw-r--r-- | src/proof/fra/fraCec.c | 35 |
2 files changed, 38 insertions, 3 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3279cf46..aeb146e2 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19731,10 +19731,10 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( Abc_NtkLatchNum(pNtk1) || Abc_NtkLatchNum(pNtk2) ) + if ( (pNtk1 && Abc_NtkLatchNum(pNtk1)) || (pNtk2 && Abc_NtkLatchNum(pNtk2)) ) { - if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); - if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); + if ( pNtk1 && fDelete1 ) Abc_NtkDelete( pNtk1 ); + if ( pNtk2 && fDelete2 ) Abc_NtkDelete( pNtk2 ); Abc_Print( -1, "Currently this command only works for networks without latches. Run \"comb\".\n" ); return 1; } diff --git a/src/proof/fra/fraCec.c b/src/proof/fra/fraCec.c index 662a1d9e..aa95b992 100644 --- a/src/proof/fra/fraCec.c +++ b/src/proof/fra/fraCec.c @@ -274,6 +274,28 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi /**Function************************************************************* + Synopsis [Recognizes what nodes are inputs of the EXOR.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCountXors( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj, * pFan0, * pFan1; + int i, Counter = 0; + Aig_ManForEachNode( p, pObj, i ) + if ( Aig_ObjIsMuxType(pObj) && Aig_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + Counter++; + return Counter; + +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -338,6 +360,19 @@ ABC_PRT( "Time", Abc_Clock() - clk ); for ( i = 0; i < 6; i++ ) { //printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter ); + // try XOR balancing + if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 ) + { +clk = Abc_Clock(); + pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 ); + Aig_ManStop( pTemp ); + if ( fVerbose ) + { + printf( "Balance-X: Nodes = %6d. ", Aig_ManNodeNum(pAig) ); +ABC_PRT( "Time", Abc_Clock() - clk ); + } + } + // run fraiging clk = Abc_Clock(); pAig = Fra_FraigPerform( pTemp = pAig, pParams ); |