1 /**CFile****************************************************************
2 
3   FileName    [intDup.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Interpolation engine.]
8 
9   Synopsis    [Specialized AIG duplication procedures.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 24, 2008.]
16 
17   Revision    [$Id: intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "intInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 ///                     FUNCTION DEFINITIONS                         ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36   Synopsis    [Create trivial AIG manager for the init state.]
37 
38   Description []
39 
40   SideEffects []
41 
42   SeeAlso     []
43 
44 ***********************************************************************/
Inter_ManStartInitState(int nRegs)45 Aig_Man_t * Inter_ManStartInitState( int nRegs )
46 {
47     Aig_Man_t * p;
48     Aig_Obj_t * pRes;
49     Aig_Obj_t ** ppInputs;
50     int i;
51     assert( nRegs > 0 );
52     ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
53     p = Aig_ManStart( nRegs );
54     for ( i = 0; i < nRegs; i++ )
55         ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) );
56     pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
57     Aig_ObjCreateCo( p, pRes );
58     ABC_FREE( ppInputs );
59     return p;
60 }
61 
62 /**Function*************************************************************
63 
64   Synopsis    [Duplicate the AIG w/o POs.]
65 
66   Description []
67 
68   SideEffects []
69 
70   SeeAlso     []
71 
72 ***********************************************************************/
Inter_ManStartDuplicated(Aig_Man_t * p)73 Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
74 {
75     Aig_Man_t * pNew;
76     Aig_Obj_t * pObj;
77     int i;
78     assert( Aig_ManRegNum(p) > 0 );
79     // create the new manager
80     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
81     pNew->pName = Abc_UtilStrsav( p->pName );
82     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
83     // create the PIs
84     Aig_ManCleanData( p );
85     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
86     Aig_ManForEachCi( p, pObj, i )
87         pObj->pData = Aig_ObjCreateCi( pNew );
88     // set registers
89     pNew->nTruePis = p->nTruePis;
90     pNew->nTruePos = Saig_ManConstrNum(p);
91     pNew->nRegs    = p->nRegs;
92     // duplicate internal nodes
93     Aig_ManForEachNode( p, pObj, i )
94         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
95 
96     // create constraint outputs
97     Saig_ManForEachPo( p, pObj, i )
98     {
99         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
100             continue;
101         Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
102     }
103 
104     // create register inputs with MUXes
105     Saig_ManForEachLi( p, pObj, i )
106         Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
107     Aig_ManCleanup( pNew );
108     return pNew;
109 }
110 
111 /**Function*************************************************************
112 
113   Synopsis    [Duplicate the AIG w/o POs and transforms to transit into init state.]
114 
115   Description []
116 
117   SideEffects []
118 
119   SeeAlso     []
120 
121 ***********************************************************************/
Inter_ManStartOneOutput(Aig_Man_t * p,int fAddFirstPo)122 Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
123 {
124     Aig_Man_t * pNew;
125     Aig_Obj_t * pObj, * pObjLi, * pObjLo;
126     Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
127     int i;
128     assert( Aig_ManRegNum(p) > 0 );
129     // create the new manager
130     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
131     pNew->pName = Abc_UtilStrsav( p->pName );
132     pNew->pSpec = Abc_UtilStrsav( p->pSpec );
133     // create the PIs
134     Aig_ManCleanData( p );
135     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
136     Aig_ManForEachCi( p, pObj, i )
137     {
138         if ( i == Saig_ManPiNum(p) )
139             pCtrl = Aig_ObjCreateCi( pNew );
140         pObj->pData = Aig_ObjCreateCi( pNew );
141     }
142     // set registers
143     pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
144     pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1;
145     pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
146     // duplicate internal nodes
147     Aig_ManForEachNode( p, pObj, i )
148         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
149 
150     // create constraint outputs
151     Saig_ManForEachPo( p, pObj, i )
152     {
153         if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
154             continue;
155         Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
156     }
157 
158     // add the PO
159     if ( fAddFirstPo )
160     {
161         pObj = Aig_ManCo( p, 0 );
162         Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
163     }
164     else
165     {
166         // create register inputs with MUXes
167         Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
168         {
169             pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
170     //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
171             Aig_ObjCreateCo( pNew, pObj );
172         }
173     }
174     Aig_ManCleanup( pNew );
175     return pNew;
176 }
177 
178 ////////////////////////////////////////////////////////////////////////
179 ///                       END OF FILE                                ///
180 ////////////////////////////////////////////////////////////////////////
181 
182 
183 ABC_NAMESPACE_IMPL_END
184 
185