#include "maig.h"#include "ntk.h"#include "cmd.h"#include "baig.h"#include "baigInt.h"#include "heap.h"#include "sat.h"#include "bmc.h"
Include dependency graph for baigTimeframe.c:
Go to the source code of this file.
Functions | |
| static int | nameCompare (const void *node1, const void *node2) |
| static int | NoOfBitEncode (int n) |
| static bAigEdge_t | CaseNew (mAig_Manager_t *manager, bAigEdge_t *arr, array_t *encodeList, int index) |
| void | bAig_ExpandTimeFrame (Ntk_Network_t *network, mAig_Manager_t *manager, int bound, int withInitialState) |
| bAigTimeFrame_t * | bAig_InitTimeFrame (Ntk_Network_t *network, mAig_Manager_t *manager, int withInitialState) |
| void | bAig_CreateNewNode (mAig_Manager_t *manager, st_table *node2MvfAigTable, Ntk_Node_t *node, bAigEdge_t *bli, bAigEdge_t *li, int *bindex, int *index) |
| bAigEdge_t | bAig_ExpandForEachCone (mAig_Manager_t *manager, bAigEdge_t v, st_table *old2new) |
| void | bAig_CheckConnect (bAig_Manager_t *manager, int from, int to) |
| int | bAig_CheckConnectFanin (bAig_Manager_t *manager, int from, int to) |
| int | bAig_CheckConnectFanout (bAig_Manager_t *manager, int from, int to) |
| void | bAig_GetCOIForNode (Ntk_Node_t *node, st_table *table) |
| void | bAig_GetCOIForNodeMain (Ntk_Network_t *network, char *name) |
| void | bAig_CheckLatchStatus (Ntk_Network_t *network, bAig_Manager_t *manager) |
| void | bAig_PrintNodeAigStatus (bAig_Manager_t *manager, Ntk_Node_t *node) |
| void | bAig_PrintNodeAigStatusWithName (Ntk_Network_t *network, bAig_Manager_t *manager, char *name) |
| void | bAig_FreeTimeFrame (bAigTimeFrame_t *timeframe) |
Variables | |
| static char rcsid[] | UNUSED = "$ $" |
Function Documentation
| void bAig_CheckConnect | ( | bAig_Manager_t * | manager, |
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Check connectivity between aig nodes]
Description [Check connectivity between aig nodes]
SideEffects []
SeeAlso []
Definition at line 1061 of file baigTimeframe.c.
{
int reached;
reached = bAig_CheckConnectFanin(manager, from, leftChild(to));
if(reached == 0)
reached = bAig_CheckConnectFanin(manager, from, rightChild(to));
if(reached == 0)
fprintf(stdout, "Node %d is not (backward) reachable from node %d\n",
from, to);
reached = bAig_CheckConnectFanout(manager, from, to);
if(reached == 0)
fprintf(stdout, "Node %d is not (forward) reachable from node %d\n",
to, from);
}
Here is the call graph for this function:
| int bAig_CheckConnectFanin | ( | bAig_Manager_t * | manager, |
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Check connectivity of each fanin aig nodes]
Description [Check connectivity of each fanin aig nodes]
SideEffects []
SeeAlso []
Definition at line 1095 of file baigTimeframe.c.
{
int left, right;
int reached;
if(bAig_NonInvertedEdge(from) == bAig_NonInvertedEdge(to))
return(1);
left = leftChild(to);
if(left == 2)
return(0);
right = leftChild(to);
reached = bAig_CheckConnectFanin(manager, from, left);
if(reached == 1)
return(1);
reached = bAig_CheckConnectFanin(manager, from, right);
if(reached == 1)
return(1);
return(0);
}
Here is the caller graph for this function:
| int bAig_CheckConnectFanout | ( | bAig_Manager_t * | manager, |
| int | from, | ||
| int | to | ||
| ) |
Function********************************************************************
Synopsis [Check connectivity of each fanout aig nodes]
Description [Check connectivity of each fanout aig nodes]
SideEffects []
SeeAlso []
Definition at line 1133 of file baigTimeframe.c.
{
long *pfan, cur;
int size, j;
int reached;
size = nFanout(from);
for(j=0, pfan = (bAigEdge_t *)fanout(from); j<size; j++) {
cur = pfan[j];
cur = cur >> 1;
reached = bAig_CheckConnectFanout(manager, cur, to);
if(reached == 1)
return(1);
}
return(0);
}
Here is the caller graph for this function:
| void bAig_CheckLatchStatus | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager | ||
| ) |
Function********************************************************************
Synopsis [Check status of latch]
Description [Check status of latch]
SideEffects []
SeeAlso []
Definition at line 1251 of file baigTimeframe.c.
{
Ntk_Node_t *node;
Ntk_Node_t *data, *init;
lsGen gen;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
int tindex1, v, i, lmAigId;
array_t *mVarList, *bVarList;
mVarList = mAigReadMulVarList(manager);
bVarList = mAigReadBinVarList(manager);
Ntk_NetworkForEachNode(network, gen, node) {
if(Ntk_NodeTestIsPrimaryInput(node)) {
fprintf(stdout, "Primary I %s :", Ntk_NodeReadName(node));
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
}
}
Ntk_NetworkForEachNode(network, gen, node) {
if(Ntk_NodeTestIsPseudoInput(node)) {
fprintf(stdout, "Pseudo I %s :", Ntk_NodeReadName(node));
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
}
}
Ntk_NetworkForEachNode(network, gen, node) {
if (Ntk_NodeTestIsLatch(node)){
fprintf(stdout, "Latch %s :", Ntk_NodeReadName(node));
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
data = Ntk_LatchReadDataInput(node);
fprintf(stdout, " data input %s :", Ntk_NodeReadName(data));
lmAigId = Ntk_NodeReadMAigId(data);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
init = Ntk_LatchReadInitialInput(node);
fprintf(stdout, " latch init %s :", Ntk_NodeReadName(init));
lmAigId = Ntk_NodeReadMAigId(init);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
}
}
Ntk_NetworkForEachNode(network, gen, node) {
lmAigId = Ntk_NodeReadMAigId(node);
if(lmAigId == 2 || lmAigId == 0) {
fprintf(stdout, "node aig id %s\n", Ntk_NodeReadName(node));
}
}
}
Here is the call graph for this function:
| void bAig_CreateNewNode | ( | mAig_Manager_t * | manager, |
| st_table * | node2MvfAigTable, | ||
| Ntk_Node_t * | node, | ||
| bAigEdge_t * | bli, | ||
| bAigEdge_t * | li, | ||
| int * | bindex, | ||
| int * | index | ||
| ) |
Function********************************************************************
Synopsis [Create aig node for free variables]
Description [Create aig node for free variables, such as primary input and pseudo input]
SideEffects []
SeeAlso []
if(v == bAig_Zero) li[(*index)++] = bAig_Zero; else if(v == bAig_One) li[(*index)++] = bAig_One; else { }
Definition at line 853 of file baigTimeframe.c.
{
int i, j, value, noBits;
bAigEdge_t *arr, v, tv;
MvfAig_Function_t *mvfAig;
array_t *encodeList;
bAigEdge_t *ManagerNodesArray;
bAigTimeFrame_t *timeframe;
timeframe = manager->timeframe;
value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
noBits = NoOfBitEncode(value);
arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
mvfAig = 0;
st_lookup(node2MvfAigTable, node, &mvfAig);
for(i=0; i<noBits; i++) {
arr[i] = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
bli[(*bindex)++] = arr[i];
flags(arr[i]) |= IsSystemMask;
}
for(i=0; i<value; i++) {
v = MvfAig_FunctionReadComponent(mvfAig, i);
encodeList = array_alloc(bAigEdge_t, 0);
for(j=0; j<value; j++) {
if(j == i)array_insert_last(bAigEdge_t, encodeList, mAig_One);
else array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
}
tv = CaseNew(manager, arr, encodeList, noBits-1);
li[(*index)++] = tv;
ManagerNodesArray = manager->NodesArray;
array_free(encodeList);
if(v == bAig_Zero){
flags(tv) |= StaticLearnMask;
if(timeframe->assertedArray == 0)
timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
array_insert_last(bAigEdge_t, timeframe->assertedArray, bAig_Not(tv));
}
else if(v == bAig_One){
flags(tv) |= StaticLearnMask;
if(timeframe->assertedArray == 0)
timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
array_insert_last(bAigEdge_t, timeframe->assertedArray, tv);
}
}
free(arr);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| bAigEdge_t bAig_ExpandForEachCone | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| st_table * | old2new | ||
| ) |
Function********************************************************************
Synopsis [Expand timeframe for aig node ]
Description [Expand timeframe for aig node ]
SideEffects []
SeeAlso []
Definition at line 1013 of file baigTimeframe.c.
{
bAigEdge_t left, right, nv;
v = bAig_GetCanonical(manager, v);
if(v == bAig_One || v == bAig_Zero) return(v);
if(v == bAig_NULL) {
fprintf(vis_stdout, "current error\n");
return(v);
}
if(st_lookup(old2new, (char *)v, &nv))
return(nv);
if(st_lookup(old2new, (char *)bAig_Not(v), &nv))
return(bAig_Not(nv));
left = bAig_ExpandForEachCone(manager, leftChild(v), old2new);
right = bAig_ExpandForEachCone(manager, rightChild(v), old2new);
nv = bAig_And(manager, left, right);
flags(nv) |= IsSystemMask;
if(bAig_IsInverted(v)) nv = bAig_Not(nv);
st_insert(old2new, (char *)v, (char *)nv);
return(nv);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_ExpandTimeFrame | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| int | bound, | ||
| int | withInitialState | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Expand timeframe n times]
Description [Expand timeframe n times. If withInitialState flag is set then unroll transition function considering initial states, otherwise the state variables of 0'th timeframe are free variables]
SideEffects []
SeeAlso []
create new primary input node
map previous time frame into current
create new time frame
fprintf(vis_stdout, "-------------------------------\n"); fprintf(vis_stdout, " Latch input %d %d\n", v, manager->nodesArraySize); fprintf(vis_stdout, "-------------------------------\n"); bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
fprintf(vis_stdout, "-------------------------------\n"); fprintf(vis_stdout, " Output %d\n", v); fprintf(vis_stdout, "-------------------------------\n"); bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
Definition at line 85 of file baigTimeframe.c.
{
bAigTimeFrame_t *timeframe;
int nLatches, nInputs, nOutputs, nInternals;
int nbLatches, nbInputs;
int i, j;
int index, index1, bindex, tindex;
int mvfSize, lmvfSize;
int lmAigId;
array_t *iindexArray;
MvfAig_Function_t *mvfAig, *lmvfAig;
bAigEdge_t *li, *bli;
bAigEdge_t *pre_li, *ori_li;
bAigEdge_t v, nv = bAig_NULL;
Ntk_Node_t *node, *latch;
st_table *node2MvfAigTable, *old2new;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
array_t *bVarList, *mVarList;
lsGen gen;
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
if(timeframe == 0)
timeframe = bAig_InitTimeFrame(network, manager, withInitialState);
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
nbLatches = timeframe->nbLatches;
nbInputs = timeframe->nbInputs;
nLatches = timeframe->nLatches;
nInputs = timeframe->nInputs;
nOutputs = timeframe->nOutputs;
nInternals = timeframe->nInternals;
iindexArray = timeframe->iindexArray;
if(bound > timeframe->currentTimeframe) {
timeframe->latchInputs = (bAigEdge_t **)
realloc(timeframe->latchInputs, sizeof(bAigEdge_t *)*(bound+2));
timeframe->inputs = (bAigEdge_t **)
realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(bound+1));
timeframe->blatchInputs = (bAigEdge_t **)
realloc(timeframe->blatchInputs, sizeof(bAigEdge_t *)*(bound+2));
timeframe->binputs = (bAigEdge_t **)
realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(bound+1));
timeframe->outputs = (bAigEdge_t **)
realloc(timeframe->outputs, sizeof(bAigEdge_t *)*(bound+1));
timeframe->internals = (bAigEdge_t **)
realloc(timeframe->internals, sizeof(bAigEdge_t *)*(bound+1));
}
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
for(j=timeframe->currentTimeframe+1; j<=bound; j++) {
timeframe->inputs = (bAigEdge_t **)
realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(j+1));
timeframe->binputs = (bAigEdge_t **)
realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(j+1));
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
timeframe->binputs[j] = bli;
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
timeframe->inputs[j] = li;
index = 0;
index1 = 0;
bindex = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
index1++;
}
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
index1++;
}
}
old2new = st_init_table(st_ptrcmp, st_ptrhash);
pre_li = timeframe->inputs[j];
ori_li = timeframe->oriInputs;
for(i=0; i<nInputs; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->latchInputs[j];
ori_li = timeframe->oriLatchInputs;
for(i=0; i<nLatches; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->binputs[j];
ori_li = timeframe->oribInputs;
for(i=0; i<nbInputs; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->blatchInputs[j];
ori_li = timeframe->oribLatchInputs;
for(i=0; i<nbLatches; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
timeframe->latchInputs[j+1] = li;
timeframe->blatchInputs[j+1] = bli;
bindex = index = 0;
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadDataInput(latch);
mvfAig = lmvfAig = 0;
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
st_lookup(node2MvfAigTable, latch, &lmvfAig);
lmvfSize = array_n(lmvfAig);
if(mvfSize != lmvfSize) {
fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
fprintf(vis_stdout, " %s(%d), %s(%d)\n",
Ntk_NodeReadName(node), mvfSize,
Ntk_NodeReadName(latch), lmvfSize);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
for(i=mvfSize; i< lmvfSize; i++){
li[index++] = nv;
}
}
else {
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
flags(nv) |= StateBitMask;
st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n",
j+1, Ntk_NodeReadName(latch), i, v, nv);
#endif
li[index++] = nv;
}
}
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
tindex++;
v = bAig_GetCanonical(manager, lbVar.node);
nv = bAig_ExpandForEachCone(manager, v, old2new);
flags(nv) |= StateBitMask;
st_insert(old2new, (char *)v, (char *)nv);
bli[bindex++] = nv;
}
}
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
timeframe->outputs[j] = li;
index = 0;
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", j+1, Ntk_NodeReadName(node), i, v, li[index]);
#endif
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
}
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
timeframe->internals[j] = li;
for(i=0; i<array_n(iindexArray); i++) {
v = array_fetch(bAigEdge_t, iindexArray, i);
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[i] = nv;
}
st_free_table(old2new);
}
timeframe->currentTimeframe = bound;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_FreeTimeFrame | ( | bAigTimeFrame_t * | timeframe | ) |
Function********************************************************************
Synopsis [ Free timeframe ]
Description [ Free timeframe ]
SideEffects []
SeeAlso []
Definition at line 1396 of file baigTimeframe.c.
{
int i;
long *li;
if(timeframe == 0) return;
if(timeframe->li2index) st_free_table(timeframe->li2index);
if(timeframe->o2index) st_free_table(timeframe->o2index);
if(timeframe->i2index) st_free_table(timeframe->i2index);
if(timeframe->pi2index) st_free_table(timeframe->pi2index);
if(timeframe->latchArr) array_free(timeframe->latchArr);
if(timeframe->inputArr) array_free(timeframe->inputArr);
if(timeframe->outputArr) array_free(timeframe->outputArr);
if(timeframe->iindexArray) array_free(timeframe->iindexArray);
if(timeframe->assertedArray) array_free(timeframe->assertedArray);
if(timeframe->oriLatchInputs)free(timeframe->oriLatchInputs);
if(timeframe->oriInputs) free(timeframe->oriInputs);
if(timeframe->oribLatchInputs)free(timeframe->oribLatchInputs);
if(timeframe->oribInputs) free(timeframe->oribInputs);
if(timeframe->inputs) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->inputs[i];
if(li) free(li);
}
free(timeframe->inputs);
}
if(timeframe->binputs) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->binputs[i];
if(li) free(li);
}
free(timeframe->binputs);
}
if(timeframe->outputs) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->outputs[i];
if(li) free(li);
}
free(timeframe->outputs);
}
if(timeframe->latchInputs) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->latchInputs[i];
if(li) free(li);
}
free(timeframe->latchInputs);
}
if(timeframe->blatchInputs) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->blatchInputs[i];
if(li) free(li);
}
free(timeframe->blatchInputs);
}
if(timeframe->internals) {
for(i=0; i<timeframe->currentTimeframe; i++) {
li = timeframe->internals[i];
if(li) free(li);
}
free(timeframe->internals);
}
}
Here is the caller graph for this function:
| void bAig_GetCOIForNode | ( | Ntk_Node_t * | node, |
| st_table * | table | ||
| ) |
Function********************************************************************
Synopsis [Get cone of influence nodes of given aig node]
Description [Get cone of influence nodes of given aig node]
SideEffects []
SeeAlso []
Definition at line 1163 of file baigTimeframe.c.
{
int i;
Ntk_Node_t *faninNode;
if(node == NIL(Ntk_Node_t)){
return;
}
if (Ntk_NodeTestIsLatch(node)){
st_insert(table, (char *)node, (char *)node);
return;
}
Ntk_NodeForEachFanin(node, i, faninNode) {
bAig_GetCOIForNode(faninNode, table);
}
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_GetCOIForNodeMain | ( | Ntk_Network_t * | network, |
| char * | name | ||
| ) |
Function********************************************************************
Synopsis [Print cone of influence nodes of given aig node]
Description [Print cone of influence nodes of given aig node]
SideEffects []
SeeAlso []
Definition at line 1194 of file baigTimeframe.c.
{
int i, found;
Ntk_Node_t *node, *faninNode;
lsGen gen;
st_generator *gen1;
st_table *table;
node = Ntk_NetworkFindNodeByName(network, name);
if(node == 0) {
found = 0;
Ntk_NetworkForEachNode(network, gen, node) {
if(!strcmp(Ntk_NodeReadName(node), name)) {
found = 1;
break;
}
}
if(found == 0)
node = 0;
}
if(node == NIL(Ntk_Node_t)){
return;
}
if (Ntk_NodeTestIsLatch(node)){
fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
return;
}
table = st_init_table(st_ptrcmp, st_ptrhash);
Ntk_NodeForEachFanin(node, i, faninNode) {
bAig_GetCOIForNode(faninNode, table);
}
st_foreach_item(table, gen1, &node, &node) {
fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
}
st_free_table(table);
return;
}
Here is the call graph for this function:
| bAigTimeFrame_t* bAig_InitTimeFrame | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Make first timeframe]
Description [Make first timeframe]
SideEffects []
SeeAlso []
count total number, insert into node array and make table for bAigEdge_t to index
make 0 index bAigEdge_t
map node of previous timeframe into current timeframe
create timeframe
Definition at line 348 of file baigTimeframe.c.
{
bAigTimeFrame_t *timeframe;
array_t *latchArr, *inputArr, *outputArr;
array_t *iindexArray;
st_table *li2index, *o2index, *i2index, *pi2index;
st_table *bli2index, *bpi2index;
Ntk_Node_t *node, *latch;
st_table *node2MvfAigTable, *old2new;
lsGen gen;
int nLatches, nInputs, nOutputs, nInternals;
int nbLatches, nbInputs;
int i;
int index, index1, mvfSize, lmvfSize;
int bindex, tindex, tindex1;
MvfAig_Function_t *mvfAig, *tmpMvfAig, *lmvfAig;
bAigEdge_t *li, *pre_li, *ori_li;
bAigEdge_t *bli, *ori_bli;
bAigEdge_t v=bAig_NULL, nv;
mAigMvar_t mVar;
mAigBvar_t bVar;
array_t *bVarList, *mVarList;
int mAigId;
int lmAigId;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
node2MvfAigTable =
(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
timeframe = ALLOC(bAigTimeFrame_t, 1);
memset(timeframe, 0, sizeof(bAigTimeFrame_t));
if(withInitialState) manager->timeframe = timeframe;
else manager->timeframeWOI = timeframe;
latchArr = array_alloc(Ntk_Node_t *, 0);
inputArr = array_alloc(Ntk_Node_t *, 0);
outputArr = array_alloc(Ntk_Node_t *, 0);
timeframe->latchArr = latchArr;
timeframe->inputArr = inputArr;
timeframe->outputArr = outputArr;
li2index = st_init_table(st_ptrcmp, st_ptrhash);
o2index = st_init_table(st_ptrcmp, st_ptrhash);
i2index = st_init_table(st_ptrcmp, st_ptrhash);
pi2index = st_init_table(st_ptrcmp, st_ptrhash);
bli2index = st_init_table(st_ptrcmp, st_ptrhash);
bpi2index = st_init_table(st_ptrcmp, st_ptrhash);
timeframe->li2index = li2index;
timeframe->o2index = o2index;
timeframe->pi2index = pi2index;
timeframe->i2index = i2index;
timeframe->bli2index = bli2index;
timeframe->bpi2index = bpi2index;
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
nLatches = 0;
nbLatches = 0;
Ntk_NetworkForEachLatch(network, gen, latch) {
array_insert_last(Ntk_Node_t *, latchArr, latch);
st_lookup(node2MvfAigTable, latch, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(li2index, (char *)v, (char *)(long)nLatches++);
}
mAigId = Ntk_NodeReadMAigId(latch);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1);
st_insert(bli2index, (char *)bVar.node, (char *)(long)nbLatches++);
index1++;
}
}
timeframe->nLatches = nLatches;
timeframe->nbLatches = nbLatches;
nOutputs = 0;
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
array_insert_last(Ntk_Node_t *, outputArr, node);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(o2index, (char *)(long)v, (char *)(long)nOutputs++);
}
}
timeframe->nOutputs = nOutputs;
timeframe->iindexArray = iindexArray = array_alloc(bAigEdge_t, 0);
nInternals = 0;
Ntk_NetworkForEachNode(network, gen, node) {
if(Ntk_NodeTestIsShadow(node)) continue;
if(Ntk_NodeTestIsCombInput(node)) continue;
if(Ntk_NodeTestIsCombOutput(node))continue;
if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
}
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
if(!st_lookup(i2index, (char *)v, &index1)) {
array_insert_last(bAigEdge_t, iindexArray, v);
st_insert(i2index, (char *)v, (char *)(long)nInternals++);
}
}
#ifdef TIMEFRAME_VERIFY_
if(!strcmp(Ntk_NodeReadName(node), "v25") ||
!strcmp(Ntk_NodeReadName(node), "v27")) {
fprintf(stdout, "current error %d %d\n", v, nInternals);
}
#endif
}
timeframe->nInternals = nInternals;
nInputs = 0;
nbInputs = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
array_insert_last(Ntk_Node_t *, inputArr, node);
if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
}
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
}
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1);
st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
index1++;
}
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
array_insert_last(Ntk_Node_t *, inputArr, node);
if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
tmpMvfAig = Bmc_NodeBuildMVF(network, node);
array_free(tmpMvfAig);
mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
}
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
}
mAigId = Ntk_NodeReadMAigId(node);
mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
bVar = array_fetch(mAigBvar_t, bVarList, index1);
st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
index1++;
}
}
timeframe->nInputs = nInputs;
timeframe->nbInputs = nbInputs;
array_sort(inputArr, nameCompare);
array_sort(latchArr, nameCompare);
array_sort(outputArr, nameCompare);
old2new = st_init_table(st_ptrcmp, st_ptrhash);
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
index1 = index = 0;
bindex = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
st_insert(old2new, (char *)v, (char *)(li[index1++]));
}
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
st_insert(old2new, (char *)v, (char *)(li[index1++]));
}
}
timeframe->blatchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
timeframe->blatchInputs[0] = bli;
timeframe->latchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
timeframe->latchInputs[0] = li;
ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
timeframe->oriLatchInputs = ori_li;
timeframe->oribLatchInputs = ori_bli;
index1 = index = 0;
bindex = tindex = tindex1 = 0;
if(withInitialState == 0) {
Ntk_NetworkForEachLatch(network, gen, latch) {
bAig_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, latch, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(old2new, (char *)v, (char *)(li[index1]));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
#endif
ori_li[index1++] = v;
}
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
tindex1++;
v = bAig_GetCanonical(manager, lbVar.node);
ori_bli[tindex++] = v ;
}
}
}
else {
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadInitialInput(latch);
mvfAig = lmvfAig = 0;
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
if(!st_lookup(node2MvfAigTable, latch, &lmvfAig)) {
tmpMvfAig = Bmc_NodeBuildMVF(network, latch);
array_free(tmpMvfAig);
lmvfAig = Bmc_ReadMvfAig(latch, node2MvfAigTable);
}
lmvfSize = array_n(lmvfAig);
if(mvfSize != lmvfSize) {
fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
fprintf(vis_stdout, " %s(%d), %s(%d)\n",
Ntk_NodeReadName(node), mvfSize,
Ntk_NodeReadName(latch), lmvfSize);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
for(i=mvfSize; i<lmvfSize; i++) {
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
}
else {
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
}
for(i=0; i< lmvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(lmvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
#endif
ori_li[index1++] = v;
}
lmAigId = Ntk_NodeReadMAigId(latch);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
tindex1++;
v = bAig_GetCanonical(manager, lbVar.node);
ori_bli[tindex++] = v;
}
node = Ntk_LatchReadInitialInput(latch);
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
tindex1++;
v = bAig_GetCanonical(manager, lbVar.node);
if(st_lookup(old2new, (char *)v, &nv))
bli[bindex++] = nv;
else
bli[bindex++] = v;
}
}
}
st_free_table(old2new);
timeframe->binputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
timeframe->binputs[0] = bli;
timeframe->inputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
timeframe->inputs[0] = li;
timeframe->oriInputs = ori_li;
timeframe->oribInputs = ori_bli;
index1 = index = 0;
tindex = bindex = tindex1 = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
ori_li[index1++] = v;
}
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
tindex1++;
v = bAig_GetCanonical(manager, lbVar.node);
ori_bli[tindex++] = v;
}
}
Ntk_NetworkForEachPseudoInput(network, gen, node) {
bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
ori_li[index1++] = v;
}
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
tindex1++;
v = bAig_GetCanonical(manager, lbVar.node);
ori_bli[tindex++] = v;
}
}
old2new = st_init_table(st_ptrcmp, st_ptrhash);
pre_li = timeframe->inputs[0];
ori_li = timeframe->oriInputs;
for(i=0; i<nInputs; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->latchInputs[0];
ori_li = timeframe->oriLatchInputs;
for(i=0; i<nLatches; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->binputs[0];
ori_li = timeframe->oribInputs;
for(i=0; i<nbInputs; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
pre_li = timeframe->blatchInputs[0];
ori_li = timeframe->oribLatchInputs;
for(i=0; i<nbLatches; i++)
st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
timeframe->latchInputs[1] = li;
bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
timeframe->blatchInputs[1] = bli;
bindex = index = 0;
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadDataInput(latch);
mvfAig = lmvfAig = 0;
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
st_lookup(node2MvfAigTable, latch, &lmvfAig);
lmvfSize = array_n(lmvfAig);
if(mvfSize != lmvfSize) {
fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
fprintf(vis_stdout, " %s(%d), %s(%d)\n",
Ntk_NodeReadName(node), mvfSize,
Ntk_NodeReadName(latch), lmvfSize);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
for(i=mvfSize; i< lmvfSize; i++){
li[index++] = nv;
}
}
else {
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
/* flags(nv) |= StateBitMask; */
st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n",
1, Ntk_NodeReadName(latch), i, v, nv);
#endif
li[index++] = nv;
}
}
/* State bit mapping **/
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
tindex++;
v = bAig_GetCanonical(manager, lbVar.node);
nv = bAig_ExpandForEachCone(manager, v, old2new);
flags(nv) |= StateBitMask;
st_insert(old2new, (char *)v, (char *)nv);
bli[bindex++] = nv;
}
}
timeframe->outputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
timeframe->outputs[0] = li;
index = 0;
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
nv = bAig_ExpandForEachCone(manager, v, old2new);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index]);
#endif
st_insert(old2new, (char *)v, (char *)nv);
li[index++] = nv;
}
}
index = 0;
timeframe->internals = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
timeframe->internals[0] = li;
for(i=0; i<array_n(iindexArray); i++) {
v = array_fetch(bAigEdge_t, iindexArray, i);
nv = bAig_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[i] = nv;
}
st_free_table(old2new);
timeframe->currentTimeframe = 0;
return(timeframe);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_PrintNodeAigStatus | ( | bAig_Manager_t * | manager, |
| Ntk_Node_t * | node | ||
| ) |
Function********************************************************************
Synopsis [Print status of aig node]
Description [Print status of aig node]
SideEffects []
SeeAlso []
Definition at line 1344 of file baigTimeframe.c.
{
mAigMvar_t lmVar;
mAigBvar_t lbVar;
int tindex1, v, i, lmAigId;
array_t *mVarList, *bVarList;
mVarList = mAigReadMulVarList(manager);
bVarList = mAigReadBinVarList(manager);
fprintf(stdout, "node %s :", Ntk_NodeReadName(node));
lmAigId = Ntk_NodeReadMAigId(node);
lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
v = bAig_GetCanonical(manager, lbVar.node);
fprintf(stdout, "%d ", v);
}
fprintf(stdout, "\n");
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_PrintNodeAigStatusWithName | ( | Ntk_Network_t * | network, |
| bAig_Manager_t * | manager, | ||
| char * | name | ||
| ) |
Function********************************************************************
Synopsis [Check status of aig node]
Description [Check status of aig node]
SideEffects []
SeeAlso []
Definition at line 1376 of file baigTimeframe.c.
{
Ntk_Node_t *node;
node = Ntk_NetworkFindNodeByName(network, name);
bAig_PrintNodeAigStatus(manager, node);
}
Here is the call graph for this function:
| static bAigEdge_t CaseNew | ( | mAig_Manager_t * | manager, |
| bAigEdge_t * | arr, | ||
| array_t * | encodeList, | ||
| int | index | ||
| ) | [static] |
Function********************************************************************
Synopsis [Extract bit from multi valued array]
Description [Extract bit from multi valued array]
SideEffects []
SeeAlso []
Definition at line 956 of file baigTimeframe.c.
{
int encodeLen;
int i, count;
bAigEdge_t v;
bAigEdge_t andResult1, andResult2, orResult, result;
bAigEdge_t node1, node2;
array_t *newEncodeList;
encodeLen = array_n(encodeList);
if (encodeLen == 1)
return array_fetch(bAigEdge_t, encodeList, 0);
newEncodeList = array_alloc(bAigEdge_t, 0);
v = arr[index];
count = 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(manager, v, node2);
andResult2 = bAig_And(manager, bAig_Not(v), node1);
orResult = bAig_Or (manager, andResult1, andResult2);
flags(andResult1) |= IsSystemMask;
flags(andResult2) |= IsSystemMask;
flags(orResult) |= IsSystemMask;
array_insert_last(bAigEdge_t, newEncodeList, orResult);
}
if(encodeLen%2){
node1 = array_fetch(bAigEdge_t, encodeList, count);
array_insert_last(bAigEdge_t, newEncodeList, node1);
}
result = CaseNew(manager, arr, newEncodeList, index-1);
array_free(newEncodeList);
return(result);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int nameCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Compare function for name ordering]
Description [Compare function for name ordering]
SideEffects []
SeeAlso []
Definition at line 323 of file baigTimeframe.c.
{
char *name1, *name2;
name1 = Ntk_NodeReadName((Ntk_Node_t *)node1);
name2 = Ntk_NodeReadName((Ntk_Node_t *)node2);
return(strcmp(*(char**)name1, *(char **)name2));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int NoOfBitEncode | ( | int | n | ) | [static] |
Function********************************************************************
Synopsis [Compute bits is needed for encode n]
Description [Compute bits is needed for encode n]
SideEffects []
SeeAlso []
Definition at line 930 of file baigTimeframe.c.
{
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;
}
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$ $" [static] |
CFile***********************************************************************
FileName [baigTimeframe.c]
PackageName [baig]
Synopsis [Functions to manage timeframe expansion.]
Author [HoonSang Jin]
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.]
Definition at line 27 of file baigTimeframe.c.
