src/puresat/puresatMain.c File Reference
#include "puresatInt.h"
Include dependency graph for puresatMain.c:
Go to the source code of this file.
Functions | |
| void | PureSat_CheckInvariant (Ntk_Network_t *network, array_t *InvariantFormulaArray, int verbosity, int dbgLevel, FILE *dbgOut, boolean printInputs, boolean incremental, boolean sss, boolean flatIP, int speed) |
| boolean | PureSatCheckInv_SSS (Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, PureSat_Manager_t *pm) |
| void | PureSatCmdParse (int argc, char **argv, PureSat_Manager_t *pm) |
Function Documentation
| void PureSat_CheckInvariant | ( | Ntk_Network_t * | network, |
| array_t * | InvariantFormulaArray, | ||
| int | verbosity, | ||
| int | dbgLevel, | ||
| FILE * | dbgOut, | ||
| boolean | printInputs, | ||
| boolean | incremental, | ||
| boolean | sss, | ||
| boolean | flatIP, | ||
| int | speed | ||
| ) |
CFile***********************************************************************
FileName [puresatMain.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 [PURESAT command interface function]
Description [PURESAT command interface function]
SideEffects []
SeeAlso []
Definition at line 101 of file puresatMain.c.
{
int result,i;
Ctlp_Formula_t *invFormula;
Ctlsp_Formula_t *invFormula_sp;
PureSat_Manager_t * pm = PureSatManagerAlloc();
pm->incre = incremental;
pm->verbosity = verbosity;
pm->dbgLevel = dbgLevel;
pm->sss = sss;
pm->printInputs = printInputs;
pm->dbgOut = dbgOut;
switch(speed){
case 0:
break;
case 1:
pm->Switch = 0;
break;
case 2:
pm->Switch = 0;
pm->CoreRefMin = 0;
break;
case 3:
pm->Switch = 0;
pm->CoreRefMin = 0;
pm->RefPredict = 0;
break;
case 4:
pm->Switch = 0;
pm->CoreRefMin = 0;
pm->RefPredict = 0;
pm->Arosat = 0;
break;
default:
pm->Switch = 0;
pm->CoreRefMin = 0;
pm->RefPredict = 0;
pm->Arosat = 0;
break;
}
arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
/* if(Ctlsp_isCtlFormula(invFormula))*/
invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
if(sss)
/*SSS-base Puresat algorithm*/
result = PureSatCheckInv_SSS(network,invFormula_sp,pm);
else
if(flatIP)
/*Interpolation algorithm without abstraction refinement*/
result = PureSatCheckInv_FlatIP(network,invFormula_sp,pm);
else
/*Interpolation-based Puresat algorithm*/
result = PureSatCheckInv_IP(network,invFormula_sp,pm);
if(result){
(void) fprintf(vis_stdout, "# INV: formula passed --- ");
Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
fprintf(vis_stdout, "\n");
}
else{
if(pm->dbgLevel != 2)
{
(void) fprintf(vis_stdout, "# INV: formula failed --- ");
Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
fprintf(vis_stdout, "\n");
}
}
}
PureSatManagerFree(pm);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean PureSatCheckInv_SSS | ( | Ntk_Network_t * | network, |
| Ctlsp_Formula_t * | ltlFormula, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [Main procedure of K-induction based PURESAT algorithm]
Description [Main procedure of K-induction based PURESAT algorithm]
SideEffects []
SeeAlso []
Definition at line 203 of file puresatMain.c.
{
lsGen gen;
st_generator *stGen;
int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
int addtoAbs=0,latchThreshHold=10000,RingPosition=0;
int oldLength=0, beginPosition=0;
int NumInSecondLevel =0;
array_t * visibleArray = array_alloc(char *,0);
array_t * invisibleArray = array_alloc(char *,0);
array_t * refinement = array_alloc(char*,0);
array_t * CoiArray,* ConClsArray;
array_t * arrayRC = NULL;
array_t *tmpRefinement;
array_t *tmpRefinement1;
char * nodeName;
Ntk_Node_t * node, *latch;
boolean ExistSimplePath = TRUE,ExistACE = FALSE;
boolean realRefine=TRUE;
boolean needSorting = FALSE, firstTime = TRUE;
mAig_Manager_t *maigManager;
BmcOption_t * options;
BmcCnfStates_t *cnfstate;
bAigEdge_t property;
st_table * nodeToMvfAigTable;
double t1,t2, t0,t3;
long *space;
PureSat_IncreSATManager_t * pism1,*pism2;
satArray_t *saved;
pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
pm->vertexTable = st_init_table(strcmp, st_strhash);
pism1 = PureSatIncreSATManagerAlloc(pm);
pism2 = PureSatIncreSATManagerAlloc(pm);
t0 = util_cpu_ctime();
options = BmcOptionAlloc();
options->satInFile = BmcCreateTmpFile();
options->satOutFile = BmcCreateTmpFile();
NumofCurrentLatch=0;
t1 = util_cpu_ctime();
PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
PureSatGenerateSupportTable(network,pm);
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Generate DFS: %g\n",(double)((t2-t1)/1000.0));
pm->vertexTable = (st_table *)PureSatCreateInitialAbstraction(network,ltlFormula,&NumofCurrentLatch,pm);
pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
Ntk_NetworkForEachLatch(network, gen, node){
if (st_lookup_int(pm->CoiTable, node, &tmp)){
NumofLatch++;
nodeName = Ntk_NodeReadName(node);
if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
{
array_insert_last(char *,visibleArray,nodeName);
latch = Ntk_NetworkFindNodeByName(network,nodeName);
PureSatComputeTableForLatch(network,pm->AbsTable,latch);
}
else
array_insert_last(char *,invisibleArray,nodeName);
}
}
if(pm->verbosity>=1){
fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
}
CoiArray = array_dup(visibleArray);
array_append(CoiArray,invisibleArray);
maigManager = Ntk_NetworkReadMAigManager(network);
if (maigManager == NIL(mAig_Manager_t)) {
(void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
BmcOptionFree(options);
return 1;
}
nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
MVFAIG_NETWORK_APPL_KEY);
/*build property clauses*/
if (Ctlsp_isPropositionalFormula(ltlFormula))
property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula);
else
property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula->left);
if (property == mAig_NULL){
fprintf(vis_stderr,"property = NULL\n");
exit(0);
}
property = bAig_Not(property);
while(NumofCurrentLatch < NumofLatch)
{
t3 = util_cpu_ctime();
if(pm->verbosity>=1)
fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
NumofCurrentLatch,NumofLatch,pm->Length);
if(pm->verbosity>=2)
fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
//tmpRefinement1 = array_alloc(char *,0);
firstTime = TRUE;
pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
if(realRefine){
arrayForEachItem(char *,refinement,i,nodeName)
{
latch = Ntk_NetworkFindNodeByName(network,nodeName);
PureSatComputeTableForLatch(network,pm->AbsTable,latch);
}
array_append(visibleArray,refinement);
latchThreshHold=(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)4)+1;
addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
addtoAbs = addtoAbs >50 ? 50: addtoAbs;
array_free(invisibleArray);
invisibleArray = array_alloc(char *,0);
st_foreach_item_int(pm->CoiTable,stGen,&latch,&i)
{
nodeName = Ntk_NodeReadName(latch);
if(!st_lookup(pm->vertexTable,nodeName,0))
array_insert_last(char *,invisibleArray,nodeName);
}
t1 = util_cpu_ctime();
PureSatGetCoiForVisibleArray_Ring(network, visibleArray,RingPosition, pm->CoiTable);
RingPosition = array_n(visibleArray);
arrayRC = PureSatGenerateRingFromAbs(network,pm,invisibleArray,&NumInSecondLevel);
if(pm->verbosity>=2){
fprintf(vis_stdout,"NumInSecondLevel is %d ",NumInSecondLevel);
fprintf(vis_stdout,"latchThreshHold is %d\n",latchThreshHold);
}
latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;
if(pm->verbosity>=2){
fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
}
t2 = util_cpu_ctime();
if(pm->verbosity>=2){
fprintf(vis_stdout,"Generate Ring: %g\n",(double)((t2-t1)/1000.0));
}
array_free(refinement);
}/* if(realRefine)*/
realRefine =FALSE; /* means no ref, just Length++.*/
t1 = util_cpu_ctime();
if((ExistSimplePath =
PureSatExistASimplePath(network,pism1,visibleArray,property,pm)))
{
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
pism1->oldLength = pm->Length;
pism1->Length = pm->Length;
pism1->beginPosition = array_n(visibleArray);
if(pm->verbosity>=1)
fprintf(vis_stdout, "Simple Path Exists, length = %d\n",pm->Length);
/*check Abs Model*/
t1 = util_cpu_ctime();
ExistACE = PureSatIncreExistCE(network,pism2,visibleArray,property,pm);
if(pm->verbosity>=2)
fprintf(vis_stdout,"beginPosition2: %d, oldLength2 %d\n",pism2->beginPosition, pism2->oldLength);
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Solve on Abs model: %g\n",(double)((t2-t1)/1000.0));
pism2->oldLength = pm->Length;
pism2->Length = pm->Length;
pism2->beginPosition = array_n(visibleArray);
needSorting = FALSE;
/*keep a record of previous position for refine's use*/
oldLength = pism2->oldLength;
beginPosition = pism2->beginPosition;
/* while(ExistACE)
loop until find sufficient set*/
if(ExistACE)
{
if(pm->verbosity>=1)
fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
cnfstate = BmcCnfClausesFreeze(pism2->cnfClauses);
pism2->propertyPos = cnfstate->nextIndex;
/*store the conflict clauses*/
ConClsArray = array_alloc(int,0);
/*if incremental */
if(pm->incre){
if(pism2->cm->savedConflictClauses){
saved = pism2->cm->savedConflictClauses;
for(i=0, space=saved->space; i<saved->num; i++, space++){
array_insert_last(int,ConClsArray,*space);
}
}
}
realRefine = TRUE;
/*incrementally check Concrete Model*/
tmpRefinement = array_alloc(char *,0);
if(pm->verbosity>=2)
fprintf(vis_stdout,"Begin building a new abstract model\n");
for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
{
if(i>0)
latchThreshHold = array_n(arrayRC)-latchThreshHold;
for(j=0;j<latchThreshHold;j++)
{
if((i+j)<array_n(arrayRC))
{
nodeName = array_fetch(char *,arrayRC,i+j);
array_insert_last(char *,tmpRefinement,nodeName);
if(pm->verbosity>=2)
fprintf(vis_stdout, "picking %s\n",nodeName);
}
else
break;
}/* for(j=0;*/
tmpRefinement1=array_dup(visibleArray);
array_append(tmpRefinement1,tmpRefinement);
t1 = util_cpu_ctime();
pism2->cm->option->incAll = 1;
pism2->cm->option->incTraceObjective = 0;
pism2->cm->option->incPreserveNonobjective = 0;
if(PureSatIncreExistCEForRefineOnAbs(network,pism2,tmpRefinement1,property,firstTime,pm)) {
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
if((i+j)>=array_n(arrayRC)){
if(pm->verbosity>=1)
fprintf(vis_stdout,"found real counterexamples\n");
if(pm->dbgLevel>=1){
options->printInputs = TRUE;
BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
pm->result, pm->Length, pm->CoiTable, options,
NIL(array_t));
array_free(pm->result);
pm->result = NIL(array_t);
}
array_free(tmpRefinement1);
array_free(tmpRefinement);
BmcOptionFree(options);
PureSatIncreSATManagerFree(pm,pism1);
PureSatIncreSATManagerFree(pm,pism2);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
array_free(visibleArray);
return FALSE;
}
else{
if(pm->result!=NIL(array_t)){
array_free(pm->result);
pm->result = NIL(array_t);
}
}
}
else{
t2 = util_cpu_ctime();
if(pm->verbosity>=1)
fprintf(vis_stdout,"found a sufficient model\n");
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
firstTime = FALSE;
arrayForEachItem(char *,tmpRefinement1,k,nodeName){
node = Ntk_NetworkFindNodeByName(network, nodeName);
if(!st_lookup(pm->SufAbsTable,node,NIL(char *)))
st_insert(pm->SufAbsTable,node, (char *)0);
else{
fprintf(vis_stderr,"wrong in sufabstable \n");
exit(0);
}
}
pism2->beginPosition = array_n(tmpRefinement1);
pism2->oldLength = Length;
array_free(tmpRefinement1);
break;
}
pism2->beginPosition = array_n(tmpRefinement1);
array_free(tmpRefinement1);
pism2->oldLength = Length;
} /*for(i=0;i<array_n(arrayRC)*/
/*recover the conflict clauses and incremental SAT option*/
pism2->cm->option->incAll = 0;
pism2->cm->option->incTraceObjective = 1;
pism2->cm->option->incPreserveNonobjective = 1;
/*if incremental*/
if(pm->incre){
if(pism2->cm->savedConflictClauses)
sat_ArrayFree(pism2->cm->savedConflictClauses);
pism2->cm->savedConflictClauses = sat_ArrayAlloc(16);
arrayForEachItem(int, ConClsArray,i,tmp)
sat_ArrayInsert(pism2->cm->savedConflictClauses,tmp);
}
array_free(tmpRefinement);
t1 = util_cpu_ctime();
refinement = PureSatRefineOnAbs(network,pm,property,addtoAbs);
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"time for RefOnAbs: %g\n",(double)((t2-t1)/1000.0));
st_free_table(pm->SufAbsTable);
pm->SufAbsTable = NIL(st_table);
/*adjust parameters*/
NumofCurrentLatch+=array_n(refinement);
pm->Length++;
pism1->Length++;
pism2->Length++;
BmcCnfClausesRestore(pism2->cnfClauses, cnfstate);
pism2->beginPosition = beginPosition;
pism2->oldLength = oldLength;
FREE(cnfstate);
}/* if(pism2->cm->status == SAT_SAT)*/
else /*if(pism2->cm->status != SAT_SAT)*/
{
if(pm->verbosity>=1)
fprintf(vis_stdout,"no Abstract Counterexample at length %d \n",pm->Length);
pm->Length++;
pism1->Length++;
pism2->Length++;
st_free_table(pm->SufAbsTable);
pm->SufAbsTable = NIL(st_table);
}
} /*if(ExistSimplePath)*/
else /* if no simple path*/
{
t2 = util_cpu_ctime();
if(pm->verbosity>=2)
fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
if(pm->verbosity>=1)
fprintf(vis_stdout,"simple Path doesn't exist, exit\n");
BmcOptionFree(options);
PureSatIncreSATManagerFree(pm,pism1);
PureSatIncreSATManagerFree(pm,pism2);
PureSatManagerFree(pm);
array_free(CoiArray);
array_free(visibleArray);
return TRUE;
}
}/* while(NumofCurrentLatch < NumofLatch)*/
/*st_free_table(AbsTable);*/
/*Now go to the concrete model*/
if(pm->verbosity>=1)
fprintf(vis_stdout,"reach concrete model\n");
array_append(visibleArray,refinement);
array_free(refinement);
while(PureSatExistASimplePath(network,pism1,visibleArray,property,pm))
{
pism1->oldLength = pism1->Length;
pism1->beginPosition = array_n(visibleArray);
if(PureSatExistCE(network,pism2,options,visibleArray,property,pm,1)) {
if(pm->verbosity>=1)
fprintf(vis_stdout,"found real counterexample of length:%d\n",pm->Length);
if(pm->dbgLevel>=1){
options->printInputs = TRUE;
BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
pm->result, pm->Length, pm->CoiTable, options,
NIL(array_t));
}
BmcOptionFree(options);
PureSatIncreSATManagerFree(pm,pism1);
PureSatIncreSATManagerFree(pm,pism2);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
array_free(visibleArray);
return FALSE;
}
else
{
pism2->oldLength = Length;
pm->Length++;
pism1->Length++;
pism2->Length++;
pism2->beginPosition = array_n(visibleArray);
}
}
BmcOptionFree(options);
PureSatIncreSATManagerFree(pm,pism1);
PureSatIncreSATManagerFree(pm,pism2);
/*PureSatManagerFree(pm);*/
array_free(CoiArray);
array_free(visibleArray);
return TRUE;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSatCmdParse | ( | int | argc, |
| char ** | argv, | ||
| PureSat_Manager_t * | pm | ||
| ) |
Function********************************************************************
Synopsis [PURESAT command parser]
Description [PURESAT command parser]
SideEffects []
SeeAlso []
Definition at line 609 of file puresatMain.c.
{
int c, incre;
util_getopt_reset();
while ((c = util_getopt(argc, argv, "t:i:h:v:I:")) != EOF) {
switch(c) {
case 'i':
strcpy(pm->ltlFileName,util_strsav(util_optarg));
break;
case 't' :
pm->timeOutPeriod = atoi(util_optarg);
break;
case 'v':
pm->verbosity = atoi(util_optarg);
break;
case 'I':
incre = atoi(util_optarg);
pm->incre = (incre==0)? FALSE:TRUE;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
return;
usage:
(void) fprintf(vis_stderr, "usage: abrf [-h][-i ltlfile][-t timeout]\n");
(void) fprintf(vis_stderr, " -i \tName of LTL file.\n");
(void) fprintf(vis_stderr, " -t \ttimeout.\n");
(void) fprintf(vis_stderr, " -v \tverbosity for more information. \n");
(void) fprintf(vis_stderr, " -I \tincremental SAT switch. \n");
(void) fprintf(vis_stderr, "\t\t0 for non-incremental, other values for incremental\n");
(void) fprintf(vis_stderr, " -h \tprint the command usage\n");
}
Here is the caller graph for this function:
