src/puresat/puresatTFrame.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatTFrame.c:
Go to the source code of this file.
Functions | |
| static int | nameCompare (const void *node1, const void *node2) |
| static int | NoOfBitEncode (int n) |
| bAigEdge_t | PureSat_CaseNew (mAig_Manager_t *manager, bAigEdge_t *arr, array_t *encodeList, int index) |
| void | PureSat_CreateNewNode (mAig_Manager_t *manager, st_table *node2MvfAigTable, Ntk_Node_t *node, bAigEdge_t *bli, bAigEdge_t *li, int *bindex, int *index, int withInitialState) |
| bAigEdge_t | PureSat_ExpandForEachCone (mAig_Manager_t *manager, bAigEdge_t v, st_table *old2new) |
| bAigTimeFrame_t * | bAig_PureSat_InitTimeFrame (Ntk_Network_t *network, mAig_Manager_t *manager, PureSat_Manager_t *pm, int withInitialState) |
| void | bAig_PureSat_ExpandTimeFrame (Ntk_Network_t *network, mAig_Manager_t *manager, PureSat_Manager_t *pm, int bound, int withInitialState) |
Function Documentation
| void bAig_PureSat_ExpandTimeFrame | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| PureSat_Manager_t * | pm, | ||
| int | bound, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [build more aig timeframes]
Description []
SideEffects []
SeeAlso []
create new primary input node
map previous time frame into current
create new time frame
Definition at line 886 of file puresatTFrame.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;
Ntk_Node_t *node, *latch;
st_table *node2MvfAigTable, *old2new;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
array_t *bVarList, *mVarList;
lsGen gen;
st_table *idx2name, *table, *MultiLatchTable;
char *name, *name1;
if(withInitialState) timeframe = manager->timeframe;
else timeframe = manager->timeframeWOI;
if(timeframe == 0)
timeframe = bAig_PureSat_InitTimeFrame(network, manager, pm,withInitialState);
idx2name = timeframe->idx2name;
MultiLatchTable = timeframe->MultiLatchTable;
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++) {
manager->class_ = j+1;
if(j>=manager->NumOfTable){
manager->NumOfTable *= 2;
manager->SymbolTableArray = REALLOC(st_table *,
manager->SymbolTableArray,manager->NumOfTable);
manager->HashTableArray = REALLOC(bAigEdge_t *,
manager->HashTableArray,manager->NumOfTable);
}
manager->SymbolTableArray[manager->class_] = st_init_table(strcmp,st_strhash);
manager->HashTableArray[manager->class_] = ALLOC(bAigEdge_t, bAig_HashTableSize);
for (i=0; i<bAig_HashTableSize; i++)
manager->HashTableArray[manager->class_][i]= bAig_NULL;
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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
name = Ntk_NodeReadName(latch);
node = Ntk_LatchReadDataInput(latch);
mvfAig = lmvfAig = 0;
st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
mvfSize = array_n(mvfAig);
st_lookup(node2MvfAigTable, (char *)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);
exit(0);
}
else {
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = PureSat_ExpandForEachCone(manager, v, old2new);
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;
flags(nv) |= StateBitMask;
if(nv==bAig_Zero||nv==bAig_One)
continue;
if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
}
else{
/*if they are not equal, resort to MultiLatchTable*/
if(strcmp(name,name1)){
if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
bAig_NonInvertedEdge(nv),name);
#endif
st_insert(table,(char*)name,(char*)0);
}
else{
table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
bAig_NonInvertedEdge(nv),name,name1);
#endif
st_insert(table,(char*)name1,(char*)0);
st_insert(table,(char*)name,(char*)0);
st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
}
}
}
}/* for(i=0; i< mvfSize; i++){*/
}/*else {*/
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);
v = bAig_GetCanonical(manager, lbVar.node);
nv = PureSat_ExpandForEachCone(manager, v, old2new);
flags(nv) |= StateBitMask;
st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
j+1, Ntk_NodeReadName(latch), i, v, nv);
#endif
bli[bindex++] = nv;
if(nv==bAig_Zero||nv==bAig_One)
continue;
if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
}
else{
/*if they are not equal, resort to MultiLatchTable*/
if(strcmp(name,name1)){
if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
bAig_NonInvertedEdge(nv),name);
#endif
st_insert(table,(char*)name,(char*)0);
}
else{
table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
bAig_NonInvertedEdge(nv),name,name1);
#endif
st_insert(table,(char*)name1,(char*)0);
st_insert(table,(char*)name,(char*)0);
st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
}
}
}
tindex++;
}
}
li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
timeframe->outputs[j] = li;
index = 0;
Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = PureSat_ExpandForEachCone(manager, v, old2new);
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 = PureSat_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:
| bAigTimeFrame_t* bAig_PureSat_InitTimeFrame | ( | Ntk_Network_t * | network, |
| mAig_Manager_t * | manager, | ||
| PureSat_Manager_t * | pm, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Initialize aig timeframes]
Description []
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 285 of file puresatTFrame.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, nv;
mAigMvar_t mVar;
mAigBvar_t bVar;
array_t *bVarList, *mVarList;
int mAigId;
int lmAigId;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
bAigEdge_t vi, tmpv1, tmpv2,tmpv3;
char * name, *name1;
int imvfSize;
st_table *idx2name,*MultiLatchTable,*table;
manager->class_ = 1;
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);
idx2name = st_init_table(st_ptrcmp,st_ptrhash);
timeframe->idx2name = idx2name;
MultiLatchTable = st_init_table(st_ptrcmp,st_ptrhash);
timeframe->MultiLatchTable = MultiLatchTable;
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) {
name = Ntk_NodeReadName(latch);
array_insert_last(Ntk_Node_t *, latchArr, latch);
st_lookup(node2MvfAigTable, (char *)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++);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"Latch:%s v-->idx:%d-->%d\n",name,v,nLatches-1);
#endif
}
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, (char *)node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(o2index, (char *)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, (char *)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++);
}
}
}
timeframe->nInternals = nInternals;
nInputs = 0;
nbInputs = 0;
Ntk_NetworkForEachPrimaryInput(network, gen, node) {
array_insert_last(Ntk_Node_t *, inputArr, node);
if(!st_lookup(node2MvfAigTable, (char *)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 *)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, (char *)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 *)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);
manager->SymbolTableArray[0] = st_init_table(strcmp,st_strhash);
manager->HashTableArray[0] = ALLOC(bAigEdge_t, bAig_HashTableSize);
for (i=0; i<bAig_HashTableSize; i++)
manager->HashTableArray[0][i]= bAig_NULL;
manager->SymbolTableArray[1] = st_init_table(strcmp,st_strhash);
manager->HashTableArray[1] = ALLOC(bAigEdge_t, bAig_HashTableSize);
for (i=0; i<bAig_HashTableSize; i++)
manager->HashTableArray[1][i]= bAig_NULL;
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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
manager->InitState = bAig_One;
Ntk_NetworkForEachLatch(network, gen, latch) {
manager->class_ = 0;
PureSat_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index,withInitialState);
node = Ntk_LatchReadInitialInput(latch);
st_lookup(node2MvfAigTable,(char*)node,&tmpMvfAig);
st_lookup(node2MvfAigTable, (char *) latch, &mvfAig);
mvfSize = array_n(mvfAig);
imvfSize = array_n(tmpMvfAig);
if(mvfSize!=imvfSize){
fprintf(vis_stdout,"mvfSize:%d!=imvSize:%d, exit\n",mvfSize, imvfSize);
exit(0);
}
tmpv3=0;
for(i=0; i< mvfSize; i++){
bAigEdge_t tmpvvv;
tmpvvv = manager->InitState;
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
st_insert(old2new, (char *)v, (char *)(li[index1]));
flags(li[index1]) |= StateBitMask;
#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;
if(tmpv3!=SATnormalNode(li[index1-1])){
vi = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(tmpMvfAig,i));
if(vi == bAig_One){
manager->InitState =
PureSat_And(manager,manager->InitState,li[index1-1]);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"%d AND %d = %d\n",li[index1-1],tmpvvv,manager->InitState);
#endif
}
else if(vi == bAig_Zero){
manager->InitState =
PureSat_And(manager,manager->InitState,bAig_Not(li[index1-1]));
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"%d AND %d = %d\n",bAig_Not(li[index1-1]),tmpvvv,manager->InitState);
#endif
}
else{
tmpv1 = PureSat_ExpandForEachCone(manager,vi,old2new);
tmpv2 = PureSat_Eq(manager,li[index1-1],tmpv1);
manager->InitState = PureSat_And(manager,manager->InitState,tmpv2);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"%d AND %d = %d, %d is EQ node for funct node %d<-->%d\n",
tmpvvv,tmpv2,manager->InitState,tmpv2,tmpv1,li[index1-1] );
#endif
}
}
tmpv3 = SATnormalNode(li[index1-1]);
}
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);
flags(bli[tindex])|=StateBitMask;
ori_bli[tindex++] = v;
}
}
#if DBG
assert(tindex==bindex&&index1==index);
#endif
}
st_free_table(old2new);
manager->class_ = 1;
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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
st_lookup(node2MvfAigTable, (char *) 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) {
char * name = Ntk_NodeReadName(latch);
node = Ntk_LatchReadDataInput(latch);
mvfAig = lmvfAig = 0;
st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
mvfSize = array_n(mvfAig);
st_lookup(node2MvfAigTable, (char *)latch, &lmvfAig);
lmvfSize = array_n(lmvfAig);
if(mvfSize != lmvfSize) {
fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
exit(0);
}
else {
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
nv = PureSat_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;
if(nv==bAig_Zero||nv==bAig_One)
continue;
if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
}
else{
/*if they are not equal, resort to MultiLatchTable*/
if(strcmp(name,name1)){
if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
bAig_NonInvertedEdge(nv),name);
#endif
st_insert(table,(char*)name,(char*)0);
}
else{
table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
bAig_NonInvertedEdge(nv),name,name1);
#endif
st_insert(table,(char*)name1,(char*)0);
st_insert(table,(char*)name,(char*)0);
st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
}
}
}
}
}
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);
v = bAig_GetCanonical(manager, lbVar.node);
nv = PureSat_ExpandForEachCone(manager, v, old2new);
flags(nv) |= StateBitMask;
st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
ffprintf(vis_stdout,vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
1, Ntk_NodeReadName(latch), i, v, nv);
#endif
bli[bindex++] = nv;
tindex++;
if(nv==bAig_Zero||nv==bAig_One)
continue;
if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
}
else{
/*if they are not equal, resort to MultiLatchTable*/
if(strcmp(name,name1)){
if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
bAig_NonInvertedEdge(nv),name);
#endif
st_insert(table,(char*)name,(char*)0);
}
else{
table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
bAig_NonInvertedEdge(nv),name,name1);
#endif
st_insert(table,(char*)name1,(char*)0);
st_insert(table,(char*)name,(char*)0);
st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
}
}
}
}/*for(i=0, tindex=lmVar.bVars; i<lmVar.en...*/
}/*Ntk_NetworkForEachLatch(network, gen, latch) {*/
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"after build latches of TF 1\n");
#endif
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, (char *) node, &mvfAig);
mvfSize = array_n(mvfAig);
for(i=0; i< mvfSize; i++){
v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
nv = PureSat_ExpandForEachCone(manager, v, old2new);
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 = PureSat_ExpandForEachCone(manager, v, old2new);
st_insert(old2new, (char *)v, (char *)nv);
li[i] = nv;
}
/*change the class of latch vars of tf */
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:
| static int nameCompare | ( | const void * | node1, |
| const void * | node2 | ||
| ) | [static] |
CFile***********************************************************************
FileName [puresatTFrame.c]
PackageName [puresat]
Synopsis [Abstraction refinement for large scale invariant checking.]
Description [This file contains the functions to check invariant properties by the PureSAT abstraction refinement algorithm, which is entirely based on SAT solver, the input of which could be either CNF or AIG. It has several parts:
Localization-reduction base Abstraction K-induction or interpolation to prove the truth of a property Bounded Model Checking to find bugs Incremental concretization based methods to verify abstract bugs Incremental SAT solver to improve efficiency UNSAT proof based method to obtain refinement AROSAT to bring in only necessary latches into unsat proofs Bridge abstraction to get compact coarse refinement Refinement minization to guarrantee minimal refinements Unsat proof-based refinement minimization to eliminate multiple candidate by on SAT test Refinement prediction to decrease the number of refinement iterations Dynamic switching to redistribute computional resources to improve efficiency
For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05 paper of Li et al., "A satisfiability-based appraoch to abstraction refinement in model checking", " Abstraction in symbolic model checking using satisfiability as the only decision procedure", "Efficient computation of small abstraction refinements", and "Efficient abstraction refinement in interpolation-based unbounded model checking"]
Author [Bing Li]
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.]AutomaticStart
Function********************************************************************
Synopsis [Name comparison function.]
Description [Name comparison function.]
SideEffects [none]
SeeAlso []
Definition at line 1206 of file puresatTFrame.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 number of encoding bits.]
Description [Compute number of encoding bits.]
SideEffects [none]
SeeAlso []
Definition at line 1230 of file puresatTFrame.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:
| bAigEdge_t PureSat_CaseNew | ( | mAig_Manager_t * | manager, |
| bAigEdge_t * | arr, | ||
| array_t * | encodeList, | ||
| int | index | ||
| ) |
AutomaticEnd Function********************************************************************
Synopsis [build conncetion between binary variables and multi-valued variables]
Description []
SideEffects []
SeeAlso []
Definition at line 101 of file puresatTFrame.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 = PureSat_And(manager, v, node2);
andResult2 = PureSat_And(manager, bAig_Not(v), node1);
orResult = PureSat_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 = PureSat_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:
| void PureSat_CreateNewNode | ( | mAig_Manager_t * | manager, |
| st_table * | node2MvfAigTable, | ||
| Ntk_Node_t * | node, | ||
| bAigEdge_t * | bli, | ||
| bAigEdge_t * | li, | ||
| int * | bindex, | ||
| int * | index, | ||
| int | withInitialState | ||
| ) |
Function********************************************************************
Synopsis [Create new aig node in expanding timeframes with initial states]
Description []
SideEffects []
SeeAlso []
Definition at line 158 of file puresatTFrame.c.
{
int i, j, value, noBits;
bAigEdge_t *arr, v, tv;
MvfAig_Function_t *mvfAig;
array_t *encodeList;
bAigEdge_t *ManagerNodesArray;
bAigTimeFrame_t *timeframe;
if(withInitialState)
timeframe = manager->timeframe;
else
timeframe = manager->timeframeWOI;
value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
noBits = NoOfBitEncode(value);
arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
mvfAig = 0;
st_lookup(node2MvfAigTable, (char *) 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 = PureSat_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 PureSat_ExpandForEachCone | ( | mAig_Manager_t * | manager, |
| bAigEdge_t | v, | ||
| st_table * | old2new | ||
| ) |
Function********************************************************************
Synopsis [Build timeframed coi for each variable]
Description []
SideEffects []
SeeAlso []
Definition at line 237 of file puresatTFrame.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 = PureSat_ExpandForEachCone(manager, leftChild(v), old2new);
right = PureSat_ExpandForEachCone(manager, rightChild(v), old2new);
nv = PureSat_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:
