Campus Units

Aerospace Engineering, Computer Science, Electrical and Computer Engineering

Document Type

Article

Conference

Formal Methods in Computer-Aided Design (FMCAD 2017)

Publication Version

Published Version

Publication Date

10-2017

Journal or Book Title

Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)

First Page

164

Last Page

171

DOI

10.23919/FMCAD.2017.8102255

Conference Title

17th Conference on Formal Methods in Computer-Aided Design (FMCAD 2017)

Conference Date

October 2-6, 2017

City

Vienna, Austria

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 implementations. 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 solving 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 onaverage 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.

Comments

This proceeding is published as Rohit Dureja and Kristin Yvonne Rozier. “FuseIC3: An Algorithm for Checking Large Design Spaces.” In Formal Methods in Computer-Aided Design (FMCAD 2017), IEEE/ACM, Vienna, Austria, October 2–6, 2017. DOI: 10.23919/FMCAD.2017.8102255. Posted with permission.

Copyright Owner

The Authors and FMCAD, Inc.

Language

en

File Format

application/pdf

Share

Article Location

 
COinS