ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
dchSim.c File Reference
#include "dchInt.h"
Include dependency graph for dchSim.c:

Go to the source code of this file.

Functions

int Dch_NodeIsConstCex (void *p, Aig_Obj_t *pObj)
 FUNCTION DEFINITIONS ///.
 
int Dch_NodesAreEqualCex (void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
unsigned Dch_NodeHash (void *p, Aig_Obj_t *pObj)
 
int Dch_NodeIsConst (void *p, Aig_Obj_t *pObj)
 
int Dch_NodesAreEqual (void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
void Dch_PerformRandomSimulation (Aig_Man_t *pAig, Vec_Ptr_t *vSims)
 
Dch_Cla_t * Dch_CreateCandEquivClasses (Aig_Man_t *pAig, int nWords, int fVerbose)
 

Function Documentation

◆ Dch_CreateCandEquivClasses()

Dch_Cla_t * Dch_CreateCandEquivClasses ( Aig_Man_t * pAig,
int nWords,
int fVerbose )

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

Synopsis [Derives candidate equivalence classes of AIG nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 264 of file dchSim.c.

265{
266 Dch_Cla_t * pClasses;
267 Vec_Ptr_t * vSims;
268 int i;
269 // allocate simulation information
270 vSims = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(pAig), nWords );
271 // run random simulation from the primary inputs
272 Dch_PerformRandomSimulation( pAig, vSims );
273 // start storage for equivalence classes
274 pClasses = Dch_ClassesStart( pAig );
275 Dch_ClassesSetData( pClasses, vSims, Dch_NodeHash, Dch_NodeIsConst, Dch_NodesAreEqual );
276 // hash nodes by sim info
277 Dch_ClassesPrepare( pClasses, 0, 0 );
278 // iterate random simulation
279 for ( i = 0; i < 7; i++ )
280 {
281 Dch_PerformRandomSimulation( pAig, vSims );
282 Dch_ClassesRefine( pClasses );
283 }
284 // clean up and return
285 Vec_PtrFree( vSims );
286 // prepare class refinement procedures
287 Dch_ClassesSetData( pClasses, NULL, NULL, Dch_NodeIsConstCex, Dch_NodesAreEqualCex );
288 return pClasses;
289}
nWords
int nWords
Definition abcNpn.c:127
Dch_ClassesPrepare
void Dch_ClassesPrepare(Dch_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition dchClass.c:336
Dch_ClassesRefine
int Dch_ClassesRefine(Dch_Cla_t *p)
Definition dchClass.c:504
Dch_ClassesSetData
void Dch_ClassesSetData(Dch_Cla_t *p, void *pManData, unsigned(*pFuncNodeHash)(void *, Aig_Obj_t *), int(*pFuncNodeIsConst)(void *, Aig_Obj_t *), int(*pFuncNodesAreEqual)(void *, Aig_Obj_t *, Aig_Obj_t *))
Definition dchClass.c:163
Dch_ClassesStart
Dch_Cla_t * Dch_ClassesStart(Aig_Man_t *pAig)
Definition dchClass.c:137
Dch_Cla_t
typedefABC_NAMESPACE_HEADER_START struct Dch_Cla_t_ Dch_Cla_t
INCLUDES ///.
Definition dchInt.h:47
Dch_NodesAreEqualCex
int Dch_NodesAreEqualCex(void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition dchSim.c:70
Dch_NodeIsConstCex
int Dch_NodeIsConstCex(void *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition dchSim.c:54
Dch_NodesAreEqual
int Dch_NodesAreEqual(void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition dchSim.c:167
Dch_NodeHash
unsigned Dch_NodeHash(void *p, Aig_Obj_t *pObj)
Definition dchSim.c:86
Dch_NodeIsConst
int Dch_NodeIsConst(void *p, Aig_Obj_t *pObj)
Definition dchSim.c:134
Dch_PerformRandomSimulation
void Dch_PerformRandomSimulation(Aig_Man_t *pAig, Vec_Ptr_t *vSims)
Definition dchSim.c:201
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Dch_NodeHash()

unsigned Dch_NodeHash ( void * p,
Aig_Obj_t * pObj )

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file dchSim.c.

87{
88 Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
89 static int s_FPrimes[128] = {
90 1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
91 1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
92 2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
93 2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
94 3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
95 3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
96 4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
97 4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
98 5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
99 6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
100 6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
101 7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
102 8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
103 };
104 unsigned * pSim;
105 unsigned uHash;
106 int k, nWords;
107 nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
108 uHash = 0;
109 pSim = Dch_ObjSim( vSims, pObj );
110 if ( pObj->fPhase )
111 {
112 for ( k = 0; k < nWords; k++ )
113 uHash ^= ~pSim[k] * s_FPrimes[k & 0x7F];
114 }
115 else
116 {
117 for ( k = 0; k < nWords; k++ )
118 uHash ^= pSim[k] * s_FPrimes[k & 0x7F];
119 }
120 return uHash;
121}
p
Cube * p
Definition exorList.c:222
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
Here is the caller graph for this function:

◆ Dch_NodeIsConst()

int Dch_NodeIsConst ( void * p,
Aig_Obj_t * pObj )

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 134 of file dchSim.c.

135{
136 Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
137 unsigned * pSim;
138 int k, nWords;
139 nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
140 pSim = Dch_ObjSim( vSims, pObj );
141 if ( pObj->fPhase )
142 {
143 for ( k = 0; k < nWords; k++ )
144 if ( ~pSim[k] )
145 return 0;
146 }
147 else
148 {
149 for ( k = 0; k < nWords; k++ )
150 if ( pSim[k] )
151 return 0;
152 }
153 return 1;
154}
Here is the caller graph for this function:

◆ Dch_NodeIsConstCex()

int Dch_NodeIsConstCex ( void * p,
Aig_Obj_t * pObj )

FUNCTION DEFINITIONS ///.

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

Synopsis [Returns 1 if the node appears to be constant 1 candidate.]

Description []

SideEffects []

SeeAlso []

Definition at line 54 of file dchSim.c.

55{
56 return pObj->fPhase == pObj->fMarkB;
57}
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Here is the caller graph for this function:

◆ Dch_NodesAreEqual()

int Dch_NodesAreEqual ( void * p,
Aig_Obj_t * pObj0,
Aig_Obj_t * pObj1 )

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file dchSim.c.

168{
169 Vec_Ptr_t * vSims = (Vec_Ptr_t *)p;
170 unsigned * pSim0, * pSim1;
171 int k, nWords;
172 nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
173 pSim0 = Dch_ObjSim( vSims, pObj0 );
174 pSim1 = Dch_ObjSim( vSims, pObj1 );
175 if ( pObj0->fPhase != pObj1->fPhase )
176 {
177 for ( k = 0; k < nWords; k++ )
178 if ( pSim0[k] != ~pSim1[k] )
179 return 0;
180 }
181 else
182 {
183 for ( k = 0; k < nWords; k++ )
184 if ( pSim0[k] != pSim1[k] )
185 return 0;
186 }
187 return 1;
188}
Here is the caller graph for this function:

◆ Dch_NodesAreEqualCex()

int Dch_NodesAreEqualCex ( void * p,
Aig_Obj_t * pObj0,
Aig_Obj_t * pObj1 )

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

Synopsis [Returns 1 if the nodes appear equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file dchSim.c.

71{
72 return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
73}
Here is the caller graph for this function:

◆ Dch_PerformRandomSimulation()

void Dch_PerformRandomSimulation ( Aig_Man_t * pAig,
Vec_Ptr_t * vSims )

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

Synopsis [Perform random simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 201 of file dchSim.c.

202{
203 unsigned * pSim, * pSim0, * pSim1;
204 Aig_Obj_t * pObj;
205 int i, k, nWords;
206 nWords = (unsigned *)Vec_PtrEntry(vSims, 1) - (unsigned *)Vec_PtrEntry(vSims, 0);
207
208 // assign const 1 sim info
209 pObj = Aig_ManConst1(pAig);
210 pSim = Dch_ObjSim( vSims, pObj );
211 memset( pSim, 0xff, sizeof(unsigned) * nWords );
212
213 // assign primary input random sim info
214 Aig_ManForEachCi( pAig, pObj, i )
215 {
216 pSim = Dch_ObjSim( vSims, pObj );
217 for ( k = 0; k < nWords; k++ )
218 pSim[k] = Dch_ObjRandomSim();
219 pSim[0] <<= 1;
220 }
221
222 // simulate AIG in the topological order
223 Aig_ManForEachNode( pAig, pObj, i )
224 {
225 pSim0 = Dch_ObjSim( vSims, Aig_ObjFanin0(pObj) );
226 pSim1 = Dch_ObjSim( vSims, Aig_ObjFanin1(pObj) );
227 pSim = Dch_ObjSim( vSims, pObj );
228
229 if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // both are compls
230 {
231 for ( k = 0; k < nWords; k++ )
232 pSim[k] = ~pSim0[k] & ~pSim1[k];
233 }
234 else if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFaninC1(pObj) ) // first one is compl
235 {
236 for ( k = 0; k < nWords; k++ )
237 pSim[k] = ~pSim0[k] & pSim1[k];
238 }
239 else if ( !Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // second one is compl
240 {
241 for ( k = 0; k < nWords; k++ )
242 pSim[k] = pSim0[k] & ~pSim1[k];
243 }
244 else // if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) ) // none is compl
245 {
246 for ( k = 0; k < nWords; k++ )
247 pSim[k] = pSim0[k] & pSim1[k];
248 }
249 }
250 // get simulation information for primary outputs
251}
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
memset
char * memset()
Here is the call graph for this function:
Here is the caller graph for this function: