没有合适的资源?快使用搜索试试~ 我知道了~
一种检查大型设计空间的算法.pdf
1.该资源内容由用户上传,如若侵权请联系客服进行举报
2.虚拟产品一经售出概不退款(资源遇到问题,请及时私信上传者)
2.虚拟产品一经售出概不退款(资源遇到问题,请及时私信上传者)
版权申诉
0 下载量 13 浏览量
2024-04-02
14:36:22
上传
评论
收藏 360KB PDF 举报
温馨提示
试读
8页
一种检查大型设计空间的算法.pdf
资源推荐
资源详情
资源评论
FuseIC3: An Algorithm for Checking Large Design Spaces
Rohit Dureja and Kristin Yvonne Rozier
Iowa State University
Abstract—The design of safety-critical systems often requires
design space exploration: comparing several system models that
differ in terms of design choices, capabilities, and implementa-
tions. Model checking can compare different models in such a set,
however, it is continuously challenged by the state space explosion
problem. Therefore, learning and reusing information from solv-
ing related models becomes very important for future checking
efforts. For example, reusing variable ordering in BDD-based
model checking leads to substantial performance improvement.
In this paper, we present a SAT-based algorithm for checking a
set of models. Our algorithm, FuseIC3, extends IC3 to minimize
time spent in exploring the common state space between related
models. Specifically, FuseIC3 accumulates artifacts from the
sequence of over-approximated reachable states, called frames,
from earlier runs when checking new models, albeit, after careful
repair. It uses bidirectional reachability; forward reachability
to repair frames, and IC3-type backward reachability to block
predecessors to bad states. We extensively evaluate FuseIC3 over
a large collection of challenging benchmarks. FuseIC3 is on-
average up to 5.48× (median 1.75×) faster than checking each
model individually, and up to 3.67× (median 1.72×) faster than
the state-of-the-art incremental IC3 algorithm.
I. INTRODUCTION
In the early phases of design, there are several models of the
system under development constituting a design space [2, 19,
23]. Each model in such a set is a valid design of the system,
and the different models differ in terms of core capabilities,
assumptions, component implementations, or configurations.
We may need to evaluate the different design choices, or to
analyze a future version against previous ones in the product
line. Model checking can be used to aid system development
via a thorough comparison of the set of models. Each model
in the set is checked one-by-one against a set of properties
representing requirements. However, for large and complex
design spaces, such an approach can be inefficient or even fail
to scale to handle the combinatorial size of the design space.
Nevertheless, model checking remains the most widely used
method in industry when dealing with such systems [5, 19,
21, 23, 24].
We assume that different models in the design space have
overlapping reachable states, and the models are checked
sequentially. In a typical scenario, a model-checking algorithm
doesn’t take advantage of this information and ends up re-
verifying “already explored” state spaces across models. For
large models this can be extremely wasteful as every model-
checking run re-explores already known reachable states. The
problem becomes acute when model differences are small, or
Artifacts for reproducibility, code, theorem proofs, and detailed experi-
mental results can be found at http://temporallogic.org/research/FMCAD17.
Thanks to NSF CAREER Award CNS-1552934 for supporting this work.
when changes in the models are outside the cone-of-influence
of the property being checked, i.e., although the reachable
states in the models vary, none of them are bad. Therefore, as
the number of models grows, learning and reusing information
from solving related models becomes very important for future
checking efforts.
We present an algorithm that automatically reuses
information from earlier model-checking runs to minimize the
time spent in exploring the symbolic state space in common
between related models. The algorithm, FuseIC3, is an
extension to one of the fastest bit-level verification methods,
IC3 [6], also known as property directed reachability (PDR)
[17]. Given a set of models and a safety property, FuseIC3
sequentially checks each model by reusing information:
reachable state approximations, counterexamples (cex), and
invariants, learned in earlier runs to reduce the set’s total
checking time. When the difference between two subsequent
models is small or beyond the cone-of-influence of the
property, the invariant or counterexample from the earlier
model may be directly used to verify the current model.
Otherwise, FuseIC3 uses reachable state approximations as
inputs to IC3 to only explore undiscovered reachable states
in the current model. In the former, verification completes
almost instantly, while in the latter, significant time is saved.
When the stored information cannot be used directly, FuseIC3
repairs and patches it using an efficient SAT-based algorithm.
The repair algorithm is the main strength of FuseIC3, and
uses features present in modern SAT solvers. It adds “just
enough” extra information to the saved reachable states to
enable reuse. We demonstrate the industrial scalability of
FuseIC3 on a large set of 1,620 real-life models for the
NASA NextGen air traffic control system [19, 23], selected
benchmarks from HWMCC 2015 [1], and a set of seven
models for the Boeing AIR6110 wheel braking system [5].
Our experiments evaluate FuseIC3 along two dimensions;
checking all models with the same property, and checking
each model with several properties. Lastly, we evaluate the
effect of model relatedness on the performance of FuseIC3.
Related Work The idea of reusing model-checking informa-
tion, like variable orderings, between runs has been extensively
used in BDD-based model checking leading to substantial
performance improvement [3, 27]. Similarly, intermediate SAT
solver clauses and interpolants are reused in bounded model
checking [22, 25]. Reusing learned invariants in IC3 speeds up
convergence of the algorithm [8]. These techniques enable effi-
cient incremental model checking and are useful in regression
verification [28] and coverage computation [9]. FuseIC3 is an
资源评论
百态老人
- 粉丝: 1891
- 资源: 2万+
下载权益
C知道特权
VIP文章
课程特权
开通VIP
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功