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

Last change on this file since 102 was 45, checked in by cecile, 13 years ago

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