VIS

src/tbl/tblAigUtil.c File Reference

#include "tblInt.h"
#include "baig.h"
Include dependency graph for tblAigUtil.c:

Go to the source code of this file.

Functions

MvfAig_Function_t * Tbl_TableBuildNonDetConstantMvfAig (Tbl_Table_t *table, int outIndex, int mAigId, mAig_Manager_t *manager)
MvfAig_Function_t * Tbl_TableBuildMvfAigFromFanins (Tbl_Table_t *table, int outIndex, array_t *faninArray, mAig_Manager_t *manager)

Variables

static char rcsid[] UNUSED = "$Id: tblAigUtil.c,v 1.3 2005/04/17 14:37:23 awedh Exp $"

Function Documentation

MvfAig_Function_t* Tbl_TableBuildMvfAigFromFanins ( Tbl_Table_t *  table,
int  outIndex,
array_t *  faninArray,
mAig_Manager_t *  manager 
)

Function********************************************************************

Synopsis [Compute the Mvf_Function_t for a table output in terms of fanins]

Description [Given a Tbl_Table_t, an integer for the table output value index, an array of fanin mAigEdge_t* , and an mAigManager, this function builds the MvfAig_Function_t associated with the output. The output cannot be equal to another output, because this would make the table a relation, and that is not permissible. For each row, the function will build the mAigEdge_t for the inputs using their MvfAig_Function_t's and AND them together. If the input is of the type equal, it will build the equivalent set mAig (see See Also) and AND it in. If the input of the type Tbl_EntryUniverse_c, this input will be set tomAig_One.]

SideEffects [ ]

SeeAlso [ MvfAig_FunctionComputeEquivalentSet, TblEntryNormalConstructAig] [Done]

Definition at line 105 of file tblAigUtil.c.

{

  lsGen gen;
  Tbl_Entry_t *entry, *equalEntry, *inputEntry;
  Tbl_Range_t *range;
  int         value, rowNum, colNum, rowColNum, i;
  mAigEdge_t  x, result, temp;
  MvfAig_Function_t *function, *mvf1, *mvf2;
  

  x = mAig_NULL;
  value = Var_VariableReadNumValues(Tbl_TableReadIndexVar(table,outIndex,1));
  function = MvfAig_FunctionAlloc(value);
  
  Tbl_TableForEachOutputEntry(table,rowNum,colNum,entry) {
    if (colNum == outIndex) {
      if (entry->type == Tbl_EntryNormal_c) {
        result = mAig_One;
        Tbl_RowForEachInputEntry(table,rowNum,inputEntry,rowColNum) {
          if (inputEntry->type == Tbl_EntryNormal_c) {
            mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum);
            x = TblEntryNormalConstructAig(manager, inputEntry, mvf1);
          }
          else if (inputEntry->type == Tbl_EntryUniverse_c) {
            x = mAig_One;
          }
          else if (inputEntry->type == Tbl_EntryEqual_c) {
            value =Tbl_EntryReadVarIndex(inputEntry);
            mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum);
            mvf2 = array_fetch(MvfAig_Function_t*,faninArray,value);
            x = MvfAig_FunctionsComputeEquivalentSet(manager, mvf1,mvf2);
          }
          temp = result;
          result = mAig_And(manager, x,temp);
        }
        /* add the result to each value of the output */
        Tbl_EntryForEachValue(entry,value,gen,range) {  
          MvfAig_FunctionAddMintermsToComponent(manager, function, value,result);
        }
        
      } /* output is not Normal */
      else  if (entry->type == Tbl_EntryEqual_c) {
        value = Tbl_EntryReadVarIndex(entry);
        if (value == -1) {
        fail("Failure: Not equal to any input var in this table\n");
        }
                  
        /* must be equal to an input */
        
        equalEntry = Tbl_TableReadEntry(table,rowNum,value,0);
        result = mAig_One;
        Tbl_RowForEachInputEntry(table,rowNum,inputEntry,rowColNum) {
          if (inputEntry->type == Tbl_EntryNormal_c) {
            /* Don't include this input if the output is set be equal to it
             */
            if ( inputEntry == equalEntry){
              continue;
            }
            mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum);
            x = TblEntryNormalConstructAig(manager, inputEntry, mvf1);
          }
          else if (inputEntry->type == Tbl_EntryUniverse_c) {
            x = mAig_One;
          }
          else if (inputEntry->type == Tbl_EntryEqual_c) {
            value =Tbl_EntryReadVarIndex(inputEntry);
            mvf1 = array_fetch(MvfAig_Function_t*,faninArray,rowColNum);
            mvf2 = array_fetch(MvfAig_Function_t*,faninArray,value);
            x = MvfAig_FunctionsComputeEquivalentSet(manager, mvf1,mvf2);
          }
          temp = result;
          result = mAig_And(manager, x, temp);
        }

        temp = result;
        rowColNum = Tbl_EntryReadVarIndex(entry);
        mvf1 = array_fetch(MvfAig_Function_t*, faninArray, rowColNum);        

        if (equalEntry->type == Tbl_EntryNormal_c) {
          /* add the result to each value of the equal input */
          Tbl_EntryForEachValue(equalEntry, value, gen, range) { 
            x = MvfAig_FunctionReadComponent(mvf1, value);
            result = mAig_And(manager, temp, x);
            MvfAig_FunctionAddMintermsToComponent(manager, function, value, result);
          }
        }else { /* Add Minterms for all vlaues */
          value = Var_VariableReadNumValues(Tbl_EntryReadActualVar(table, equalEntry));
          for(i=0; i< value; i++) {
            x = MvfAig_FunctionReadComponent(mvf1,i);
            result = mAig_And(manager, temp, x);
            MvfAig_FunctionAddMintermsToComponent(manager, function, i,result);
          }
        }
      }  
    }
  }

  /* accounting for the defaults */
  entry = Tbl_TableDefaultReadEntry(table,outIndex);
  if (entry != NIL(Tbl_Entry_t)) {  
    temp = MvfAig_FunctionComputeDomain(manager, function);
    result = mAig_Not(temp);

    if (entry->type == Tbl_EntryNormal_c) {    
      Tbl_EntryForEachValue(entry,value,gen,range) {
        MvfAig_FunctionAddMintermsToComponent(manager, function, value, result);
      }
    }
    else {
      value = Tbl_EntryReadVarIndex(entry);
      if (value == -1) {
        fail("Failure: Not equal to any input var in this table\n");
      }
      mvf1 = array_fetch(MvfAig_Function_t*, faninArray, value);
      
      MvfAig_FunctionForEachComponent(mvf1, i, x) {
        temp = mAig_And(manager, x, result);
        MvfAig_FunctionAddMintermsToComponent(manager, function, i ,temp);
      }
    }
    
  }
        
  return function;  
}

Here is the call graph for this function:

Here is the caller graph for this function:

MvfAig_Function_t* Tbl_TableBuildNonDetConstantMvfAig ( Tbl_Table_t *  table,
int  outIndex,
int  mAigId,
mAig_Manager_t *  manager 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Compute the Mvf_Function_t for a non-deterministic constant.]

Description [Given a Tbl_Table_t, an integer for the table output value index, an integer MAigId, and an mAig Manager, this function builds the MvfAig_Function_t associated with the output. The table cannot have any inputs; the function fails if it does. The output cannot be equal to another output, because this would make the table a relation, and that is not permissible. If this occurs, the function will fail on an assert statement.]

SideEffects [ Table must have no inputs.]

SeeAlso [] [Done]

Definition at line 55 of file tblAigUtil.c.

{

  lsGen gen;
  Tbl_Entry_t       *entry;
  Tbl_Range_t       *range;
  int value,         rowNum, colNum;
  mAigEdge_t         x;
  MvfAig_Function_t *function;
  
  assert(Tbl_TableReadNumInputs(table) ==0);

  value = Var_VariableReadNumValues(Tbl_TableReadIndexVar(table, outIndex, 1));
  function = MvfAig_FunctionAlloc(value);  
  Tbl_TableForEachOutputEntry(table,rowNum,colNum,entry) {
    if (colNum == outIndex) {
      assert(entry->type == Tbl_EntryNormal_c);
      Tbl_EntryForEachValue(entry,value,gen,range) {
        x = mAig_EquC(manager, mAigId, value);
        MvfAig_FunctionAddMintermsToComponent(manager, function, value, x);
      }
    }
  }
  return function;
}

Here is the call graph for this function:

Here is the caller graph for this function:


Variable Documentation

char rcsid [] UNUSED = "$Id: tblAigUtil.c,v 1.3 2005/04/17 14:37:23 awedh Exp $" [static]

CFile***********************************************************************

FileName [ tblAigUtil.c ]

PackageName [ tbl ]

Synopsis []

Description []

SeeAlso [ tbl.h, tblEntryUtil.c, tblAigEntryUtil, tblUtil.c ]

Author [Mohammad Awedh ]

Copyright []

Definition at line 21 of file tblAigUtil.c.