#include "grabInt.h"
Include dependency graph for grabGrab.c:
Go to the source code of this file.
Functions | |
| static array_t * | GrabFsmComputeExRings (Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, int cexType, int verbose) |
| static int | GrabCompareScores (const void *ptr1, const void *ptr2) |
| static void | GrabMddAppendSupports (mdd_manager *mddManager, mdd_t *mdd1, st_table *supportsTable) |
| static array_t * | ComputeDependence (Ntk_Network_t *network, st_table *vertexTable, array_t *leftVars) |
| void | GrabRefineAbstractionByGrab (Fsm_Fsm_t *absFsm, array_t *SORs, st_table *absVarTable, st_table *BnvTable, array_t *addedVars, array_t *addedBnvs, int refine_direction, st_table *nodeToFaninNumberTable, int verbose) |
| int | GrabNodeComputeFaninNumberTableItem (Ntk_Network_t *network, st_table *nodeToFaninNumberTable, Ntk_Node_t *node) |
Variables | |
| static st_table * | Sel0ScoreTable |
| static st_table * | SelScoreTable |
| static st_table * | Sel2ScoreTable |
| static st_table * | Sel3ScoreTable |
Function Documentation
| static array_t * ComputeDependence | ( | Ntk_Network_t * | network, |
| st_table * | vertexTable, | ||
| array_t * | leftVars | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compute the degree of dependence that the abstract model has on the invisible variables.]
Description [Compute the degree of dependence that the abstract model has on the invisible variables.]
SideEffects []
Definition at line 590 of file grabGrab.c.
{
array_t *roots, *supports;
st_table *supportTable;
st_generator *stgen;
array_t *dependenceArray = array_alloc(int, array_n(leftVars));
int i,mddId;
Ntk_Node_t *node, *node1;
int count;
/* initialize the scores to 0 */
supportTable = st_init_table(st_ptrcmp, st_ptrhash);
arrayForEachItem(int, leftVars, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
assert(node);
st_insert(supportTable, node, (char *)0);
}
/* compute the supports of the absFsm */
roots = array_alloc(Ntk_Node_t *, 0);
st_foreach_item(vertexTable, stgen, &node, 0) {
node = Ntk_LatchReadDataInput(node);
array_insert(Ntk_Node_t *, roots, 0, node);
supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE,
FALSE);
arrayForEachItem(Ntk_Node_t *, supports, i, node1) {
if (st_lookup_int(supportTable, node1, &count)) {
count++;
st_insert(supportTable, node1, (char *)(long)count);
}
}
array_free(supports);
}
array_free(roots);
/* put into an array */
arrayForEachItem(int, leftVars, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
assert(node);
st_lookup_int(supportTable, node, &count);
array_insert(int, dependenceArray, i, count);
}
st_free_table(supportTable);
return dependenceArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static int GrabCompareScores | ( | const void * | ptr1, |
| const void * | ptr2 | ||
| ) | [static] |
Function********************************************************************
Synopsis [Compare the scores of the two invisible variables.]
Description [Compare the scores of the two invisible variables. It is used inside GrabRefineAbstractionByGrab() for sorting the array of invisible variables.
Note that the hash tables like Sel0ScoreTable are declareled as static global variables -- they are visible inside this source file.]
SideEffects []
Definition at line 503 of file grabGrab.c.
{
int item1 = *((int *)ptr1);
int item2 = *((int *)ptr2);
double *first0, *first, *first2, *first3;
double *second0, *second, *second2, *second3;
double value0, value, value2, value3;
st_lookup(Sel0ScoreTable, (char *)(long)item1, &first0);
st_lookup(SelScoreTable, (char *)(long)item1, &first);
st_lookup(Sel2ScoreTable, (char *)(long)item1, &first2);
st_lookup(Sel3ScoreTable, (char *)(long)item1, &first3);
st_lookup(Sel0ScoreTable, (char *)(long)item2, &second0);
st_lookup(SelScoreTable, (char *)(long)item2, &second);
st_lookup(Sel2ScoreTable, (char *)(long)item2, &second2);
st_lookup(Sel3ScoreTable, (char *)(long)item2, &second3);
value0 = *second0 - *first0;
value = *second - *first;
value2 = *second2 - *first2;
value3 = *second3 - *first3;
if (value0 > 0) return 1;
if (value0 < 0) return -1;
if (value > 0) return 1;
if (value < 0) return -1;
return 0;
/* Chao: The tie-breakers are not used for this release. We achieved
* the best performance on the suite of testing cases at hand
* without the tie-breakers. But the code is retained for the
* purpose of future experiments.
*/
if (value2 > 0) return 1;
if (value2 < 0) return -1;
if (value3 > 0) return 1;
if (value3 < 0) return -1;
return 0;
}
Here is the caller graph for this function:
| static array_t * GrabFsmComputeExRings | ( | Fsm_Fsm_t * | absFsm, |
| st_table * | absVarTable, | ||
| st_table * | absBnvTable, | ||
| array_t * | oldRings, | ||
| int | cexType, | ||
| int | verbose | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Compute the extended Synchronous Onion Rings (SORs).]
Description [Compute the extended Synchronous Onion Rings (SORs) on the absFSm whose present state variables includes the invisible variables. The preimages, therefore, may have invisible variables in their support. The result is used only inside GrabRefineAbstractionByGrab.]
SideEffects []
Definition at line 413 of file grabGrab.c.
{
Img_ImageInfo_t *imageInfo;
Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
array_t *careStatesArray = array_alloc(mdd_t *, 0);
array_t *allPsVars, *invisibleVarMddIds;
array_t *onionRings, *synOnionRings;
mdd_t *mdd1, *mdd2, *mdd3, *mdd4, *initStates;
int i, j, mddId;
Ntk_Node_t *node;
imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0);
/* Compute the initial states based on all the related latches
* (i.e. visible latches and invisible ones that are in the
* immediate support)
*/
allPsVars = GrabGetVisibleVarMddIds(absFsm, absVarTable);
invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absVarTable,
absBnvTable);
arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
if (Ntk_NodeTestIsLatch(node))
array_insert_last(int, allPsVars, mddId);
}
initStates = GrabComputeInitialStates(network, allPsVars);
array_free(allPsVars);
array_free(invisibleVarMddIds);
onionRings = oldRings;
if (onionRings == NIL(array_t))
onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm);
assert(onionRings);
synOnionRings = array_alloc(mdd_t *, array_n(onionRings));
for (j=array_n(onionRings)-2; j>=0; j--) {
mdd1 = array_fetch(mdd_t *, onionRings, j+1);
mdd2 = array_fetch(mdd_t *, onionRings, j);
array_insert(mdd_t *, careStatesArray, 0, mdd2);
mdd3 = Img_ImageInfoComputeEXWithDomainVars(imageInfo,
mdd1,
mdd1,
careStatesArray);
mdd4 = mdd_and(mdd2, mdd3, 1, 1);
mdd_free(mdd3);
array_insert(mdd_t *, synOnionRings, j+1, mdd4);
/* when the more accurate initial states is available, use it */
if (j == 0) {
mdd1 = mdd_and(mdd4, initStates, 1, 1);
if (mdd_is_tautology(mdd1, 0)) {
mdd_free(mdd1);
mdd1 = mdd_dup(mdd4);
}
array_insert(mdd_t *, synOnionRings, j, mdd1);
}
}
/* clean-up's */
mdd_free(initStates);
array_free(careStatesArray);
return synOnionRings;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void GrabMddAppendSupports | ( | mdd_manager * | mddManager, |
| mdd_t * | mdd1, | ||
| st_table * | supportsTable | ||
| ) | [static] |
Function********************************************************************
Synopsis [Add the supporting mddIds into the table.]
Description [Add the supporting mddIds into the table.]
SideEffects []
Definition at line 562 of file grabGrab.c.
{
int mddId, k;
array_t *supports = mdd_get_support(mddManager, mdd1);
arrayForEachItem(int, supports, k, mddId) {
if (!st_is_member(supportsTable, (char *)(long)mddId))
st_insert(supportsTable, (char *)(long)mddId, (char *)0);
}
array_free(supports);
}
Here is the caller graph for this function:
| int GrabNodeComputeFaninNumberTableItem | ( | Ntk_Network_t * | network, |
| st_table * | nodeToFaninNumberTable, | ||
| Ntk_Node_t * | node | ||
| ) |
Function********************************************************************
Synopsis [Compute the number of fanin nodes]
Description [Compute the number of fanin nodes. The result is inserted in the hash table.]
SideEffects []
Definition at line 369 of file grabGrab.c.
{
int count;
array_t *roots, *supports;
roots = array_alloc(Ntk_Node_t *, 0);
if (!st_lookup_int(nodeToFaninNumberTable, node, &count)) {
if (Ntk_NodeTestIsLatch(node))
array_insert(Ntk_Node_t *, roots, 0, Ntk_LatchReadDataInput(node));
else
array_insert(Ntk_Node_t *, roots, 0, node);
supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE,FALSE);
count = array_n(supports);
array_free(supports);
st_insert(nodeToFaninNumberTable, node, (char *)(long)count);
}
array_free(roots);
return count;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void GrabRefineAbstractionByGrab | ( | Fsm_Fsm_t * | absFsm, |
| array_t * | SORs, | ||
| st_table * | absVarTable, | ||
| st_table * | BnvTable, | ||
| array_t * | addedVars, | ||
| array_t * | addedBnvs, | ||
| int | refine_direction, | ||
| st_table * | nodeToFaninNumberTable, | ||
| int | verbose | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [Pick a set of refinement variables using Grab.]
Description [Pick a set of refinement variables using Grab. When refine_direction is 1, refine in both directions (by adding latches and bnvs); when refine_direction is 0, refine only in the boolean direction (by adding bnvs).
The present state variables of absFsm must include all the invisible variables; its next state variables must include only the visible ones. On such a FSM, the preimage may contain some invisible variables in its support. The set of preimages, ExRings, is the set of augmented preimages (with invisible variables in the support).
The refinement variable will be put into either addedVars or addedBnvs, depending on which class it bolongs to; at the same time, it will be put into either absVarTable or BnvTable.
nodeToFaninNumber is a global variable, whose values are used as tie-breakers.]
SideEffects []
Definition at line 96 of file grabGrab.c.
{
Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm);
mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
array_t *ExRings;
array_t *visibleVarMddIds, *invisibleVarMddIds, *allPSVars;
array_t *tempArray;
mdd_t *mdd1, *mdd2;
char *nodeName;
Ntk_Node_t *node;
double *Scores, *SelScores, *Sel0Scores, *Sel2Scores, *Sel3Scores;
double epd, baseNum;
int i, j, nRow, nCol;
long mddId, value, value0;
boolean isSupport, isLatch;
int max_num_of_added_vars;
/* compute the preimages (with invisible vars in their support)
*/
ExRings = GrabFsmComputeExRings(absFsm, absVarTable, BnvTable, SORs,
GRAB_CEX_SOR, verbose);
assert(ExRings != NIL(array_t));
visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm,absVarTable);
invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm,absVarTable,BnvTable);
allPSVars = array_dup(visibleVarMddIds);
array_append(allPSVars, invisibleVarMddIds);
assert(array_n(invisibleVarMddIds) > 0 );
/* Compute the normalized number of "winning positions" for each individual
* invisibleVar, and store them in 'Scores'!
*/
nRow = array_n(ExRings);
nCol = array_n(invisibleVarMddIds);
Scores = ALLOC(double, nRow*nCol);
memset(Scores, 0, sizeof(double)*nRow*nCol);
/*********************************************************
* for each set of abstract states in (mdd1, Ring[j+1] )
*********************************************************/
arrayForEachItem(mdd_t *, ExRings, j, mdd1) {
st_table *localSupportsTable = st_init_table(st_numcmp, st_numhash);
GrabMddAppendSupports(mddManager, mdd1, localSupportsTable);
if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023 )
baseNum = mdd_count_onset(mddManager, mdd1, allPSVars);
else {
mdd_t *stateMdd = mdd_smooth(mddManager, mdd1, invisibleVarMddIds);
baseNum = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds);
mdd_free(stateMdd);
}
/***********************************************************
* compute the impact of refining with each invisible var
***********************************************************/
arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
/* for debugging purpose. won't affect the algorithm */
Scores[j*nCol+i] = -9E-99;
/* give credit simply for the appearance */
isSupport = st_is_member(localSupportsTable, (char *)mddId);
if (!isSupport || baseNum==0.0) continue;
Scores[j*nCol+i] += 0.001;
node = Ntk_NetworkFindNodeByMddId(network, mddId);
isLatch = (Ntk_NodeTestIsLatch(node));
if (refine_direction==0 && isLatch) continue;
{
array_t *universalQVars = array_alloc(int, 0);
/* MX */
array_insert_last(int, universalQVars, mddId);
mdd2 = mdd_consensus(mddManager, mdd1, universalQVars);
array_free(universalQVars);
if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023)
epd = mdd_count_onset(mddManager, mdd2, allPSVars);
else {
mdd_t *stateMdd = mdd_smooth(mddManager, mdd2, invisibleVarMddIds);
epd = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds);
mdd_free(stateMdd);
}
mdd_free(mdd2);
Scores[j*nCol+i] = (baseNum - epd)/baseNum;
}
if (j == 0)
Scores[j*nCol+i] /= 10.0;
}
st_free_table(localSupportsTable);
}
/* For each column, sum up the score over all the rows. The
* selection of refinement variables will be based mainly on these
* scores.
*/
SelScores = ALLOC(double, nCol);
memset(SelScores, 0, sizeof(double)*nCol);
for (i=0; i<nRow; i++) {
for (j=0; j<nCol; j++) {
SelScores[j] += Scores[i*nCol+j];
}
}
/* Other selection criteria:
* (0) when in the BOOLEAN refinement direction, only add bnvs
* (2) how many absLatches depending on the invisible var?
* (3) how much will the invisible var cost?
*/
Sel0Scores = ALLOC(double, nCol);
Sel2Scores = ALLOC(double, nCol);
Sel3Scores = ALLOC(double, nCol);
tempArray = ComputeDependence(network, absVarTable, invisibleVarMddIds);
value0 = lsLength(Ntk_NetworkReadNodes(network));
for (j=0; j<nCol; j++) {
mddId = array_fetch(int, invisibleVarMddIds, j);
node = Ntk_NetworkFindNodeByMddId(network, mddId);
isLatch = (Ntk_NodeTestIsLatch(node));
/* when refinement is in the BOOLEAN direction, only add bnvs
* otherwise, add either latches or bnvs
*/
if (refine_direction==0 && !isLatch)
Sel0Scores[j] = 1.0;
else
Sel0Scores[j] = 0.0;
/* dependence */
value = array_fetch(int, tempArray, j);
Sel2Scores[j] = ((double)value)/st_count(absVarTable);
/* cost */
value = GrabNodeComputeFaninNumberTableItem(network,
nodeToFaninNumberTable,
node);
Sel3Scores[j] = 1.0 - ((double)value)/value0;
}
array_free(tempArray);
/* Print out the 'Scores' matrix when requested
*/
if (verbose >= 5) {
/* the entire score table */
fprintf(vis_stdout, "\n Scores[%d][%d] = \n", nRow, nCol);
arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
fprintf(vis_stdout, "%s ", (Ntk_NodeTestIsLatch(node)?" L ":" "));
}
fprintf(vis_stdout, "\n");
arrayForEachItem(int, invisibleVarMddIds, i, mddId) {
node = Ntk_NetworkFindNodeByMddId(network, mddId);
fprintf(vis_stdout, "%5d ", i);
}
fprintf(vis_stdout, "\n");
for (i=0; i<nRow; i++) {
for (j=0; j<nCol; j++) {
fprintf(vis_stdout, "%+1.2f ", Scores[i*nCol+j]);
}
fprintf(vis_stdout, "\n");
}
/* best score in each row */
for (i=0; i<nRow; i++) {
int best_local = 0;
for (j=0; j<nCol; j++) {
if (Scores[i*nCol+best_local] < Scores[i*nCol+j])
best_local = j;
}
fprintf(vis_stdout, "best_local: Scores[%d][%d] = %5g\n",
i, best_local, Scores[i*nCol+best_local]);
}
}
/* Sorting the invisibleVarMddIds according to the Selection Scores
*/
Sel0ScoreTable = st_init_table(st_numcmp, st_numhash);
SelScoreTable = st_init_table(st_numcmp, st_numhash);
Sel2ScoreTable = st_init_table(st_numcmp, st_numhash);
Sel3ScoreTable = st_init_table(st_numcmp, st_numhash);
arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
st_insert(Sel0ScoreTable, (char *)mddId, (char *)(Sel0Scores+j));
st_insert(SelScoreTable, (char *)mddId, (char *)(SelScores+j));
st_insert(Sel2ScoreTable, (char *)mddId, (char *)(Sel2Scores+j));
st_insert(Sel3ScoreTable, (char *)mddId, (char *)(Sel3Scores+j));
}
array_sort(invisibleVarMddIds, GrabCompareScores);
if (verbose >= 4) {
fprintf(vis_stdout, " \t Sel0 Sel Sel2 Sel3\n");
arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
double *addr;
st_lookup(Sel0ScoreTable, (char *)mddId, &addr);
i = (int)(addr-Sel0Scores);
node = Ntk_NetworkFindNodeByMddId(network, mddId);
isLatch = (Ntk_NodeTestIsLatch(node));
fprintf(vis_stdout,
"%s[%d]\t %+1.3f %+1.3f %+1.3f %+1.3f %s\n",
(isLatch? "L":" "),
i,
Sel0Scores[i], SelScores[i], Sel2Scores[i], Sel3Scores[i],
Ntk_NodeReadName(node)
);
/* only output the top 20 variables */
if (j >= 19) break;
}
}
st_free_table(Sel0ScoreTable);
st_free_table(SelScoreTable);
st_free_table(Sel2ScoreTable);
st_free_table(Sel3ScoreTable);
/* Now find the best (largest score) invisible Var */
{
int num_absBnvs = BnvTable? st_count(BnvTable):0;
if ((st_count(absVarTable) + num_absBnvs) < 10)
max_num_of_added_vars = 1;
else
max_num_of_added_vars = 2 + (st_count(absVarTable)+num_absBnvs)/30;
}
arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
if (j >= max_num_of_added_vars) break;
node = Ntk_NetworkFindNodeByMddId(network, mddId);
nodeName = Ntk_NodeReadName(node);
if (Ntk_NodeTestIsLatch(node)) {
assert(!st_is_member(absVarTable, node));
st_insert(absVarTable, node, (char *)(long)st_count(absVarTable));
array_insert_last(int, addedVars, mddId);
CHKPRINT2( (verbose>=3), " add Latch %s\n", nodeName );
}else if (!Ntk_NodeTestIsLatch(node)) {
assert(!st_is_member(BnvTable, node));
st_insert(BnvTable, node, (char *)0);
array_insert_last(int, addedBnvs, mddId);
CHKPRINT2( (verbose>=3), " add BNV %s\n", nodeName );
}
}
/* Clean-ups */
array_free(invisibleVarMddIds);
array_free(visibleVarMddIds);
array_free(allPSVars);
mdd_array_free(ExRings);
FREE(Scores);
FREE(Sel0Scores);
FREE(SelScores);
FREE(Sel2Scores);
FREE(Sel3Scores);
}
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
st_table* Sel0ScoreTable [static] |
CFile***********************************************************************
FileName [grabGrab.c]
PackageName [grab]
Synopsis [The GRAB algorithm of computing a set of refinement variables.]
Description [The computation is based on all the shortest abstract counter-examples.]
Author [Chao Wang]
Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved.
Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]
Definition at line 43 of file grabGrab.c.
st_table* Sel2ScoreTable [static] |
Definition at line 45 of file grabGrab.c.
st_table* Sel3ScoreTable [static] |
Definition at line 46 of file grabGrab.c.
st_table* SelScoreTable [static] |
Definition at line 44 of file grabGrab.c.
