#include "amcInt.h"
Include dependency graph for amcCmd.c:
Go to the source code of this file.
Functions | |
| static int | CommandAmc (Hrc_Manager_t **hmgr, int argc, char **argv) |
| static void | ApproximateModelCheckUsage (void) |
| static void | TimeOutHandle (void) |
| void | Amc_Init (void) |
| void | Amc_End (void) |
| boolean | FormulaTestIsForallQuantifier (Ctlp_Formula_t *formula) |
Variables | |
| static char rcsid[] | UNUSED = "$Id: amcCmd.c,v 1.44 2005/05/19 02:36:36 awedh Exp $" |
| static jmp_buf | timeOutEnv |
Function Documentation
| void Amc_End | ( | void | ) |
| void Amc_Init | ( | void | ) |
AutomaticEnd Function********************************************************************
Synopsis [Initializes the amc package.]
SideEffects []
SeeAlso [Amc_End]
Definition at line 71 of file amcCmd.c.
{
Cmd_CommandAdd("approximate_model_check", CommandAmc, 0);
/* Cmd_CommandAdd("approximate_compute_reach", CommandApproxReach, 0); */
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ApproximateModelCheckUsage | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Prints the usage of the approximate_model_checking command.]
SideEffects []
SeeAlso [CommandAmc]
Definition at line 495 of file amcCmd.c.
{
(void) fprintf(vis_stderr, "usage: approximate_model_check [-h] ");
(void) fprintf(vis_stderr, "[-t secs] [-v] ctlfile\n");
(void) fprintf(vis_stderr, " -h print the command usage\n");
(void) fprintf(vis_stderr, " -t secs Seconds allowed for computation\n");
(void) fprintf(vis_stderr, " -v number verbosity level\n");
(void) fprintf(vis_stderr, " ctlfile File containing the ctl formulas\n");
return;
} /* End of ApproximateModelCheckUsage */
Here is the caller graph for this function:
| static int CommandAmc | ( | Hrc_Manager_t ** | hmgr, |
| int | argc, | ||
| char ** | argv | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [The approximate_model_check command.]
CommandName [approximate_model_check]
CommandSynopsis [perform ACTL model checking on an abstracted and flattened network]
CommandArguments [\[-h\] \[-v <verbosity_level>\] <ctl_file> ]
CommandDescription [Performs ACTL model checking on an abstracted and flattened network. Predefined abstractions are performed prior to model checking. Before calling this command, the user should have initialized the design by calling the command init_verify.
The command includes two dual algorithms. The user should set appropriate environment parameters associated with the command to execute proper algorithm. By default, the command makes its effort to prove whether given ACTL formula is positive. To check whether the ACTL formula is negative, user should set the environment parameter amc_prove_false prior to executing the command. See below for the environment parameters associated with this command.
Properties to be verified should be provided as ACTL formulas in the file <ctl_file>. The command only accepts ACTL formulas. Mixed, ECTL expressions are not supported. ACTL formulas are those in which all quantifiers are universal and negation is only allowed at the level of atomic propositions. For the precise syntax of CTL formulas, see the VIS CTL and LTL syntax manual.
The command is designed to tackle the state explosion problem we encounter when dealing with large and complex circuits. Based on the initial size of the group, the command constructs over- or under-approximation of the transition relation of the system. A group (subsystem) is a portion of the original circuit containing a subset of the latches and their next state functions. The initial size of a group can be set with the amc_sizeof_group environment variable. These initial approximations may not contain every detail of the exact system. However they may contain enough information to determine whether the formula is positive or negative. Starting from an initial coarse approximation, the command makes its effort to prove whether given ACTL formula is positive or negative. When the procedure fails to prove correctness of the formula with initial approximations, it automatically refines the approximations. It repeats the process until the algorithm produces a reliable result or the available resources are exhausted.
Due to the overhead procedures, for some circuits, the exact model_check method may evaluate formulas faster with less resources. If any formula evaluates to false, a debug trace is reported.
The command does not use fairness constraints even if they have been read with the read_fairness command.
Command options:
-hPrint the command usage.
-v <verbosity_level>Specify verbosity level.
verbosity_levelmust be one of the following:0: No feedback provided. This is the default.
1: Some feedback.
2: Lots of feedback.- -t
<timeOutPeriod> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
<ctl_file>File containing ACTL formulas to be model checked.
Environment parameters should be set using the set command from the VIS shell
(e.g. vis> set amc_prove_false).
amc_prove_falseWhen the parameter is set, the command makes its effort to prove whether given ACTL formula is negative. The command constructs a set of under-approximations of the transition relations of the system. When the formula evaluates to false, a debug trace is reported by default.amc_grouping_method <grouping method>Specifies grouping method. Grouping method is a method for grouping number of latches into single subsystem. Two methods are supported.Grouping based on hierarchy<code>(default) : The method groups latches based on the hierarchy of the system. Normally, complex circuits are designed in multiple processes. Furthermore, processes form a hierarchy. The method uses this information provided by the original design. When a design described in high level description language is transformed into low level BLIF format, the processes are transformed into subcircuits. The method groups those latches that are within same subcircuit.
Grouping based on latch dependencies(latch_dependency): The method groups those latches that are closely related. Closely related latches are those who has many (transitive) connections between them.
When the parameter is not specified, the command by default uses hierarchical grouping method.
amc_sizeof_group <integer value>Determines the number of latches in each group(subsystem). The default value is 8. The initial size of the subsystem determines the initial degree of approximations of the transition relations. There's no proven rule of setting the value. Some experimental results show that setting the value to about 5-20% of overall number of latches is reasonable(e.g. if the system contains 100 latches set the value to 5-20). However, the suggested range may not work well with some examples.amc_DC_level <integer value>Specifies don't care levels. Default level is 0. Absence of the parameter sets the amc_DC_level to 0. amc_DC_level must be one of the following:0: No don't cares are used. This is the default.1: Use unreachable states as don't cares.2: Aggressively use DC's to simplify MDD's in model checking.
Using don't cares may take more time for some examples since the approximate model checker computes the reachable states for each subsystem. For some large circuits it is undesirable to set don't care level.
Related "set" options:
ctl_change_bracket <yes/no> Vl2mv automatically converts "\[\]" to "<>" in node names, therefore CTL parser does the same thing. However, in some cases a user does not want to change node names in CTL parsing. Then, use this set option by giving "no". Default is "yes".
See also commands : model_check, incremental_ctl_verification
Examples:
Here are some example sequences of the VIS executions using the approximate model checker.
read_blif_mv abp/abp.mv
flatten_hierarchy
static_order
build_partition_mdds
set amc_sizeof_group 4
approximate_model_check abp/abpt.ctl
time
quit
read_blif_mv coherence/coherence.mv
flatten_hierarchy
static_order
build_partition_mdds
set amc_sizeof_group 8
set amc_prove_false
set amc_DC_level 0
approximate_model_check coherence/coherence2.ctl
time
quit
The algorithm used by approximate_model_check is described in detail in ftp://vlsi.colorado.edu/pub/iccad96.ps ]
SideEffects []
Definition at line 317 of file amcCmd.c.
{
static int timeOutPeriod; /* CPU seconds allowed */
char *ctlFileName; /* Name of file containing formulas */
FILE *ctlFile; /* File to read the formulas from */
Ntk_Network_t *network; /* Pointer to the current network */
array_t *ctlFormulaArray; /* Array of read ctl formulas */
array_t *ctlNormalForm; /* Array of normal ctl formulas */
Ctlp_Formula_t *currentFormula; /* Formula being verified */
int c, i;
Amc_VerbosityLevel verbosity; /* Verbosity level */
long initialTime;
long finalTime;
/* Initialize Default Values */
timeOutPeriod = 0;
ctlFileName = NIL(char);
verbosity = Amc_VerbosityNone_c;
/*
* Parse command line options.
*/
util_getopt_reset();
while ((c = util_getopt(argc, argv, "ht:v:")) != EOF) {
switch(c) {
case 'h':
ApproximateModelCheckUsage();
return 1;
case 't':
timeOutPeriod = atoi(util_optarg);
break;
case 'v':
verbosity = (Amc_VerbosityLevel) atoi(util_optarg);
break;
default:
ApproximateModelCheckUsage();
return 1;
}
}
/* Make sure the CTL file has been provided */
if (argc == util_optind) {
ApproximateModelCheckUsage();
return 1;
}
else {
ctlFileName = argv[util_optind];
}
/*
* Obtain the network from the hierarchy manager
*/
network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
if (network == NIL(Ntk_Network_t)) {
return 1;
}
/*
* Check whether the fairness was read.
*/
{
Fsm_Fsm_t *exactFsm = Fsm_NetworkReadOrCreateFsm(network);
Fsm_Fairness_t *fairCons = Fsm_FsmReadFairnessConstraint(exactFsm);
int numOfDisjuncts = Fsm_FairnessReadNumDisjuncts(fairCons);
if (numOfDisjuncts > 1) {
/* non-Buchi */
fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
}
else {
int numOfConj = Fsm_FairnessReadNumConjunctsOfDisjunct(fairCons, 0);
if (numOfConj > 1) {
/* Buchi */
fprintf(vis_stdout, "** amc warning: Fairness Constraint is not supported.\n");
}
}
}
/*
* Read in the array of CTL formulas provided in ctlFileName
*/
ctlFile = Cmd_FileOpen(ctlFileName, "r", NIL(char *), 0);
if (ctlFile == NIL(FILE)) {
return 1;
}
ctlFormulaArray = Ctlp_FileParseFormulaArray(ctlFile);
fclose(ctlFile);
if (ctlFormulaArray == NIL(array_t)) {
(void) fprintf(vis_stderr, "** amc error: Error while parsing ctl formulas in file.\n");
return 1;
}
ctlNormalForm = Ctlp_FormulaArrayConvertToExistentialFormTree(ctlFormulaArray);
/*
* Start the timer.
*/
if (timeOutPeriod > 0) {
(void) signal(SIGALRM, (void (*)(int))TimeOutHandle);
(void) alarm(timeOutPeriod);
/* The second time setjmp is called, it returns here !!*/
if (setjmp(timeOutEnv) > 0) {
(void) fprintf(vis_stdout, "# AMC: timeout ocurred after %d seconds.\n",
timeOutPeriod);
alarm(0);
/* Note that there is a huge memory leak here. */
Ctlp_FormulaArrayFree(ctlFormulaArray);
Ctlp_FormulaArrayFree(ctlNormalForm);
return 1;
}
}
/*
* Loop over every CTL formula in the array
*/
arrayForEachItem(Ctlp_Formula_t *, ctlNormalForm, i, currentFormula) {
boolean validFormula;
validFormula = FormulaTestIsForallQuantifier(currentFormula);
if (!validFormula) {
fprintf(vis_stderr, "Formula ");
Ctlp_FormulaPrint(vis_stderr, currentFormula);
fprintf(vis_stderr, " is not a valid ACTL formula. Skipping it\n");
}
else if (!Mc_FormulaStaticSemanticCheckOnNetwork(currentFormula, network,
FALSE)) {
(void) fprintf(vis_stdout, "\n** amc error: Error in parsing Atomic Formula:\n%s\n", error_string());
error_init();
Ctlp_FormulaFree( currentFormula );
continue;
}
else {
error_init();
initialTime = util_cpu_time();
Amc_AmcEvaluateFormula(network, currentFormula, verbosity);
finalTime = util_cpu_time();
if(verbosity == Amc_VerbosityVomit_c) {
(void) fprintf(vis_stdout, "\n%-20s%10ld\n", "analysis time =",
(finalTime - initialTime) / 1000);
}
fprintf(vis_stdout, "\n");
}
} /* End of arrayForEachItem in ctlFormulaArray */
/* Deactivate the alarm */
alarm(0);
/* Clean up */
Ctlp_FormulaArrayFree(ctlFormulaArray);
Ctlp_FormulaArrayFree(ctlNormalForm);
error_cleanup();
/* normal exit */
return 0;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| boolean FormulaTestIsForallQuantifier | ( | Ctlp_Formula_t * | formula | ) |
Function********************************************************************
Synopsis [Tests recursively if a formula is a valid ACTL formula.]
Description [This function implements the recursive steps needed for the function FormulaTestIsForallQuantifier.]
SideEffects []
SeeAlso [CommandAmc]
Definition at line 522 of file amcCmd.c.
{
Ctlp_Formula_t *newFormula;
boolean converted;
Ctlp_FormulaClass result;
if (!Ctlp_FormulaTestIsConverted(formula)) {
newFormula = Ctlp_FormulaConvertToExistentialForm(formula);
converted = TRUE;
}
else {
newFormula = formula;
converted = FALSE;
}
result = Ctlp_CheckClassOfExistentialFormula(newFormula);
if (converted) {
Ctlp_FormulaFree(newFormula);
} /* End of if */
return result == Ctlp_ACTL_c || result == Ctlp_QuantifierFree_c;
} /* End of FormulaTestIsForallQuantifier */
Here is the call graph for this function:
Here is the caller graph for this function:
| static void TimeOutHandle | ( | void | ) | [static] |
Function********************************************************************
Synopsis [Handle the timeout signal.]
Description [This function is called when the time out occurs. In principle it could do something smarter, but so far it just transfers control to the point in the code where setjmp was called.]
SideEffects [This function gains control at any point in the middle of the computation, therefore the memory allocated so far leaks.]
Definition at line 562 of file amcCmd.c.
{
longjmp(timeOutEnv, 1);
} /* End of TimeOutHandle */
Here is the caller graph for this function:
Variable Documentation
jmp_buf timeOutEnv [static] |
char rcsid [] UNUSED = "$Id: amcCmd.c,v 1.44 2005/05/19 02:36:36 awedh Exp $" [static] |
CFile***********************************************************************
FileName [amcCmd.c]
PackageName [amc]
Synopsis [Command interface for the amc package.]
Author [Woohyuk Lee <woohyuk@duke.colorado.edu>]
Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.]
