ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
mfsStrash.c File Reference
#include "mfsInt.h"
#include "proof/fra/fra.h"
Include dependency graph for mfsStrash.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Abc_MfsConvertAigToHop_rec (Aig_Obj_t *pObj, Hop_Man_t *pHop)
 DECLARATIONS ///.
 
Hop_Obj_tAbc_MfsConvertAigToHop (Aig_Man_t *pMan, Hop_Man_t *pHop)
 
void Abc_MfsConvertHopToAig_rec (Hop_Obj_t *pObj, Aig_Man_t *pMan)
 
void Abc_MfsConvertHopToAig (Abc_Obj_t *pObjOld, Aig_Man_t *pMan)
 
Aig_Obj_tAbc_NtkConstructAig_rec (Mfs_Man_t *p, Abc_Obj_t *pNode, Aig_Man_t *pMan)
 
Aig_Obj_tAbc_NtkConstructCare_rec (Aig_Man_t *pCare, Aig_Obj_t *pObj, Aig_Man_t *pMan)
 
Aig_Man_tAbc_NtkConstructAig (Mfs_Man_t *p, Abc_Obj_t *pNode)
 
Aig_Man_tAbc_NtkAigForConstraints (Mfs_Man_t *p, Abc_Obj_t *pNode)
 
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START double Abc_NtkConstraintRatio (Mfs_Man_t *p, Abc_Obj_t *pNode)
 

Function Documentation

◆ Abc_MfsConvertAigToHop()

Hop_Obj_t * Abc_MfsConvertAigToHop ( Aig_Man_t * pMan,
Hop_Man_t * pHop )

Function*************************************************************

Synopsis [Converts AIG from Aig_Man_t into Hop_Obj_t.]

Description [Assumes that Aig_Man_t has exactly one primary outputs. Returns the pointer to the root node (Hop_Obj_t) in Hop_Man_t.]

SideEffects []

SeeAlso []

Definition at line 67 of file mfsStrash.c.

68{
69 Aig_Obj_t * pRoot, * pObj;
70 int i;
71 assert( Aig_ManCoNum(pMan) == 1 );
72 pRoot = Aig_ManCo( pMan, 0 );
73 // check the case of a constant
74 if ( Aig_ObjIsConst1( Aig_ObjFanin0(pRoot) ) )
75 return Hop_NotCond( Hop_ManConst1(pHop), Aig_ObjFaninC0(pRoot) );
76 // set the PI mapping
77 Aig_ManCleanData( pMan );
78 Aig_ManForEachCi( pMan, pObj, i )
79 pObj->pData = Hop_IthVar( pHop, i );
80 // construct the AIG
81 Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pRoot), pHop );
82 return Hop_NotCond( (Hop_Obj_t *)Aig_ObjFanin0(pRoot)->pData, Aig_ObjFaninC0(pRoot) );
83}
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Hop_Obj_t * Hop_IthVar(Hop_Man_t *p, int i)
FUNCTION DEFINITIONS ///.
Definition hopOper.c:63
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
ABC_NAMESPACE_IMPL_START void Abc_MfsConvertAigToHop_rec(Aig_Obj_t *pObj, Hop_Man_t *pHop)
DECLARATIONS ///.
Definition mfsStrash.c:44
void * pData
Definition aig.h:87
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Abc_MfsConvertAigToHop_rec()

ABC_NAMESPACE_IMPL_START void Abc_MfsConvertAigToHop_rec ( Aig_Obj_t * pObj,
Hop_Man_t * pHop )

DECLARATIONS ///.

CFile****************************************************************

FileName [mfsStrash.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The good old minimization with complete don't-cares.]

Synopsis [Structural hashing of the window with ODCs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
mfsStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Recursively converts AIG from Aig_Man_t into Hop_Obj_t.]

Description []

SideEffects []

SeeAlso []

Definition at line 44 of file mfsStrash.c.

45{
46 assert( !Aig_IsComplement(pObj) );
47 if ( pObj->pData )
48 return;
49 Abc_MfsConvertAigToHop_rec( Aig_ObjFanin0(pObj), pHop );
50 Abc_MfsConvertAigToHop_rec( Aig_ObjFanin1(pObj), pHop );
51 pObj->pData = Hop_And( pHop, (Hop_Obj_t *)Aig_ObjChild0Copy(pObj), (Hop_Obj_t *)Aig_ObjChild1Copy(pObj) );
52 assert( !Hop_IsComplement((Hop_Obj_t *)pObj->pData) );
53}
Hop_Obj_t * Hop_And(Hop_Man_t *p, Hop_Obj_t *p0, Hop_Obj_t *p1)
Definition hopOper.c:104
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_MfsConvertHopToAig()

void Abc_MfsConvertHopToAig ( Abc_Obj_t * pObjOld,
Aig_Man_t * pMan )

Function*************************************************************

Synopsis [Converts the network from AIG to BDD representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file mfsStrash.c.

122{
123 Hop_Man_t * pHopMan;
124 Hop_Obj_t * pRoot;
125 Abc_Obj_t * pFanin;
126 int i;
127 // get the local AIG
128 pHopMan = (Hop_Man_t *)pObjOld->pNtk->pManFunc;
129 pRoot = (Hop_Obj_t *)pObjOld->pData;
130 // check the case of a constant
131 if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
132 {
133 pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) );
134 pObjOld->pNext = pObjOld->pCopy;
135 return;
136 }
137
138 // assign the fanin nodes
139 Abc_ObjForEachFanin( pObjOld, pFanin, i )
140 Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
141 // construct the AIG
142 Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
143 pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
144 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
145
146 // assign the fanin nodes
147 Abc_ObjForEachFanin( pObjOld, pFanin, i )
148 Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
149 // construct the AIG
150 Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
151 pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( (Aig_Obj_t *)Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
152 Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
153}
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
void Hop_ConeUnmark_rec(Hop_Obj_t *pObj)
Definition hopDfs.c:257
typedefABC_NAMESPACE_HEADER_START struct Hop_Man_t_ Hop_Man_t
INCLUDES ///.
Definition hop.h:49
void Abc_MfsConvertHopToAig_rec(Hop_Obj_t *pObj, Aig_Man_t *pMan)
Definition mfsStrash.c:98
void * pManFunc
Definition abc.h:191
void * pData
Definition abc.h:145
Abc_Ntk_t * pNtk
Definition abc.h:130
Abc_Obj_t * pCopy
Definition abc.h:148
Abc_Obj_t * pNext
Definition abc.h:131
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_MfsConvertHopToAig_rec()

void Abc_MfsConvertHopToAig_rec ( Hop_Obj_t * pObj,
Aig_Man_t * pMan )

Function*************************************************************

Synopsis [Construct BDDs and mark AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 98 of file mfsStrash.c.

99{
100 assert( !Hop_IsComplement(pObj) );
101 if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
102 return;
103 Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan );
104 Abc_MfsConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan );
105 pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) );
106 assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
107 Hop_ObjSetMarkA( pObj );
108}
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
void * pData
Definition hop.h:68
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkAigForConstraints()

Aig_Man_t * Abc_NtkAigForConstraints ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Creates AIG for the window with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 325 of file mfsStrash.c.

326{
327 Abc_Obj_t * pFanin;
328 Aig_Man_t * pMan;
329 Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot;
330 Vec_Int_t * vOuts;
331 int i, k, iOut;
332 if ( p->pCare == NULL )
333 return NULL;
334 pMan = Aig_ManStart( 1000 );
335 // mark the care set
336 Aig_ManIncrementTravId( p->pCare );
337 Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
338 {
339 pPi = Aig_ManCi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
340 Aig_ObjSetTravIdCurrent( p->pCare, pPi );
341 pPi->pData = Aig_ObjCreateCi(pMan);
342 }
343 // construct the constraints
344 pObjRoot = Aig_ManConst1(pMan);
345 Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
346 {
347 vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
348 Vec_IntForEachEntry( vOuts, iOut, k )
349 {
350 pPo = Aig_ManCo( p->pCare, iOut );
351 if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
352 continue;
353 Aig_ObjSetTravIdCurrent( p->pCare, pPo );
354 if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
355 continue;
356 pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
357 if ( pObjAig == NULL )
358 continue;
359 pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
360 pObjRoot = Aig_And( pMan, pObjRoot, pObjAig );
361 }
362 }
363 Aig_ObjCreateCo( pMan, pObjRoot );
364 Aig_ManCleanup( pMan );
365 return pMan;
366}
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cube * p
Definition exorList.c:222
Aig_Obj_t * Abc_NtkConstructCare_rec(Aig_Man_t *pCare, Aig_Obj_t *pObj, Aig_Man_t *pMan)
Definition mfsStrash.c:203
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkConstraintRatio()

ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_START double Abc_NtkConstraintRatio ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Compute the ratio of don't-cares.]

Description []

SideEffects []

SeeAlso []

Definition at line 386 of file mfsStrash.c.

387{
388 int nSimWords = 256;
389 Aig_Man_t * pMan;
390 Fra_Sml_t * pSim;
391 int Counter;
392 pMan = Abc_NtkAigForConstraints( p, pNode );
393 pSim = Fra_SmlSimulateComb( pMan, nSimWords, 0 );
394 Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManCo(pMan, 0) );
395 Aig_ManStop( pMan );
396 Fra_SmlStop( pSim );
397 return 1.0 * Counter / (32 * nSimWords);
398}
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
void Fra_SmlStop(Fra_Sml_t *p)
Definition fraSim.c:839
struct Fra_Sml_t_ Fra_Sml_t
Definition fra.h:58
Fra_Sml_t * Fra_SmlSimulateComb(Aig_Man_t *pAig, int nWords, int fCheckMiter)
Definition fraSim.c:856
int Fra_SmlNodeCountOnes(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition fraSim.c:177
Aig_Man_t * Abc_NtkAigForConstraints(Mfs_Man_t *p, Abc_Obj_t *pNode)
Definition mfsStrash.c:325
Here is the call graph for this function:

◆ Abc_NtkConstructAig()

Aig_Man_t * Abc_NtkConstructAig ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Creates AIG for the window with constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file mfsStrash.c.

234{
235 Aig_Man_t * pMan;
236 Abc_Obj_t * pFanin;
237 Aig_Obj_t * pObjAig, * pPi, * pPo;
238 Vec_Int_t * vOuts;
239 int i, k, iOut;
240 // start the new manager
241 pMan = Aig_ManStart( 1000 );
242 // construct the root node's AIG cone
243 pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
244// assert( Aig_ManConst1(pMan) == pObjAig );
245 Aig_ObjCreateCo( pMan, pObjAig );
246 if ( p->pCare )
247 {
248 // mark the care set
249 Aig_ManIncrementTravId( p->pCare );
250 Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
251 {
252 pPi = Aig_ManCi( p->pCare, (int)(ABC_PTRUINT_T)pFanin->pData );
253 Aig_ObjSetTravIdCurrent( p->pCare, pPi );
254 pPi->pData = pFanin->pCopy;
255 }
256 // construct the constraints
257 Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pFanin, i )
258 {
259 vOuts = (Vec_Int_t *)Vec_PtrEntry( p->vSuppsInv, (int)(ABC_PTRUINT_T)pFanin->pData );
260 Vec_IntForEachEntry( vOuts, iOut, k )
261 {
262 pPo = Aig_ManCo( p->pCare, iOut );
263 if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
264 continue;
265 Aig_ObjSetTravIdCurrent( p->pCare, pPo );
266 if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
267 continue;
268 pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
269 if ( pObjAig == NULL )
270 continue;
271 pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
272 Aig_ObjCreateCo( pMan, pObjAig );
273 }
274 }
275/*
276 Aig_ManForEachCo( p->pCare, pPo, i )
277 {
278// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
279 if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
280 continue;
281 pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
282 if ( pObjAig == NULL )
283 continue;
284 pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
285 Aig_ObjCreateCo( pMan, pObjAig );
286 }
287*/
288 }
289 if ( p->pPars->fResub )
290 {
291 // construct the node
292 pObjAig = (Aig_Obj_t *)pNode->pCopy;
293 Aig_ObjCreateCo( pMan, pObjAig );
294 // construct the divisors
295 Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs, pFanin, i )
296 {
297 pObjAig = (Aig_Obj_t *)pFanin->pCopy;
298 Aig_ObjCreateCo( pMan, pObjAig );
299 }
300 }
301 else
302 {
303 // construct the fanins
304 Abc_ObjForEachFanin( pNode, pFanin, i )
305 {
306 pObjAig = (Aig_Obj_t *)pFanin->pCopy;
307 Aig_ObjCreateCo( pMan, pObjAig );
308 }
309 }
310 Aig_ManCleanup( pMan );
311 return pMan;
312}
Aig_Obj_t * Abc_NtkConstructAig_rec(Mfs_Man_t *p, Abc_Obj_t *pNode, Aig_Man_t *pMan)
Definition mfsStrash.c:166
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkConstructAig_rec()

Aig_Obj_t * Abc_NtkConstructAig_rec ( Mfs_Man_t * p,
Abc_Obj_t * pNode,
Aig_Man_t * pMan )

Function*************************************************************

Synopsis [Computes the care set of the node under ODCs.]

Description []

SideEffects []

SeeAlso []

Definition at line 166 of file mfsStrash.c.

167{
168 Aig_Obj_t * pRoot, * pExor;
169 Abc_Obj_t * pObj;
170 int i;
171 // assign AIG nodes to the leaves
172 Vec_PtrForEachEntry( Abc_Obj_t *, p->vSupp, pObj, i )
173 pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreateCi( pMan );
174 // strash intermediate nodes
175 Abc_NtkIncrementTravId( pNode->pNtk );
176 Vec_PtrForEachEntry( Abc_Obj_t *, p->vNodes, pObj, i )
177 {
178 Abc_MfsConvertHopToAig( pObj, pMan );
179 if ( pObj == pNode )
180 pObj->pNext = Abc_ObjNot(pObj->pNext);
181 }
182 // create the observability condition
183 pRoot = Aig_ManConst0(pMan);
184 Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
185 {
186 pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
187 pRoot = Aig_Or( pMan, pRoot, pExor );
188 }
189 return pRoot;
190}
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
void Abc_MfsConvertHopToAig(Abc_Obj_t *pObjOld, Aig_Man_t *pMan)
Definition mfsStrash.c:121
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkConstructCare_rec()

Aig_Obj_t * Abc_NtkConstructCare_rec ( Aig_Man_t * pCare,
Aig_Obj_t * pObj,
Aig_Man_t * pMan )

Function*************************************************************

Synopsis [Adds relevant constraints.]

Description []

SideEffects []

SeeAlso []

Definition at line 203 of file mfsStrash.c.

204{
205 Aig_Obj_t * pObj0, * pObj1;
206 if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
207 return (Aig_Obj_t *)pObj->pData;
208 Aig_ObjSetTravIdCurrent( pCare, pObj );
209 if ( Aig_ObjIsCi(pObj) )
210 return (Aig_Obj_t *)(pObj->pData = NULL);
211 pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
212 if ( pObj0 == NULL )
213 return (Aig_Obj_t *)(pObj->pData = NULL);
214 pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
215 if ( pObj1 == NULL )
216 return (Aig_Obj_t *)(pObj->pData = NULL);
217 pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
218 pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
219 return (Aig_Obj_t *)(pObj->pData = Aig_And( pMan, pObj0, pObj1 ));
220}
Here is the call graph for this function:
Here is the caller graph for this function: