#include "puresatInt.h"
Include dependency graph for puresat.c:
Go to the source code of this file.
Functions | |
| static int | CommandPureSatAbRf (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | TimeOutHandle (void) |
| void | PureSat_Init (void) |
| void | PureSat_End (void) |
Variables | |
| static jmp_buf | timeOutEnv |
Function Documentation
| static int CommandPureSatAbRf | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Check invariant formulae with abstraction refinement method PureSat.]
Description [Check invariant formulae with abstraction refinement method PureSat.]
SideEffects []
SeeAlso []
Definition at line 172 of file puresat.c.
{
Ntk_Network_t * network;
FILE * ltlFile;
array_t * formulaArray;
boolean re;
int i;
PureSat_Manager_t *pm;
int timeOutPeriod;
pm = PureSatManagerAlloc();
timeOutPeriod = pm->timeOutPeriod;
PureSatCmdParse(argc, argv,pm);
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
fprintf(vis_stdout, "Num of latches is %d\n",Ntk_NetworkReadNumLatches(network));
if (network == NIL(Ntk_Network_t)) {
fprintf(vis_stderr,
"No network, please read in the circuit, and init_verify\n");
return 1;
}
ltlFile = Cmd_FileOpen(pm->ltlFileName, "r", NIL(char *), 0);
if (ltlFile == NIL(FILE)) {
fprintf(vis_stdout,"Cannot open LTL file %s\n", pm->ltlFileName);
exit(1);
}
formulaArray = Ctlsp_FileParseFormulaArray(ltlFile);
if(!array_n(formulaArray))
{fprintf(vis_stderr,"ltlfile doesn't contain any formula \n");
exit (1);}
/*timeout*/
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
fprintf(vis_stdout, "signal\n");
(void) alarm(timeOutPeriod);
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout,
"# PURESAT: timeout occurred after %d seconds.\n", timeOutPeriod);
(void) fprintf(vis_stdout, "# PURESAT: data may be corrupted.\n");
alarm(0);
return 1;
}
}
for (i = 0; i < array_n(formulaArray); i++) {
Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, formulaArray, i);
re = PureSatCheckInv_SSS(network,ltlFormula,pm);
if(re)
fprintf(vis_stdout,"formula #%d is true\n",i);
else
fprintf(vis_stdout,"formula #%d is False\n",i);
}
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| void PureSat_End | ( | void | ) |
| void PureSat_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the puresat package. The added command is for testing purpose only; the same algorithm can be activated by the check_invariant command.]
Description [Initializes the puresat package. The added command is for testing purpose only; the same algorithm can be activated by the check_invariant command.]
SideEffects []
SeeAlso [PureSat_End]
Definition at line 102 of file puresat.c.
{
/*
* Add a command to the global command table. By using the leading
* underscore, the command will be listed under "help -a" but not "help".
*/
Cmd_CommandAdd("_puresat_test", CommandPureSatAbRf, 0);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [time out function]
Description [time out function]
SideEffects []
SeeAlso []
Definition at line 153 of file puresat.c.
{
longjmp(timeOutEnv, 1);
}
Here is the caller graph for this function:
Variable Documentation
jmp_buf timeOutEnv [static] |
CFile***********************************************************************
FileName [puresat.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.]
