From 7ff4c2b2719a78ba7d1ddcfdf9356affa291e876 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 20 Apr 2008 08:01:00 -0700 Subject: Version abc80420 --- src/aig/ntl/ntl.h | 1 + src/aig/ntl/ntlExtract.c | 30 +++++++++++- src/aig/ntl/ntlFraig.c | 122 +++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 151 insertions(+), 2 deletions(-) (limited to 'src/aig/ntl') diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index 4f00cbda..fc9d21bc 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -120,6 +120,7 @@ struct Ntl_Net_t_ { Ntl_Net_t * pNext; // next net in the hash table void * pCopy; // the copy of this object + void * pCopy2; // the copy of this object Ntl_Obj_t * pDriver; // driver of the net char nVisits; // the number of times the net is visited char fMark; // temporary mark diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 18ca1a53..5a681a7e 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -233,7 +233,10 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p ) pRoot = Ntl_ManRootModel( p ); // clear net visited flags Ntl_ModelForEachNet( pRoot, pNet, i ) + { pNet->nVisits = 0; + pNet->pCopy = NULL; + } // collect primary inputs Ntl_ModelForEachPi( pRoot, pObj, i ) { @@ -417,7 +420,10 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) pRoot = Ntl_ManRootModel( p ); // clear net visited flags Ntl_ModelForEachNet( pRoot, pNet, i ) + { pNet->nVisits = 0; + pNet->pCopy = NULL; + } // collect primary inputs Ntl_ModelForEachPi( pRoot, pObj, i ) { @@ -486,9 +492,17 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p ) Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p ) { Aig_Man_t * pAig; + Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; Ntl_Net_t * pNet; int i; + // clear net visited flags + pRoot = Ntl_ManRootModel(p); + Ntl_ModelForEachNet( pRoot, pNet, i ) + { + pNet->nVisits = 0; + pNet->pCopy = NULL; + } // create the manager p->pAig = Aig_ManStart( 10000 ); p->pAig->pName = Aig_UtilStrsav( p->pName ); @@ -557,6 +571,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ) Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) ); ///////////////////////////////////////////////////// + // clear net visited flags + pRoot1 = Ntl_ManRootModel(p1); + Ntl_ModelForEachNet( pRoot1, pNet, i ) + { + pNet->nVisits = 0; + pNet->pCopy = NULL; + } // primary inputs Ntl_ManForEachCiNet( p1, pObj, i ) { @@ -571,7 +592,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ) pNet->nVisits = 2; } // latch outputs - pRoot1 = Ntl_ManRootModel(p1); Ntl_ModelForEachLatch( pRoot1, pObj, i ) { assert( Ntl_ObjFanoutNum(pObj) == 1 ); @@ -614,6 +634,13 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ) } ///////////////////////////////////////////////////// + // clear net visited flags + pRoot2 = Ntl_ManRootModel(p2); + Ntl_ModelForEachNet( pRoot2, pNet, i ) + { + pNet->nVisits = 0; + pNet->pCopy = NULL; + } // primary inputs Ntl_ManForEachCiNet( p2, pObj, i ) { @@ -628,7 +655,6 @@ Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 ) pNet->nVisits = 2; } // latch outputs - pRoot2 = Ntl_ManRootModel(p2); Ntl_ModelForEachLatch( pRoot2, pObj, i ) { assert( Ntl_ObjFanoutNum(pObj) == 1 ); diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index 63725558..86d92b3c 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -369,6 +369,128 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) } + + +/**Function************************************************************* + + Synopsis [Transfers the copy field into the second copy field.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManTransferCopy( Ntl_Man_t * p ) +{ + Ntl_Net_t * pNet; + Ntl_Mod_t * pRoot; + int i; + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachNet( pRoot, pNet, i ) + { + pNet->pCopy2 = pNet->pCopy; + pNet->pCopy = NULL; + } +} + +/**Function************************************************************* + + Synopsis [Reattaches one white-box.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManAttachWhiteBox( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, Ntl_Obj_t * pBox ) +{ +} + +/**Function************************************************************* + + Synopsis [Reattaches white-boxes after reducing the netlist.] + + Description [The following parameters are given: + Original netlist (p) whose nets point to the nodes of collapsed AIG. + Collapsed AIG (pAigCol) whose objects point to those of reduced AIG. + Reduced AIG (pAigRed) whose objects point to the nets of the new netlist. + The new netlist is changed by this procedure to have those white-boxes + from the original AIG (p) those outputs are preserved after reduction. + Note that if outputs are preserved, the inputs are also preserved.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManAttachWhiteBoxes( Ntl_Man_t * p, Aig_Man_t * pAigCol, Aig_Man_t * pAigRed, Ntl_Man_t * pNew, int fVerbose ) +{ + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pBox; + Ntl_Net_t * pNet; + int i, k, Counter = 0; + // go through the white-boxes and check if they are preserved + pRoot = Ntl_ManRootModel( p ); + Ntl_ModelForEachBox( pRoot, pBox, i ) + { + Ntl_ObjForEachFanout( pBox, pNet, k ) + { + // skip dangling outputs of the box + if ( pNet->pCopy == NULL ) + continue; + // skip the outputs that are not preserved after merging equivalence + if ( Aig_Regular(pNet->pCopy2)->pData == NULL ) + continue; + break; + } + if ( k == Ntl_ObjFanoutNum(pBox) ) + continue; + // the box is preserved + Ntl_ManAttachWhiteBox( p, pAigCol, pAigRed, pNew, pBox ); + Counter++; + } + if ( fVerbose ) + printf( "Attached %d boxed (out of %d).\n", Counter, Ntl_ModelBoxNum(pRoot) ); +} + +/**Function************************************************************* + + Synopsis [Returns AIG with WB after sequential SAT sweeping.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars ) +{ + Ntl_Man_t * pNew; + Aig_Man_t * pAigRed, * pAigCol; + // collapse the AIG + pAigCol = Ntl_ManCollapse( p ); + pAigCol->nRegs = Ntl_ModelLatchNum(Ntl_ManRootModel(p)); + // transform the collapsed AIG + pAigRed = Fra_FraigInduction( pAigCol, pPars ); + Aig_ManStop( pAigRed ); + pAigRed = Aig_ManDupReprBasic( pAigCol ); + // insert the result back + Ntl_ManTransferCopy( p ); + pNew = Ntl_ManInsertAig( p, pAigRed ); + // attach the white-boxes + Ntl_ManAttachWhiteBoxes( p, pAigCol, pAigRed, pNew, pPars->fVerbose ); + Ntl_ManSweep( pNew, pPars->fVerbose ); + // cleanup + Aig_ManStop( pAigRed ); + Aig_ManStop( pAigCol ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3