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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Ssw_CreatePair (Vec_Int_t *vPairs, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 DECLARATIONS ///.
 
void Ssw_MatchingStart (Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs)
 
void Ssw_MatchingExtendOne (Aig_Man_t *p, Vec_Ptr_t *vNodes)
 
int Ssw_MatchingCountUnmached (Aig_Man_t *p)
 
void Ssw_MatchingExtend (Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose)
 
void Ssw_MatchingComplete (Aig_Man_t *p0, Aig_Man_t *p1)
 
Vec_Int_t * Ssw_MatchingPairs (Aig_Man_t *p0, Aig_Man_t *p1)
 
Vec_Int_t * Ssw_MatchingMiter (Aig_Man_t *pMiter, Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairsAll)
 
Aig_Man_t * Ssw_SecWithSimilaritySweep (Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
 
int Ssw_SecWithSimilarityPairs (Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
 
Vec_Int_t * Saig_StrSimPerformMatching_hack (Aig_Man_t *p0, Aig_Man_t *p1)
 
int Ssw_SecWithSimilarity (Aig_Man_t *p0, Aig_Man_t *p1, Ssw_Pars_t *pPars)
 

Function Documentation

◆ Saig_StrSimPerformMatching_hack()

Vec_Int_t * Saig_StrSimPerformMatching_hack ( Aig_Man_t * p0,
Aig_Man_t * p1 )

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

Synopsis [Dummy procedure to detect structural similarity.]

Description []

SideEffects []

SeeAlso []

Definition at line 514 of file sswIslands.c.

515{
516 Vec_Int_t * vPairs;
517 Aig_Obj_t * pObj;
518 int i;
519 // create array of pairs
520 vPairs = Vec_IntAlloc( 100 );
521 Aig_ManForEachObj( p0, pObj, i )
522 {
523 if ( !Aig_ObjIsConst1(pObj) && !Aig_ObjIsCi(pObj) && !Aig_ObjIsNode(pObj) )
524 continue;
525 Vec_IntPush( vPairs, i );
526 Vec_IntPush( vPairs, i );
527 }
528 return vPairs;
529}
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition aig.h:403
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37

◆ Ssw_CreatePair()

ABC_NAMESPACE_IMPL_START void Ssw_CreatePair ( Vec_Int_t * vPairs,
Aig_Obj_t * pObj0,
Aig_Obj_t * pObj1 )

DECLARATIONS ///.

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

FileName [sswIslands.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Inductive prover with constraints.]

Synopsis [Detection of islands of difference.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - September 1, 2008.]

Revision [

Id
sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp

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

Synopsis [Creates pair of structurally equivalent nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sswIslands.c.

46{
47 pObj0->pData = pObj1;
48 pObj1->pData = pObj0;
49 Vec_IntPush( vPairs, pObj0->Id );
50 Vec_IntPush( vPairs, pObj1->Id );
51}
Aig_Obj_t_::Id
int Id
Definition aig.h:85
Aig_Obj_t_::pData
void * pData
Definition aig.h:87

◆ Ssw_MatchingComplete()

void Ssw_MatchingComplete ( Aig_Man_t * p0,
Aig_Man_t * p1 )

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

Synopsis [Used differences in p0 to complete p1.]

Description []

SideEffects []

SeeAlso []

Definition at line 287 of file sswIslands.c.

288{
289 Vec_Ptr_t * vNewLis;
290 Aig_Obj_t * pObj0, * pObj0Li, * pObj1;
291 int i;
292 // create register outputs in p0 that are absent in p1
293 vNewLis = Vec_PtrAlloc( 100 );
294 Saig_ManForEachLiLo( p0, pObj0Li, pObj0, i )
295 {
296 if ( pObj0->pData != NULL )
297 continue;
298 pObj1 = Aig_ObjCreateCi( p1 );
299 pObj0->pData = pObj1;
300 pObj1->pData = pObj0;
301 Vec_PtrPush( vNewLis, pObj0Li );
302 }
303 // add missing nodes in the topological order
304 Aig_ManForEachNode( p0, pObj0, i )
305 {
306 if ( pObj0->pData != NULL )
307 continue;
308 pObj1 = Aig_And( p1, Aig_ObjChild0Copy(pObj0), Aig_ObjChild1Copy(pObj0) );
309 pObj0->pData = pObj1;
310 pObj1->pData = pObj0;
311 }
312 // create register outputs in p0 that are absent in p1
313 Vec_PtrForEachEntry( Aig_Obj_t *, vNewLis, pObj0Li, i )
314 Aig_ObjCreateCo( p1, Aig_ObjChild0Copy(pObj0Li) );
315 // increment the number of registers
316 Aig_ManSetRegNum( p1, Aig_ManRegNum(p1) + Vec_PtrSize(vNewLis) );
317 Vec_PtrFree( vNewLis );
318}
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#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:

◆ Ssw_MatchingCountUnmached()

int Ssw_MatchingCountUnmached ( Aig_Man_t * p)

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

Synopsis [Establishes relationship between nodes using pairing.]

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file sswIslands.c.

194{
195 Aig_Obj_t * pObj;
196 int i, Counter = 0;
197 Aig_ManForEachObj( p, pObj, i )
198 {
199 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
200 continue;
201 if ( pObj->pData != NULL )
202 continue;
203 Counter++;
204 }
205 return Counter;
206}
p
Cube * p
Definition exorList.c:222
Here is the caller graph for this function:

◆ Ssw_MatchingExtend()

void Ssw_MatchingExtend ( Aig_Man_t * p0,
Aig_Man_t * p1,
int nDist,
int fVerbose )

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

Synopsis [Establishes relationship between nodes using pairing.]

Description []

SideEffects []

SeeAlso []

Definition at line 219 of file sswIslands.c.

220{
221 Vec_Ptr_t * vNodes0, * vNodes1;
222 Aig_Obj_t * pNext0, * pNext1;
223 int d, k;
224 Aig_ManFanoutStart(p0);
225 Aig_ManFanoutStart(p1);
226 vNodes0 = Vec_PtrAlloc( 1000 );
227 vNodes1 = Vec_PtrAlloc( 1000 );
228 if ( fVerbose )
229 {
230 int nUnmached = Ssw_MatchingCountUnmached(p0);
231 Abc_Print( 1, "Extending islands by %d steps:\n", nDist );
232 Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
233 0, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
234 nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
235 }
236 for ( d = 0; d < nDist; d++ )
237 {
238 Ssw_MatchingExtendOne( p0, vNodes0 );
239 Ssw_MatchingExtendOne( p1, vNodes1 );
240 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes0, pNext0, k )
241 {
242 pNext1 = (Aig_Obj_t *)pNext0->pData;
243 if ( pNext1 == NULL )
244 continue;
245 assert( pNext1->pData == pNext0 );
246 if ( Saig_ObjIsPi(p0, pNext1) )
247 continue;
248 pNext0->pData = NULL;
249 pNext1->pData = NULL;
250 }
251 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes1, pNext0, k )
252 {
253 pNext1 = (Aig_Obj_t *)pNext0->pData;
254 if ( pNext1 == NULL )
255 continue;
256 assert( pNext1->pData == pNext0 );
257 if ( Saig_ObjIsPi(p1, pNext1) )
258 continue;
259 pNext0->pData = NULL;
260 pNext1->pData = NULL;
261 }
262 if ( fVerbose )
263 {
264 int nUnmached = Ssw_MatchingCountUnmached(p0);
265 Abc_Print( 1, "%2d : Total = %6d. Unmatched = %6d. Ratio = %6.2f %%\n",
266 d+1, Aig_ManCiNum(p0) + Aig_ManNodeNum(p0),
267 nUnmached, 100.0 * nUnmached/(Aig_ManCiNum(p0) + Aig_ManNodeNum(p0)) );
268 }
269 }
270 Vec_PtrFree( vNodes0 );
271 Vec_PtrFree( vNodes1 );
272 Aig_ManFanoutStop(p0);
273 Aig_ManFanoutStop(p1);
274}
Aig_ManFanoutStart
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition aigFanout.c:56
Aig_ManFanoutStop
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition aigFanout.c:89
Ssw_MatchingCountUnmached
int Ssw_MatchingCountUnmached(Aig_Man_t *p)
Definition sswIslands.c:193
Ssw_MatchingExtendOne
void Ssw_MatchingExtendOne(Aig_Man_t *p, Vec_Ptr_t *vNodes)
Definition sswIslands.c:130
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_MatchingExtendOne()

void Ssw_MatchingExtendOne ( Aig_Man_t * p,
Vec_Ptr_t * vNodes )

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

Synopsis [Establishes relationship between nodes using pairing.]

Description []

SideEffects []

SeeAlso []

Definition at line 130 of file sswIslands.c.

131{
132 Aig_Obj_t * pNext, * pObj;
133 int i, k, iFan = -1;
134 Vec_PtrClear( vNodes );
135 Aig_ManIncrementTravId( p );
136 Aig_ManForEachObj( p, pObj, i )
137 {
138 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
139 continue;
140 if ( pObj->pData != NULL )
141 continue;
142 if ( Saig_ObjIsLo(p, pObj) )
143 {
144 pNext = Saig_ObjLoToLi(p, pObj);
145 pNext = Aig_ObjFanin0(pNext);
146 if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) && !Aig_ObjIsConst1(pNext) )
147 {
148 Aig_ObjSetTravIdCurrent(p, pNext);
149 Vec_PtrPush( vNodes, pNext );
150 }
151 }
152 if ( Aig_ObjIsNode(pObj) )
153 {
154 pNext = Aig_ObjFanin0(pObj);
155 if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
156 {
157 Aig_ObjSetTravIdCurrent(p, pNext);
158 Vec_PtrPush( vNodes, pNext );
159 }
160 pNext = Aig_ObjFanin1(pObj);
161 if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
162 {
163 Aig_ObjSetTravIdCurrent(p, pNext);
164 Vec_PtrPush( vNodes, pNext );
165 }
166 }
167 Aig_ObjForEachFanout( p, pObj, pNext, iFan, k )
168 {
169 if ( Saig_ObjIsPo(p, pNext) )
170 continue;
171 if ( Saig_ObjIsLi(p, pNext) )
172 pNext = Saig_ObjLiToLo(p, pNext);
173 if ( pNext->pData && !Aig_ObjIsTravIdCurrent(p, pNext) )
174 {
175 Aig_ObjSetTravIdCurrent(p, pNext);
176 Vec_PtrPush( vNodes, pNext );
177 }
178 }
179 }
180}
Aig_ObjForEachFanout
#define Aig_ObjForEachFanout(p, pObj, pFanout, iFan, i)
Definition aig.h:427
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_MatchingMiter()

Vec_Int_t * Ssw_MatchingMiter ( Aig_Man_t * pMiter,
Aig_Man_t * p0,
Aig_Man_t * p1,
Vec_Int_t * vPairsAll )

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

Synopsis [Transfers the result of matching to miter.]

Description [The array of pairs should be complete.]

SideEffects []

SeeAlso []

Definition at line 370 of file sswIslands.c.

371{
372 Vec_Int_t * vPairsMiter;
373 Aig_Obj_t * pObj0, * pObj1;
374 int i;
375 // create matching of nodes in the miter
376 vPairsMiter = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
377 for ( i = 0; i < Vec_IntSize(vPairsAll); i += 2 )
378 {
379 pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairsAll, i) );
380 pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairsAll, i+1) );
381 assert( pObj0->pData != NULL );
382 assert( pObj1->pData != NULL );
383 if ( pObj0->pData == pObj1->pData )
384 continue;
385 if ( Aig_ObjIsNone((Aig_Obj_t *)pObj0->pData) || Aig_ObjIsNone((Aig_Obj_t *)pObj1->pData) )
386 continue;
387 // get the miter nodes
388 pObj0 = (Aig_Obj_t *)pObj0->pData;
389 pObj1 = (Aig_Obj_t *)pObj1->pData;
390 assert( !Aig_IsComplement(pObj0) );
391 assert( !Aig_IsComplement(pObj1) );
392 assert( Aig_ObjType(pObj0) == Aig_ObjType(pObj1) );
393 if ( Aig_ObjIsCo(pObj0) )
394 continue;
395 assert( Aig_ObjIsNode(pObj0) || Saig_ObjIsLo(pMiter, pObj0) );
396 assert( Aig_ObjIsNode(pObj1) || Saig_ObjIsLo(pMiter, pObj1) );
397 assert( pObj0->Id < pObj1->Id );
398 Vec_IntPush( vPairsMiter, pObj0->Id );
399 Vec_IntPush( vPairsMiter, pObj1->Id );
400 }
401 return vPairsMiter;
402}
Here is the caller graph for this function:

◆ Ssw_MatchingPairs()

Vec_Int_t * Ssw_MatchingPairs ( Aig_Man_t * p0,
Aig_Man_t * p1 )

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

Synopsis [Derives matching for all pairs.]

Description [Modifies both AIGs.]

SideEffects []

SeeAlso []

Definition at line 332 of file sswIslands.c.

333{
334 Vec_Int_t * vPairsNew;
335 Aig_Obj_t * pObj0, * pObj1;
336 int i;
337 // check correctness
338 assert( Aig_ManCiNum(p0) == Aig_ManCiNum(p1) );
339 assert( Aig_ManCoNum(p0) == Aig_ManCoNum(p1) );
340 assert( Aig_ManRegNum(p0) == Aig_ManRegNum(p1) );
341 assert( Aig_ManObjNum(p0) == Aig_ManObjNum(p1) );
342 // create complete pairs
343 vPairsNew = Vec_IntAlloc( 2*Aig_ManObjNum(p0) );
344 Aig_ManForEachObj( p0, pObj0, i )
345 {
346 if ( Aig_ObjIsCo(pObj0) )
347 continue;
348 pObj1 = (Aig_Obj_t *)pObj0->pData;
349 Vec_IntPush( vPairsNew, pObj0->Id );
350 Vec_IntPush( vPairsNew, pObj1->Id );
351 }
352 return vPairsNew;
353}
Here is the caller graph for this function:

◆ Ssw_MatchingStart()

void Ssw_MatchingStart ( Aig_Man_t * p0,
Aig_Man_t * p1,
Vec_Int_t * vPairs )

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

Synopsis [Establishes relationship between nodes using pairing.]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file sswIslands.c.

65{
66 Aig_Obj_t * pObj0, * pObj1;
67 int i;
68 // create matching
69 Aig_ManCleanData( p0 );
70 Aig_ManCleanData( p1 );
71 for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
72 {
73 pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
74 pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
75 assert( pObj0->pData == NULL );
76 assert( pObj1->pData == NULL );
77 pObj0->pData = pObj1;
78 pObj1->pData = pObj0;
79 }
80 // make sure constants are matched
81 pObj0 = Aig_ManConst1( p0 );
82 pObj1 = Aig_ManConst1( p1 );
83 assert( pObj0->pData == pObj1 );
84 assert( pObj1->pData == pObj0 );
85 // make sure PIs are matched
86 Saig_ManForEachPi( p0, pObj0, i )
87 {
88 pObj1 = Aig_ManCi( p1, i );
89 assert( pObj0->pData == pObj1 );
90 assert( pObj1->pData == pObj0 );
91 }
92 // make sure the POs are not matched
93 Aig_ManForEachCo( p0, pObj0, i )
94 {
95 pObj1 = Aig_ManCo( p1, i );
96 assert( pObj0->pData == NULL );
97 assert( pObj1->pData == NULL );
98 }
99
100 // check that LIs/LOs are matched in sync
101 Saig_ManForEachLo( p0, pObj0, i )
102 {
103 if ( pObj0->pData == NULL )
104 continue;
105 pObj1 = (Aig_Obj_t *)pObj0->pData;
106 if ( !Saig_ObjIsLo(p1, pObj1) )
107 Abc_Print( 1, "Mismatch between LO pairs.\n" );
108 }
109 Saig_ManForEachLo( p1, pObj1, i )
110 {
111 if ( pObj1->pData == NULL )
112 continue;
113 pObj0 = (Aig_Obj_t *)pObj1->pData;
114 if ( !Saig_ObjIsLo(p0, pObj0) )
115 Abc_Print( 1, "Mismatch between LO pairs.\n" );
116 }
117}
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SecWithSimilarity()

int Ssw_SecWithSimilarity ( Aig_Man_t * p0,
Aig_Man_t * p1,
Ssw_Pars_t * pPars )

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

Synopsis [Solves SEC with structural similarity.]

Description []

SideEffects []

SeeAlso []

Definition at line 542 of file sswIslands.c.

543{
544 Vec_Int_t * vPairs;
545 Aig_Man_t * pPart0, * pPart1;
546 int RetValue;
547 if ( pPars->fVerbose )
548 Abc_Print( 1, "Performing sequential verification using structural similarity.\n" );
549 // consider the case when a miter is given
550 if ( p1 == NULL )
551 {
552 if ( pPars->fVerbose )
553 {
554 Aig_ManPrintStats( p0 );
555 }
556 // demiter the miter
557 if ( !Saig_ManDemiterSimpleDiff( p0, &pPart0, &pPart1 ) )
558 {
559 Abc_Print( 1, "Demitering has failed.\n" );
560 return -1;
561 }
562 }
563 else
564 {
565 pPart0 = Aig_ManDupSimple( p0 );
566 pPart1 = Aig_ManDupSimple( p1 );
567 }
568 if ( pPars->fVerbose )
569 {
570// Aig_ManPrintStats( pPart0 );
571// Aig_ManPrintStats( pPart1 );
572 if ( p1 == NULL )
573 {
574// Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
575// Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
576// Abc_Print( 1, "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
577 }
578 }
579 assert( Aig_ManRegNum(pPart0) > 0 );
580 assert( Aig_ManRegNum(pPart1) > 0 );
581 assert( Saig_ManPiNum(pPart0) == Saig_ManPiNum(pPart1) );
582 assert( Saig_ManPoNum(pPart0) == Saig_ManPoNum(pPart1) );
583 // derive pairs
584// vPairs = Saig_StrSimPerformMatching_hack( pPart0, pPart1 );
585 vPairs = Saig_StrSimPerformMatching( pPart0, pPart1, 0, pPars->fVerbose, NULL );
586 RetValue = Ssw_SecWithSimilarityPairs( pPart0, pPart1, vPairs, pPars );
587 Aig_ManStop( pPart0 );
588 Aig_ManStop( pPart1 );
589 Vec_IntFree( vPairs );
590 return RetValue;
591}
Aig_ManDupSimple
Aig_Man_t * Aig_ManDupSimple(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigDup.c:46
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_ManPrintStats
void Aig_ManPrintStats(Aig_Man_t *p)
Definition aigMan.c:379
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Saig_StrSimPerformMatching
Vec_Int_t * Saig_StrSimPerformMatching(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose, Aig_Man_t **ppMiter)
Definition saigStrSim.c:873
Saig_ManDemiterSimpleDiff
int Saig_ManDemiterSimpleDiff(Aig_Man_t *p, Aig_Man_t **ppAig0, Aig_Man_t **ppAig1)
Definition saigMiter.c:660
Ssw_SecWithSimilarityPairs
int Ssw_SecWithSimilarityPairs(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
Definition sswIslands.c:478
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SecWithSimilarityPairs()

int Ssw_SecWithSimilarityPairs ( Aig_Man_t * p0,
Aig_Man_t * p1,
Vec_Int_t * vPairs,
Ssw_Pars_t * pPars )

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

Synopsis [Solves SEC with structural similarity.]

Description [The first two arguments are pointers to the AIG managers. The third argument is the array of pairs of IDs of structurally equivalent nodes from the first and second managers, respectively.]

SideEffects [The managers will be updated by adding "islands of difference".]

SeeAlso []

Definition at line 478 of file sswIslands.c.

479{
480 Ssw_Pars_t Pars;
481 Aig_Man_t * pAigRes;
482 int RetValue;
483 abctime clk = Abc_Clock();
484 // derive parameters if not given
485 if ( pPars == NULL )
486 Ssw_ManSetDefaultParams( pPars = &Pars );
487 // reduce the AIG with pairs
488 pAigRes = Ssw_SecWithSimilaritySweep( p0, p1, vPairs, pPars );
489 // report the result of verification
490 RetValue = Ssw_MiterStatus( pAigRes, 1 );
491 if ( RetValue == 1 )
492 Abc_Print( 1, "Verification successful. " );
493 else if ( RetValue == 0 )
494 Abc_Print( 1, "Verification failed with a counter-example. " );
495 else
496 Abc_Print( 1, "Verification UNDECIDED. The number of remaining regs = %d (total = %d). ",
497 Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0)+Aig_ManRegNum(p1) );
498 ABC_PRT( "Time", Abc_Clock() - clk );
499 Aig_ManStop( pAigRes );
500 return RetValue;
501}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Ssw_SecWithSimilaritySweep
Aig_Man_t * Ssw_SecWithSimilaritySweep(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs, Ssw_Pars_t *pPars)
Definition sswIslands.c:419
Ssw_ManSetDefaultParams
void Ssw_ManSetDefaultParams(Ssw_Pars_t *p)
DECLARATIONS ///.
Definition sswCore.c:45
Ssw_Pars_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Pars_t_ Ssw_Pars_t
INCLUDES ///.
Definition ssw.h:40
Ssw_MiterStatus
int Ssw_MiterStatus(Aig_Man_t *p, int fVerbose)
DECLARATIONS ///.
Definition sswPairs.c:45
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Ssw_SecWithSimilaritySweep()

Aig_Man_t * Ssw_SecWithSimilaritySweep ( Aig_Man_t * p0,
Aig_Man_t * p1,
Vec_Int_t * vPairs,
Ssw_Pars_t * pPars )

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

Synopsis [Solves SEC using structural similarity.]

Description [Modifies both p0 and p1 by adding extra logic.]

SideEffects []

SeeAlso []

Definition at line 419 of file sswIslands.c.

420{
421 Ssw_Man_t * p;
422 Vec_Int_t * vPairsAll, * vPairsMiter;
423 Aig_Man_t * pMiter, * pAigNew;
424 // derive full matching
425 Ssw_MatchingStart( p0, p1, vPairs );
426 if ( pPars->nIsleDist )
427 Ssw_MatchingExtend( p0, p1, pPars->nIsleDist, pPars->fVerbose );
428 Ssw_MatchingComplete( p0, p1 );
429 Ssw_MatchingComplete( p1, p0 );
430 vPairsAll = Ssw_MatchingPairs( p0, p1 );
431 // create miter and transfer matching
432 pMiter = Saig_ManCreateMiter( p0, p1, 0 );
433 vPairsMiter = Ssw_MatchingMiter( pMiter, p0, p1, vPairsAll );
434 Vec_IntFree( vPairsAll );
435 // start the induction manager
436 p = Ssw_ManCreate( pMiter, pPars );
437 // create equivalence classes using these IDs
438 if ( p->pPars->fPartSigCorr )
439 p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
440 else
441 p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
442 if ( p->pPars->fDumpSRInit )
443 {
444 if ( p->pPars->fPartSigCorr )
445 {
446 Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p );
447 Aig_ManDumpBlif( pSRed, "srm_part.blif", NULL, NULL );
448 Aig_ManStop( pSRed );
449 Abc_Print( 1, "Speculatively reduced miter is saved in file \"%s\".\n", "srm_part.blif" );
450 }
451 else
452 Abc_Print( 1, "Dumping speculative miter is possible only for partial signal correspondence (switch \"-c\").\n" );
453 }
454 p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
455 Ssw_ClassesSetData( p->ppClasses, p->pSml, (unsigned(*)(void *,Aig_Obj_t *))Ssw_SmlObjHashWord, (int(*)(void *,Aig_Obj_t *))Ssw_SmlObjIsConstWord, (int(*)(void *,Aig_Obj_t *,Aig_Obj_t *))Ssw_SmlObjsAreEqualWord );
456 // perform refinement of classes
457 pAigNew = Ssw_SignalCorrespondenceRefine( p );
458 // cleanup
459 Ssw_ManStop( p );
460 Aig_ManStop( pMiter );
461 Vec_IntFree( vPairsMiter );
462 return pAigNew;
463}
Aig_ManDumpBlif
void Aig_ManDumpBlif(Aig_Man_t *p, char *pFileName, Vec_Ptr_t *vPiNames, Vec_Ptr_t *vPoNames)
Definition aigUtil.c:746
Saig_ManCreateMiter
Aig_Man_t * Saig_ManCreateMiter(Aig_Man_t *p1, Aig_Man_t *p2, int Oper)
Definition saigMiter.c:100
Ssw_SpeculativeReduction
Aig_Man_t * Ssw_SpeculativeReduction(Ssw_Man_t *p)
Definition sswAig.c:272
Ssw_ClassesPreparePairsSimple
Ssw_Cla_t * Ssw_ClassesPreparePairsSimple(Aig_Man_t *pMiter, Vec_Int_t *vPairs)
Definition sswClass.c:928
Ssw_ClassesPrepare
Ssw_Cla_t * Ssw_ClassesPrepare(Aig_Man_t *pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose)
Definition sswClass.c:596
Ssw_ClassesSetData
void Ssw_ClassesSetData(Ssw_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 sswClass.c:167
Ssw_SignalCorrespondenceRefine
Aig_Man_t * Ssw_SignalCorrespondenceRefine(Ssw_Man_t *p)
Definition sswCore.c:235
Ssw_Man_t
typedefABC_NAMESPACE_HEADER_START struct Ssw_Man_t_ Ssw_Man_t
INCLUDES ///.
Definition sswInt.h:47
Ssw_SmlStart
Ssw_Sml_t * Ssw_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition sswSim.c:1148
Ssw_ManStop
void Ssw_ManStop(Ssw_Man_t *p)
Definition sswMan.c:189
Ssw_ManCreate
Ssw_Man_t * Ssw_ManCreate(Aig_Man_t *pAig, Ssw_Pars_t *pPars)
DECLARATIONS ///.
Definition sswMan.c:45
Ssw_SmlObjHashWord
unsigned Ssw_SmlObjHashWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition sswSim.c:63
Ssw_SmlObjIsConstWord
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition sswSim.c:102
Ssw_MatchingExtend
void Ssw_MatchingExtend(Aig_Man_t *p0, Aig_Man_t *p1, int nDist, int fVerbose)
Definition sswIslands.c:219
Ssw_MatchingStart
void Ssw_MatchingStart(Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairs)
Definition sswIslands.c:64
Ssw_MatchingPairs
Vec_Int_t * Ssw_MatchingPairs(Aig_Man_t *p0, Aig_Man_t *p1)
Definition sswIslands.c:332
Ssw_MatchingComplete
void Ssw_MatchingComplete(Aig_Man_t *p0, Aig_Man_t *p1)
Definition sswIslands.c:287
Ssw_MatchingMiter
Vec_Int_t * Ssw_MatchingMiter(Aig_Man_t *pMiter, Aig_Man_t *p0, Aig_Man_t *p1, Vec_Int_t *vPairsAll)
Definition sswIslands.c:370
Ssw_SmlObjsAreEqualWord
int Ssw_SmlObjsAreEqualWord(Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
Definition sswSim.c:124
Here is the call graph for this function:
Here is the caller graph for this function: