src/spfd/spfdSpfd.c File Reference
#include "spfdInt.h"
Include dependency graph for spfdSpfd.c:
Go to the source code of this file.
Functions | |
| static bdd_node * | ComputeAuxRel (SpfdApplData_t *applData, bdd_node *faninRel, Ntk_Node_t *from, int piSwap) |
| bdd_node * | SpfdNodeComputeSpfdFromOnAndOffSet (SpfdApplData_t *applData, Ntk_Node_t *regNode, bdd_node *bdd1, bdd_node *bdd0) |
| bdd_node * | SpfdNodeComputeSpfdFromFanouts (SpfdApplData_t *applData, Ntk_Node_t *from) |
| st_table * | SpfdNodeComputeSCCs (SpfdApplData_t *applData, Ntk_Node_t *regNode, bdd_node **tempVars) |
Function Documentation
| static bdd_node * ComputeAuxRel | ( | SpfdApplData_t * | applData, |
| bdd_node * | faninRel, | ||
| Ntk_Node_t * | from, | ||
| int | piSwap | ||
| ) | [static] |
CFile***********************************************************************
FileName [spfdSpfd.c]
PackageName [spfd]
Synopsis [Routines to perform SPFD computation.]
Description [Routines to perform SPFD computation.]
SeeAlso [spfdProg.c]
Author [Balakrishna Kumthekar]
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.]AutomaticStart
Function********************************************************************
Synopsis [Convert faninRel which is interms of Y, to Y', the auxillary variables.]
SideEffects [None]
Definition at line 451 of file spfdSpfd.c.
{
bdd_node **fromVars,**toVars;
int numFi = Ntk_NodeReadNumFanins(from);
int k,altId;
Ntk_Node_t *fanin;
bdd_node *faninRelAux;
st_table *piAltVars;
bdd_manager *ddManager = applData->ddManager;
piAltVars = applData->currPiAltVars;
/* Collect variables for swapping. */
fromVars = ALLOC(bdd_node *,numFi);
toVars = ALLOC(bdd_node *,numFi);
Ntk_NodeForEachFanin(from,k,fanin) {
int id = Ntk_NodeReadMddId(fanin);
if (piSwap && st_lookup(piAltVars,(char *)(long)id,&altId)) {
fromVars[k] = bdd_bdd_ith_var(ddManager,altId);
} else {
fromVars[k] = bdd_bdd_ith_var(ddManager,id);
}
toVars[k] = bdd_bdd_ith_var(ddManager,SpfdNodeReadAuxId(applData,fanin));
}
bdd_ref(faninRelAux = bdd_bdd_swap_variables(ddManager,faninRel,fromVars,
toVars,numFi));
FREE(fromVars);
FREE(toVars);
return faninRelAux;
} /* End of ComputeAuxRel */
Here is the call graph for this function:
Here is the caller graph for this function:
| st_table* SpfdNodeComputeSCCs | ( | SpfdApplData_t * | applData, |
| Ntk_Node_t * | regNode, | ||
| bdd_node ** | tempVars | ||
| ) |
Function********************************************************************
Synopsis [Compute the strongly connected components in the SPFD of regNode. 'tempVars' are extra variables required during this computation. For detailed description please refer to:
Subarnarekha Sinha and Robert K. Brayton. Implementation and use of SPFDs in optimizaing Boolean networks. In International Conference on Computer Aided Design, 1998.]
SideEffects [None]
Definition at line 325 of file spfdSpfd.c.
{
bdd_manager *ddManager = applData->ddManager;
st_table *inUseVars = applData->currInUseVars;
Ntk_Node_t *fanin;
st_table *SCC;
bdd_node *spfd,*spfd2,*auxCube;
bdd_node *ddTemp1,*ddTemp2,*logicZero,*faninCube;
bdd_node *Ny,*E1y,*E0y;
bdd_node *from,*To,*new_,*reached;
bdd_node **faninVars,**auxVars;
int i,numFanin,varsAllocated;
numFanin = Ntk_NodeReadNumFanins(regNode);
SCC = st_init_table(st_ptrcmp,st_ptrhash);
spfd = SpfdNodeReadSpfd(applData,regNode);
logicZero = bdd_read_logic_zero(ddManager);
if (spfd == logicZero)
return SCC;
varsAllocated = 0;
/* Allocate variables if necessary */
if (tempVars == NIL(bdd_node *)) {
tempVars = SpfdAllocateTemporaryVariables(ddManager,inUseVars,numFanin);
varsAllocated = 1;
}
faninVars = ALLOC(bdd_node *,numFanin);
auxVars = ALLOC(bdd_node *,numFanin);
Ntk_NodeForEachFanin(regNode,i,fanin) {
faninVars[i] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
auxVars[i] = bdd_bdd_ith_var(ddManager,
SpfdNodeReadAuxId(applData,fanin));
}
bdd_ref(auxCube = bdd_bdd_compute_cube(ddManager,auxVars,
NIL(int),numFanin));
/* Compute spfd2 = \exists_{\hat{y}} spfd(y,\hat{y}) *
spfd(\hat{y},\tilde{y}) */
bdd_ref(ddTemp1 = bdd_bdd_swap_variables(ddManager,spfd,faninVars,
auxVars,numFanin));
bdd_ref(ddTemp2 = bdd_bdd_swap_variables(ddManager,ddTemp1,faninVars,
tempVars,numFanin));
bdd_recursive_deref(ddManager,ddTemp1);
bdd_ref(spfd2 = bdd_bdd_and_abstract(ddManager,spfd,ddTemp2,auxCube));
bdd_recursive_deref(ddManager,ddTemp2);
/* SCC computation */
bdd_ref(faninCube = bdd_bdd_compute_cube(ddManager,faninVars,
NIL(int),numFanin));
/* Compute N(y) = \exists_{\hat{y}} spfd(y,\hat{y}) */
bdd_ref(Ny = bdd_bdd_exist_abstract(ddManager,spfd,auxCube));
bdd_recursive_deref(ddManager,auxCube);
while (Ny != logicZero) {
/* To compute E1(y) perform the fixpoint image computation */
bdd_ref(from = bdd_bdd_pick_one_minterm(ddManager,Ny,faninVars,numFanin));
bdd_ref(reached = from);
do {
bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd2,from,faninCube));
bdd_recursive_deref(ddManager,from);
bdd_ref(To = bdd_bdd_swap_variables(ddManager,ddTemp1,tempVars,
faninVars,numFanin));
bdd_recursive_deref(ddManager,ddTemp1);
bdd_ref(new_ = bdd_bdd_and(ddManager,To,bdd_not_bdd_node(reached)));
bdd_recursive_deref(ddManager,To);
bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,reached,new_));
bdd_recursive_deref(ddManager,reached);
reached = ddTemp1;
from = new_;
} while (new_ != logicZero);
E1y = reached;
/* E_0(y) = \exists_{\hat{y}} spfd(y,\hat{y}) * E_1(y) */
bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd,E1y,faninCube));
bdd_ref(E0y = bdd_bdd_swap_variables(ddManager,ddTemp1,auxVars,
faninVars,numFanin));
bdd_recursive_deref(ddManager,ddTemp1);
/* Update Ny: Ny = Ny * (E1y + E0y)' */
bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,E1y,E0y));
bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,Ny,bdd_not_bdd_node(ddTemp1)));
bdd_recursive_deref(ddManager,ddTemp1);
bdd_recursive_deref(ddManager,Ny);
Ny = ddTemp2;
/* Store E1y and E0y in an st_table */
st_insert(SCC,(char *)E1y,(char *)E0y);
}
bdd_recursive_deref(ddManager,faninCube);
bdd_recursive_deref(ddManager,Ny);
FREE(auxVars);
FREE(faninVars);
if (varsAllocated) {
long id;
for (i = 0; i < numFanin; i++) {
id = (long) bdd_node_read_index(tempVars[i]);
st_delete(inUseVars,&id,NIL(char *));
}
FREE(tempVars);
}
return SCC;
} /* End of SpfdNodeComputeSCCs */
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SpfdNodeComputeSpfdFromFanouts | ( | SpfdApplData_t * | applData, |
| Ntk_Node_t * | from | ||
| ) |
Function********************************************************************
Synopsis [Compute the SPFD of 'from', as the union of SPFDs of its fanout wires.]
SideEffects [None]
Definition at line 144 of file spfdSpfd.c.
{
bdd_manager *ddManager = applData->ddManager;
st_table *currBddReq;
st_table *wireTable,*wiresRemoved;
array_t *ordArray;
bdd_node *result,*var,*varAux,*ddTemp,*ddTemp2;
bdd_node *wireSpfd,*toSpfd,*fromSpfd,*xCube;
bdd_node *step1,*faninRel,*faninRelAux,*inter,*final;
bdd_node **firstCompose,**secondCompose;
bdd_node *logicZero;
Ntk_Node_t *fanin,*to;
int index,i,j;
int size,piSwap;
if (Ntk_NodeReadNumFanouts(from) < 1) {
(void) fprintf(vis_stdout,
"** spfd error: Node %s has no fanouts.\n",
Ntk_NodeReadName(from));
return NIL(bdd_node);
}
currBddReq = applData->currBddReq;
xCube = applData->currXCube;
logicZero = bdd_read_logic_zero(ddManager);
/* Compute the characteristic function of the fanin relation:
faninRel = \prod y_i == f_i(X) */
faninRel = SpfdComputeNodeArrayRelation(applData,currBddReq,NIL(array_t),
Ntk_NodeReadFanins(from),
TRUE,&piSwap);
/* Convert faninRel(y,pi) to faninRel(\hat{y},pi) */
faninRelAux = ComputeAuxRel(applData,faninRel,from,piSwap);
/* Compute SPFD wire by wire according to the order specified for
each fanout node. */
wireTable = applData->currWireTable;
wiresRemoved = applData->wiresRemoved;
bdd_ref(fromSpfd = logicZero);
Ntk_NodeForEachFanout(from,j,to) {
bdd_ref(result = bdd_read_one(ddManager));
ordArray = SpfdNodeReadFaninOrder(applData,to);
arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
var = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
index = SpfdNodeReadAuxId(applData,fanin);
varAux = bdd_bdd_ith_var(ddManager,index);
if (fanin != from) {
/* XNOR */
bdd_ref(ddTemp = bdd_bdd_xnor(ddManager,var,varAux));
} else {
/* XOR */
bdd_ref(ddTemp = bdd_bdd_xor(ddManager,var,varAux));
}
bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,result,ddTemp));
bdd_recursive_deref(ddManager,result);
bdd_recursive_deref(ddManager,ddTemp);
result = ddTemp2;
if (fanin == from)
break;
}
/* Compute AND of result and the SPFD of 'to'. */
toSpfd = SpfdNodeReadSpfd(applData,to);
if (toSpfd == NIL(bdd_node)) {
(void) fprintf(vis_stderr,
"** spfd error: Spfd expected but not found.\n");
(void) fprintf(vis_stderr, "To node:\n");
Ntk_NodePrint(vis_stderr, to, TRUE, TRUE);
(void) fprintf(vis_stderr, "From node:\n");
Ntk_NodePrint(vis_stderr, from, TRUE, TRUE);
fflush(vis_stderr);
assert(0);
}
bdd_ref(wireSpfd = bdd_bdd_and(ddManager,toSpfd,result));
bdd_recursive_deref(ddManager,result);
/* Convert wireSpfd from fanout space to fanin space */
/* Prepare the vectors for composition */
size = bdd_num_vars(ddManager);
firstCompose = ALLOC(bdd_node *,size);
secondCompose = ALLOC(bdd_node *,size);
for (i = 0; i < size; i++) {
firstCompose[i] = bdd_bdd_ith_var(ddManager,i);
secondCompose[i] = bdd_bdd_ith_var(ddManager,i);
}
arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
int id,auxId;
id = Ntk_NodeReadMddId(fanin);
auxId = SpfdNodeReadAuxId(applData,fanin);
st_lookup(currBddReq,(char *)fanin,(char **)&firstCompose[id]);
secondCompose[auxId] = firstCompose[id];
}
/* Perform the steps of compose --> existential abstraction twice */
bdd_ref(step1 = bdd_bdd_vector_compose(ddManager,wireSpfd,firstCompose));
bdd_recursive_deref(ddManager,wireSpfd);
FREE(firstCompose);
bdd_ref(inter = bdd_bdd_and_abstract(ddManager,faninRel,step1,xCube));
bdd_recursive_deref(ddManager,step1);
/* The second of compose --> existential abstraction steps */
bdd_ref(ddTemp = bdd_bdd_vector_compose(ddManager,inter,secondCompose));
bdd_recursive_deref(ddManager,inter);
FREE(secondCompose);
bdd_ref(final = bdd_bdd_and_abstract(ddManager,faninRelAux,
ddTemp,xCube));
bdd_recursive_deref(ddManager,ddTemp);
/* Now 'final' is in the fanin space */
if (final == logicZero) {
st_table *sinkTable;
Ntk_Node_t *tempNode;
boolean add;
/* Check if this wire has already been removed. If yes, skip */
add = TRUE;
if (st_lookup(wiresRemoved,(char *)from,&sinkTable) &&
st_lookup(sinkTable,(char *)to,&tempNode)) {
add = FALSE;
}
if (add) {
if (spfdVerbose > 2)
(void) fprintf(vis_stdout,
"** spfd info: wire %s --> %s has empty spfd.\n",
Ntk_NodeReadName(from),Ntk_NodeReadName(to));
/* Add to the wireTable */
if (st_lookup(wireTable,(char *)from,&sinkTable)) {
st_insert(sinkTable,(char *)to,(char *)to);
} else {
sinkTable = st_init_table(st_ptrcmp,st_ptrhash);
st_insert(sinkTable,(char *)to,(char *)to);
st_insert(wireTable,(char *)from,(char *)sinkTable);
}
}
}
bdd_ref(ddTemp = bdd_bdd_or(ddManager,fromSpfd,final));
bdd_recursive_deref(ddManager,fromSpfd);
bdd_recursive_deref(ddManager,final);
fromSpfd = ddTemp;
}
bdd_recursive_deref(ddManager,faninRel);
bdd_recursive_deref(ddManager,faninRelAux);
/* Swap variables for fromSpfd if necessary */
if (piSwap) { /* If we have used alternate PI ids */
ddTemp = SpfdSwapPiAndAltPi(applData,fromSpfd);
bdd_recursive_deref(ddManager,fromSpfd);
fromSpfd = ddTemp;
}
return fromSpfd;
} /* End of SpfdNodeComputeSpfdFromFanouts */
Here is the call graph for this function:
Here is the caller graph for this function:
| bdd_node* SpfdNodeComputeSpfdFromOnAndOffSet | ( | SpfdApplData_t * | applData, |
| Ntk_Node_t * | regNode, | ||
| bdd_node * | bdd1, | ||
| bdd_node * | bdd0 | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Given two functions represented by bdd1 and bdd0, compute its SPFD.]
SideEffects [None]
Definition at line 77 of file spfdSpfd.c.
{
bdd_manager *ddManager = applData->ddManager;
int numFanin = Ntk_NodeReadNumFanins(regNode);
bdd_node **yVars,**yAuxVars;
bdd_node *ddTemp,*rel,*spfd;
Ntk_Node_t *fanin;
int j,clean;
/* If bdd1 and bdd0 are not specified, replace bdd1 and bdd0 by the
node's local ON-set and OFF-set respectively */
clean = 0;
if (bdd1 == NIL(bdd_node) ||
bdd0 == NIL(bdd_node)) {
Ntk_Network_t *network;
network = Ntk_NodeReadNetwork(regNode);
bdd_ref(bdd1 = SpfdNodeReadLocalBdd(network,regNode));
bdd_ref(bdd0 = bdd_not_bdd_node(bdd1));
/* Delete bdd1 and bdd0 at the end.*/
clean = 1;
}
/* Array of variables for swapping */
numFanin = Ntk_NodeReadNumFanins(regNode);
yVars = ALLOC(bdd_node *,numFanin);
yAuxVars = ALLOC(bdd_node *,numFanin);
Ntk_NodeForEachFanin(regNode,j,fanin) {
yVars[j] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
yAuxVars[j] = bdd_bdd_ith_var(ddManager,
SpfdNodeReadAuxId(applData,fanin));
}
/* spfd is bdd1(y) * bdd0(y') + bdd1(y') * bdd0(y) */
bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,bdd0,
yVars,yAuxVars,numFanin));
bdd_ref(rel = bdd_bdd_and(ddManager,bdd1,ddTemp));
bdd_recursive_deref(ddManager,ddTemp);
bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,rel,
yVars,yAuxVars,numFanin));
bdd_ref(spfd = bdd_bdd_or(ddManager,rel,ddTemp));
bdd_recursive_deref(ddManager,rel);
bdd_recursive_deref(ddManager,ddTemp);
FREE(yVars);
FREE(yAuxVars);
if (clean) {
bdd_recursive_deref(ddManager,bdd1);
bdd_recursive_deref(ddManager,bdd0);
}
return spfd;
} /* End of SpfdNodeComputeSpfdFromOnAndOffSet */
Here is the call graph for this function:
Here is the caller graph for this function:
