/**CFile*********************************************************************** FileName [maigUtil.c] PackageName [maig] Synopsis [Utilities for Multi-Valued AndInv graph] Author [Mohammad Awedh] Copyright [ This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "maigInt.h" #include "mvfaig.h" #include "mvfaigInt.h" #include "ctlspInt.h" #include "ctlsp.h" #include "ntk.h" static char rcsid[] UNUSED = "$Id: maigUtil.c,v 1.20 2005/05/18 18:11:59 jinh Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Stucture declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int NoOfBitEncode(int n); static bAigEdge_t Case(mAig_Manager_t * mgr, array_t * encodeList, int index); static int mCommandmAigTest(void); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initialize maig package] SideEffects [none] SeeAlso [mAig_End] ******************************************************************************/ void mAig_Init(void) { Cmd_CommandAdd("_mAig_test", (int(*)(Hrc_Manager_t **, int, char **)) mCommandmAigTest, 0); } /**Function******************************************************************** Synopsis [End maig package] SideEffects [] SeeAlso [mAig_Init] ******************************************************************************/ void mAig_End(void) { } /**Function******************************************************************** Synopsis [] Description [] SideEffects [] ******************************************************************************/ array_t * mAig_ArrayDuplicate( array_t *mAigArray) { int i; int length = array_n(mAigArray); array_t *result = array_alloc(mAigEdge_t *, length); for (i = 0; i < length; i++) { mAigEdge_t *tempMAig = array_fetch(mAigEdge_t *, mAigArray, i); array_insert(mAigEdge_t *, result, i, tempMAig); } return (result); } /**Function******************************************************************** Synopsis [Creates a new mAig manager] SideEffects [] SeeAlso [] ******************************************************************************/ mAig_Manager_t * mAig_initAig(void) { return bAig_initAig(5000); /* Initial number of nodes in the bAIG greaph*/ } /**Function******************************************************************** Synopsis [Quit mAig manager] SideEffects [] SeeAlso [] ******************************************************************************/ void mAig_quit( mAig_Manager_t *manager) { bAig_quit(manager); } /**Function******************************************************************** Synopsis [Build the binary representation of multi-valued variable that equal to constant.] Description [It builds the binary And/Inverter graph of a multi-valued variable of value equal to constant.] SideEffects [] SeeAlso [Case] ******************************************************************************/ mAigEdge_t mAig_EquC( mAig_Manager_t * mgr, mAigEdge_t mVarId, int constant) { array_t *mVarList = mAigReadMulVarList(mgr); mAigMvar_t mVar = array_fetch(mAigMvar_t, mVarList, mVarId); array_t *encodeList = array_alloc(bAigEdge_t, 0); int i; bAigEdge_t bVarId; for(i=0; i< mVar.values; i++){ if( i == constant){ array_insert_last(bAigEdge_t, encodeList, mAig_One); } else{ array_insert_last(bAigEdge_t, encodeList, mAig_Zero); } /* if */ } /* for */ bVarId = Case(mgr, encodeList, mVar.bVars + mVar.encodeLength-1); /* Build the bAig grpah */ array_free(encodeList); return bVarId; } /**Function******************************************************************** Synopsis [Creates Multi-valued Variable] Description [Creates Multi-valued variable of name 'name' and value 'value', and returns the Id for this variable. It creates the binary variable that are used to rpresent this multi-valued variable.] SideEffects [] SeeAlso [bAig_CreateVarNode] ******************************************************************************/ mAigEdge_t mAig_CreateVar( mAig_Manager_t * mgr, char * name, int value) { array_t *mVarList = mAigReadMulVarList(mgr); array_t *bVarList = mAigReadBinVarList(mgr); int noBits = NoOfBitEncode(value); int i, startBvar, startMvar; /* char bName[100]; */ char *bName = ALLOC(char, strlen(name) + 10); mAigMvar_t mVar; mAigBvar_t bVar; assert(mVarList != NIL(array_t)); assert(bVarList != NIL(array_t)); startBvar = array_n(bVarList); startMvar = array_n(mVarList); /* Create Multi-valued variable */ mVar.mVarId = startMvar; mVar.bVars = startBvar; mVar.values = value; mVar.name = name; mVar.encodeLength = noBits; array_insert_last(mAigMvar_t, mVarList, mVar); /* Create binary Variables of the Multi-valued variable */ for (i=0; ibVarList); } /**Function******************************************************************** Synopsis [Retunrs the Multi-Valued variables List] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ array_t * mAigReadMulVarList( mAig_Manager_t * manager) { return (manager->mVarList); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Returns no. of Bit encoding needed for n] Description [] SideEffects [] SeeAlso [] ******************************************************************************/ static int NoOfBitEncode( int n) { int i = 0; int j = 1; if (n < 2) return 1; /* Takes care of mv.values <= 1 */ while (j < n) { j = j * 2; i++; } return i; } /**Function******************************************************************** Synopsis [Returns the binary And/Inverter graph of a multi-valued variable.] Description [The encodingList array has bAig_Zero in all its entries except the enrty at which the multi-valued variable equal to the required value. At which the value is bAig_One.] SideEffects [] SeeAlso [mAig_EquC] ******************************************************************************/ static bAigEdge_t Case( mAig_Manager_t * mgr, array_t * encodeList, int index) { array_t *bVarList = mAigReadBinVarList(mgr); mAigBvar_t bVar; array_t *newEncodeList; int encodeLen = array_n(encodeList); bAigEdge_t andResult1, andResult2, orResult, result; bAigEdge_t node1, node2; int i; int count=0; if (encodeLen == 1){ return array_fetch(bAigEdge_t, encodeList, 0); } bVar = array_fetch(mAigBvar_t, bVarList, index); newEncodeList = array_alloc(bAigEdge_t, 0); for (i=0; i< (encodeLen/2); i++){ node1 = array_fetch(bAigEdge_t, encodeList, count++); node2 = array_fetch(bAigEdge_t, encodeList, count++); /* performs ITE operator */ andResult1 = bAig_And(mgr, bVar.node, node2); andResult2 = bAig_And(mgr, bAig_Not(bVar.node), node1); orResult = bAig_Or (mgr, andResult1, andResult2); array_insert_last(bAigEdge_t, newEncodeList, orResult); } if (encodeLen %2){ /* Odd */ node1 = array_fetch(bAigEdge_t, encodeList, count); array_insert_last(bAigEdge_t, newEncodeList, node1); } result = Case(mgr, newEncodeList, index-1); array_free(newEncodeList); return result; } /**Function******************************************************************** Synopsis [] CommandName [_mAig_test] SideEffects [] ******************************************************************************/ static int mCommandmAigTest(void) { array_t *mVarList; array_t *bVarList; MvfAig_Function_t * aa; MvfAig_Function_t * bb; MvfAig_Function_t * cc; mAigMvar_t mVar; mAigBvar_t bVar; int i; mAig_Manager_t *manager = mAig_initAig(); mAigEdge_t node1, node2, node3, node4, node5, node6; node1 = mAig_CreateVar(manager,"a",5); /* var a of 5 values */ node2 = mAig_CreateVar(manager,"b",6); /* var b of 6 values */ node3 = mAig_CreateVar(manager,"c",2); /* var c of 2 values */ aa = MvfAig_FunctionCreateFromVariable(manager, node1); bb = MvfAig_FunctionCreateFromVariable(manager, node2); cc = MvfAig_FunctionCreateFromVariable(manager, node3); mVarList = mAigReadMulVarList(manager); bVarList = mAigReadBinVarList(manager); fprintf(vis_stdout,"mValist: \n"); for (i=0; i< array_n(mVarList); i++){ mVar = array_fetch(mAigMvar_t, mVarList, i); fprintf(vis_stdout,"mVarId=%d name=%s bVarId=%d values:%d\n", mVar.mVarId, mVar.name, mVar.bVars, mVar.values); } fprintf(vis_stdout,"bValist: \n"); for (i=0; i< array_n(bVarList); i++){ bVar = array_fetch(mAigBvar_t, bVarList, i); fprintf(vis_stdout,"mVar ID=%d bVar ID=%ld \n", bVar.mVarId, bVar.node); } node4 = array_fetch(bAigEdge_t, aa, 3); node5 = array_fetch(bAigEdge_t, bb, 2); node6 = mAig_Or(manager, node4, node5); node4 = array_fetch(bAigEdge_t, cc, 0); node5 = bAig_Eq(manager, node6, node4); fprintf(vis_stdout,"%ld %ld %ld %ld %ld %ld\n",node1, node2, node3, node4, node5, node6); fprintf(vis_stdout,"Nodes Array:\n\n"); for (i=0; i< manager->nodesArraySize ; i++) fprintf(vis_stdout,"Node #%d value=%ld \n",i,manager->NodesArray[i]); fprintf(vis_stdout,"\n\nName List:\n"); for (i=0; i< 20; i++) fprintf(vis_stdout,"index %d Name %s \n",i, manager->nameList[i]); bAig_PrintDot(vis_stdout, manager); return 0; }