source: vis_dev/vis-2.3/src/io/ioWriteBlif.c @ 93

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

vis2.3
File size: 52.6 KB
RevLine 
[14]1 /**CFile***********************************************************************
2
3  FileName    [ ioWriteBlif.c ]
4
5  PackageName [ io ]
6
7  Synopsis    [ This file contains blifmv -> blif write routines ]
8
9  Description [ Routines for (determinizing, encoding and) writing a blifmv table
10                into a blif description are provided. The encoding of multivalued
11                vars is written to separate files. ]
12
13  SeeAlso     [ ioReadBlifmv.c, ioWriteBlifIo.c, IoWriteBlifUtil.c]
14
15  Author      [ Sunil P. Khatri ]
16
17  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
18  All rights reserved.
19
20  Permission is hereby granted, without written agreement and without license
21  or royalty fees, to use, copy, modify, and distribute this software and its
22  documentation for any purpose, provided that the above copyright notice and
23  the following two paragraphs appear in all copies of this software.
24
25  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
26  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
27  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
28  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
29
30  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
31  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
32  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
33  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
34  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
35
36******************************************************************************/
37
38#include "ioInt.h"
39
40static char rcsid[] UNUSED = "$Id: ioWriteBlif.c,v 1.14 2005/04/29 14:23:29 fabio Exp $";
41
42/*---------------------------------------------------------------------------*/
43/* Constant declarations                                                     */
44/*---------------------------------------------------------------------------*/
45#define MAX_NUMBER_BDD_VARS 500
46
47/*---------------------------------------------------------------------------*/
48/* Macro declarations                                                        */
49/*---------------------------------------------------------------------------*/
50
51
52
53/**AutomaticStart*************************************************************/
54
55/*---------------------------------------------------------------------------*/
56/* Static function prototypes                                                */
57/*---------------------------------------------------------------------------*/
58
59static int _IoTableWriteBlif(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, Tbl_Table_t *origBlifmvTable, st_table *blifInputsStTable, FILE *fp, FILE *encFp, int verbosity);
60static int _IoMakeInitialEncodings(IoBlifInfo_t *blifInfo, Hrc_Node_t *hnode);
61static void _IoDeterminizeEncodeOutputPart(IoBlifInfo_t *blifInfo, st_table *blifInputsStTable);
62static void _IoDeterminizeEncodeRows(IoBlifInfo_t *blifInfo, st_table *blifInputsStTable);
63static void _IoMakeDcTables(IoBlifInfo_t *blifInfo);
64static void _IoMakeBinTable(IoBlifInfo_t *blifInfo);
65static int _IoCheckHnodeTreeIsBooleanAndDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode, st_table *modelTable, boolean *pSymVarsPresent, int verbosity);
66static int _IoCheckHnodeVarsAreBoolean(Hrc_Node_t *hnode, boolean *pSymVarsPresent);
67static int _IoCheckHnodeLatchResetIsConstant(Hrc_Node_t *hnode);
68static int _IoCheckHnodeTablesAreDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode);
69static void _MddManagerResetIfNecessary(mdd_manager **mddMgr);
70static void _IoHnodeWriteBlifRecursively(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, st_table *modelTable, FILE *fp, FILE *encFp, int verbosity);
71static int _IoHnodeWriteBlifRecursivelyStep(Io_Encoding_Type_t encodingType, Hrc_Node_t *hnode, FILE *fp, FILE *encFp, int verbosity);
72static int _IoCheckHnodeIsBooleanAndDeterministic(mdd_manager **mddMgr, Hrc_Node_t *hnode, boolean *pSymVarsPresent);
73static int _IoCheckPseudoinputIsPO(Tbl_Table_t *table);
74
75/**AutomaticEnd***************************************************************/
76
77
78/*---------------------------------------------------------------------------*/
79/* Definition of exported functions                                          */
80/*---------------------------------------------------------------------------*/
81
82/**Function***********************************************************
83
84
85  Synopsis      [ Recursively write out the entire hierarchy below the current
86                  hnode to a blif file. ]
87
88  Description   [ This routine recursively writes out the entire hierarchy below
89                  the given hnode to a named blif file. This sub-hierarchy must
90                  comply with the following restrictions. First all tables in it
91                  should be deterministic. Secondly, all variables should be
92                  binary. The function returns a 0 upon success, 1 in case of
93                  failure. Upon failure, appropriate error messages are printed
94                  to stderr. The function is passed an enumerated type called
95                  encodingType, only SIMPLE is supported. Refer to the description
96                  of Io_HnodeWriteBlif for more information on this. The hnode
97                  is passed, along with the file pointer fp, for the file into which
98                  the resulting blif network is to be written. A verbosity flag
99                  (valid values are between 0 and 2) causes intermediate information
100                  to be printed to stderr.
101                  ]
102
103  SideEffects   [ ]
104
105  SeeAlso       [  ]
106**********************************************************************/
107int
108Io_HnodeWriteBlifTotal(
109    Io_Encoding_Type_t encodingType,
110    Hrc_Node_t *hnode, 
111    FILE *fp, 
112    int verbosity)
113{
114  st_table *modelTable;
115  Hrc_Manager_t *manager;
116  mdd_manager *mddMgr;
117  FILE *encFp;
118  boolean symVarsPresent;
119 
120  manager = Hrc_NodeReadManager(hnode);
121  modelTable = st_init_table(st_ptrcmp, st_ptrhash);
122  mddMgr = mdd_init_empty();
123  bdd_dynamic_reordering(mddMgr, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY_DEFAULT);
124  symVarsPresent = FALSE;
125
126  /* check that the node and all its children are boolean and deterministic. */
127  if(_IoCheckHnodeTreeIsBooleanAndDeterministic(&mddMgr, hnode, modelTable, &symVarsPresent, verbosity)){
128    mdd_quit(mddMgr);
129    st_free_table(modelTable);
130    return 1;
131  }
132  if(verbosity > 0){
133    fprintf(vis_stderr, "Done with hierarcy checks\n");
134  }
135 
136  if(symVarsPresent == TRUE){
137    fprintf(vis_stderr, "Warning - some variables in the hierarchy are symbolic\n");
138  }
139 
140  st_free_table(modelTable);
141  modelTable = st_init_table(st_ptrcmp, st_ptrhash); 
142  encFp = Cmd_FileOpen("/dev/null", "w", NIL(char *), 1);
143
144  _IoHnodeWriteBlifRecursively(encodingType, hnode, modelTable, fp, encFp, verbosity);
145  Hrc_ManagerSetCurrentNode(manager, hnode);
146
147  st_free_table(modelTable);
148  mdd_quit(mddMgr);
149  return 0;
150}
151   
152
153/**Function***********************************************************
154
155
156  Synopsis      [ Determinize, encode and write all blifmv tables in a hnode
157                  to a blif file. Also writes all encoding information to a
158                  encoding file. This encoding file can later be read in, along
159                  with the blif file (potentially after optimization in SIS),
160                  into that hnode (see "read_blif -i" for details).  Currently, only the
161                  combinational part of the hnode is written to the blif file.]
162
163  Description   [ This routine determinizes, encodes and writes all blifmv tables
164                  in a hnode to a named blif file.
165                  It also writes encoding information to another named file.
166                  This encoding file must be used while reading back the (optimized)
167                  blif file into blifmv.
168                  The function returns a 0 upon success, 1 in case of failure. It
169                  should be supplied a Io_Encoding_Type_t. Currently only SIMPLE is
170                  supported. Under this scheme, binary encoding is done on the
171                  multi-valued variables, and the binary variable with smallest length
172                  is chosen at any step of the  determinization process. Other parameters
173                  to this function  include a Hrc_Node_t *, and file pointers for the
174                  blif output file and the encoding file. The default blif file is
175                  stdout, and the default encoding file is <model>.enc. A verbosity flag
176                  (valid values are between 0 and 2) print intermediate information to
177                  stdout.
178                  ]
179
180  SideEffects   [ ]
181
182  SeeAlso       [  ]
183  **********************************************************************/
184int
185Io_HnodeWriteBlif(
186    Io_Encoding_Type_t encodingType,
187    Hrc_Node_t *hnode,
188    FILE *fp,
189    FILE *encFp,
190    int verbosity,
191    int combinationalOnly,
192    int makeLatchIOsPOs)
193{
194    Tbl_Table_t *table, *singleOutputTable;
195    Tbl_Entry_t *entry;
196    int i, j, k, numVal, numInputs, numOutputs;
197    Var_Variable_t *var, *actualVar, *outputVar;
198    char *name, *instanceName, *modelName, *newModelName;
199    st_generator *gen;
200    st_table *blifInputsStTable, *blifOutputsStTable, *printedMvsStTable;
201    st_table *encOutputsStTable, *encInputsStTable;
202    Hrc_Node_t *subcktHnode;
203    Hrc_Model_t *model, *subcktModel;
204    Hrc_Subckt_t *subckt;
205    Hrc_Manager_t *manager;
206    array_t *subcktActualInputVars, *subcktActualOutputVars;
207   
208
209    Hrc_NodeForEachNameTable(hnode, i, table){
210      if(_IoCheckPseudoinputIsPO(table)){
211        fprintf(stdout, "Hnode contains a pseudoinput which is also a primary output - quitting\n");
212        return 1;
213      }
214      for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
215        entry = Tbl_TableDefaultReadEntry(table, j);
216        if(entry != NIL(Tbl_Entry_t)){
217          if(Tbl_EntryReadType(entry) == Tbl_EntryNormal_c){
218            if(Tbl_EntryReadNumValues(entry) > 1){
219              outputVar = Tbl_TableReadIndexVar(table, j, 1);
220              (void)fprintf(stdout, "The table with %s as an output has non-singleton default values - quitting\n", Var_VariableReadName(outputVar));
221              return 1;
222            }
223          }
224          else{
225            var = Tbl_EntryReadVar(table, entry);
226            k = Tbl_TableReadVarIndex(table, var, 1);
227            if(k<0){
228              outputVar = Tbl_TableReadIndexVar(table, j, 1);         
229              (void)fprintf(stdout, "Output %s has a default value that refers to an input variable - quitting\n", Var_VariableReadName(outputVar));
230              return 1;
231            }
232          }
233        }
234      }
235    }
236
237    printedMvsStTable = st_init_table(strcmp, st_strhash);
238
239    if(!(combinationalOnly || makeLatchIOsPOs)){
240      fprintf(encFp,"# This encoding file and the blif file that was written out with it cannot\n");           
241      fprintf(encFp,"# currently be read back into VIS. If you would like to read the blif and\n");           
242      fprintf(encFp,"# encoding files back into VIS, then use the 'write_blif -l' or\n");
243      fprintf(encFp,"#'write_blif -c' options.\n");
244    }
245
246  /* .model */
247    modelName = Hrc_NodeReadModelName(hnode);
248    manager = Hrc_NodeReadManager(hnode);
249    model = Hrc_ManagerFindModelByName(manager, modelName);
250    newModelName = ALLOC(char, strlen(modelName) + 256);
251    i = 0;
252    sprintf(newModelName, "%s[%d]", modelName, i);
253
254    while(Hrc_ManagerFindModelByName(manager, newModelName) != NIL(Hrc_Model_t)){
255        i++;
256        sprintf(newModelName, "%s[%d]", modelName, i);
257    }
258    (void)fprintf(encFp,".model %s\n",newModelName);
259    FREE(newModelName);
260    /* .inputs line of enc file*/
261    if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
262        (void)fprintf(encFp,".inputs ");
263        Hrc_NodeForEachFormalInput(hnode,i,var){
264            (void)fprintf(encFp,"%s ",Var_VariableReadName(var));
265        }
266        (void)fprintf(encFp,"\n");
267    }
268   
269    /* .outputs line of enc file*/
270    if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
271        (void)fprintf(encFp,".outputs ");
272        Hrc_NodeForEachFormalOutput(hnode,i,var){
273            (void)fprintf(encFp,"%s ",Var_VariableReadName(var));
274        }
275        (void)fprintf(encFp,"\n");
276    }
277   
278    /* .mv for primary inputs, printed to enc file*/
279    Hrc_NodeForEachFormalInput(hnode,i,var){
280        IoMvCheckPrint(encFp,var,printedMvsStTable);
281    }
282    /* .mv for primary outputs, printed to enc file*/
283    Hrc_NodeForEachFormalOutput(hnode,i,var){
284        IoMvCheckPrint(encFp,var,printedMvsStTable);
285    }
286   
287    /* .subckt stuff */
288    Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
289        subcktModel = Hrc_SubcktReadModel(subckt);
290        subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
291        subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
292        subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);
293       
294        /* .mv for subckt inputs */
295        for (i=0; i < array_n(subcktActualInputVars); i++){
296            var = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
297            IoMvCheckPrint(encFp,var,printedMvsStTable);
298        }
299
300        /* .mv for subckt outputs */
301        for (i=0; i < array_n(subcktActualOutputVars); i++){
302            var = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
303            IoMvCheckPrint(encFp,var,printedMvsStTable);
304        }
305
306        /* .subckt declarations */
307        (void)fprintf(encFp,".subckt %s %s ",
308                      Hrc_ModelReadName(subcktModel), Hrc_SubcktReadInstanceName(subckt));
309        Hrc_NodeForEachFormalInput(subcktHnode,i,var){
310            actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
311            (void)fprintf(encFp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
312        }   
313        Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
314            actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
315            (void)fprintf(encFp,"%s = %s ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
316        }   
317        (void)fprintf(encFp,"\n");
318    }
319
320    encOutputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
321    encInputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
322    blifInputsStTable = st_init_table(strcmp, st_strhash);
323    blifOutputsStTable = st_init_table(strcmp, st_strhash);
324
325    /* encoding tables to .enc file */
326    IoEncWriteMvToBinTables(hnode, encFp, encOutputsStTable, encInputsStTable, combinationalOnly);
327
328    /* decoding tables to .enc file */
329    IoEncWriteBinToMvTables(hnode, encFp, encOutputsStTable, encInputsStTable, combinationalOnly, makeLatchIOsPOs);
330
331    /* if write_blif called without -c or -l options, then print a warning saying
332       that the files cant be read back into vis..
333    */
334    if(!(combinationalOnly || makeLatchIOsPOs)){
335      fprintf(fp,"# This blif file and the encoding file that was written out with it cannot\n");           
336      fprintf(fp,"# currently be read back into VIS. If you would like to read the blif and\n");           
337      fprintf(fp,"# encoding files back into VIS, then use the 'write_blif -l' or\n");
338      fprintf(fp,"#'write_blif -c' options.\n");
339    }
340   
341    /* .inputs declarations for blif file */
342    fprintf(fp,".model %s\n",modelName );     
343    numInputs = IoBlifWriteInputs(hnode, fp, blifInputsStTable, combinationalOnly, makeLatchIOsPOs);
344
345    /* .outputs declarations for blif file */
346    numOutputs = IoBlifWriteOutputs(hnode, fp, blifOutputsStTable, combinationalOnly, makeLatchIOsPOs);
347
348    if((numInputs == 0) && (numOutputs != 0)){
349      fprintf(vis_stderr, "Warning: Blif file has zero inputs\n");
350    }
351    if((numOutputs == 0) && (numInputs != 0)){
352      fprintf(vis_stderr, "Warning: Blif file has zero outputs\n");
353    }
354    if((numInputs == 0) && (numOutputs == 0)){
355      fprintf(vis_stderr, "Warning: Blif file has zero inputs and zero outputs\n");
356    }
357
358    /* .latch declarations for blif file */
359    IoWriteLatches(hnode, fp, encFp, printedMvsStTable, blifOutputsStTable, blifInputsStTable, encOutputsStTable, encInputsStTable, combinationalOnly, makeLatchIOsPOs, verbosity);
360    Hrc_NodeForEachNameTable(hnode, i, table){
361        if((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1)){
362            (void)fprintf(stdout, "Warning: ");
363            Tbl_TableForEachOutputVar(table, j, var){
364                (void)fprintf(stdout, "%s, ", Var_VariableReadName(var));
365            }
366            (void)fprintf(stdout, "assumed to be pseudoinputs\n");
367            Tbl_TableForEachOutputVar(table, j, var){
368                singleOutputTable = Tbl_TableAlloc();
369                Tbl_TableAddColumn(singleOutputTable, var, 1);
370                (void) Tbl_TableAddRow(singleOutputTable);
371                entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
372                numVal = Var_VariableReadNumValues(var);
373                Tbl_EntrySetValue(entry, 0, numVal - 1);
374                Tbl_TableSetEntry(singleOutputTable, entry, 0, 0, 1);
375                _IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
376                                  verbosity);
377                Tbl_TableFree(singleOutputTable);
378            }
379        }
380        else{
381          if(IoOutputExpansionRequired(table)){
382            if(verbosity > 0){
383              (void)fprintf(stdout, "Splitting into Single Output Table before Processing\n");
384            }
385            for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
386              singleOutputTable = IoMakeSingleOutputTable(table, j);
387              _IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
388                                verbosity);
389              Tbl_TableFree(singleOutputTable);
390            }
391          }
392          else{
393            if(!((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1))){
394              _IoTableWriteBlif(encodingType, hnode, table, blifInputsStTable, fp, encFp,
395                                verbosity);
396            }
397          }
398        }
399    }
400    st_foreach_item_int(blifInputsStTable, gen, &name, &i){
401        FREE(name);
402    }
403    st_free_table(blifInputsStTable);
404    st_foreach_item_int(blifOutputsStTable, gen, &name, &i){
405        FREE(name);
406    }
407    st_free_table(blifOutputsStTable);
408    st_free_table(encInputsStTable);
409    st_free_table(encOutputsStTable);
410    st_foreach_item_int(printedMvsStTable, gen, &name, &i){
411        FREE(name);
412    }
413    st_free_table(printedMvsStTable);
414    /* printing an empty .exdc network keeps sis from sweeping away the
415       dummy buffers that latch outputs are made to drive as a result of the
416       "write_blif -l" cmd. The dummy buffers were added because if they were
417       not present, sis would introduce buffers whenever latch outputs drive POs
418       directly (in the "xdc" command), ruining the name correspondence required
419       for read_blif to work and reinstate mv latches.
420    */
421    fprintf(fp,".exdc\n");
422    fprintf(fp,".end\n");
423    if(encFp != stdout){
424      (void) fclose(encFp);
425    }
426    return 0;
427}
428
429
430/*---------------------------------------------------------------------------*/
431/* Definition of internal functions                                          */
432/*---------------------------------------------------------------------------*/
433
434   
435/*---------------------------------------------------------------------------*/
436/* Definition of static functions                                            */
437/*---------------------------------------------------------------------------*/
438
439
440/**Function***********************************************************
441
442
443  Synopsis      [ Determinize, encode and write a blifmv table to blif file ]
444
445  Description   [ Note that this routine cannot handle the "=" construct of
446                  blifmv. It is my opinion that a front-end routine should be
447                  used to remove the "="'s. ]
448
449  SideEffects   [ ]
450
451  SeeAlso       [  ]
452  **********************************************************************/
453static int
454_IoTableWriteBlif(
455    Io_Encoding_Type_t encodingType,
456    Hrc_Node_t *hnode,           
457    Tbl_Table_t *origBlifmvTable,
458    st_table *blifInputsStTable,
459    FILE *fp,
460    FILE *encFp,
461    int verbosity )
462{
463    IoBlifInfo_t *blifInfo;
464
465    blifInfo = ALLOC(IoBlifInfo_t, 1);
466    if(verbosity > 1){
467        (void)fprintf(stdout, "Original Blifmv Table :\n");
468        Tbl_TableWriteBlifMvToFile(origBlifmvTable, 0, stdout);
469    }
470    IoInitBlifInfo(blifInfo, origBlifmvTable, fp, encFp, verbosity);
471    if(encodingType == SIMPLE){
472        if(_IoMakeInitialEncodings(blifInfo, hnode)){
473            blifInfo->binTblArray = array_alloc(Tbl_Table_t *, 0);
474            IoFreeBlifInfo(blifInfo);
475            return 0;
476        }
477        _IoDeterminizeEncodeOutputPart(blifInfo, blifInputsStTable);
478        _IoMakeBinTable(blifInfo);
479        if(blifInfo->verbosity > 0){
480            (void)fprintf(stdout, "Done with Output Singletonization\n");
481        }
482        if(blifInfo->verbosity > 1){
483            (void)fprintf(stdout, "Final Blifmv Table After Output Singletonization:\n");
484            Tbl_TableWriteBlifMvToFile(blifInfo->blifmvTable, 0, stdout);   
485            (void)fprintf(stdout, "Bin Table After Output Singletonization:\n");
486            Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);   
487        }
488        _IoDeterminizeEncodeRows(blifInfo, blifInputsStTable);     
489        if(blifInfo->verbosity > 0){
490            (void)fprintf(stdout, "Done with Row Intersection and Determinization\n");
491        }
492        if(blifInfo->verbosity > 1){
493            (void)fprintf(stdout, "Final Bin Table After Determinization \n");
494            Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);   
495        }
496        _IoMakeDcTables(blifInfo);
497        blifInfo->binTblArray = Tbl_TableSplit(blifInfo->binTable);
498        IoWriteBinTablesToFile(blifInfo);
499        IoFreeBlifInfo(blifInfo);
500        return 0;
501    }
502    else{
503        (void)fprintf(vis_stderr, "This encoding strategy has not been implemented yet\n");
504        return 1;
505    }
506}
507 
508
509/**Function********************************************************************
510
511  Synopsis    [Encodes variables based on their ranges]
512
513  Description [Returns encodings in the form of an array of tables for each
514               multivalued variable. ]
515
516  SideEffects [Populates the array of tables describing the encoding]
517
518  SeeAlso     []
519
520******************************************************************************/
521static int
522_IoMakeInitialEncodings(
523   IoBlifInfo_t *blifInfo,
524   Hrc_Node_t *hnode                   
525   )
526{
527    Var_Variable_t *var, *origVar;
528    int i, colnum, numRows, numValues, varRange, value, numEncBits;
529    char *name, *varname, *dupName;
530    Tbl_Entry_t *entry, *newEntry, *defEntry, *newDefEntry;
531    lsGen gen;
532    Tbl_Range_t *range;
533    Tbl_Table_t *table, *origTable;
534
535    if(Tbl_TableReadNumInputs(blifInfo->blifmvTable) == 0){
536        value = -1;
537        if(Tbl_TableReadNumRows(blifInfo->blifmvTable) != 0){
538          entry = Tbl_TableReadEntry(blifInfo->blifmvTable, 0, 0, 1);
539          numValues = Tbl_EntryReadNumValues(entry);
540        }
541        else{
542          entry = Tbl_TableDefaultReadEntry(blifInfo->blifmvTable, 0);
543          numValues = Tbl_EntryReadNumValues(entry);
544        }
545        origTable = Tbl_TableHardDup(blifInfo->blifmvTable);
546
547        if(Tbl_TableReadNumRows(blifInfo->blifmvTable) <= 1){
548            if(numValues == 1){
549            /* not a pseudoinput */
550                Tbl_EntryForEachValue(entry, value, gen, range);
551                assert(value != -1);
552                var = Tbl_TableReadIndexVar(blifInfo->blifmvTable, 0, 1);
553                varRange = Var_VariableReadNumValues(var);
554                numEncBits = IoNumEncBits(varRange);
555                varname = Var_VariableReadName(var);
556                for(i = numEncBits - 1; i >= 0; i--){
557                    dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
558                    sprintf(dupName, "%s%d", varname, i);
559                    (void)fprintf(blifInfo->BlifFp, ".names %s\n", dupName);
560                    FREE(dupName);
561                    if(value > (int) pow((double) 2, (double) i)){
562                        (void)fprintf(blifInfo->BlifFp, "1\n");
563                        value -= (int) pow((double) 2, (double) i);
564                    }
565                    else{
566                        (void)fprintf(blifInfo->BlifFp, "0\n");
567                    }
568                }
569                Tbl_TableFree(origTable);
570                return 1;
571            }
572            else{
573                /* is a pseudoinput! */
574                /* make it look like a table with many rows, and singleton output entries per row */
575                table = Tbl_TableAlloc();
576
577                Tbl_TableForEachOutputVar(blifInfo->blifmvTable, i, var){
578                    Tbl_TableAddColumn(table, var, 1);
579                }
580                Tbl_TableForEachDefaultEntry(blifInfo->blifmvTable, defEntry, i) {
581                    if (defEntry != NIL(Tbl_Entry_t)) {
582                        newDefEntry = Tbl_EntryDup(defEntry);
583                    }
584                    else {
585                        newDefEntry = NIL(Tbl_Entry_t);
586                    }
587                    (void) Tbl_TableDefaultSetEntry(table, newDefEntry, i);
588                }
589                Tbl_EntryForEachValue(entry, value, gen, range){
590                    i = Tbl_TableAddRow(table);
591                    newEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
592                    Tbl_EntrySetValue(newEntry, value, value);
593                    Tbl_TableSetEntry(table, newEntry, i, 0, 1);
594                }
595                Tbl_TableFree(blifInfo->blifmvTable);
596                blifInfo->blifmvTable = table;
597            }
598        }
599        /* it is a pseudoinput, and has been singletonized wrt outputs */
600        if(Tbl_TableReadNumRows(blifInfo->blifmvTable) > 1){
601            name = ALLOC(char, 256);
602            i = 0;
603            sprintf(name, "[%d]", i);
604            while(!(Hrc_NodeFindVariableByName(hnode, name) == NULL)){ 
605                i++;
606                sprintf(name, "[%d]", i);
607            }
608           
609            blifInfo->pseudoinputFlag = TRUE;
610            var = Var_VariableAlloc(hnode, name);
611            Tbl_TableAddColumn(blifInfo->blifmvTable, var, 0);
612            (void)fprintf(blifInfo->BlifFp, ".inputs %s0\n", name);
613            origVar = Tbl_TableReadIndexVar(origTable, 0, 1);
614            IoMvPrint(blifInfo->EncFp, origVar);
615            Tbl_TableWriteBlifMvToFile(origTable, 0, blifInfo->EncFp);   
616            Tbl_TableFree(origTable);
617            numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
618            for(i = 0; i < numRows; i++){
619                if(i % 2 == 1){
620                    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
621                    Tbl_EntrySetValue(entry, 1, 1);
622                    Tbl_TableSetEntry(blifInfo->blifmvTable, entry, i, 0, 0);
623                }
624                else{
625                    entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
626                    Tbl_EntrySetValue(entry, 0, 0);
627                    Tbl_TableSetEntry(blifInfo->blifmvTable, entry, i, 0, 0);
628                }
629            }
630            FREE(name);
631        }
632    }
633
634    Tbl_TableForEachInputVar(blifInfo->blifmvTable, colnum, var){
635        IoEncodeVariable(blifInfo, var, colnum, 0);
636    }
637
638    Tbl_TableForEachOutputVar(blifInfo->blifmvTable, colnum, var){
639        IoEncodeVariable(blifInfo, var, colnum, 1);
640    }
641    return 0;
642}
643
644
645/**Function********************************************************************
646
647  Synopsis    [Encodes variables to make singleton output values in every row]
648
649  Description [Returns modified table along with a modified array of tables for
650               encoding the multivalued variables. If the original table
651               has singleton output values then it is returned unmodified,
652               with the unmodified variable encoding tables.]
653
654  SideEffects [Potentially modifies the array of tables describing the encoding]
655
656  SeeAlso     []
657
658******************************************************************************/
659static void
660_IoDeterminizeEncodeOutputPart( 
661   IoBlifInfo_t *blifInfo,
662   st_table *blifInputsStTable
663   )
664{
665    Tbl_Entry_t *entry;
666    int numValues, i, j, numRows, numOutputs;
667    IoVarEncEntry_t *varEnc;
668    array_t *MvOutputArray;
669
670    numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
671    numOutputs = Tbl_TableReadNumOutputs(blifInfo->blifmvTable);
672    for(i = 0; i < numRows; i++){
673        MvOutputArray = array_alloc(int, 0);
674        numValues = 1;
675        for(j = 0; j < numOutputs; j++){
676            entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, j, 1);
677            numValues *= Tbl_EntryReadNumValues(entry);
678            array_insert_last(int, MvOutputArray, Tbl_EntryReadNumValues(entry));
679        }
680        if(numValues > 1){
681            varEnc = IoFindSmallestCode(blifInfo);
682            if(blifInfo->verbosity > 2){
683                (void)fprintf(stdout, "Singletonizing Outputs in Row %d\n", i);
684                (void)fprintf(stdout, "Best Variable is %s\n", Var_VariableReadName(varEnc->variable));
685            }
686            IoIncreaseCodeSize(varEnc, numValues, blifInfo->verbosity);
687            IoChangeBlifmvTableEntries(blifInfo, i, numValues, varEnc, MvOutputArray);
688            IoChangeEncTableEntries(blifInfo, blifInputsStTable, varEnc, numValues);
689            i = -1;
690            array_free(MvOutputArray);
691           
692            if(blifInfo->verbosity > 2){
693                (void)fprintf(stdout, "Blifmv Table After Output Singletonization\n");
694                Tbl_TableWriteBlifMvToFile(blifInfo->blifmvTable, 0, stdout);   
695            }
696        }
697        else{
698            array_free(MvOutputArray);
699        }
700    }
701}
702
703
704/**Function********************************************************************
705
706  Synopsis    [Encodes variables to make table deterministic]
707
708  Description [Returns modified table along with a modified array of tables for
709               encoding the multivalued variables. If the original table
710               is deterministic, then it is returned unmodified,
711               with the unmodified variable encoding tables.]
712
713  SideEffects [Potentially modifies the array of tables describing the encoding]
714
715  SeeAlso     []
716
717******************************************************************************/
718static void
719_IoDeterminizeEncodeRows( 
720   IoBlifInfo_t *blifInfo,
721   st_table *blifInputsStTable
722   )
723{
724    int i, j, k, numRows, numOutputs, numInputs, mvValue;
725    boolean rowsIntersect;
726    IoVarEncEntry_t *varEnc;
727    char *pseudoInputName, *realPseudoInputName;
728    Var_Variable_t *outvar, *var, *origVar;
729    Tbl_Entry_t *entry;
730   
731   
732    numRows = Tbl_TableReadNumRows(blifInfo->binTable);
733    for(i = 0; i < numRows; i++){
734        for(j = i + 1; j < numRows; j++){       
735            if(blifInfo->verbosity > 2){
736                (void)fprintf(stdout, "Intersecting Rows %d and %d \n", i, j);
737            }
738            rowsIntersect = Tbl_RowInputIntersect(blifInfo->binTable, i, j); 
739            if(rowsIntersect == 1){ 
740                if(blifInfo->verbosity > 2){
741                    (void)fprintf(stdout, "Input Intersection non-null\n");
742                }
743                if(!Tbl_RowOutputIntersect(blifInfo->binTable, i, j)){
744                    varEnc = IoFindSmallestCode(blifInfo);
745                    if(blifInfo->verbosity > 2){
746                        (void)fprintf(stdout, "Output Intersection null\n");
747                        (void)fprintf(stdout, "Best Variable is %s\n", Var_VariableReadName(varEnc->variable));
748
749                    }
750                    IoIncreaseCodeSize(varEnc, 2, blifInfo->verbosity); 
751                    IoChangeBlifmvTableRows(blifInfo, varEnc, i, j);
752                    IoChangeEncTableEntries(blifInfo, blifInputsStTable, varEnc, 2); 
753                   
754                    if(blifInfo->verbosity > 2){
755                        (void)fprintf(stdout, "Bin Table After Row Overlap elimination \n");
756                        Tbl_TableWriteBlifMvToFile(blifInfo->binTable, 0, stdout);   
757                    }
758                }
759            }
760        }
761    }
762    if(blifInfo->pseudoinputFlag == TRUE){
763        /* pseudoinput cant have .def construct */
764        outvar = Tbl_TableReadIndexVar(blifInfo->binTable, 0, 1);
765        pseudoInputName = Var_VariableReadName(outvar);
766        realPseudoInputName = ALLOC(char, strlen(pseudoInputName) + 2);
767        sprintf(realPseudoInputName, "%s", pseudoInputName);
768        realPseudoInputName[strlen(pseudoInputName) - 1] = '\0';
769        numOutputs = Tbl_TableReadNumOutputs(blifInfo->binTable);
770        numInputs = Tbl_TableReadNumInputs(blifInfo->binTable);
771        for(i = 0; i < numInputs; i++){
772            (void)fprintf(blifInfo->EncFp, ".table %s ->", realPseudoInputName);
773            var = Tbl_TableReadIndexVar(blifInfo->binTable, i, 0);
774            (void)fprintf(blifInfo->EncFp, "%s\n", Var_VariableReadName(var));         
775            (void)fprintf(blifInfo->EncFp, ".default 0\n");
776            for(j = 0; j < numRows; j++){
777                mvValue = 0;
778                for(k = 0; k < numOutputs; k++){
779                    entry = Tbl_TableReadEntry(blifInfo->binTable, j, k, 1);
780                    if(Tbl_EntryCheckRange(entry, 1, 1)){
781                        mvValue += (int) pow((double)2, (double) k);
782                    }
783                }
784                origVar = Tbl_TableReadIndexVar(blifInfo->blifmvTable, 0, 1);
785                if(Var_VariableTestIsSymbolic(origVar)){
786                    (void)fprintf(blifInfo->EncFp, "%s ",
787                                  Var_VariableReadSymbolicValueFromIndex(origVar, mvValue));               
788                }
789                else{
790                    (void)fprintf(blifInfo->EncFp, "%d ", mvValue);
791                }
792
793                entry = Tbl_TableReadEntry(blifInfo->binTable, j, i, 0);
794                if(Tbl_EntryCheckRange(entry, 1, 1)){
795                    (void)fprintf(blifInfo->EncFp, "%d\n", 1);
796                }
797                else{ 
798                    if(Tbl_EntryCheckRange(entry, 0, 0)){
799                        (void)fprintf(blifInfo->EncFp, "%d\n", 0);
800                    }
801                    else{
802                        (void)fprintf(blifInfo->EncFp, "-\n");
803                    }
804                }
805            }
806        }
807        FREE(realPseudoInputName);
808    }
809}
810
811
812/**Function********************************************************************
813
814  Synopsis    [Creates Dont-Care Tables for Variable Encodings]
815
816  Description [For each table in the blifInfo->inputEncTblArray, this
817               function creates dont-care tables]
818
819  SideEffects []
820
821  SeeAlso     []
822
823******************************************************************************/
824static void
825_IoMakeDcTables( 
826   IoBlifInfo_t *blifInfo
827   )
828{
829}
830
831
832
833/**Function********************************************************************
834
835  Synopsis    [Writes out blifmvTable to binTable in encoded form]
836
837  Description []
838
839  SideEffects []
840
841  SeeAlso     []
842
843******************************************************************************/
844static void
845_IoMakeBinTable( 
846  IoBlifInfo_t *blifInfo
847  )
848{
849    int i, j, k, m, n, colnum, numRowsAfterExpansion, numEncBits;
850    int rootCol, rootRow, entryRepetitionCount, numCycles, value, numBits, currRow;
851    int numOutputs, numRows, numInputs, defValue, varRange;
852    Tbl_Entry_t *entry, *workingEntry;
853    array_t *binRangesArray, *mvEntryBinRanges;
854    IoVarEncEntry_t *varEnc;
855    char *varname, *dupName;
856    Var_Variable_t *var;
857    lsGen gen, gen2;
858    Tbl_Range_t *range, *range2;
859    IoBinRangeEntry_t *binRangeEntry;
860   
861   
862    /* initialize the binTable, defining input vars etc   */
863   
864    numRows = Tbl_TableReadNumRows(blifInfo->blifmvTable);
865    numInputs = Tbl_TableReadNumInputs(blifInfo->blifmvTable);
866    numOutputs = Tbl_TableReadNumOutputs(blifInfo->blifmvTable);
867    for(j = 0; j < Tbl_TableReadNumInputs(blifInfo->blifmvTable); j++){
868        varEnc = array_fetch(IoVarEncEntry_t *, blifInfo->inputEncTblArray, j);
869        numEncBits = varEnc->numEncBits;
870        for(k = 0; k < numEncBits ; k++){
871            varname = Var_VariableReadName(varEnc->variable);
872            dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
873            sprintf(dupName, "%s%d", varname, k);
874            var = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
875            FREE(dupName);
876            array_insert_last(Var_Variable_t *, blifInfo->varArray, var);
877            colnum = Tbl_TableAddColumn(blifInfo->binTable, var, 0);
878        }
879    }
880   
881    for(j = 0; j < Tbl_TableReadNumOutputs(blifInfo->blifmvTable); j++){
882        varEnc = array_fetch(IoVarEncEntry_t *, blifInfo->outputEncTblArray, j);
883        numEncBits = varEnc->numEncBits;
884        for(k = 0; k < numEncBits ; k++){
885            varname = Var_VariableReadName(varEnc->variable);
886            dupName = ALLOC(char, strlen(varname) + IoNumDigits(numEncBits) + 2);
887            sprintf(dupName, "%s%d", varname, k);
888            var = Var_VariableAlloc(NIL(Hrc_Node_t), dupName);
889            FREE(dupName);
890            array_insert_last(Var_Variable_t *, blifInfo->varArray, var);
891            colnum = Tbl_TableAddColumn(blifInfo->binTable, var, 1);
892        }
893    }
894   
895   
896/*
897    fprintf(stdout, "\n");   
898*/
899    for(i = 0; i < numRows; i++){
900       
901        /* make temp array of number of values for each input var  */
902        numRowsAfterExpansion = 1;
903        binRangesArray = array_alloc(array_t *, 0);
904       
905        for(colnum = 0; colnum < numInputs; colnum++){
906            entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, colnum, 0);
907            workingEntry = Tbl_EntryDup(entry);
908            mvEntryBinRanges = IoMakeBinaryRangesArray(workingEntry, colnum, blifInfo);
909            numRowsAfterExpansion *= array_n(mvEntryBinRanges);
910            array_insert_last(array_t *, binRangesArray, mvEntryBinRanges); 
911        }
912
913/*
914        for(j = 0; j < array_n(binRangesArray); j++){
915            mvEntryBinRanges = array_fetch(array_t *, binRangesArray, j);
916            for(k = 0; k < array_n(mvEntryBinRanges); k++){
917                binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, k);
918                fprintf(stdout, "start %d\t runlen%d\t skip %d\n", binRangeEntry->startValue, binRangeEntry->runLength, binRangeEntry->skipLength);
919            }
920            (void)fprintf(stdout, "\n");
921        }
922        fprintf(stdout, "numRowsAfterExpansion %d\n", numRowsAfterExpansion);
923
924*/
925        /* add numRowsAfterExpansion rows to binTable */
926       
927        rootCol = 0;
928        rootRow = Tbl_TableReadNumRows(blifInfo->binTable);
929        for(j = 0; j < numRowsAfterExpansion; j++){
930            Tbl_TableAddRow(blifInfo->binTable);
931        }
932
933        /* write out binary encoded variable values for the determinized, encoded blifmvTable
934           (input parts) */
935
936        entryRepetitionCount = numRowsAfterExpansion;
937        m = 0;
938        numCycles = 1;
939
940        for(colnum = 0; colnum < numInputs; colnum++){
941            mvEntryBinRanges = array_fetch(array_t *, binRangesArray, colnum);
942            currRow = rootRow;
943            rootCol += IoNumBinVars(colnum, blifInfo->inputEncTblArray);
944            entryRepetitionCount = entryRepetitionCount / array_n(array_fetch(array_t *, binRangesArray, m));
945            numCycles *= IoNumValuesFromBinRangesArray(colnum, binRangesArray);
946            numBits = IoNumBinVars(colnum + 1, blifInfo->inputEncTblArray);
947            for(k=0; k<numCycles; k++){
948                for(n = 0; n < array_n(mvEntryBinRanges); n++){
949                    binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, n);
950                    IoWriteExpandedValueToBinTable(blifInfo->binTable, currRow, rootCol, binRangeEntry, entryRepetitionCount, numBits, 0);
951                    currRow = currRow + entryRepetitionCount;
952                }
953            }
954            m++;
955        }
956
957        /* write out binary encoded variable values for the determinized, encoded blifmvTable
958           (output parts) */
959
960        rootCol = 0;
961
962        for(colnum = 0; colnum < numOutputs; colnum++){
963            entry = Tbl_TableReadEntry(blifInfo->blifmvTable, i, colnum, 1);
964            rootCol += IoNumBinVars(colnum, blifInfo->outputEncTblArray);
965            numBits = IoNumBinVars(colnum + 1, blifInfo->outputEncTblArray);
966            Tbl_EntryForEachValue(entry, value, gen, range){
967                binRangeEntry = ALLOC(IoBinRangeEntry_t, 1);
968                binRangeEntry->startValue = value;
969                binRangeEntry->runLength = 1;
970                binRangeEntry->skipLength = 1;
971                IoWriteExpandedValueToBinTable(blifInfo->binTable, rootRow, rootCol, binRangeEntry, numRowsAfterExpansion, numBits, 1);
972                FREE(binRangeEntry);
973            }
974        }
975        for(j = 0; j < array_n(binRangesArray); j++){
976            mvEntryBinRanges = array_fetch(array_t *, binRangesArray, j);
977            for(n = 0; n < array_n(mvEntryBinRanges); n++){
978                binRangeEntry = array_fetch(IoBinRangeEntry_t *, mvEntryBinRanges, n);
979                FREE(binRangeEntry);
980            }
981            array_free(mvEntryBinRanges);
982        }
983        array_free(binRangesArray);
984    }
985   
986    rootCol = 0;
987    Tbl_TableForEachOutputVar(blifInfo->blifmvTable, colnum, var){
988        entry = Tbl_TableDefaultReadEntry(blifInfo->blifmvTable, colnum);
989        if(entry != NIL(Tbl_Entry_t)){
990            varRange = Var_VariableReadNumValues(var);
991            numEncBits = IoNumEncBits(varRange);
992            defValue = -1;
993            Tbl_EntryForEachValue(entry, value, gen2, range2){
994                defValue = value;
995                assert(defValue != -1);
996            }
997            for(j = numEncBits - 1; j >= 0; j--){
998                if(((int)(defValue / pow((double) 2, (double) j))) == 1){
999                    IoInvertBinTableOutput(blifInfo, rootCol + j);
1000                    defValue = defValue - (int)pow((double)2,(double)j);
1001                }
1002            }
1003            rootCol += numEncBits;
1004        }
1005    }
1006}
1007
1008
1009/**Function********************************************************************
1010
1011  Synopsis    [Checks that all hnodes rooted at the give hnode are boolean and
1012               deterministic]
1013
1014  Description []
1015
1016  SideEffects []
1017
1018  SeeAlso     []
1019
1020******************************************************************************/
1021static int
1022_IoCheckHnodeTreeIsBooleanAndDeterministic(
1023  mdd_manager **mddMgr,                               
1024  Hrc_Node_t *hnode, 
1025  st_table *modelTable,
1026  boolean *pSymVarsPresent,
1027  int verbosity
1028  )
1029{
1030  char *modelName, *childName;
1031  Hrc_Model_t *model;
1032  st_generator *stGen;
1033  Hrc_Manager_t *manager; 
1034  Hrc_Node_t *childNode;
1035
1036  manager = Hrc_NodeReadManager(hnode);
1037  /* enter current model in modelTable */
1038  modelName = Hrc_NodeReadModelName(hnode);
1039  model = Hrc_ManagerFindModelByName(manager, modelName);
1040  if(st_is_member(modelTable, (char *) model)){
1041    return 0;
1042  }
1043  else{
1044    st_insert(modelTable, (char *)model, (char *) (long) (-1));
1045  }
1046 
1047  if(_IoCheckHnodeIsBooleanAndDeterministic(mddMgr, hnode, pSymVarsPresent)){
1048    if(verbosity > 1){
1049      fprintf(vis_stderr, "Model %s is NOT boolean and deterministic\n", modelName);
1050    }
1051    return 1;
1052  }
1053  if(verbosity > 1){
1054    fprintf(vis_stderr, "Model %s is boolean and deterministic\n", modelName);
1055  }
1056  Hrc_NodeForEachChild(hnode, stGen, childName, childNode){
1057    if(_IoCheckHnodeTreeIsBooleanAndDeterministic(mddMgr, childNode, modelTable, pSymVarsPresent, verbosity)){
1058      st_free_gen(stGen);
1059      return 1;
1060    }
1061  }
1062  return 0;
1063}
1064
1065
1066/**Function********************************************************************
1067
1068  Synopsis    [Checks that the given hnode is boolean and deterministic]
1069
1070  Description []
1071
1072  SideEffects []
1073
1074  SeeAlso     []
1075
1076******************************************************************************/
1077static int
1078_IoCheckHnodeIsBooleanAndDeterministic(
1079  mdd_manager **mddMgr,                               
1080  Hrc_Node_t *hnode,
1081  boolean *pSymVarsPresent
1082  )
1083{
1084 
1085  /* check that variables of all models are boolean */
1086  if(_IoCheckHnodeVarsAreBoolean(hnode, pSymVarsPresent)){
1087    return 1;
1088  }
1089
1090  /* check that latch resets of all models are either 0/1/2 */
1091  if(_IoCheckHnodeLatchResetIsConstant(hnode)){
1092    return 1;
1093  }
1094
1095  /* check that tables of all models are deterministic */
1096  if(_IoCheckHnodeTablesAreDeterministic(mddMgr, hnode)){
1097    return 1;
1098  }
1099
1100  return 0;
1101}
1102
1103/**Function********************************************************************
1104
1105  Synopsis    [Checks that the variables of a model are boolean]
1106
1107  Description []
1108
1109  SideEffects []
1110
1111  SeeAlso     []
1112
1113******************************************************************************/
1114static int
1115_IoCheckHnodeVarsAreBoolean(
1116  Hrc_Node_t *hnode,
1117  boolean *pSymVarsPresent
1118  )
1119{
1120  st_generator *stGen;
1121  char *varName;
1122  Var_Variable_t *var;
1123 
1124  Hrc_NodeForEachVariable(hnode, stGen, varName, var){
1125    if(Var_VariableReadNumValues(var) > 2){
1126      fprintf(vis_stderr, "Variable %s is not boolean - quitting.\n", varName);     
1127      st_free_gen(stGen);
1128      return 1;
1129    }
1130    if(Var_VariableTestIsSymbolic(var)){
1131      *pSymVarsPresent = TRUE;
1132    }
1133  }
1134  return 0;
1135}
1136
1137
1138/**Function********************************************************************
1139
1140  Synopsis    [Checks that the latches of a model have constant reset tables]
1141
1142  Description []
1143
1144  SideEffects []
1145
1146  SeeAlso     []
1147
1148******************************************************************************/
1149static int
1150_IoCheckHnodeLatchResetIsConstant(
1151  Hrc_Node_t *hnode
1152  )
1153{
1154  st_generator *stGen;
1155  char *latchName;
1156  Hrc_Latch_t *latch;
1157  boolean test;
1158  Tbl_Table_t *table, *resetTable;
1159  Tbl_Entry_t *entry;
1160  Var_Variable_t *var, *parentVar;
1161  int i, j;
1162
1163  Hrc_NodeForEachLatch(hnode, stGen, latchName, latch){
1164    resetTable = Hrc_LatchReadResetTable(latch);
1165    test = Tbl_TableTestIsConstant(resetTable, 0);
1166    /*
1167      Tbl_TableTestIsConstant gives 0 result for reset tables of
1168      the type .reset a ->b; - =a; where a is a constant defined
1169      in another table. So check for this case as well.
1170      */
1171    if(test == FALSE){
1172      if(Tbl_TableReadNumRows(resetTable) == 1){
1173        entry = Tbl_TableReadEntry(resetTable, 0, 0, 1);
1174        if(Tbl_EntryReadType(entry) == Tbl_EntryEqual_c){
1175          parentVar = Tbl_EntryReadVar(resetTable, entry);
1176          Hrc_NodeForEachNameTable(hnode, i, table){
1177            Tbl_TableForEachOutputVar(table, j, var){
1178              if(var == parentVar){
1179                test = Tbl_TableTestIsConstant(table, j);
1180              }
1181            }
1182          }
1183        }
1184      }
1185    }
1186    if (test == FALSE){
1187      fprintf(vis_stderr, "Latch %s has a non-constant reset value - quitting.\n", latchName);
1188      st_free_gen(stGen);
1189      return 1;
1190    }
1191  }
1192  return 0;
1193}
1194
1195/**Function********************************************************************
1196
1197  Synopsis    [Checks that all tables in a model are deterministic]
1198
1199  Description []
1200
1201  SideEffects []
1202
1203  SeeAlso     []
1204
1205******************************************************************************/
1206static int
1207_IoCheckHnodeTablesAreDeterministic(
1208  mdd_manager **mddMgr,                             
1209  Hrc_Node_t *hnode
1210  )
1211{
1212  int i, j, k, index, colNum, offset, numInputs;
1213  Tbl_Table_t *table;
1214  Var_Variable_t *inputVar, *outputVar, *var;
1215  Mvf_Function_t *faninMvf, *outMvf;
1216  array_t *faninMvfArray;
1217  array_t *mvarValues;
1218  Tbl_Entry_t *entry;
1219
1220
1221  /* note that reset tables are not handled here */
1222  Hrc_NodeForEachNameTable(hnode, i, table){
1223    Tbl_TableForEachOutputVar(table, index, outputVar){
1224
1225      faninMvfArray = array_alloc(Mvf_Function_t *, 0);
1226      mvarValues = array_alloc(int, 0);
1227     
1228      /* Create MDD variables for the table inputs. */
1229      Tbl_TableForEachInputVar(table, colNum, inputVar) {
1230        array_insert_last(int, mvarValues, Var_VariableReadNumValues(inputVar));
1231      }
1232      offset = array_n(mdd_ret_mvar_list(*mddMgr));  /* number of existing mvars */
1233      mdd_create_variables(*mddMgr, mvarValues, NIL(array_t), NIL(array_t));
1234      array_free(mvarValues);
1235     
1236      /*
1237       * Construct an MVF for each table input. The MVF for column j is the MVF
1238       * for MDD variable j.
1239       */
1240     
1241      numInputs = Tbl_TableReadNumInputs(table );
1242      for (j = 0; j < numInputs; j++) {
1243        faninMvf = Mvf_FunctionCreateFromVariable(*mddMgr, (j + offset));
1244        array_insert_last(Mvf_Function_t *, faninMvfArray, faninMvf);
1245      }
1246     
1247      /* Compute the MVF of the output indexed by index. */
1248      outMvf = Tbl_TableBuildMvfFromFanins(table, index, faninMvfArray, *mddMgr);
1249      Mvf_FunctionArrayFree(faninMvfArray);
1250     
1251      /*
1252       * If the function is a non-deterministic constant, or it has some
1253       * inputs, and is non-deterministic, then fail
1254       */
1255      if((numInputs > 0) && !Mvf_FunctionTestIsDeterministic(outMvf)){
1256        (void) fprintf(vis_stderr, "Table %s is non-deterministic - quitting\n", Var_VariableReadName(outputVar));
1257        Mvf_FunctionFree(outMvf);
1258        return 1;
1259      }
1260      if(Mvf_FunctionTestIsNonDeterministicConstant(outMvf)){
1261        (void) fprintf(vis_stderr, "Table %s is a non-deterministic constant - quitting\n", Var_VariableReadName(outputVar));
1262        Mvf_FunctionFree(outMvf);
1263        return 1;
1264      }
1265      if (!Mvf_FunctionTestIsCompletelySpecified(outMvf)) {
1266        (void) fprintf(vis_stderr, "Table %s is not completely specified - quitting\n", Var_VariableReadName(outputVar));
1267        Mvf_FunctionFree(outMvf);
1268        return 1; 
1269      } 
1270      Mvf_FunctionFree(outMvf);
1271      _MddManagerResetIfNecessary(mddMgr);
1272
1273    }
1274  }
1275
1276  Hrc_NodeForEachNameTable(hnode, i, table){
1277    for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
1278      entry = Tbl_TableDefaultReadEntry(table, j);
1279      if(entry != NIL(Tbl_Entry_t)){
1280        if(Tbl_EntryReadType(entry) == Tbl_EntryNormal_c){
1281          if(Tbl_EntryReadNumValues(entry) > 1){
1282            outputVar = Tbl_TableReadIndexVar(table, j, 1);
1283            (void)fprintf(stdout, "The table with %s as an output has non-singleton default values - quitting\n", Var_VariableReadName(outputVar));
1284            return 1;
1285          }
1286        }
1287        else{
1288          var = Tbl_EntryReadVar(table, entry);
1289          k = Tbl_TableReadVarIndex(table, var, 1);
1290          if(k<0){
1291            outputVar = Tbl_TableReadIndexVar(table, j, 1);
1292            (void)fprintf(stdout, "Output %s has a default value that refers to an input variable - quitting\n", Var_VariableReadName(outputVar));
1293            return 1;
1294          }
1295        }
1296      }
1297    }
1298  }
1299  return 0;
1300}
1301
1302
1303/**Function********************************************************************
1304
1305  Synopsis    [Potentially quits mddMgr and starts a new one.]
1306
1307  Description [Quits mddMgr if the number of binary variables exceeds
1308  MAX_NUMBER_BDD_VARS, and starts a new manager with no variables.
1309  Initializing an empty MDD manager is costly in some BDD packages, so we want
1310  to avoid doing it often (say, once per table).  On the other hand, we don't
1311  want the manager to have too many variables, because then reordering becomes
1312  expensive.]
1313
1314  SideEffects []
1315
1316******************************************************************************/
1317static void
1318_MddManagerResetIfNecessary(
1319  mdd_manager **mddMgr)
1320{
1321  if (bdd_num_vars(*mddMgr) > MAX_NUMBER_BDD_VARS) {
1322    mdd_quit(*mddMgr);
1323    *mddMgr = mdd_init_empty();
1324  }
1325}
1326
1327
1328
1329/**Function********************************************************************
1330
1331  Synopsis    [Write out a Hnode and recurse on its children]
1332
1333  Description [Call the function to write out the given hnode in blif, and
1334  recursively call the same function on its children.]
1335
1336  SideEffects []
1337
1338******************************************************************************/
1339static void
1340_IoHnodeWriteBlifRecursively(
1341   Io_Encoding_Type_t encodingType,
1342   Hrc_Node_t *hnode,
1343   st_table *modelTable, 
1344   FILE *fp,
1345   FILE *encFp,
1346   int verbosity
1347  )
1348{
1349  char *modelName, *childName;
1350  Hrc_Model_t *model;
1351  Hrc_Manager_t *manager; 
1352  st_generator *stGen;
1353  Hrc_Node_t *childNode;
1354
1355  manager = Hrc_NodeReadManager(hnode);
1356  /* enter current model in modelTable */
1357  modelName = Hrc_NodeReadModelName(hnode);
1358  model = Hrc_ManagerFindModelByName(manager, modelName);
1359  if(st_is_member(modelTable, (char *) model)){
1360    return;
1361  }
1362  else{
1363    st_insert(modelTable, (char *)model, (char *) (long) (-1));
1364  }
1365
1366  _IoHnodeWriteBlifRecursivelyStep(encodingType, hnode, fp, encFp, verbosity); 
1367  Hrc_NodeForEachChild(hnode, stGen, childName, childNode){
1368    _IoHnodeWriteBlifRecursively(encodingType, childNode, modelTable, fp, encFp, verbosity);
1369  }
1370  return;
1371}
1372
1373
1374/**Function***********************************************************
1375
1376
1377  Synopsis      [ Writes out an hnode to blif]
1378
1379  Description   [ Writes out IO declarations, subckt declarations and tables to
1380                  the blif file specified.]
1381
1382  SideEffects   [ ]
1383
1384  SeeAlso       [  ]
1385**********************************************************************/
1386static int
1387_IoHnodeWriteBlifRecursivelyStep(
1388    Io_Encoding_Type_t encodingType,
1389    Hrc_Node_t *hnode,
1390    FILE *fp,
1391    FILE *encFp,
1392    int verbosity)
1393{
1394    Tbl_Table_t *table, *singleOutputTable;
1395    int i, j;
1396    Var_Variable_t *var, *actualVar;
1397    char *name, *instanceName, *modelName;
1398    st_generator *gen;
1399    st_table *blifInputsStTable, *blifOutputsStTable, *printedMvsStTable;
1400    st_table *encOutputsStTable, *encInputsStTable;
1401    Hrc_Node_t *subcktHnode;
1402    Hrc_Model_t *model, *subcktModel;
1403    Hrc_Subckt_t *subckt;
1404    Hrc_Manager_t *manager;
1405    array_t *subcktActualInputVars, *subcktActualOutputVars;
1406
1407
1408    printedMvsStTable = st_init_table(strcmp, st_strhash);
1409
1410  /* .model */
1411    modelName = Hrc_NodeReadModelName(hnode);
1412    manager = Hrc_NodeReadManager(hnode);
1413    model = Hrc_ManagerFindModelByName(manager, modelName);
1414    (void)fprintf(fp,".model %s\n", modelName);
1415
1416    /* .inputs line of blif file*/
1417    if (Hrc_NodeReadNumFormalInputs(hnode) != 0){
1418        (void)fprintf(fp,".inputs ");
1419        Hrc_NodeForEachFormalInput(hnode,i,var){
1420            (void)fprintf(fp,"%s0 ",Var_VariableReadName(var));
1421        }
1422        (void)fprintf(fp,"\n");
1423    }
1424   
1425    /* .outputs line of blif file*/
1426    if (Hrc_NodeReadNumFormalOutputs(hnode) != 0){
1427        (void)fprintf(fp,".outputs ");
1428        Hrc_NodeForEachFormalOutput(hnode,i,var){
1429            (void)fprintf(fp,"%s0 ",Var_VariableReadName(var));
1430        }
1431        (void)fprintf(fp,"\n");
1432    }
1433   
1434    /* .subckt stuff */
1435    Hrc_ModelForEachSubckt(model,gen,instanceName,subckt){
1436      subcktModel = Hrc_SubcktReadModel(subckt);
1437      subcktHnode = Hrc_ModelReadMasterNode(subcktModel);
1438      subcktActualInputVars = Hrc_SubcktReadActualInputVars(subckt);
1439      subcktActualOutputVars = Hrc_SubcktReadActualOutputVars(subckt);
1440     
1441      /* .subckt declarations */
1442      (void)fprintf(fp,".subckt %s ",
1443                    Hrc_ModelReadName(subcktModel));
1444      Hrc_NodeForEachFormalInput(subcktHnode,i,var){
1445        actualVar = array_fetch(Var_Variable_t *,subcktActualInputVars,i);
1446        (void)fprintf(fp,"%s0=%s0 ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
1447      }   
1448      Hrc_NodeForEachFormalOutput(subcktHnode,i,var){
1449        actualVar = array_fetch(Var_Variable_t *,subcktActualOutputVars,i);
1450        (void)fprintf(fp,"%s0=%s0 ",Var_VariableReadName(var),Var_VariableReadName(actualVar)); 
1451      }   
1452      (void)fprintf(fp,"\n");
1453    }
1454
1455    encOutputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
1456    encInputsStTable = st_init_table(st_ptrcmp, st_ptrhash);
1457    blifInputsStTable = st_init_table(strcmp, st_strhash);
1458    blifOutputsStTable = st_init_table(strcmp, st_strhash);
1459
1460    /* .latch declarations for blif file */
1461    IoWriteLatches(hnode, fp, encFp, printedMvsStTable, blifOutputsStTable, blifInputsStTable, encOutputsStTable, encInputsStTable, 0, 0, verbosity);
1462    Hrc_NodeForEachNameTable(hnode, i, table){
1463        if(IoOutputExpansionRequired(table)){
1464            if(verbosity > 0){
1465                (void)fprintf(stdout, "Splitting into Single Output Table before Processing\n");
1466            }
1467            for(j = 0; j < Tbl_TableReadNumOutputs(table); j++){
1468                singleOutputTable = IoMakeSingleOutputTable(table, j);
1469                _IoTableWriteBlif(encodingType, hnode, singleOutputTable, blifInputsStTable, fp, encFp,
1470                                  verbosity);
1471                Tbl_TableFree(singleOutputTable);
1472            }
1473        }
1474        else{
1475            if(!((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1))){
1476                _IoTableWriteBlif(encodingType, hnode, table, blifInputsStTable, fp, encFp,
1477                                  verbosity);
1478            }
1479        }
1480    }
1481    st_foreach_item_int(blifInputsStTable, gen, &name, &i){
1482        FREE(name);
1483    }
1484    st_foreach_item_int(blifOutputsStTable, gen, &name, &i){
1485        FREE(name);
1486    }
1487    st_free_table(blifInputsStTable);
1488    st_free_table(blifOutputsStTable);
1489    st_free_table(encInputsStTable);
1490    st_free_table(encOutputsStTable);
1491    st_foreach_item_int(printedMvsStTable, gen, &name, &i){
1492        FREE(name);
1493    }
1494    st_free_table(printedMvsStTable);
1495    fprintf(fp,".end\n");
1496    return 1;
1497}
1498
1499
1500
1501/**Function***********************************************************
1502
1503
1504  Synopsis      [ Checks if pseudoinput is also a PO]
1505
1506  Description   [ Checks if table has 0input, >1 output, or 1 output
1507                  with multiple valued entry]
1508
1509  SideEffects   [ ]
1510
1511  SeeAlso       [  ]
1512**********************************************************************/
1513static int
1514_IoCheckPseudoinputIsPO(
1515   Tbl_Table_t *table)
1516{
1517  int j;
1518  Var_Variable_t *var = NIL(Var_Variable_t); /* to suppress warning */
1519  Tbl_Entry_t *entry;
1520  int numValues;
1521   
1522  if((Tbl_TableReadNumInputs(table) == 0) && (Tbl_TableReadNumOutputs(table) > 1)){
1523    /* assume all are pseudoinputs */
1524    Tbl_TableForEachOutputVar(table, j, var){
1525      if(Var_VariableTestIsPO(var)){
1526        return 1;
1527      }
1528    }
1529  }
1530
1531  if(Tbl_TableReadNumInputs(table) == 0){
1532    if(Tbl_TableReadNumRows(table) != 0){
1533      entry = Tbl_TableReadEntry(table, 0, 0, 1);
1534      numValues = Tbl_EntryReadNumValues(entry);
1535    }
1536    else{
1537      entry = Tbl_TableDefaultReadEntry(table, 0);
1538      numValues = Tbl_EntryReadNumValues(entry);
1539    }
1540
1541    Tbl_TableForEachOutputVar(table, j, var);
1542    if(Tbl_TableReadNumRows(table) <= 1){
1543      if(numValues > 1){
1544        if(Var_VariableTestIsPO(var)){
1545          return 1;
1546        }
1547      }
1548    }
1549    else{
1550      if(Var_VariableTestIsPO(var)){     
1551        return 1;
1552      }
1553    }
1554  }
1555
1556  return 0;
1557}
Note: See TracBrowser for help on using the repository browser.