extra.h

主要进行大规模的电路综合

/**CFile****************************************************************

  FileName    [extra.h]

  PackageName [extra]

  Synopsis    [Experimental version of some DD-based procedures.]

  Description [This library contains a number of operators and 
  traversal routines developed to extend the functionality of 
  CUDD v.2.3.x, by Fabio Somenzi (http://vlsi.colorado.edu/~fabio/)
  To compile your code with the library, #include "extra.h" 
  in your source files and link your project to CUDD and this 
  library. Use the library at your own risk and with caution. 
  Notice that debugging of some operators still continues.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - February 1, 2003.]

  Revision    [$Id: extra.h,v 1.9 2003/05/27 23:14:36 alanmi Exp $]

***********************************************************************/

#ifndef __EXTRA_H__
#define __EXTRA_H__

/*---------------------------------------------------------------------------*/
/* Nested includes                                                           */
/*---------------------------------------------------------------------------*/

#include <string.h>
#include <time.h>
#include "util.h"
#include "st.h"
#include "cuddInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

// an assuption about the maximum number of BDD variables
#define MAXINPUTS   1000       

/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

/* constants of the manager */
#define		b0     Cudd_Not((dd)->one)
#define		b1              (dd)->one
#define		z0              (dd)->zero
#define		z1              (dd)->one
#define		a0              (dd)->zero
#define		a1              (dd)->one


// hash key macros
#define hashKey1(a,TSIZE) \
((unsigned)(a) % TSIZE)

#define hashKey2(a,b,TSIZE) \
(((unsigned)(a) + (unsigned)(b) * DD_P1) % TSIZE)

#define hashKey3(a,b,c,TSIZE) \
(((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 ) % TSIZE)

#define hashKey4(a,b,c,d,TSIZE) \
((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
   (unsigned)(d)) * DD_P3) % TSIZE)

#define hashKey5(a,b,c,d,e,TSIZE) \
(((((((unsigned)(a) + (unsigned)(b)) * DD_P1 + (unsigned)(c)) * DD_P2 + \
   (unsigned)(d)) * DD_P3 + (unsigned)(e)) * DD_P1) % TSIZE)


// complementation and testing for pointers for hash entries
#define Hash_IsComplement(p)  ((int)((long) (p) & 02))
#define Hash_Regular(p)       ((DdNode*)((unsigned)(p) & ~02))
#define Hash_Not(p)           ((DdNode*)((long)(p) ^ 02))
#define Hash_NotCond(p,c)     ((DdNode*)((long)(p) ^ (02*c)))

// print the BDD of the function in the SOP form
#define PRB(dd,f)       printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
// print the ZDD of the function in the SOP form
#define PRZ(dd,f)       printf("%s = \n", #f); Cudd_zddPrintCover(dd,f); 
// print the number of nodes in the BDD
#define PRN(f)          printf("Nodes in %s = %d\n", #f, Cudd_DagSize(f))
// print the support of the BDD
#define PRS(dd,f)       printf("Support of %s = ", #f ); Extra_PrintSupport((dd),(f)); printf("\n")
// print the Karnaugh map of the completely-specified function
#define PRK(dd,f,n)     printf("K-map for function <%s> is:\n", #f); Extra_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0)
// print the Karnaugh map of the incompletely-specified function
#define PRK2(dd,f,g,n)  printf("K-map for function <%s> is:\n", #f); Extra_PrintKMap(stdout,dd,(f),(g),(n),NULL,0)
// print the time spent by the process "a"
#define PRT(a,t)        printf("%s = ", (a)); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) )

#define CALLOC(type, num)  ((type *) calloc((long)(num), (long)sizeof(type)))

/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/


/*===========================================================================*/
/*    ADD-based procedures                                                   */
/*===========================================================================*/

/*=== extraAddMisc.c =============================================================*/

/* remaps the function to depend on the topmost variables on the manager. */
extern DdNode *     Extra_addRemapUp ARGS((DdManager * dd, DdNode * aF));
/* counts the number of different constant nodes of the ADD */
extern int          Extra_addCountConst ARGS((DdManager * dd, DdNode * aFunc));
/* counts the the number of different constant nodes of the array of ADDs */
extern int          Extra_addCountConstArray ARGS((DdManager * dd, DdNode ** paFuncs, int nFuncs));
/* finds the minimum value terminal node in the array of ADDs */
extern DdNode *     Extra_addFindMinArray ARGS((DdManager * dd, DdNode ** paFuncs, int nFuncs));
/* finds the maximum value terminal node in the array of ADDs */
extern DdNode *     Extra_addFindMaxArray ARGS((DdManager * dd, DdNode ** paFuncs, int nFuncs));
/* absolute value of an ADD */
extern DdNode *     Extra_addAbs ARGS((DdManager * dd, DdNode * f));
/* the encoded set of absolute values of the constant nodes of an ADD */
extern DdNode *     Extra_bddAddConstants ARGS((DdManager * dd, DdNode * aFunc));
/* determines whether this is an ADD or a BDD */
extern int          Extra_addDetectAdd ARGS((DdManager * dd, DdNode * Func));
/* restructure the ADD by replacing negative terminals with their abs value */
extern DdNode *     Cudd_addAbs ARGS((DdManager * dd, DdNode * f));
/* Coudert's restrict applicable to true ADDs (takes the don't-care set, not the care set). */
extern DdNode *     Extra_addRestrictAdd ARGS((DdManager * dd, DdNode * aF, DdNode * aD));
extern DdNode *      extraAddRestrictAdd ARGS((DdManager * dd, DdNode * aF, DdNode * aD));
/* intersection, union, and sharp of paths for each terminal */
extern DdNode *     Extra_addForeachTerminalAnd ARGS((DdManager * dd, DdNode ** f, DdNode ** g));
extern DdNode *     Extra_addForeachTerminalOr ARGS((DdManager * dd, DdNode ** f, DdNode ** g));
extern DdNode *     Extra_addForeachTerminalSharp ARGS((DdManager * dd, DdNode ** f, DdNode ** g));
/* swapping a given terminal node with zero terminal node */
extern DdNode *     Extra_addSwapTerminals ARGS((DdManager * dd, DdNode * aFunc, DdNode * aTerm));
extern DdNode *      extraAddSwapTerminals ARGS((DdManager * dd, DdNode * aFunc, DdNode * aTerm));

/*=== extraAddSpectra.c =============================================================*/

/* Walsh spectrum computation */
extern DdNode *     Extra_bddWalsh ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
extern DdNode *      extraBddWalsh ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
/* Reed-Muller spectrum computation */
extern DdNode *     Extra_bddReedMuller ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
extern DdNode *      extraBddReedMuller ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
/* Haar spectrum computation */
extern DdNode *     Extra_bddHaar ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
extern DdNode *      extraBddHaar ARGS((DdManager * dd, DdNode * bFunc, DdNode * bVars));
/* inverse Haar spectrum computation */
extern DdNode *     Extra_bddHaarInverse ARGS((DdManager * dd, DdNode * aFunc, DdNode * bVars));
extern DdNode *      extraBddHaarInverse ARGS((DdManager * dd, DdNode * aFunc, DdNode * aSteps, DdNode * bVars, DdNode * bVarsAll, int nVarsAll, int * InverseMap));
/* remapping from the natural order into the sequential order */
extern DdNode *     Extra_addRemapNatural2Sequential ARGS((DdManager * dd, DdNode * aSource, DdNode * bVars));
/* addition function to update the negative-variable-assignment cube value in the ADD */
extern DdNode *      extraAddUpdateZeroCubeValue ARGS((DdManager * dd, DdNode * aFunc, DdNode * bVars, DdNode * aNode));
/* the generalized ITE for ADDs */
extern DdNode *      extraAddIteRecurGeneral ARGS((DdManager * dd, DdNode * bX, DdNode * aF, DdNode * aG));



/*===========================================================================*/
/*    BDD-based procedures                                                   */
/*===========================================================================*/