Peer Reviewed Conferences
-
IC3 with Interal Signals (Best Paper Award)
Rohit Dureja, Arie Gurfinkel, Alexander Ivrii, and Yakir Vizel
Proceedings of Formal Methods in Computer-Aided Design (FMCAD) ,2021
abstract preprint bibtex
Abstract: IC3 is a highly-effective algorithm for formal hardware verification. It cleverly uses a SAT solver to compute an inductive invariant, an over-approximation of reachable states, of a hardware design. The invariant is computed in CNF as a conjunction of lemmas. This CNF representation over state variables, although efficient, leads to an obvious deficiency: IC3 is not effective for designs that do not have a concise CNF invariant over state variables. We show how to remedy this deficiency by extending traditional IC3 to learn invariants not only in terms of state variables, but also in terms of internal signals of the design. Our proposed method can learn significantly more compact invariants than IC3, while maintaining a highly-efficient CNF representation. We evaluate our technique on several industrial sequential equivalence checking (SEC) problems from IBM, SEC problems derived from designs in the Hardware Model Checking Competition (HWMCC) and SEC problems from academia. In addition, we evaluate it on HWMCC benchmarks. IC3 with internal signals is efficient for SEC and outperforms traditional IC3 on an important class of benchmarks.
-
Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration
Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Y. Rozier
Proceedings of Formal Methods in Computer-Aided Design (FMCAD) ,2020
abstract preprint website bibtex
Abstract: Industrial hardware verification tasks often require checking a large number of properties within a testbench. Verification tools often utilize parallelism to improve scalability, either in portfolio mode where different solver strategies run concurrently, or in partitioning mode where disjoint property subsets are verified independently. While most tools focus solely upon reducing end-to-end wall-time, reducing overall CPU-time is a comparably-important goal influencing power consumption, competition for available machines, and IT costs. Portfolio approaches often degrade into highly-redundant work across processes, where similar strategies address properties in nearly- identical order. Partitioning should take property affinity into account, atomically verifying high-affinity properties to minimize redundant work of applying identical strategies on individual properties with nearly-identical logic cones. We improve multi- property parallel verification with respect to both wall- and CPU-time. We extend affinity-based partitioning to guarantee complete utilization of available processes, with provable partition quality. We propose methods to minimize redundant computation, and dynamically optimize work distribution. We deploy our techniques in a sequential redundancy removal framework, using localization to solve non-inductive properties. Our techniques offer up to 3× speedup as demonstrated by extensive experiments.
-
Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of Properties
Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman, and Kristin Y. Rozier
Proceedings of Formal Methods in Computer-Aided Design (FMCAD) ,2019
abstract preprint slides website bibtex
Abstract: From equivalence checking to functional verification to design-space exploration, industrial verification tasks entail checking a large number of properties on the same design. State-of-the-art tools typically solve all properties concurrently, or one-at-a-time. They do not optimally exploit subproblem sharing between properties, leaving an opportunity to save considerable verification resource via concurrent verification of properties with nearly identical cone of influence (COI). These high-affinity properties can be concurrently solved; the verification effort expended for one can be directly reused to accelerate the verification of the others, without hurting per-property verification resources through bloating COI size. We present a near-linear runtime algorithm for partitioning properties into provably high-affinity groups for concurrent solution. We also present an effective method to partition high-structural-affinity groups using semantic feedback, to yield an optimal multi-property localization abstraction solution. Experiments demonstrate substantial end-to-end verification speedups through these techniques, leveraging parallel solution of individual groups
-
Intersection and Rotation of Assumption Literals Boosts Bug-Finding
Rohit Dureja, Jianwen Li, Geguang Pu, Moshe Y. Vardi, and Kristin Y. Rozier
Proceedings of Verified Software: Theories, Tools, and Experiments (VSTTE) ,2019
abstract preprint slides website bibtex
Abstract: SAT-based techniques comprise the state-of-the-art in functional verification of safety-critical hardware and software, including IC3/PDR-based model checking and Bounded Model Checking (BMC). BMC is the incontrovertible best method for unsafety checking, aka bug-finding. Complementary Approximate Reachability (CAR) and IC3/PDR complement BMC for bug-finding by detecting different sets of bugs. To boost the efficiency of formal verification, we introduce heuristics involving intersection and rotation of the assumption literals used in the SAT encodings of these techniques. The heuristics generate smaller unsat cores and diverse satisfying assignments that help in faster convergence of these techniques, and have negligible runtime overhead. We detail these heuristics, incorporate them in CAR, and perform an extensive experimental evaluation of their performance, showing a 25% boost in bug-finding efficiency of CAR. We contribute a detailed analysis of the effectiveness of these heuristics: their influence on SAT-based bug-finding enables detection of different bugs from BMC-based checking. We find the new heuristics are applicable to IC3/PDR-based algorithms as well, and contribute a modified clause generalization procedure.
-
SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Jianwen Li, Rohit Dureja, Geguang Pu, Kristin Y. Rozier, and Moshe Y. Vardi
Proceedings of Computer Aided Verification (CAV) ,2018
abstract preprint slides website bibtex
Abstract: We present a new safety hardware model checker SimpleCAR that serves as a reference implementation for evaluating Complementary Approximate Reachability (CAR), a new SAT-based model checking framework inspired by classical reachability analysis. The tool gives a “bottom-line” performance measure for comparing future extensions to the framework. We demonstrate the performance of SimpleCAR on challenging benchmarks from the Hardware Model Checking Competition. Our experiments indicate that SimpleCAR is particularly suited for unsafety checking, or bug-finding; it is able to solve 7 unsafe instances within 1 hour that are not solvable by any other state-of-the-art techniques, including BMC and IC3/PDR, within 8 hours. We also identify a bug (reports safe instead of unsafe) and 48 counterexample generation errors in the tools compared in our analysis.
-
More Scalable LTL Model Checking via Discovering Design-Space Dependencies
Rohit Dureja and Kristin Y. Rozier
Proceedings of Tools and Algorithms for the Construction and Analysis of Systems (TACAS) ,2018
abstract preprint slides website poster bibtex
Abstract: Modern system design often requires comparing several models over a large design space. Different models arise out of a need to weigh different design choices, to check core capabilities of versions with varying features, or to analyze a future version against previous ones. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. We exploit relationships between different models of the same (or related) systems to optimize the model-checking search. Our algorithm, D3, preprocesses the design space and checks fewer model-checking instances, e.g., using nuXmv. It automatically prunes the search space by reducing both the number of models to check, and the number of LTL properties that need to be checked for each model in order to provide the complete model-checking verdict for every individual model-property pair. We formalize heuristics that improve the performance of D3. We demonstrate the scalability of D3 by extensive experimental evaluation, e.g., by checking 1,620 real-life models for NASA’s NextGen air traffic control system. Compared to checking each model-property pair individually, D3 is up to 9.4× faster.
-
FuseIC3: An Algorithm for Checking Large Design Spaces
Rohit Dureja and Kristin Y. Rozier
Proceedings of Formal Methods in Computer-Aided Design (FMCAD) ,2017
abstract preprint slides website bibtex
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 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.
-
A Case Study in Safety, Security, and Availability of Wireless-Enabled Aircraft Communication Networks
Rohit Dureja, Eric W. D. Rozier, and Kristin Y. Rozier
Proceedings of AIAA Aviation Technology, Integration, and Operations Conference (AVIATION) ,2017
abstract preprint slides bibtex
Abstract: As the costs of fuel and maintenance increase and regulations on weight and environmental impact tighten, there is an increasing push to transition on-board aircraft networks to wireless, reducing weight, fuel, maintenance time, and pollution. We outline a candidate short-range hybrid wired/wireless network for aircraft on-board communications using the common ZigBee protocol and privacy-preserving search implemented as a secure publish/subscribe system using specially coded meta-data. Formally specifying safety and security properties and modeling the network in nuXmv enables verification and fault analysis via model checking and lays the groundwork for future certification avenues. We report on our experiments building and testing our candidate hybrid network and report on overhead and availability for encrypted and fault-tolerant communications, and propose a system that allows system designers to directly trade fault-tolerance for bandwidth, or vice-versa, in an encrypted privacy-preserving framework.
Journals
-
Incremental Design-Space Model Checking via Resuable Reachable State Approximations
Rohit Dureja and Kristin Y. Rozier
Formal Methods in System Design ,2022
abstract preprint bibtex
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 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. Moreover, we evaluate the performance improvement of FuseIC3 by smarter ordering of models and property grouping using a linear-time hashing approach.
-
Formal Framework for Safety, Security, and Availability of Aircraft Communication Networks
Rohit Dureja and Kristin Yvonne Rozier
Journal of Aerospace Information Systems ,2020
abstract preprint bibtex
Abstract: As the costs of fuel and maintenance increase and regulations on weight and environmental impact tighten, there is an increasing push to transition on-board aircraft networks to wireless, reducing weight, fuel, maintenance time, and pollution. We outline a candidate short-range wireless network for aircraft on-board communications using the common ZigBee protocol and privacy-preserving search implemented as a secure publish/subscribe system using specially coded meta-data. Formally specifying safety and security properties and modeling the network in nuXmv enables verification and fault analysis via model checking and lays the groundwork for future certification avenues. We report on experiments formally analyzing our candidate wireless network, showing overhead and availability for encrypted and fault-tolerant communications. We propose a formal model that allows system designers to estimate communication failure rates, and directly trade off fault-tolerance for bandwidth, while preserving communication security.
Theses
-
Model Checking Large Design Space: Theory, Tools, and Experiments (Research Excellence Award)
Rohit Dureja
Ph.D. Thesis, Iowa State University ,2020
pdf bibtex
Workshops and Posters
-
Scalable Verification of Designs with Multiple Properties (Best Student Contribution Award)
Rohit Dureja and Kristin Y. Rozier
Formal Methods in Computer-Aided Design (FMCAD) Student Forum ,2019
abstract pdf slides poster bibtex
Abstract: Many industrial verification tasks entail checking a large number of properties on the same design. Formal verification techniques, such as model checking, can verify multiple properties concurrently, or sequentially one-at-a-time. State-of-the-art verification tools do not optimally exploit subproblem sharing between properties, leaving an opportunity to save considerable verification resources. A significant need therefore exists to develop efficient and scalable techniques that intelligently check multiple properties by utilizing implicit inter-property logical dependencies and subproblem sharing, and improve tool orchestration. We report on our investigation of the multi-property model checking problem, and discuss research results, and highlight future research directions.
-
From One to Many: Checking A Set of Models
Rohit Dureja and Kristin Y. Rozier
Formal Methods in Computer-Aided Design (FMCAD) Student Forum ,2017
abstract pdf slides poster bibtex
Abstract: Whether the objective is to narrow in on the final system design, check capabilities of system versions with varying features, or regression testing to make a design more robust, several models of the system under development have to be analyzed. Model checking can compare different models; however, applying model checking off-the-shelf may not scale due to the large size of the design space for today’s complex systems. There is a need to develop new algorithms that intelligently use inherent properties of models in a design space to increase scalability of checking the complete model-set. We report on our investigation of the model-set checking problem, highlight preliminary results, and discuss ongoing work and future research directions.
-
Comparative Safety Analysis of Wireless Communication Networks in Avionics
Rohit Dureja and Kristin Y. Rozier
Formal Methods in Computer-Aided Design (FMCAD) Student Forum ,2016
abstract pdf slides poster bibtex
Abstract: —Existing wired networks add weight and complexity to current aircraft design. To reduce weight of aircraft, it is essential to decrease the number of wired components and move them to wireless. However, migration of wired to wireless needs to be supported by a thorough analysis of the complexities and failure aspects of the two mediums. The wireless network needs to be at least as reliable and fault tolerant as the existing wired network. This paper proposes a formal framework for a comparative safety analysis of wired and wireless networks. Due to the plug-and-play nature of the framework, it is adaptable to a wide variety of network protocols. It facilitates identification of the minimum set of events that lead to system failure, and using quantified failure probabilities recommends fault tolerant mechanisms that increase system reliability. Designers can then compare candidates for wireless protocols among each other, as well as the wired network, and make informed design decisions