#include "ntmaigInt.h"
Include dependency graph for ntmaigCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandBuildPartitionMAigs (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static int | nodenameCompare (const void *node1, const void *node2) |
| void | bAig_BuildAigBFSManner (Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep) |
| void | bAig_BddSweepMain (Ntk_Network_t *network, array_t *nodeArray) |
| void | ntmaig_Init (void) |
| void | ntmaig_End (void) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: ntmaigCmd.c,v 1.26 2009/01/18 01:54:51 fabio Exp $" |
Function Documentation
| void bAig_BddSweepMain | ( | Ntk_Network_t * | network, |
| array_t * | nodeArray | ||
| ) |
Function********************************************************************
Synopsis [BDD sweeping for aig nodes]
Description [BDD sweeping for aig nodes rooted at latch data inputs and primary outputs]
SideEffects []
SeeAlso []
Definition at line 120 of file baigBddSweep.c.
{
array_t *mVarList, *bVarList;
bdd_t *bdd, *func;
int bddIdIndex;
int i, count, sizeLimit, mvfSize;
int maxSize, curSize;
array_t *tnodeArray;
lsGen gen;
st_generator *gen1;
Ntk_Node_t *node;
bAigEdge_t v;
MvfAig_Function_t *mvfAig;
mAig_Manager_t *manager;
mdd_manager *mgr;
st_table *node2MvfAigTable;
st_table * bdd2vertex;
mAigMvar_t mVar;
mAigBvar_t bVar;
int index1, mAigId;
manager = Ntk_NetworkReadMAigManager(network);
mgr = Ntk_NetworkReadMddManager(network);
if(mgr == 0) {
Ord_NetworkOrderVariables(network, Ord_RootsByDefault_c,
Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
Ord_Unassigned_c, 0, 0);
mgr = Ntk_NetworkReadMddManager(network);
}
node2MvfAigTable =
(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
bdd2vertex = st_init_table(SweepBddCompare, SweepBddHash);
sizeLimit = 500;
maxSize = manager->nodesArraySize;
tnodeArray = 0;
if(nodeArray == 0) {
bVarList = mAigReadBinVarList(manager);
mVarList = mAigReadMulVarList(manager);
tnodeArray = array_alloc(bAigEdge_t, 0);
Ntk_NetworkForEachLatch(network, gen, node) {
node = Ntk_LatchReadDataInput(node);
st_lookup(node2MvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i<mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
array_insert_last(bAigEdge_t, tnodeArray, v);
}
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++);
v = bVar.node;
v = bAig_GetCanonical(manager, v);
array_insert_last(bAigEdge_t, tnodeArray, v);
}
}
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));
array_insert_last(bAigEdge_t, tnodeArray, v);
}
}
}
count = bAigNodeID(manager->nodesArraySize);
for(i=0; i<count; i++) {
manager->bddIdArray[i] = -1;
manager->bddArray[i] = 0;
}
manager->bddArray[0] = bdd_zero(mgr);
bddIdIndex = 0;
for(i=bAigNodeSize; i<manager->nodesArraySize; i+=bAigNodeSize) {
if(leftChild(i) != 2) continue;
bdd = bdd_get_variable(mgr, bddIdIndex);
manager->bddIdArray[bAigNodeID(i)] = bddIdIndex;
manager->bddArray[bAigNodeID(i)] = bdd;
bddIdIndex++;
}
if(nodeArray) {
for(i=0; i<array_n(nodeArray); i++) {
v = array_fetch(bAigEdge_t, nodeArray, i);
v = bAig_GetCanonical(manager, v);
bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
}
}
else {
for(i=0; i<array_n(tnodeArray); i++) {
v = array_fetch(bAigEdge_t, tnodeArray, i);
v = bAig_GetCanonical(manager, v);
bAig_BddSweepSub(manager, mgr, v, bdd2vertex, sizeLimit, &bddIdIndex);
}
array_free(tnodeArray);
}
count = bAigNodeID(manager->nodesArraySize);
for(i=0; i<count; i++) {
if(manager->bddArray[i]) {
bdd_free(manager->bddArray[i]);
manager->bddArray[i] = 0;
}
}
st_foreach_item(bdd2vertex, gen1, &func, &v) {
bdd_free(func);
}
st_free_table(bdd2vertex);
count = bAigNodeID(manager->nodesArraySize);
curSize = 0;
for(i=0; i<count; i++) {
if(bAigGetPassFlag(manager, i*bAigNodeSize)) {
curSize++;
}
}
/*
fprintf(vis_stdout, "NOTICE : Before %d after %d used %d\n",
maxSize/bAigNodeSize, count, (maxSize-curSize)/bAigNodeSize);
fflush(vis_stdout);
*/
return;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void bAig_BuildAigBFSManner | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| st_table * | leaves, | ||
| int | sweep | ||
| ) |
AutomaticEnd
AutomaticEnd
Function********************************************************************
Synopsis [Build aig nodes in breath first manner]
Description [Build aig nodes in breath first manner]
SideEffects []
SeeAlso []
Definition at line 397 of file baigBddSweep.c.
{
array_t *nodeArray, *result;
lsGen gen1;
int iter, maxLevel, level;
int i, j, k;
bAigEdge_t v;
Ntk_Node_t *node, *fanin, *fanout;
st_table *node2mvfAigTable;
array_t *curArray, *nextArray, *tmpArray;
array_t *levelArray, *clevelArray;
MvfAig_Function_t *mvfAig;
int mvfSize;
st_generator *gen;
Ntk_NetworkForEachNode(network, gen1, node) {
Ntk_NodeSetUndef(node, (void *)0);
}
curArray = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(leaves, gen, &node, &fanout) {
array_insert_last(Ntk_Node_t *, curArray, node);
Ntk_NodeSetUndef(node, (void *)1);
}
levelArray = array_alloc(array_t *, 10);
nextArray = array_alloc(Ntk_Node_t *, 0);
iter = 0;
while(1) {
clevelArray = array_alloc(array_t *, 10);
array_insert_last(array_t *, levelArray, clevelArray);
for(i=0; i<array_n(curArray); i++) {
node = array_fetch(Ntk_Node_t *, curArray, i);
Ntk_NodeForEachFanout(node, j, fanout) {
level = (int)(long)Ntk_NodeReadUndef(fanout);
if(level > 0) continue;
maxLevel = 0;
Ntk_NodeForEachFanin(fanout, k, fanin) {
level = (int)(long)Ntk_NodeReadUndef(fanin);
if(level == 0) {
maxLevel = 0;
break;
}
else if(level > maxLevel) {
maxLevel = level;
}
}
if(maxLevel > 0) {
Ntk_NodeSetUndef(fanout, (void *)(long)(maxLevel+1));
array_insert_last(Ntk_Node_t *, nextArray, fanout);
array_insert_last(Ntk_Node_t *, clevelArray, fanout);
}
}
}
curArray->num = 0;
tmpArray = curArray;
curArray = nextArray;
nextArray = tmpArray;
if(curArray->num == 0) break;
iter++;
}
Ntk_NetworkForEachNode(network, gen1, node) {
Ntk_NodeSetUndef(node, (void *)0);
}
for(i=0; i<array_n(levelArray); i++) {
clevelArray = array_fetch(array_t *, levelArray, i);
result = ntmaig_NetworkBuildMvfAigs(network, clevelArray, leaves);
MvfAig_FunctionArrayFree(result);
node2mvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(
network, MVFAIG_NETWORK_APPL_KEY);
if(i < 50 && sweep) {
nodeArray = array_alloc(bAigEdge_t, 0);
for(j=0; j<array_n(clevelArray); j++) {
node = array_fetch(Ntk_Node_t *, clevelArray, j);
st_lookup(node2mvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(k=0; k<mvfSize; k++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
array_insert_last(bAigEdge_t, nodeArray, v);
}
}
bAig_BddSweepForceMain(network, nodeArray);
for(j=0; j<array_n(clevelArray); j++) {
node = array_fetch(Ntk_Node_t *, clevelArray, j);
st_lookup(node2mvfAigTable, node, &mvfAig);
mvfSize = array_n(mvfAig);
for(k=0; k<mvfSize; k++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, k));
array_insert(bAigEdge_t, nodeArray, v, k);
}
}
array_free(nodeArray);
}
array_free(clevelArray);
}
array_free(levelArray);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int CommandBuildPartitionMAigs | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Implements the build_partition_maigs command.]
Description []
CommandName [build_partition_maigs]
CommandSynopsis [build a partition of MAIGs for the flattened network]
CommandArguments [\[-h\] \[-d\] \[-n\] ]
CommandDescription [ Build the multi-valued AND/INVERTER graph (MAIG) of a flattened network. It builds the MAIG for the combinational outputs (COs) in terms of the combinational inputs (CIs). The pointer to this graph is stored in the network to be used by other commands, such as bounded_model_check.
This command must be preceded by the commands flatten_hierarchy. This command will remove any previous build to this graph.
Command options:
- -n
Disable BDD sweeping.
- -d
Build aig structure in depth first manner.
]
SideEffects []
SeeAlso []
fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node));
Definition at line 148 of file ntmaigCmd.c.
{
Ntk_Node_t *node, *latch;
lsGen gen;
array_t *result; /* array of MvfAig_Function_t* */
array_t *roots;
st_table *leaves;
array_t *inputs;
Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
mAig_Manager_t *manager;
MvfAig_Function_t *mvfAig;
st_table *nodeToMvfAigTable; /* mapes each node with its mvfAig */
int c, sweepFlag, DFSFlag;
int i;
sweepFlag = 1;
DFSFlag = 0;
util_getopt_reset();
while ((c = util_getopt(argc,argv,"sdnh")) != EOF){
switch(c){
case 's':
sweepFlag = 1;
break;
case 'd':
DFSFlag = 1;
break;
case 'n':
sweepFlag = 0;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if (network == NIL(Ntk_Network_t)) {
return 1;
}
manager = Ntk_NetworkReadMAigManager(network);
if (manager == NIL(mAig_Manager_t)) {
manager = mAig_initAig();
Ntk_NetworkSetMAigManager(network, manager);
/*
mAig_mAigSetNetwork(manager, network);
*/
}
/* Check if there is already a MvfAigs Table attached to the network */
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
if (nodeToMvfAigTable != NIL(st_table)){
/*
st_foreach_item(nodeToMvfAigTable, stGen, (char **) &node, (char **) &MvfAig) {
printf("\nNode name = %s :",Ntk_NodeReadName(node));
for (j=0; j< array_n(MvfAig); j++){
printf(" %d ",array_fetch(bAigEdge_t, (array_t *) MvfAig, j));
}
}
*/
(void) fprintf(vis_stderr, "maig partition already built; reinvoke\n");
(void) fprintf(vis_stderr, "flatten_hierarchy to remove the current maig partition\n");
return 1;
}
roots = array_alloc(Ntk_Node_t *, 0);
Ntk_NetworkForEachCombOutput(network, gen, node) {
array_insert_last(Ntk_Node_t *, roots, node);
}
Ntk_NetworkForEachNode(network, gen, node) {
if(Ntk_NodeTestIsShadow(node)) continue;
if(Ntk_NodeTestIsCombInput(node)) continue;
if(Ntk_NodeTestIsCombOutput(node))continue;
if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) {
array_insert_last(Ntk_Node_t *, roots, node);
}
}
leaves = st_init_table(st_ptrcmp, st_ptrhash);
inputs = array_alloc(Ntk_Node_t *, 16);
Ntk_NetworkForEachCombInput(network, gen, node) {
array_insert_last(Ntk_Node_t *, inputs, node);
}
array_sort(inputs, nodenameCompare);
for(i=0; i<array_n(inputs); i++) {
node = array_fetch(Ntk_Node_t *, inputs, i);
st_insert(leaves, node, (char *) ntmaig_UNUSED);
Ntk_NodeSetMAigId(node,
mAig_CreateVar(manager,
Ntk_NodeReadName(node),
Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
}
if(DFSFlag == 0)
bAig_BuildAigBFSManner(network, manager, leaves, sweepFlag);
result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves);
nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
Ntk_NetworkForEachLatch(network, gen, latch) {
node = Ntk_LatchReadDataInput(latch);
st_lookup(nodeToMvfAigTable, node, &mvfAig);
Ntk_NodeSetMAigId(node,
mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
node = Ntk_LatchReadInitialInput(latch);
st_lookup(nodeToMvfAigTable, node, &mvfAig);
Ntk_NodeSetMAigId(node,
mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
}
roots->num = 0;
Ntk_NetworkForEachLatch(network, gen, latch) {
if(!st_lookup(nodeToMvfAigTable, latch, &mvfAig))
array_insert_last(Ntk_Node_t *, roots, latch);
}
result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves);
array_free(roots);
array_free(inputs);
st_free_table(leaves);
/*
* Free the array of MvfAigs.
*/
MvfAig_FunctionArrayFree(result);
if(sweepFlag)
bAig_BddSweepMain(network, 0);
return 0;
usage:
(void) fprintf(vis_stderr, "usage: build_partition_maig [-h]\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -n disable bdd sweeping\n");
(void) fprintf(vis_stderr, " -d build AIG DFS manner\n");
return 1; /* error exit */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int nodenameCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
Function********************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
Definition at line 90 of file ntmaigCmd.c.
{
Ntk_Node_t *v1, *v2;
char *name1, *name2;
v1 = *(Ntk_Node_t **)(node1);
v2 = *(Ntk_Node_t **)(node2);
name1 = Ntk_NodeReadName(v1);
name2 = Ntk_NodeReadName(v2);
return (strcmp(name1, name2));
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void ntmaig_End | ( | void | ) |
Function********************************************************************
Synopsis [Ends the network to MAIG package.]
SideEffects []
SeeAlso [ntmaig_Init]
Definition at line 64 of file ntmaigCmd.c.
{
}
Here is the caller graph for this function:
| void ntmaig_Init | ( | void | ) |
Function********************************************************************
Synopsis [Initializes the network to MAIG package.]
SideEffects []
SeeAlso [ntmaig_End]
Definition at line 49 of file ntmaigCmd.c.
{
Cmd_CommandAdd("build_partition_maigs", CommandBuildPartitionMAigs, /* doesn't changes_network */ 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
char rcsid [] UNUSED = "$Id: ntmaigCmd.c,v 1.26 2009/01/18 01:54:51 fabio Exp $" [static] |
CFile***********************************************************************
FileName [ntmaigCmd.c]
PackageName [ntmaig]
Synopsis [Command interface for the Aig partition package]
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.]
Definition at line 19 of file ntmaigCmd.c.
