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
|
/**CFile****************************************************************
FileName [sswAig.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [Inductive prover with constraints.]
Synopsis [AIG manipulation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - September 1, 2008.]
Revision [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
***********************************************************************/
#include "sswInt.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Performs speculative reduction for one node.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame )
{
Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
// skip nodes without representative
if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
return;
p->nConstrTotal++;
assert( pObjRepr->Id < pObj->Id );
// get the new node
pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
// get the new node of the representative
pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
// if this is the same node, no need to add constraints
if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
return;
p->nConstrReduced++;
// these are different nodes - perform speculative reduction
pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
// set the new node
Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
// add the constraint
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) );
Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) );
}
/**Function*************************************************************
Synopsis [Prepares the inductive case with speculative reduction.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
{
Aig_Man_t * pFrames;
Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
int i, k, f;
assert( p->pFrames == NULL );
assert( Aig_ManRegNum(p->pAig) > 0 );
assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
// start the fraig package
pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
// create latches for the first frame
Saig_ManForEachLo( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
// create PI nodes for the frames
for ( f = 0; f < p->pPars->nFramesK; f++ )
Aig_ManForEachPiSeq( p->pAig, pObj, i )
Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
// map constant nodes
for ( f = 0; f < p->pPars->nFramesK; f++ )
Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
// add timeframes
p->nConstrTotal = p->nConstrReduced = 0;
for ( f = 0; f < p->pPars->nFramesK; f++ )
{
// set the constraints on the latch outputs
Aig_ManForEachLoSeq( p->pAig, pObj, i )
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
// add internal nodes of this frame
Aig_ManForEachNode( p->pAig, pObj, i )
{
pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
Ssw_ObjSetFraig( p, pObj, f, pObjNew );
Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
}
// transfer latch input to the latch outputs
Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
}
// add the POs for the latch outputs of the last frame
Saig_ManForEachLo( p->pAig, pObj, i )
Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
// remove dangling nodes
Aig_ManCleanup( pFrames );
// make sure the satisfying assignment is node assigned
assert( pFrames->pData == NULL );
return pFrames;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
