1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
|
/**CFile****************************************************************
FileName [fraAnd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Fraig FRAIG package.]
Synopsis []
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 30, 2007.]
Revision [$Id: fraAnd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
***********************************************************************/
#include "fra.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
{
Dar_Obj_t * pObjOldRepr, * pObjFraig, * pFanin0Fraig, * pFanin1Fraig, * pObjOldReprFraig;
int RetValue;
assert( !Dar_IsComplement(pObjOld) );
assert( Dar_ObjIsNode(pObjOld) );
// get the fraiged fanins
pFanin0Fraig = Fra_ObjChild0Fra(pObjOld);
pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
// get the fraiged node
pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
// get representative of this class
pObjOldRepr = Fra_ObjRepr(pObjOld);
if ( pObjOldRepr == NULL || // this is a unique node
(!p->pPars->fDoSparse && pObjOldRepr == Dar_ManConst1(p->pManAig)) ) // this is a sparse node
{
assert( Dar_Regular(pFanin0Fraig) != Dar_Regular(pFanin1Fraig) );
assert( pObjFraig != Dar_Regular(pFanin0Fraig) );
assert( pObjFraig != Dar_Regular(pFanin1Fraig) );
return pObjFraig;
}
// get the fraiged representative
pObjOldReprFraig = Fra_ObjFraig(pObjOldRepr);
// if the fraiged nodes are the same, return
if ( Dar_Regular(pObjFraig) == Dar_Regular(pObjOldReprFraig) )
return pObjFraig;
assert( Dar_Regular(pObjFraig) != Dar_ManConst1(p->pManFraig) );
// if they are proved different, the c-ex will be in p->pPatWords
RetValue = Fra_NodesAreEquiv( p, Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) );
if ( RetValue == 1 ) // proved equivalent
{
pObjOld->fMarkA = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
if ( RetValue == -1 ) // failed
{
if ( !p->pPars->fSpeculate )
return pObjFraig;
// substitute the node
pObjOld->fMarkB = 1;
return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
}
// simulate the counter-example and return the Fraig node
Fra_Resimulate( p );
return pObjFraig;
}
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Fra_Sweep( Fra_Man_t * p )
{
Dar_Obj_t * pObj, * pObjNew;
int i, k = 0;
p->nClassesZero = Vec_PtrSize(p->vClasses1);
p->nClassesBeg = Vec_PtrSize(p->vClasses);
// duplicate internal nodes
// p->pProgress = Extra_ProgressBarStart( stdout, Dar_ManNodeNum(p->pManAig) );
Dar_ManForEachNode( p->pManAig, pObj, i )
{
// Extra_ProgressBarUpdate( p->pProgress, k++, NULL );
// default to simple strashing if simulation detected a counter-example for a PO
if ( p->pManFraig->pData )
pObjNew = Dar_And( p->pManFraig, Fra_ObjChild0Fra(pObj), Fra_ObjChild1Fra(pObj) );
else
pObjNew = Fra_And( p, pObj ); // pObjNew can be complemented
assert( Fra_ObjFraig(pObj) != NULL );
Fra_ObjSetFraig( pObj, pObjNew );
}
// Extra_ProgressBarStop( p->pProgress );
p->nClassesEnd = Vec_PtrSize(p->vClasses);
// try to prove the outputs of the miter
p->nNodesMiter = Dar_ManNodeNum(p->pManFraig);
// Fra_MiterStatus( p->pManFraig );
// if ( p->pPars->fProve && p->pManFraig->pData == NULL )
// Fra_MiterProve( p );
// add the POs
Dar_ManForEachPo( p->pManAig, pObj, i )
Dar_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj) );
// remove dangling nodes
Dar_ManCleanup( p->pManFraig );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
