source: vis_dev/vis-2.3/src/debug/debugAbnormal.c @ 41

Last change on this file since 41 was 41, checked in by cecile, 14 years ago

new command generate cnf from network
File size: 10.8 KB
Line 
1#include "debugInt.h"
2/**Function********************************************************************
3 
4  Synopsis    [create New node]
5
6  Description [Create new primary input in the current network at a given
7  output node.  Return the variable created]
8
9  SideEffects [Modify the network]
10
11  SeeAlso     []
12
13******************************************************************************/
14Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t*
15node, char * varName  )
16{
17        array_t * fanin = array_dup(Ntk_NodeReadFanins(node));
18        array_t * fanout = array_alloc(Ntk_Node_t*,0);
19        char * nodeName = util_strsav(Ntk_NodeReadName(node));
20        //Create var Name
21        char * newVarName = (char *) malloc(strlen(nodeName) + strlen(varName) +1);
22        sprintf(newVarName,"%s_%s",nodeName,varName);
23        Var_Variable_t * var = Var_VariableAlloc(NIL(Hrc_Node_t),newVarName);
24        //Create new Node
25        Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, newVarName,var);
26        Ntk_NodeDeclareAsPrimaryInput(newNode);
27        //Add in the fanin of the node
28    array_insert_last(Ntk_Node_t*,fanin,newNode);
29        Ntk_NodeSetFanins(node,fanin);
30        //Add Fanout to the newNode
31    array_insert_last(Ntk_Node_t*,fanout,node);
32        Ntk_NodeSetFanouts(newNode,fanout);
33        free(newVarName);
34
35        return newNode;
36
37}
38/**Function********************************************************************
39 
40  Synopsis    [Add abnormal predicates to the network]
41
42  Description [Given a network after flatten the hierarchy,
43  change the table of each combinatorial node
44  with a new table including the abnormal predicate.
45  For a combinatorial node n is tranformed into (abn_n)?i_n:n
46  If the abnormal predicate is activ then n is replaced by a free input]
47
48  SideEffects [fill the abnormal structure]
49
50  SeeAlso     []
51
52******************************************************************************/
53
54void Dbg_AddAbnormalPredicatetoNetwork(Dbg_Abnormal_t* abnormal ) /*abnormal struct*/
55{
56
57  Ntk_Network_t * ntk = abnormal->network;
58  lsGen gen;
59  Ntk_Node_t* node;
60  Ntk_NetworkForEachNode(ntk,gen,node){
61  //For each combinatorial node
62  if(Ntk_NodeTestIsCombinational(node)){
63        if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
64        {
65                char * nodeName = util_strsav(Ntk_NodeReadName(node));
66        printf("%s \n",  nodeName); 
67
68                Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
69                (void) fprintf(vis_stdout, "** old table\n");
70                Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
71                // Build new variables abnormal  and  input
72                Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn");
73                Ntk_Node_t * iNode   = Dbg_CreateNewNode(ntk,node,"i");
74                Dbg_AddFreeInput(abnormal,iNode);
75                Dbg_AddAbnormalPredicate(abnormal,abnNode);
76                Var_Variable_t * abn = Ntk_NodeReadVariable(abnNode);
77                Var_Variable_t * i   = Ntk_NodeReadVariable(iNode);
78                //Add in the table
79                Tbl_TableAddColumn(table,abn,0);
80                int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
81                Tbl_TableAddColumn(table,i,0);
82                int iIndex = Tbl_TableReadVarIndex(table, i, 0);
83
84                //For each row already there in the table
85                int rowNum;
86                for(rowNum = 0; rowNum <  Tbl_TableReadNumRows(table);rowNum++){
87                        Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
88                        Tbl_EntrySetValue(abnEntry,0,0);
89                        Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
90                        Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
91                        Tbl_EntrySetValue(iEntry,0,1);
92                        Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
93                }
94                //the new row
95                int r = Tbl_TableAddRow(table);
96
97                int colNum;
98            for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
99                        Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
100                        if(colNum == abnIndex || colNum == iIndex)
101                                Tbl_EntrySetValue(entry,1,1);
102                        else
103                                Tbl_EntrySetValue(entry,0,1);
104                    Tbl_TableSetEntry(table, entry, r, colNum, 0);
105                }
106                for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
107                        Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
108                        Tbl_EntrySetValue(entry,1,1);
109                    Tbl_TableSetEntry(table, entry, r, colNum, 1);
110                }
111                 printf("---------------\n");
112                 Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
113          }
114        }
115}
116 Ntk_NetworkAddApplInfo(ntk, DBG_NETWORK_APPL_KEY,
117 (Ntk_ApplInfoFreeFn) Dbg_AbnormalFreeCallback,
118 (void *) abnormal);
119}
120/**Function********************************************************************
121 
122  Synopsis    [Allocate a new abnormal structure]
123
124  Description [The structure contains the network with abnormal predicate,
125  and two sets of Ntk_Node_t for the abnormal and the free inputs]
126
127  SideEffects [Allocate the abnormal structure]
128
129  SeeAlso     []
130
131******************************************************************************/
132
133Dbg_Abnormal_t * Dbg_DebugAbnormalAlloc(Ntk_Network_t * network)
134{
135         Dbg_Abnormal_t * abn = ALLOC(Dbg_Abnormal_t, 1);
136
137         abn->network = network;
138         abn->abnormal = array_alloc(Ntk_Node_t*,0);
139         abn->freeInputs = array_alloc(Ntk_Node_t*,0);
140     abn->abnAigArray = NIL(array_t);
141     abn->abnCnfIndexArray = NIL(array_t);
142         abn->verbose = 0;
143         return abn;
144}       
145
146/**Function********************************************************************
147 
148  Synopsis    [Deallocate a new abnormal structure]
149
150  Description [Free the arrays not the network]
151
152  SideEffects [free the abnormal structure]
153
154  SeeAlso     []
155
156******************************************************************************/
157
158void  Dbg_DebugAbnormalFree(Dbg_Abnormal_t * abn)
159{
160         array_free(abn->abnormal);
161         array_free(abn->freeInputs);
162     array_free(abn->abnCnfIndexArray);
163     array_free(abn->abnAigArray);
164         FREE(abn);
165}       
166/**Function********************************************************************
167
168  Synopsis    [Call-back function to free an abnormal structure.]
169
170  Description [This function will be stored in the network together with the
171  pointer to the structure. Whenever the network deletes the partitioning
172  information, this function is called and it will deallocate the abnormal and
173  the information attached to it.]
174
175  SideEffects []
176
177  SeeAlso     [Ntk_NetworkAddApplInfo]
178
179******************************************************************************/
180void
181Dbg_AbnormalFreeCallback(
182   void *data)
183{
184  Dbg_DebugAbnormalFree((Dbg_Abnormal_t *) data);
185} /* End of Part_PartitionFreeCallback */
186
187
188/**Function********************************************************************
189 
190  Synopsis    [Add abnormal predicate]
191
192  Description [add a node to the predicates array, it should not be already
193  present by construction of abnormal predicate]
194
195  SideEffects []
196
197  SeeAlso     []
198
199******************************************************************************/
200
201void  Dbg_AddAbnormalPredicate(Dbg_Abnormal_t * abn, Ntk_Node_t* abnNode)
202{
203        assert(abnNode != NIL(Ntk_Node_t*));
204        array_insert_last(Ntk_Node_t*,abn->abnormal, abnNode);
205}
206/**Function********************************************************************
207 
208  Synopsis    [Add free inputs]
209
210  Description [add a node to the free inputs, it should not be already
211  present by construction of abnormal predicate]
212
213  SideEffects []
214
215  SeeAlso     []
216
217******************************************************************************/
218void  Dbg_AddFreeInput(Dbg_Abnormal_t * abn, Ntk_Node_t* fNode)
219{
220        assert(fNode != NIL(Ntk_Node_t*));
221        array_insert_last(Ntk_Node_t*,abn->freeInputs, fNode);
222}
223
224/**Function********************************************************************
225 
226  Synopsis    [returns a free inputs]
227
228  Description [returns the array of freeinputs]
229
230  SideEffects []
231
232  SeeAlso     [Dbg_ReadAbn]
233
234******************************************************************************/
235array_t* Dbg_ReadFreeInputs(Dbg_Abnormal_t *abnormal)
236{
237        assert(abnormal != NIL(Dbg_Abnormal_t));
238        return abnormal->freeInputs;
239}
240/**Function********************************************************************
241 
242  Synopsis    [returns a abnormal predicates]
243
244  Description [returns the array of abnormal predicates]
245
246  SideEffects []
247
248  SeeAlso     [Dbg_ReadFreeInputs]
249
250******************************************************************************/
251array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal)
252{
253        assert(abnormal != NIL(Dbg_Abnormal_t));
254        return abnormal->abnormal;
255}
256/**Function********************************************************************
257 
258  Synopsis    [returns the abnormal structure]
259
260  Description [returns the abnormal structure associated to the network]
261
262  SideEffects []
263
264  SeeAlso     []
265
266******************************************************************************/
267Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network)
268{
269        Dbg_Abnormal_t * abn = (Dbg_Abnormal_t *) Ntk_NetworkReadApplInfo(network, DBG_NETWORK_APPL_KEY);
270
271        return abn;
272}
273/**Function********************************************************************
274 
275  Synopsis    [Initialize the abnormal predicate in the clauses array abni =0]
276
277  Description [Fill the Dbg data structure, abnAigArray conains the set of Aig
278  for the set of abnormal perdicate. Each abnormal are set to zero in the clause
279  array.predicabnCnfIndexArray is the cnf index. The   correspondance is made by
280  the index in the table, the index of a node in   abnArray is the same in
281  abnAigArray and in abnIndexArray. If this array were  alredy computed nothing
282  is done, if the aig or index information either.]
283
284  SideEffects [Fill abnAigArray and abnCnfIndexArray]
285
286  SeeAlso     []
287
288******************************************************************************/
289void Dbg_InitAbn(Dbg_Abnormal_t * abn,
290bAig_Manager_t   * manager,
291st_table * nodeToMvfAigTable,
292BmcCnfClauses_t *cnfClauses)
293{
294  if(abn->abnAigArray != NIL(array_t))
295    (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
296  if(abn->abnCnfIndexArray != NIL(array_t)){
297    (void) fprintf(vis_stdout, "Abnormal index alredy filled\n"); 
298     return;
299  }
300  //Fill
301   int size = array_n(abn->abnormal);
302   array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
303   array_t * abnIndexArray = array_alloc(int,size);
304   int aIndex;
305   Ntk_Node_t * abnNode;
306   Dbg_ForEachAbnormal(abn, aIndex,abnNode){
307   MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
308    if (abnMvfAig ==  NIL(MvfAig_Function_t)){
309     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
310     create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
311     return ;
312    }
313    int mvfSize   = array_n(abnMvfAig);
314    int i;
315    bAigEdge_t         * abnBAig  = ALLOC(bAigEdge_t, mvfSize);
316
317    for(i=0; i< mvfSize; i++)
318    {
319      abnBAig[i] = bAig_GetCanonical(manager,
320      MvfAig_FunctionReadComponent(abnMvfAig,  i));
321    }
322    array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
323    int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
324    array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
325    // Create clause
326     array_t           *abnClause = NIL(array_t);
327         abnClause = array_alloc(int, 0);   
328         array_insert_last(int, abnClause, abnIndex);
329         BmcCnfInsertClause(cnfClauses, abnClause);
330     array_free(abnClause);
331   }
332   abn->abnAigArray = abnAigArray;
333   abn->abnCnfIndexArray = abnIndexArray;
334}
Note: See TracBrowser for help on using the repository browser.