src/puresat/puresatIPRefine.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatIPRefine.c:
Go to the source code of this file.
Functions | |
| void | PureSat_GetSufAbsFromCoreRecur (mAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable) |
| void | PureSat_GetSufAbsFromCoreRecur_2side (mAig_Manager_t *manager, satManager_t *cm, RTnode_t RTnode, st_table *ctTable, st_table *refineTable, st_table *SufNameTable) |
| array_t * | PureSat_GetSufAbsFromCore (Ntk_Network_t *network, satManager_t *cm, PureSat_Manager_t *pm, bAigEdge_t property, st_table *SufAbsNameTable) |
| array_t * | PureSat_RefineOnAbs (Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, array_t *previousResultArray, int latchThreshHold, int *sccArray, array_t *sufArray) |
| array_t * | PureSat_RefineOnAbs_DA (Ntk_Network_t *network, PureSat_Manager_t *pm, bAigEdge_t property, array_t *previousResultArray, int latchThreshHold, int *sccArray, array_t *sufArray) |
Function Documentation
| array_t* PureSat_GetSufAbsFromCore | ( | Ntk_Network_t * | network, |
| satManager_t * | cm, | ||
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | property, | ||
| st_table * | SufAbsNameTable | ||
| ) |
Function********************************************************************
Synopsis [Generate sufficient set from unsat proof]
Description []
SideEffects []
SeeAlso []
Definition at line 451 of file puresatIPRefine.c.
{
array_t * refArray = array_alloc(char *,0);
char *name;
st_generator *stgen;
Ntk_Node_t *latch;
bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table * ctTable = st_init_table(st_numcmp,st_numhash);
st_table * refineTable = st_init_table(strcmp,st_strhash);
int times;
#if UNSATCORE
FILE * fp = fopen("unsatcore.txt","w");
#endif
#if LAI
st_table * refineTable1 = st_init_table(strcmp,st_strhash);
#endif
PureSat_CleanMask(manager,ResetVisited1234NewMask);
#if UNSATCORE
fprintf(fp,"p cnf %d line, # nodes:%d\n",
cm->initNumVariables,cm->nodesArraySize);
cm->line = 0;
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
ctTable,refineTable,SufAbsNameTable,fp);
fprintf(fp,"total lines: %d\n",cm->line);
#else
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
ctTable,refineTable,SufAbsNameTable);
#endif
PureSat_CleanMask(manager,ResetVisited1234NewMask);
#if LAI
ResetRTree(cm->rm);
PureSat_GetLIAForNode(manager,property);
PureSat_GetSufAbsByLIA(manager,cm,cm->rm->root,
refineTable1);
#endif
st_foreach_item(refineTable,stgen,&name,×){
latch = Ntk_NetworkFindNodeByName(network,name);
if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
st_lookup(pm->SufAbsTable, (char*)latch,NIL(char*))){
array_insert_last(char *,refArray,name);
if(pm->verbosity>=2)
fprintf(vis_stdout,"ref cand:%s %d\n",name,times);
}
}
#if LAI
st_foreach_item(refineTable1,stgen,(char**)&name,NIL(char*)){
latch = Ntk_NetworkFindNodeByName(network,name);
if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
st_lookup(pm->CoiTable, (char*)latch,NIL(char*))){
if(pm->verbosity>=2)
fprintf(vis_stdout,"from LIA ref candidate:%s\n",name);
}
}
#endif
#if UNSATCORE
fclose(fp);
#endif
st_free_table(ctTable);
st_free_table(refineTable);
#if LAI
st_free_table(refineTable1);
#endif
return refArray;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_GetSufAbsFromCoreRecur | ( | mAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| RTnode_t | RTnode, | ||
| st_table * | ctTable, | ||
| st_table * | refineTable | ||
| ) |
CFile***********************************************************************
FileName [puresatIPRefine.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 AutomaticEnd Function********************************************************************
Synopsis [Generate sufficient set from unsat proof]
Description []
SideEffects []
SeeAlso []
Definition at line 103 of file puresatIPRefine.c.
{
int i,ct;
bAigTimeFrame_t *tf = manager->timeframeWOI;
char *name;
bAigEdge_t v,*lp;
st_table *table;
st_generator *stgen;
RTManager_t * rm = cm->rm;
if(RT_flag(RTnode)&RT_VisitedMask)
return;
RT_flag(RTnode) |= RT_VisitedMask;
/*leaf*/
if(RT_pivot(RTnode)==0){
#if DBG
assert(RT_oriClsIdx(RTnode)==0);
#endif
if(RT_oriClsIdx(RTnode)!=0)
lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
else
lp = RT_formula(RTnode) + cm->rm->fArray;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(RT_oriClsIdx(RTnode)!=0)
v = SATgetNode(*lp);
else
v = *lp;
if(*lp<0)
continue;
#if UNSATCORE
v = SATnormalNode(v);
fprintf(fp,"%d_%d ",v,SATclass(v));
if(SATflags(v)&DummyMask)
fprintf(fp,"DM ");
if(SATflags(v)&VisibleVarMask)
fprintf(fp,"Visible ");
else
if(SATflags(v)&StateBitMask)
fprintf(fp, "InvSV ");
#endif
v = SATnormalNode(v);
if((SATflags(v)&VisibleVarMask)){
if(SATclass(v)==0){
if(!st_lookup(tf->idx2name,(char*)v,&name)&&
!st_lookup(tf->MultiLatchTable,(char*)v,&table))
continue;
}
#if 1
/* at least 2 times to be choosen as a candidate*/
if(st_lookup(ctTable,(char*)v,&ct)){
if(ct<0)
continue;
if(ct>=1){
if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
int retVal = st_lookup(tf->idx2name,(char*)v,&name);
assert(retVal);
st_insert(refineTable,(char*)name,(char*)0);
st_insert(ctTable,(char*)v,(char*)-1);
}
else{
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"%d is in MultiLatchTable: ",v);
#endif
st_foreach_item(table,stgen,(char**)&name,
NIL(char*)){
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"%s ",name);
#endif
st_insert(refineTable,(char*)name,(char*)0);
}
#ifdef TIMEFRAME_VERIFY_
fprintf(vis_stdout,"\n");
#endif
st_insert(ctTable,(char*)v,(char*)-1);
}
}
}
else{
ct=1;
st_insert(ctTable,(char*)v,(char*)(long)ct);
}
#else
retVal = st_lookup(tf->idx2name,(char*)v,(char**)&name);
assert(retVal);
st_insert(refineTable,(char*)name,(char*)0);
#endif
}/* if(SATflags(v)&StateBitMask){*/
}
#if UNSATCORE
fprintf(fp,"0\n");
#endif
}
/*non leaf*/
else{
assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#if UNSATCORE
PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
ctTable,refineTable,fp);
PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
ctTable,refineTable,fp);
#else
PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
ctTable,refineTable);
PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
ctTable,refineTable);
#endif
}
return;
}
| void PureSat_GetSufAbsFromCoreRecur_2side | ( | mAig_Manager_t * | manager, |
| satManager_t * | cm, | ||
| RTnode_t | RTnode, | ||
| st_table * | ctTable, | ||
| st_table * | refineTable, | ||
| st_table * | SufNameTable | ||
| ) |
Function********************************************************************
Synopsis [Generate sufficient set from unsat proof by bridge abstraction]
Description []
SideEffects []
SeeAlso []
Definition at line 248 of file puresatIPRefine.c.
{
int i,j,find,find1,times;
bAigTimeFrame_t *tf = manager->timeframeWOI;
char *name,*name1;
bAigEdge_t v,v1,*lp,*lp1, *lp2, left,right;
st_table *table;
st_generator *stgen;
RTManager_t * rm = cm->rm;
long maxNode;
if(RT_flag(RTnode)&RT_VisitedMask)
return;
RT_flag(RTnode) |= RT_VisitedMask;
if(RT_pivot(RTnode)==0){
#if DBG
assert(RT_oriClsIdx(RTnode)==0);
#endif
if(RT_oriClsIdx(RTnode)!=0)
lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
else
lp = RT_formula(RTnode) + cm->rm->fArray;
lp1 = lp;
(cm->line)++;
for(i=0;i<RT_fSize(RTnode);i++,lp++){
if(RT_oriClsIdx(RTnode)!=0)
v = SATgetNode(*lp);
else
v = *lp;
if(*lp<0)
continue;
#if UNSATCORE
v = SATnormalNode(v);
fprintf(fp,"%d_%d ",v,SATclass(v));
if(SATflags(v)&DummyMask)
fprintf(fp,"DM ");
if(SATflags(v)&VisibleVarMask)
fprintf(fp,"Visible ");
else
if(SATflags(v)&StateBitMask)
fprintf(fp, "InvSV ");
#endif
v = SATnormalNode(v);
#if LAI
/*mark every node in core for latch interface abs*/
flags(v) |= VisitedMask;
#endif
if(SATflags(v)&VisibleVarMask){
if((SATclass(v)==0)&&
(st_lookup(tf->idx2name,(char*)v,&name)==0)&&
(st_lookup(tf->MultiLatchTable,(char*)v,&table)==0))
continue;
lp2 = lp1;
left = SATnormalNode(leftChild(v));
right = SATnormalNode(rightChild(v));
//find largest node
maxNode = -1;
for(j=0;j<RT_fSize(RTnode);j++,lp2++){
if(RT_oriClsIdx(RTnode)!=0)
v1 = SATgetNode(*lp2);
else
v1 = *lp2;
if(maxNode < SATnormalNode(v1))
maxNode = SATnormalNode(v1);
}
if(maxNode == v){
#if DBG
lp2 = lp1;
for(j=0;j<RT_fSize(RTnode);j++,lp2++){
if(RT_oriClsIdx(RTnode)!=0)
v1 = SATgetNode(*lp2);
else
v1 = *lp2;
if(*lp2<0||SATnormalNode(v1)==v)
continue;
assert((SATnormalNode(v1) == SATnormalNode(leftChild(v)))||
SATnormalNode(v1) == SATnormalNode(rightChild(v)));
}
#endif
SATflags(v) |= Visited2Mask; /*left side*/
}
else{
#if DBG
lp2 = lp1;
for(j=0;j<RT_fSize(RTnode);j++,lp2++){
if(RT_oriClsIdx(RTnode)!=0)
v1 = SATgetNode(*lp2);
else
v1 = *lp2;
if(*lp2<0||SATnormalNode(v1)==maxNode)
continue;
assert((SATnormalNode(v1) == SATnormalNode(leftChild(maxNode)))||
(SATnormalNode(v1) == SATnormalNode(rightChild(maxNode))));
}
#endif
SATflags(v) |= Visited3Mask; /*right side*/
#if THROUGHPICK
/*pick latch due to split*/
if(SATflags(v)&VPGVMask){
if(SATclass(maxNode)<=1)
SATflags(v) |= NewMask; /*the same tf*/
else
SATflags(v) |= Visited4Mask; /* larger tf*/
}
#endif
}
}
#if THROUGHPICK
if((SATflags(v)&VisibleVarMask)&&
(((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))||
((SATflags(v)&Visited4Mask)&&(SATflags(v)&NewMask)))){
#else
if((SATflags(v)&VisibleVarMask)&&
((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))){
#endif
times = 1;
if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
int retVal = st_lookup(tf->idx2name,(char*)v,&name);
assert(retVal);
if(st_lookup(refineTable,(char*)name,×))
times++;
st_insert(refineTable,(char*)name,(char*)(long)times);
}
/*for iden latches, we only add one, which is enough*/
else{
find = 0;
find1 = 0;
st_foreach_item(table,stgen,(char**)&name,
NIL(char*)){
if(st_lookup(refineTable,name,NIL(char*))){
find = 1;
break;
}
if(find1==0){
if(st_lookup(SufNameTable,name, NIL(char*))){
name1 = name;
find1 = 1;
}
}
}
if(find==0){
times = 1;
if(st_lookup(refineTable,(char*)name1,×))
times++;
st_insert(refineTable,(char*)name1,(char*)(long)times);
}
}
}
}
#if UNSATCORE
fprintf(fp,"0\n");
#endif
}
/*non leaf*/
else{
assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#if UNSATCORE
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
ctTable,refineTable,SufNameTable,fp);
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
ctTable,refineTable,SufNameTable,fp);
#else
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
ctTable,refineTable,SufNameTable);
PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
ctTable,refineTable,SufNameTable);
#endif
}
return;
}
Here is the caller graph for this function:
| array_t* PureSat_RefineOnAbs | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | property, | ||
| array_t * | previousResultArray, | ||
| int | latchThreshHold, | ||
| int * | sccArray, | ||
| array_t * | sufArray | ||
| ) |
Function********************************************************************
Synopsis [Main procedure of refinement computation]
Description []
SideEffects []
SeeAlso []
Definition at line 546 of file puresatIPRefine.c.
{
array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3;
array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
satManager_t *cm;
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table *table;
char * name;
int i,j;
int NumInSecondLevel;
st_generator *stgen;
Ntk_Node_t *latch;
double t1,t2,t3,t4;
st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
st_table * junkTable;
int noArosat = 1;
tmpRef = array_alloc(char *,0);
st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
name = Ntk_NodeReadName(latch);
if(st_lookup(pm->vertexTable,name,NIL(char *)))
array_insert_last(char *,tmpModel,name);
array_insert_last(char *,tmpRef,name);
st_insert(SufAbsNameTable,name,(char *)0);
}
t1 = util_cpu_ctime();
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
if(pm->Arosat){
cm->option->decisionHeuristic &= RESET_LC;
cm->option->decisionHeuristic |= DVH_DECISION;
cm->option->arosat = 1;
}
cm->option->coreGeneration = 1;
cm->option->AbRf = 1;
cm->property = property;
cm->option->IP = 1;
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
array_free(tmpRef);
t3 = util_cpu_ctime();
PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
t4 = util_cpu_ctime();
pm->tPro += t4-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t4-t3)/1000.0),pm->tPro/1000);
if(cm->option->arosat){
PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
cm->Length = pm->Length;
AS_Main(cm);
noArosat = 0;
st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
st_free_table(table);
st_free_table(cm->layerTable);
FREE(cm->assignedArray);
FREE(cm->numArray);
}
else
sat_Main(cm);
manager->NodesArray = cm->nodesArray;;
assert(cm->status==SAT_UNSAT);
t3 = util_cpu_ctime();
PureSatPostprocess(manager,cm,pm);
PureSatProcessDummy(manager,cm,cm->rm->root);
ResetRTree(cm->rm);
t4 = util_cpu_ctime();
pm->tPro += t4-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t4-t3)/1000.0),pm->tPro/1000);
t2 = util_cpu_ctime();
pm->tCoreGen += t2 - t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
(double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);
t1 = util_cpu_ctime();
tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
t2 = util_cpu_ctime();
st_free_table(SufAbsNameTable);
RT_Free(cm->rm);
sat_ArrayFree(manager->assertArray);
PureSat_SatFreeManager(cm);
/*Get suff set*/
tmpRef2 = array_alloc(char *,0);
tmpRef3 = array_alloc(char *,0);
tmpArray1 = array_alloc(char *,0);
tmpArray2 = array_alloc(char *,0);
if(noArosat){
t1 = util_cpu_ctime();
if(array_n(tmpRef1)){
tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
&NumInSecondLevel);
array_free(pm->latchArray);
}
}
else{
if(array_n(tmpRef1)){
tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
&NumInSecondLevel);
array_free(pm->latchArray);
}
else
tmpRef = array_alloc(char*,0);
#if NOREFMIN
if(pm->verbosity>=1){
fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
arrayForEachItem(char *,tmpRef,i,name)
fprintf(vis_stdout,"%s\n",name);
}
PureSatAddIdenLatchToAbs(network,pm,tmpRef);
array_free(tmpRef1);
array_free(tmpModel);
return tmpRef;
#endif
}
/*Ref Minimization
//try all the candidates*/
t1 = util_cpu_ctime();
if(pm->CoreRefMin && array_n(tmpRef)>=5){
if(pm->verbosity>=1)
fprintf(vis_stdout,"Core Ref Min\n");
junkTable = st_init_table(strcmp,st_strhash);
for(i=array_n(tmpRef)-1;i>=0;i--)
{
array_t * tmpA;
name = array_fetch(char *,tmpRef,i);
if(pm->verbosity>=1)
fprintf(vis_stdout,"RefMin: testing %s\n",name);
tmpArray2 = PureSatRemove_char(tmpRef,i);
if(st_lookup(junkTable,name,NIL(char))){
array_free(tmpRef);
tmpRef = tmpArray2;
if(pm->verbosity>=1)
fprintf(vis_stdout,"%s is junk\n",name);
continue;
}
tmpA = array_dup(tmpModel);
array_append(tmpA,tmpArray2);
t3 = util_cpu_time();
tmpArray1 = array_alloc(char*,0);
arrayForEachItem(char*,tmpA,j,name)
if(!st_lookup(junkTable,name,NIL(char)))
array_insert_last(char*,tmpArray1,name);
array_free(tmpA);
if(!PureSat_ConcretTest_Core(network,pm,tmpArray1,property,
previousResultArray,junkTable)){
/*then the candidate can' be deleted*/
t4 = util_cpu_time();
if(pm->verbosity>=2)
fprintf(vis_stdout," %g\n",(t4-t3)/1000);
array_free(tmpArray2);
}
else /*delete it*/
{
t4 = util_cpu_time();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
array_free(tmpRef);
tmpRef = tmpArray2;
}
array_free(tmpArray1);
}
st_free_table(junkTable);
}
else{
for(i=array_n(tmpRef)-1;i>=0;i--)
{
name = array_fetch(char *,tmpRef,i);
if(pm->verbosity>=1)
fprintf(vis_stdout,"RefMin: testing %s\n",name);
tmpArray2 = PureSatRemove_char(tmpRef,i);
tmpArray1 = array_dup(tmpModel);
array_append(tmpArray1,tmpArray2);
t3 = util_cpu_time();
if(!PureSat_ConcretTest(network,pm,tmpArray1,property,
previousResultArray,0,0,0)){
t4 = util_cpu_time();
if(pm->verbosity>=2)
fprintf(vis_stdout," %g\n",(t4-t3)/1000);
array_free(tmpArray2);
}
else /*delete it*/
{
t4 = util_cpu_time();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
array_free(tmpRef);
tmpRef = tmpArray2;
}
array_free(tmpArray1);
}
}
t2 = util_cpu_ctime();
pm->tRefMin += t2 - t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"\ntime for Ref Min: %g, total:%g\n",
(t2-t1)/1000,pm->tRefMin/1000);
if(pm->verbosity>=1){
fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
arrayForEachItem(char *,tmpRef,i,name)
fprintf(vis_stdout,"%s\n",name);
}
PureSatAddIdenLatchToAbs(network,pm,tmpRef);
array_free(tmpRef1);
array_free(tmpModel);
return tmpRef;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| array_t* PureSat_RefineOnAbs_DA | ( | Ntk_Network_t * | network, |
| PureSat_Manager_t * | pm, | ||
| bAigEdge_t | property, | ||
| array_t * | previousResultArray, | ||
| int | latchThreshHold, | ||
| int * | sccArray, | ||
| array_t * | sufArray | ||
| ) |
Function********************************************************************
Synopsis [Refinement procedure without refinement minimization]
Description []
SideEffects []
SeeAlso []
Definition at line 795 of file puresatIPRefine.c.
{
array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3; //= array_alloc(char *,0);
array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
satManager_t *cm;
mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
st_table *table;
char * name;
int i;
int NumInSecondLevel;
st_generator *stgen;
Ntk_Node_t *latch;
double t1,t2,t3,t4;
st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
int noArosat = 1;
tmpRef = array_alloc(char *,0);
st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
name = Ntk_NodeReadName(latch);
if(st_lookup(pm->vertexTable,name,NIL(char *)))
array_insert_last(char *,tmpModel,name);
array_insert_last(char *,tmpRef,name);
st_insert(SufAbsNameTable,name,(char *)0);
}
t1 = util_cpu_ctime();
manager->assertArray = sat_ArrayAlloc(1);
sat_ArrayInsert(manager->assertArray,manager->InitState);
cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
#if AROSAT
cm->option->decisionHeuristic &= RESET_LC;
cm->option->decisionHeuristic |= DVH_DECISION;
cm->option->arosat = 1;
#endif
cm->option->coreGeneration = 1;
cm->option->AbRf = 1;
cm->option->IP = 1;
cm->property = property;
PureSat_CleanMask(manager,ResetVisibleVarMask);
PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
array_free(tmpRef);
t3 = util_cpu_ctime();
PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
t4 = util_cpu_ctime();
pm->tPro += t4-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t4-t3)/1000.0),pm->tPro/1000);
#if DBG
PureSatCheckCoi(manager);
#endif
if(cm->option->arosat){
PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
cm->Length = pm->Length;
AS_Main(cm);
noArosat = 0;
st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
st_free_table(table);
st_free_table(cm->layerTable);
FREE(cm->assignedArray);
FREE(cm->numArray);
}
else
sat_Main(cm);
manager->NodesArray = cm->nodesArray;;
assert(cm->status==SAT_UNSAT);
t3 = util_cpu_ctime();
PureSatPostprocess(manager,cm,pm);
PureSatProcessDummy(manager,cm,cm->rm->root);
ResetRTree(cm->rm);
t4 = util_cpu_ctime();
pm->tPro += t4-t3;
if(pm->verbosity>=2)
fprintf(vis_stdout,"process time:%g,total:%g\n",
(double)((t4-t3)/1000.0),pm->tPro/1000);
t2 = util_cpu_ctime();
pm->tCoreGen += t2 - t1;
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
(double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);
#if DBG
PureSat_CheckFanoutFanin(manager);
#endif
t1 = util_cpu_ctime();
tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
t2 = util_cpu_ctime();
st_free_table(SufAbsNameTable);
RT_Free(cm->rm);
sat_ArrayFree(manager->assertArray);
PureSat_SatFreeManager(cm);
/*Get suff set*/
tmpRef2 = array_alloc(char *,0);
tmpRef3 = array_alloc(char *,0);
tmpArray1 = array_alloc(char *,0);
tmpArray2 = array_alloc(char *,0);
if(noArosat){
t1 = util_cpu_ctime();
if(array_n(tmpRef1)){
tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
&NumInSecondLevel);
array_free(pm->latchArray);
}
}
/*if arosat*/
else{
if(array_n(tmpRef1)){
tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
&NumInSecondLevel);
array_free(pm->latchArray);
}
else
tmpRef = array_alloc(char*,0);
if(pm->verbosity>=1){
fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
arrayForEachItem(char *,tmpRef,i,name)
fprintf(vis_stdout,"%s\n",name);
}
PureSatAddIdenLatchToAbs(network,pm,tmpRef);
array_free(tmpRef1);
array_free(tmpModel);
return tmpRef;
}
}
Here is the call graph for this function:
Here is the caller graph for this function:
