approximate_model_check - perform ACTL model checking on an abstracted and flattened network

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:

-h

Print the command usage.

-v <verbosity_level>

Specify verbosity level. verbosity_level must 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_false
When 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(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

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