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
139
140
141
142
143
144
145
146
|
/**CFile****************************************************************
FileName [dchSweep.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Choice computation for tech-mapping.]
Synopsis [One round of SAT sweeping.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 29, 2008.]
Revision [$Id: dchSweep.c,v 1.00 2008/07/29 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dchInt.h"
#include "bar.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static inline Aig_Obj_t * Dch_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL; }
static inline Aig_Obj_t * Dch_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Dch_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs fraiging for one node.]
Description [Returns the fraiged node.]
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
{
Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
int RetValue;
// get representative of this class
pObjRepr = Aig_ObjRepr( p->pAigTotal, pObj );
if ( pObjRepr == NULL )
return;
// get the fraiged node
pObjFraig = Dch_ObjFraig( pObj );
if ( pObjFraig == NULL )
return;
// get the fraiged representative
pObjReprFraig = Dch_ObjFraig( pObjRepr );
if ( pObjReprFraig == NULL )
return;
// if the fraiged nodes are the same, return
if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
{
// remember the proved equivalence
p->pReprsProved[ pObj->Id ] = pObjRepr;
return;
}
assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pAigFraig) );
RetValue = Dch_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
if ( RetValue == -1 ) // timed out
{
Dch_ObjSetFraig( pObj, NULL );
return;
}
if ( RetValue == 1 ) // proved equivalent
{
pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
Dch_ObjSetFraig( pObj, pObjFraig2 );
// remember the proved equivalence
p->pReprsProved[ pObj->Id ] = pObjRepr;
return;
}
// disproved the equivalence
if ( p->pPars->fSimulateTfo )
Dch_ManResimulateCex( p, pObj, pObjRepr );
else
Dch_ManResimulateCex2( p, pObj, pObjRepr );
assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
}
/**Function*************************************************************
Synopsis [Performs fraiging for the internal nodes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dch_ManSweep( Dch_Man_t * p )
{
Bar_Progress_t * pProgress = NULL;
Aig_Obj_t * pObj, * pObjNew;
int i;
// map constants and PIs
p->pAigFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAigTotal) );
Aig_ManCleanData( p->pAigTotal );
Aig_ManConst1(p->pAigTotal)->pData = Aig_ManConst1(p->pAigFraig);
Aig_ManForEachPi( p->pAigTotal, pObj, i )
pObj->pData = Aig_ObjCreatePi( p->pAigFraig );
// sweep internal nodes
pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAigTotal) );
Aig_ManForEachNode( p->pAigTotal, pObj, i )
{
Bar_ProgressUpdate( pProgress, i, NULL );
if ( Dch_ObjFraig(Aig_ObjFanin0(pObj)) == NULL ||
Dch_ObjFraig(Aig_ObjFanin1(pObj)) == NULL )
continue;
pObjNew = Aig_And( p->pAigFraig, Dch_ObjChild0Fra(pObj), Dch_ObjChild1Fra(pObj) );
if ( pObjNew == NULL )
continue;
Dch_ObjSetFraig( pObj, pObjNew );
Dch_ManSweepNode( p, pObj );
}
Bar_ProgressStop( pProgress );
// update the representatives of the nodes (makes classes invalid)
ABC_FREE( p->pAigTotal->pReprs );
p->pAigTotal->pReprs = p->pReprsProved;
p->pReprsProved = NULL;
// clean the mark
Aig_ManCleanMarkB( p->pAigTotal );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END
|
