**CONFERENCE SERIES: FORMAL METHODS IN COMPUTER-AIDED DESIGN 1**

Alexander Ivrii / Ofer Strichman (Eds.)

# **PROCEEDINGS OF THE 20TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2020**

Alexander Ivrii / Ofer Strichman (Eds.) PROCEEDINGS OF THE 20TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2020

### **Conference Series: Formal Methods in Computer-Aided Design Volume 1**

Conference Series: Formal Methods in Computer-Aided Design

Series edited by:

Warren A. Hunt, Jr., The University of Texas at Austin Austin, TX 78705 |<EMAIL_ADDRESS>Georg Weissenbacher, TU Wien Karlsplatz 13, 1040 Wien, Austria |<EMAIL_ADDRESS>
The Conference on Formal Methods in Computer-Aided Design (FMCAD) is an annual conference on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.

Information on this publication series and the volumes published therein is available at www.tuwien.ac.at/academicpress.

Volume 1 edited by: Alexander Ivrii, IBM Research Haifa University Campus, Mount Carmel, Haifa, 3498825, Israel |<EMAIL_ADDRESS>Ofer Strichman, Technion - Israel Institute of Technology Technion City, Haifa 3200003, Israel |<EMAIL_ADDRESS>
Alexander Ivrii / Ofer Strichman (Eds.)

# **PROCEEDINGS OF THE 20TH CONFERENCE ON FORMAL METHODS IN COMPUTER-AIDED DESIGN – FMCAD 2020**

#### **TU Wien Academic Press, 2020**

c/o TU Wien Bibliothek TU Wien Resselgasse 4, 1040 Wien<EMAIL_ADDRESS>www.tuwien.at/academicpress

This work is licensed under a Creative Commons attribution 4.0 international license (CC BY 4.0). https://creativecommons.org/licenses/by/4.0/

ISSN (online): 2708-7824

ISBN (online): 978-3-85448-042-6

Available online: https://doi.org/10.34727/2020/isbn.978-3-85448-042-6

Media proprietor: TU Wien, Karlsplatz 13, 1040 Wien Publisher: TU Wien Academic Press Publication series editor: Warren A. Hunt, Jr. and Georg Weissenbacher Editors (responsible for the content): Alexander Ivrii and Ofer Strichman

### Preface

These are the proceedings of the twentieth International Conference on Formal Methods in Computer-Aided Design (FMCAD), which was held online during Sep 21 – Sep 24, 2020 (the Coronavirus year). It was the 20th in a series of meetings on the theory and applications of rigorous formal techniques for the automated design of systems. The FMCAD conference covers formal aspects of specification, verification, synthesis, testing, and security, and is a leading forum for researchers and practitioners in academia and industry alike.

The program of FMCAD 2020 is comprised of three tutorials, two invited talks, a student forum, the Hardware Model Checking Competition 2020, and the main program consisting of presentations of 28 accepted papers.

The tutorial day featured three presentations

### The invited talks were

FMCAD'20 also hosted the eighth edition of the Student Forum, which has been held annually since 2013 and provides a platform for graduate students at any career stage to introduce their research to the FMCAD community. The FMCAD Student Forum 2020 was organized by Peter Schrammel and featured short presentations of 8 accepted contributions. A detailed description of the Student Forum, listing all accepted contributions, is provided in the conference proceedings.

The Hardware Model Checking Competition 2020, affiliated with FMCAD 2020 and organized by Armin Biere, Nils Froleyks and Mathias Preiner, is a competitive event for hardware model checking tools from academia and industry.

FMCAD 2020 received 59 submissions out of which the committee decided to accept 28 for publication. Each submission received at least four reviews. The topics of the accepted papers include hardware and software verification, SAT, SMT, learning, synthesis, Neural-Network verification, and more. Out of the accepted papers, 22 are classified as regular papers (20 long and 2 short) and 6 are classified as tool papers (4 long and 2 short).

Organizing this event would not have been possible without the support of a large number of people and our sponsors. The program committee members and additional reviewers, listed on the following pages, did an excellent job providing detailed and insightful reviews, which helped the authors to improve their submissions and guided the selection of the papers accepted for publication. We thank each and every one of them for dedicating their time and providing their expertise.

We thank Ryan Berryhill (University of Toronto) for being the web master, and Peter Schrammel for organizing this year's FMCAD Student Forum. We thank Georg Weissenbacher (TU Wien) both for his exceptional assistance in organizing the event, communicating to us the decisions of the steering committee, as well as being the publication chair.

Holding a conference like FMCAD would not be feasible without the financial support of our sponsors. We would like to express our gratitude to our sponsors (in alphabetical order): Amazon, Centaur Technology Inc., IBM, Novi, Synopsys, and the Technion, Israel institute of Technology.

The conference proceedings are available as Open Access Proceedings published by TU Wien Academic Press, and through the IEEE Xplore Digital Library. Last but not least, we thank all authors who submitted their papers to FMCAD 2020 (accepted or not), and whose contributions and presentations form the core of the conference. We are grateful to everyone who presented their paper, gave a keynote or gave a tutorial. We thank all attendees of FMCAD for supporting the conference and making FMCAD a stimulating and enjoyable event.

Ofer Strichman, Technion, Haifa Alexander Ivrii, IBM, Haifa September 2020

### Message from the Steering Committee Chairman

#### Hello FMCAD people!

Over the past two years, we have been transitioning the FMCAD organization from a USA-based company to an Austrian-based association. Unlike most conferences, the FMCAD Conference meetings have been supported privately by the FMCAD Corporation. For 2020, the newly-formed FMCAD Association will support the FMCAD Conference, and this Association is expected to support the FMCAD Conference in the years to come.

After serving as FMCAD Steering Committee Chairman for more than 15 years now, I will step down and Georg Weissenbacher will assume the leadership of the FMCAD Conference series along with managing the FMCAD Association. Except when I was sick in 2017, I have attended every FMCAD conference since its 1996 inception – and even during the 2017 conference, I was transacting business needed to get FMCAD catered. I have enjoyed working on the FMCAD Conference, and I'm very proud of the technical results presented at FMCAD. And, I'm humbled by the faith that our authors have placed in FMCAD to make their results known.

FMCAD was an early adopter of what has become known as Open Access. After the first ten years of FMCAD publications, we moved from a commercial publisher to self-publishing the FMCAD Conference proceedings – since 2006, all of the FMCAD Conference proceedings are freely available. In addition, through in-kind arrangements with the ACM and the IEEE, the FMCAD Proceedings are available through the ACM and IEEE Digital libraries. In addition, the FMCAD Proceedings are available on the FMCAD website.

I urge everyone to get involved; see http://www.fmcad.org. Talk with FMCAD attendees. Volunteer to assist with a future conference. I have benefited enormously from my association with FMCAD. I have met many people, and over the years, I have come to realize that the conversations and associations I have had participating with FMCAD people are an important part of my life. On a personal note, I met (for just the second time) my wife at FMCAD 1996; she is also my best friend and colleague, and a co-owner co-owner of FMCAD, Inc. With the three or four weeks a year I have invested annually in the FMCAD Conference, the FMCAD community has become an extended family for me. The friendships and comradery from my participation have provided me with tremendous rewards, and continue to do so.

I want to thank everyone for making FMCAD such a pleasant conference to attend. The fellowship I feel when attending FMCAD has kept me invested in preserving and enhancing the FMCAD experience. I also want to thank all of the FMCAD Conference steering committee members, Conference co-chairs, and program committee members for their outstanding work. I'm amazed at the results that have been reported at FMCAD; your efforts have truly enhanced the course of engineering, science, technology, and theory.

Cheers,

Warren A. Hunt, Jr. Steering Committee Chair President, FMCAD, Inc.

# Organizing Committee

### Program Co-Chairs

Alan J. Hu University of British Columbia Warren A. Hunt, Jr. University of Texas at Austin

Georg Weissenbacher TU Wien

### Program Committee

Timos Antonopoulos Yale University Pranav Ashar Real Intent Clark Barrett Stanford University Per Bjesse Synopsys Inc. Supratik Chakraborty IIT Bombay Sylvain Conchon Universite Paris-Sud Vijay D'Silva Google Fei He Tsinghua University Alexander Ivrii IBM Dejan Jovanovic´ SRI International Ken McMillan Microsoft Alexander Nadel Intel Nina Narodytska VMware Research Peter Schrammel DiffBlue Anna Slobodova Centaur Technology Daryl Stewart ARM Christoph Sticksel The MathWorks Ofer Strichman Technion Yakir Vizel The Technion Georg Weissenbacher TU Wien

Erika Abraham RWTH Aachen University Jade Alglave University College London Armin Biere Johannes Kepler University Linz Roderick Bloem Graz University of Technology Gianpiero Cabodi Politecnico di Torino Rayna Dimitrova University of Sheffield Dino Distefano Facebook and University of London Grigory Fedyukovich Florida State University Alberto Griggio Fondazione Bruno Kessler Arie Gurfinkel University of Waterloo Liana Hadarean Amazon Web Services Ziyad Hanna Cadence Design System Warren A. Hunt, Jr. The University of Texas at Austin Ziv Nevo IBM Haifa Research Lab Corina Pas˘ areanu ˘ CMU/NASA Ames Research Center Giles Reger The University of Manchester Christoph Scholl University of Freiburg Natasha Sharygina Universita della Svizzera italiana (USI Lugano, Switzerland) ` Chao Wang University of Southern California

### Additional Reviewers

Asadi, Sepideh

Bella, Giampaolo Blicha, Martin Brotherston, James

Chen, Jianhui

Ebrahimi, Masoud

Fleury, Mathias Fraer, Ranan Fried, Dror

Gal, Anna Gal, Raviv Genest, Blaise Goel, Shilpi Gopinath, Divya Gupta, Ashutosh

Hadzic, Vedad Hjort, Hakan ˚ Hoereth, Stefan Hu, Qinheping Hyvarinen, Antti ¨

Jain, Himanshu Jain, Mitesh Judson, Samuel

Kaufmann, Daniela Kim, Hyondeuk King, Tim Kojevnikov, Arist Kremer, Gereon Kwan, Carl Konighofer, Bettina ¨ Malacaria, Pasquale Mann, Makai Marescotti, Matteo Moran, Shiri Mordvinov, Dmitry

Naraynaswami, Ramesh Noller, Yannic

Otoni, Rodrigo Ozdemir, Alex

Padon, Oded Palena, Marco Pasini, Paolo Pick, Lauren Prakash, Ravi

Ramanathan, Vivek Redondi, Gianluca

Sanyal, Amitabha Sosnovich, Adi Sumners, Rob

Temel, Mertcan Tiemeyer, Andreas Tsiskaridze, Nestan

Unadkat, Divyesh Usman, Muhammad

Vediramana Krishnan, Hari Govind Vendraminetto, Danilo

Wolfovitz, Guy Wu, Haoze

### Table of Contents

### Software Verification and Learning

#### Verification and Neural Networks

### SAT / SMT

### Anytime Algorithms for MaxSAT and Beyond

Alexander Nadel Intel Corporation, P.O. Box 1659, Haifa 31015 Israel Email<EMAIL_ADDRESS>
*Abstract*—Given a propositional formula F in Conjunctive Normal Form (CNF), a SAT solver decides whether it is satisfiable or not. It is often required to find a solution to a satisfiable CNF formula F, which optimizes a given Pseudo-Boolean objective function Ψ, that is, to extend SAT to optimization.

MaxSAT is a widely used extension of SAT to optimization. A MaxSAT solver can be applied to optimize a Pseudo-Boolean objective function Ψ, given a CNF formula F, whenever Ψ is a linear function.

MaxSAT has a diverse plethora of applications, including applications in computer-aided design, artificial intelligence, planning, scheduling and bioinformatics. A variety of approaches to MaxSAT have been developed over the last two decades. In this tutorial, we focus on anytime MaxSAT algorithms, where an anytime algorithm is expected to find better and better solutions, the longer it keeps running. The anytime property is crucial in industrial applications, since it allows the user to: *1*) get an approximate solution even for very difficult instances, and *2*) trade quality for performance by regulating the timeout.

Anytime MaxSAT solvers have been evaluated at yearly MaxSAT Evaluations since 2011 in the so-called incomplete tracks. We trace the evolvement of anytime MaxSAT algorithms over the last decade and lay out the algorithms, applied by the winners of MaxSAT Evaluation 2020.

Furthermore, we touch upon anytime algorithms for optimization problems beyond MaxSAT, such as bit-vector optimization and the problem of optimizing an arbitrary not-necessarily-linear function, given a CNF formula.

Finally, we discuss challenges and future work.

### Formal Verification for Natural and Engineered Biological Systems

Hillel Kugler *Faculty of Engineering, Bar-Ilan University* Ramat Gan, Israel<EMAIL_ADDRESS>
*Abstract*—Computational modeling is now used effectively to complement experimental work in biology, allowing to identify gaps in our understanding of the biological systems studied, and to predict system behavior based on a mechanistic model. We provide an overview of several areas in biology for which formal verification has been successfully used. We highlight examples from both natural and engineered biological systems. In natural biological systems the main goal is to understand how a system works and predict its behavior, whereas for engineered biological systems the main goal is to engineer biological systems for new purposes, e.g. for building biology-based computational devices. We compare between the challenges in applying formal verification in biology and the application to traditional domains. Finally, we outline future research directions and opportunities for formal verification experts to contribute to the field.

*Index Terms*—Formal Verification, Computational Systems Biology, DNA Computing, Biological Systems Modeling

#### I. INTRODUCTION

We provide an overview of the use of formal verification methods in biology and outline future research challenges and opportunities. We broadly divide applications of formal verification methods in biology to natural biological systems and engineered biological systems.

#### II. NATURAL BIOLOGICAL SYSTEMS

Biologists employ a wide range of experimental and theoretical approaches to decipher the mechanisms underlying the dynamic behavior of biological systems. Biological systems are the ultimate reactive system [4] as they need to constantly react to changes in their environment to maintain life. Viewing biological systems as reactive systems leads naturally to specifying their behavior using a subset of temporal logic [1], [2] and applying formal verification to prove system properties. An important class of computational models deals with the genotype/phenotype question - how does the genetic information in a cell or organism determine the dynamics and observable behavior. In particular, Gene Regulatory Networks (GRNs) capture the interactions between the genetic components of the system and define the system dynamics. Simulating GRN models allows us to study the network behavior under different experimental conditions including genetic mutations. Formal verification becomes useful since

The research was supported by the Horizon 2020 research and innovation programme for the Bio4Comp project under grant agreement number 732482 and by the ISRAEL SCIENCE FOUNDATION (grantNo. 190/19).

it is important to verify that known experimental results are indeed satisfied by the GRN models, and to identify behavior that may lead to new biological insights. In addition to using formal verification, synthesis methods [3], [7] can automate the process of deriving consistent models and offers a way to synthesize all solutions of a certain class and thus avoid the inherent bias in focusing on one model.

#### III. ENGINEERED BIOLOGICAL SYSTEMS

Engineering biological devices to perform specified computation is of major interest due to the potential of utilizing the inherent parallelism in biological components to speed computation, construct low energy consuming devices and interface with biological material. We focus on two main approaches of engineering such systems: DNA Strand Displacement Systems (DSD) [6] that utilize the complementarity of DNA sequences to bind together and perform designed reactions, and Network-Based Biocomputation (NBC) [5] that uses biological agents that operate in parallel to explore manufactured planar devices. We show computational design tools for these approaches and the use of formal verification methods and tools to improve the development process and ensure robust system design.

#### REFERENCES

### Tutorial on World-Level Model Checking

#### Armin Biere

Johannes Kepler University Linz, Altenbergerstr. 69, 4040 Linz, Austria

<EMAIL_ADDRESS>
*Abstract*—In SMT bit-vectors and thus word-level reasoning is common and widely used in industry. However, it took until 2019 that the hardware model checking competition started to use word-level benchmarks. Reasoning on the word-level opens up many possibilities for simplification and more powerful reasoning. In SMT we do see advantages due to operating on the wordlevel, even though, ultimately, bit-blasting and thus transforming the word-level problem into SAT is still the dominant and most important technique. For word-level model checking the situation is different. As the hardware model checking competition in 2019 has shown bit-level solvers are far superior (after bit-blasting the model through an SMT solver though). On the other hand wordlevel model checking shines for problems with memory modeled with arrays. In this tutorial we revisit the problem of word level model checking, also from a theoretical perspective, give an overview on classical and more recent approaches for word-level model checking and then discuss challenges and future work. The tutorial covered material from the following papers.

#### REFERENCES

### How testable is business software?

Peter Schrammel University of Sussex, Brighton, UK Diffblue Limited, Oxford, UK Email<EMAIL_ADDRESS>
*Abstract*—Most businesses rely on a significant stack of software to perform their daily operations. This software is business-critical as defects in this software have major impacts on revenue and customer satisfaction. The primary means for verification of this software is testing. We conducted a large-scale analysis of Java software packages to evaluate their testability. The results show that code in software repositories is typically split into portions of very trivial code, non-trivial code that is unit-testable, and code that cannot be unit-tested easily. This brings up interesting considerations regarding the use of test coverage metrics and design for testability, which is crucial for testing efficiency and effectiveness, but unfortunately too often an afterthought. Lack of testability is an obstacle to applying tools that perform automated verification and test generation. These tools cannot make up for poor testability of the code and have a hard time in succeeding or are not even applicable without first improving the design of the software system.

### From Correctness to High Quality

Orna Kupferman *School of Computer Science and Engineering The Hebrew University* Jerusalem, Israel

#### Abstract

In the synthesis problem, we are given a specification ψ over input and output signals, and we synthesize a system that realizes ψ: with every sequence of input signals, the system associates a sequence of output signals so that the generated computation satisfies ψ. The above classical formulation of the problem is Boolean. The talk surveys recent efforts to automatically synthesize reactive systems that are not only correct, but also of high quality. Indeed, designers would be willing to give up manual design only after being convinced that the automatic procedure that replaces it generates systems of comparable quality.

We distinguish between *behavioral quality*, which refers to the way the specification is satisfied, and *costs*, which refer to resources that the system consumes. For the first, we focus on the temporal logics LTL[F] and LTL[D], which extend LTL by quality operators [1]. The satisfaction value of LTL[F] and LTL[D] formulas is a real value in [0, 1], where the higher the value is, the higher is the quality in which the computation satisfies the specification. Essentially, LTL[F] contains *propositional quality operators*, like weighted-average, and LTL[D] contains *discounted eventuality operators*. Using LTL[F] and LTL[D], a designer can prioritize different ways to satisfy the specification and formally weight parameters such as security, maintainability, runtime, delays, and more.

For the second, we distinguish between four classes of costs, induced by the following two characteristics: (1) *construction* vs. *activaty* costs, and (2) *physical* vs. *monetary* costs. For example, the sensing cost of a system is physical, and we distinguish between the number of sensors in the system (construction cost) and the sensing required during its operation (activity cost) [2], [3].

#### Index Terms

Synthesis, Temporal Logic, Sensing

#### REFERENCES

Supported in part by the Israel Science Foundation, grant No. 2357/19.

### The FMCAD 2020 Student Forum

Peter Schrammel University of Sussex, Brighton, UK Diffblue Limited, Oxford, UK Email<EMAIL_ADDRESS>
*Abstract*—The Student Forum at the International Conference on Formal Methods in Computer-Aided Design (FMCAD) allows undergraduate and graduate students to introduce their research to the Formal Methods community and receive feedback. Originally planned to take place in Haifa, Israel, the event was actually run online via video conferencing. Eight students were invited to give a short talk and discuss their work with their peers and FMCAD attendees. The presentations covered a broad range of topics in the fields of verification and synthesis in various application areas.

The Student Forum gives an opportunity to students at any career stage to introduce their research to the audience of the FMCAD conference. The first edition took place in Portland, Oregon, USA in 2013 [6], with subsequent editions held in Lausanne, Switzerland in 2014 [5], Austin, Texas, USA in 2015 [7] and 2018 [4], Mountain View, CA, USA in 2016 [3], Vienna, Austria in 2017 [2], and San Jose, CA, USA in 2019 [1].

As in 2019, the 2020 Student Forum was open to graduate and undergraduate students.<sup>1</sup> The students were invited to submit 2-page reports describing their ongoing research in the scope of the FMCAD conference. Members of the program committee of FMCAD reviewed the reports and accepted eight submissions. The reviews evaluated the novelty of the work, its potential impact on the Formal Methods community, the quality and the soundness of the presentation.

The contributions covered a wide range of topics, from foundational aspects of automated reasoning to applications of Formal Methods to cloud security, neural networks and medicine. The following contributions have been accepted:

<sup>1</sup>https://fmcad.forsyte.at/FMCAD20/student-forum/

• Daniella Vo and Debashis Sahoo: *Boolean Analysis Reveals Microbes Significant to Inflammatory Bowel Disease*

The Student Forum would not have been possible without the excellent contributions of the student authors. We would also like to express our gratitude to the reviewers of the FMCAD Student Forum for their help.

#### REFERENCES

### Effective System Level Liveness Verification

Alexander Fedotov<sup>∗</sup> , Jeroen J.A. Keiren<sup>∗</sup> , Julien Schmaltz†

<sup>∗</sup>*Eindhoven University of Technology* Eindhoven, The Netherlands {a.fedotov<EMAIL_ADDRESS>† *ICT Group* Eindhoven, The Netherlands<EMAIL_ADDRESS>
*Abstract*—The language xMAS has been designed by Intel with the purpose of modelling and verification of hardware. Recently, the language was extended with finite state machines to make it more expressive [19]. Furthermore, it was shown how to prove liveness of such extended xMAS networks [19]. Unfortunately, we demonstrate that the proof technique is unsound. We provide an alternative approach which we have carefully proven to be correct. Moreover, we show that our approach scales very well, which makes it possible to prove liveness properties at the system level. In particular, we show that using our approach, it is possible to verify a power control architecture composed of 1299 state machines representing 50 power domains where each domain contains 5 master and 5 slave devices. Proving liveness of this system takes less than 10 minutes.

*Index Terms*—Formal verification, liveness, communication networks, finite state machines

#### I. INTRODUCTION

Formal verification has been successfully introduced in many design flows of hardware and software systems. More and more often, the sign-off decision for hardware blocks is taken solely on the results of formal proofs, the so-called *formal sign-off*. However, scaling formal verification to the system level remains a challenge.

Originally proposed by researchers at Intel, the xMAS language [7] and associated techniques for invariant generation [6], property checking [6], and deadlock hunting [12, 16]<sup>1</sup> have been developed to address this challenge. These techniques are very efficient and were extended to performance validation [15], asynchronous circuits [4], progress verification [8], generalized to language families [17], and directly related to the Register Transfer Level [11, 13, 14].

Regarding liveness analysis, the key contribution of Gotmanov *et al.* [12] is to encode the existence of a deadlock state as a satisfiability problem. This technique is sound and can prove the absence of deadlock states. It is incomplete because a satisfiable solution does not necessarily represent a reachable state of the xMAS network. Checking reachability of potential xMAS deadlock states is efficient [20].

Verbeek *et al.* introduced state machines into xMAS together with extensions of liveness analysis techniques [19].

<sup>1</sup>Note that in the literature related to liveness verification of xMAS networks, it is common to call states with non-live channels deadlock states. We adhere to this terminology, although it is different from the conventional notion of deadlock.

Their extension enables the modeling and analysis of complex cooperating state machines under the constraints imposed by micro-architectural choices. They demonstrated the verification of large systems consisting of nodes running cache coherence protocols and communicating via a Network-on-Chip. Inspired by Gotmanov *et al.*, Verbeek *et al.* encode liveness verification of xMAS extended with (finite) state machines to satisfiability. As we will show in this paper, their method is *unsound*.

We present a counter-example that is composed of a network with a deadlock that is not found by the technique of Verbeek *et al.* [19]. Subsequently, we propose an alternative encoding of liveness into a satisfiability problem. We carefully prove that if an xMAS network has a path to a state with a deadlock, there exists a satisfying assignment to the satisfiability problem we generate, i.e., our encoding is sound. Finally, we introduce two sets of benchmarks including a simplified power control architecture inspired by industrial case-studies.

The benchmarks and our implementation are publicly available [2]. A network with 1299 state machines can be proven live in less than 10 minutes.

We introduce xMAS, liveness of channels and idle and block equations in Section II. In Section III we introduce xMAS finite state machines, and show why the approach from [19] is unsound. Our approach using idle and block equations is described in Section IV. Our implementation is evaluated in Section V. We conclude in Section VI.

#### II. PRELIMINARIES

#### *A. xMAS syntax*

xMAS [7] is a graphical language aimed at modeling and verifying communication fabrics. An xMAS network comprises a set of primitives connected by typed channels. The progress of messages between primitives is controlled by a simple handshake protocol. Each channel consists of three signals, one for data and two boolean control signals, irdy and trdy. Consider the transfer of data from primitive A to primitive B via channel x. When primitive A is ready to transfer datum d through channel x, it sets x.data to d, and x.irdy to true, indicating the *initiator* is ready to transfer data. Whenever B is ready to accept data, it sets x.trdy to true, indicating the *target* is ready to receive. The data transfer happens if and only if x.irdy ∧ x.trdy, i.e., the initiator is

ready to send and the target is ready to receive. The core xMAS primitives are shown in Figure 1.

Figure 1: Core xMAS primitives

We provide detailed descriptions of the source, sink and queue primitives as they are used directly in this paper. For details of the other primitives the reader is referred to [7].

A source non-deterministically injects data into the network infinitely often. This is modelled using the unconstrained primary input oracle. Once a source decides to transfer datum d, it will keep trying until the transfer succeeds. This is modelled using the standard synchronous operator pre that returns the value of its argument in the previous clock cycle, and false in the very first cycle. Formally, the source is described as follows:

$$\begin{aligned} o.\mathbf{irdy} &:= \mathbf{oracle} \lor \mathbf{pre}(o.\mathbf{irdy} \land \neg o.\mathbf{trdy}) \\ o.\mathbf{data} &:= d.\end{aligned}$$

A sink consumes data from the network infinitely often:

i.trdy := oracle ∨ pre(i.trdy ∧ ¬i.irdy).

A queue is a FIFO buffer with k places. A queue is ready to write data to the output when it is not empty. The data the queue is ready to write is the head of the queue. A queue is ready to accept data when it is not full. Formally,

$$\begin{aligned} \boldsymbol{\rho}.\mathbf{irdy} &:= \neg \mathbf{is\\_empty}, & \boldsymbol{\rho}.\mathbf{data} &:= \mathbf{head}, \\ \boldsymbol{i}.\mathbf{trdy} &:= \neg \mathbf{is\\_full}, \end{aligned}$$

where i and o are the input and output channels of the queue respectively.

Example 1. Consider the simple xMAS network depicted in Figure 2. We use this network as a running example. The network consists of a source, a queue, and a sink. The source produces tokens t. The source controls the x.irdy and x.data signals of its output channel x. The queue controls the x.trdy signal of channel x, and y.irdy and y.data of its output

Figure 2: xMAS example

channel y. The sink controls the y.trdy signal of channel y. The signals are defined as follows.

$$\begin{aligned} \boldsymbol{x}.\texttt{irdy} &:= \texttt{oracle}\_{src} \vee \texttt{pre}(\boldsymbol{x}.\texttt{irdy} \wedge \neg \boldsymbol{x}.\texttt{try}) \\ \boldsymbol{x}.\texttt{data} &:= \boldsymbol{t} \\ \boldsymbol{x}.\texttt{trdy} &:= \neg \texttt{is}\_{\texttt{full}} \\ \boldsymbol{y}.\texttt{irdy} &:= \neg \texttt{is}\_{\texttt{empty}} \\ \boldsymbol{y}.\texttt{data} &:= \texttt{head} \\ \boldsymbol{y}.\texttt{trdy} &:= \texttt{oracle}\_{snk} \vee \texttt{pre}(\boldsymbol{y}.\texttt{try} \wedge \neg \boldsymbol{y}.\texttt{irdy}). \end{aligned}$$

The semantics of an xMAS network consists of a combinatorial and a sequential phase. In the first, all data, irdy and trdy signals are updated. In the second all components with state update their state. The global state of an xMAS network is the product of the local states of all components. We write ~s <sup>X</sup> −→ s~<sup>0</sup> for the transition between global states ~s and s~<sup>0</sup> , where X is a set of (channel,data) pairs representing the simultaneous data transfers in the current clock cycle.

#### *B. Liveness of channels*

Liveness of channels is defined using linear temporal logic (LTL). LTL and its semantics are considered standard, and we refer to text books such as [3] for the details. To interpret LTL on xMAS networks, we first define paths and maximal paths in such networks. In the rest of this paper, we implicitly fix an xMAS network N = (P, G), where P is the set of primitives, and G is the set of channels. Given a channel x ∈ G, by C(x) we denote the set of all possible values of x.data. By C we denote the set of all data of N, that is C = S <sup>x</sup>∈<sup>G</sup> C(x).

Definition 1. A *path* is a possibly infinite sequence of global states π = ~s0, ~s1, ~s2, . . . such that for all j > 0, ~sj−<sup>1</sup> X −→ ~s<sup>j</sup> for some X. The set of paths starting in a state ~s is denoted using Paths(~s), and for xMAS network N we write Paths(N) to denote Paths(~s0), where ~s<sup>0</sup> is the initial state of the network N. For finite paths π = ~s0, . . . , ~s<sup>n</sup> we define last(π) = ~sn. A path π is called *maximal* if and only if it is infinite, or it is finite and last(π) has no outgoing transitions.

A channel is *live* whenever, always when its initiator is ready to transfer data, the transfer will eventually be successful.

Definition 2 ([12]<sup>2</sup> ). Channel x ∈ G is *live* for d ∈ C(x) iff

$$\begin{aligned} N &= \mathsf{G}((x.\mathsf{irdy} \wedge x.\mathsf{data} = d) \\ &\implies \mathsf{F}(x.\mathsf{irdy} \wedge x.\mathsf{try} \wedge x.\mathsf{data} = d)). \end{aligned}$$

We henceforth make the (standard) assumption that channels are (forward) persistent. This means that whenever the initiator is ready to send d along x, it will remain ready to do so until the transfer is successful. Formally, the network satisfies G((x.irdy ∧ x.data = d ∧ ¬x.trdy) =⇒ X(x.irdy ∧ x.data = d)). Under this assumption, channel x is live if and only if it is live for all d ∈ C(x).

<sup>2</sup>Gotmanov et al. [12] use property G(x.irdy =⇒ F x.trdy), which does not guarantee that the transfer eventually succeeds if persistency is not assumed.

We recall the notions *idle* and *block* from [12]. A channel is *idle* for d if eventually the initiator will never send message d along that channel, and it is *blocked* if eventually the target will never be able to receive a message along that channel.

Definition 3 ([12]). Let x ∈ G and d ∈ C(x). We define

$$\begin{aligned} \mathbf{idle}(x(d)) &:= \mathsf{FG}(\neg x.\mathbf{irdy} \lor x.\mathbf{data} \neq d) \\ \mathbf{block}(x) &:= \mathsf{FG}\neg x.\mathbf{trdy} \end{aligned}$$

A local deadlock is defined as a *dead* channel, where a channel is dead for value d if and only if it is not live for d. This means there exists a path in the xMAS network to a state that satisfies ¬idle(x(d)) ∧ block(x). In other words, a channel is dead whenever its initiator is ready to transfer datum d and its target will never be ready to accept the data.

Definition 4. Let N be an xMAS network, with x a forward persistent channel in N, and d ∈ C(x). We define

$$\begin{aligned} \mathsf{live}(x(d)) &:= \mathsf{idle}(x(d)) \lor \neg \mathsf{block}(x) \\ \mathsf{dead}(x(d)) &:= \neg \mathsf{live}(x(d)) \\ \mathsf{live}(x) &:= \bigwedge\_{d \in C(x)} \mathsf{live}(x(d)) \\ \mathsf{dead}(x) &:= \bigvee\_{d \in C(x)} \mathsf{dead}(x(d)) \end{aligned}$$

Persistency now allows us to simplify the definition of liveness using the following theorem adapted from [12].

#### Theorem 1.

Note that the formula for *live* channels is evaluated over the *network* (i.e., over *all* paths), and the formula for *dead* channels is evaluated over a *path* due to the LTL semantics.

In Definition 3, we only defined block(x). We can refine this definition by introducing block(x(d)) as follows.

$$\mathbf{block}(x(d)) := \mathsf{FG}(\neg x.\mathbf{trdy} \lor x.\mathbf{data} \neq d)$$

It is easy to see that block(x) implies block(x(d)) for any d ∈ C(x). The following then follows immediately.

Lemma 1. *For all persistent channels* x ∈ G*,* d ∈ C(x)*, and all paths* π ∈ Paths(N)*,* π |= dead(x(d)) *implies* π |= V <sup>e</sup>∈C(x) block(x(e))*.*

#### *C. Idle and block equations*

The main contribution of Gotmanov *et al.* [12] is to express deadlock conditions for each primitive using equations over boolean variables. If these *idle and block equations* are satisfiable, a (possible) deadlock has been detected; otherwise, the network is guaranteed to be deadlock free. The method is sound but incomplete: if the equations are satisfiable, the assignment to the boolean variables may constitute an unreachable deadlock state. This is alleviated to some extent by using invariants to approximate the reachable states.

The boolean variables express the conditions under which a primitive will eventually never try to output value d, denoted using variable idle<sup>d</sup> x , or eventually never try to read from channel x, denoted using variable blockx. The encoding essentially approximates the LTL specifications of idle and block defined before. In particular, if there exists a path π in the xMAS network such that π |= dead(x(d)), then there is a satisfying assignment to the variables in the idle and block equations in which idle<sup>d</sup> x is *false*, and block<sup>x</sup> is *true*.

Example 2. Recall the network from Example 1. Sources are never idle, and sinks are never blocked. The input channel of the queue, x, is blocked when the queue is full and its output channel y is blocked. The output channel of the queue is idle when the queue is empty and its incoming channel x is idle. This results in the following equations.

$$\begin{aligned} \mathsf{idle}\_x &\equiv \bot & \mathsf{block}\_x &\equiv \mathsf{full} \wedge \mathsf{block}\_y\\ \mathsf{idle}\_y &\equiv \mathsf{empty} \wedge \mathsf{idle}\_x & \mathsf{block}\_y &\equiv \bot \\ \mathsf{dead}\_x &\equiv \neg \mathsf{idle}\_x \vee \mathsf{block}\_x &\quad \mathsf{dead}\_y &\equiv \neg \mathsf{idle}\_y \vee \mathsf{block}\_y \end{aligned}$$

We can conclude that neither x nor y is dead.

III. LIFE AND DEATH OF STATE MACHINES IN XMAS

#### *A. xMAS finite state machines*

Verbeek *et al.* describe an extension of xMAS with finite state machines for the integrated verification of, for instance, cache coherence protocols together with their underlying communication fabric [18, 19]. The xMAS automata allow for the symbolic description of the channels and data read and written along transitions. However, every transition reads and writes (at most) one channel. In this paper we require explicit definition of every datum read/written on a transition to simplify the presentation. The results could equally be expressed using symbolic notation as in [18, 19]. However, since the number of channels and the data transferred are typically assumed to be finite, they can be expanded in the FSM, and this change does not alter the expressive power.

Definition 5. A *finite state machine (FSM)* is a tuple (S, s0, I, O, T), where S is a finite set of states; s<sup>0</sup> ∈ S is an initial state; I is a finite set of input channels; O is a finite set of output channels; and T ⊆ S × (I × C) × (O × C) × S is the total transition relation.

Since T is total, every state has at least one outgoing transition. We use names s, s<sup>0</sup> , s1, . . . for states. We write s x(d)/y(e) −−−−−−→ s 0 for (s,(x, d),(y, e), s<sup>0</sup> ) ∈ T. We sometimes write ?x(d) and !y(e) to stress d is read from channel x, and e is written to y. For state s ∈ S, in(s) and out(s) denote the sets of incoming and outgoing transitions of s, respectively. Likewise, for channels x ∈ (I ∪ O), and data d ∈ C(x), read(x, d) and write(x, d) represent the sets of transitions reading d from x and writing d to x, respectively.

Note that the requirement that every transition reads from and writes to exactly one channel is not fundamental. Transitions t = s !y(e) −−−→ s 0 that do not read from an input channel can be modeled by introducing a new channel x<sup>t</sup> that is connected to a source and the FSM, and be replaced by s ?xt/!y(e) −−−−−−→ s 0 . Transitions that do not write to an output channel and transitions that do not read or write any channel can be modeled in a similar way.

In an FSM, exactly one state is current at a time, this state is denoted cur (s). A transition s x(d)/y(e) −−−−−−→ s 0 is enabled if and only if s is the current state, the input channel x is ready to send d, and the output channel y is ready to receive. Note that whether the input and output channels are ready depends on the environment of the FSM.

Definition 6. Given FSM (S, s0, I, O, T), transition s x(d)/y(e) −−−−−−→s <sup>0</sup> ∈ T is enabled, denoted enabled(s x(d)/y(e) −−−−−−→ s 0 ) iff cur (s) ∧ x.irdy ∧ x.data = d ∧ y.trdy.

In any state, there can be multiple enabled transitions. To resolve this non-determinism, a scheduler sel is introduced that, at every clock cycle, selects an enabled transition. If transition t is selected, this is denoted sel = t.

The FSM needs to indicate to its environment whether it is ready to send along an outgoing channel, or to read along an incoming channel. This is defined in terms of irdy, trdy and data as follows.

Definition 7. Given FSM (S, s0, I, O, T), for x ∈ I, y ∈ O: x.trdy := ∃s x(d)/y(e) −−−−−−→s <sup>0</sup> ∈ T.sel = s x(d)/y(e) −−−−−−→s 0 y.irdy := ∃s x(d)/y(e) −−−−−−→ s <sup>0</sup> ∈ T.sel = s x(d)/y(e) −−−−−−→ s 0 y.data := ( e if ∃s x(d)/y(e) −−−−−−→ s <sup>0</sup> ∈ T.sel = s x(d)/y(e) −−−−−−→ s 0 ⊥ otherwise

Since the scheduler non-deterministically chooses between enabled transitions, and irdy is only set for the output channel of a selected transition, whenever irdy is set for an output channel of an FSM, the target of that channel is ready to receive, i.e., trdy is set. Non-determinism of the scheduler could lead to an enabled transition being ignored for an infinite amount of time. However, we assume scheduler sel to be fair, i.e., if state s is visited infinitely often with s x(d)/y(e) −−−−−−→ s 0 enabled, then s x(d)/y(e) −−−−−−→ s <sup>0</sup> will be selected infinitely often. We therefore only verify liveness of the xMAS network along fair paths. Such paths are defined as follows.

Definition 8. Given a path π, we say that π is fair if and only if for all FSM primitives M = (S<sup>M</sup>, s<sup>m</sup> 0 , I<sup>M</sup>, O<sup>M</sup>, T <sup>M</sup>) and local transitions t ∈ T <sup>M</sup>, we have π |= (GFenabled(t)) =⇒ (GFsel = t)

#### *B. Idle and block equations by Verbeek* et al.

Verbeek *et al.* define a SAT encoding using idle and block equations for xMAS automata as follows. Given M = (S, s0, I, O, T), for s x(d)/y(e) −−−−−−→ s <sup>0</sup> ∈ T, x ∈ I, y ∈ O, d ∈ C(x), e ∈ C(y), they define the following.

$$\begin{aligned} \mathsf{dead}\_s \underline{\mathop{\rm ad}}\_{s} \underline{\mathop{\rm id}}\_{s'} &\equiv \mathsf{id} \mathsf{id} \mathsf{e}\_x^d \vee \mathsf{block}\_y\\ \mathsf{dead}\_s &\equiv \mathsf{c}ur\_s \wedge \bigwedge\_{t \in \mathsf{out}(s)} \mathsf{dead}\_t\\ \mathsf{dead}\_M &\equiv \bigvee\_{s \in S} \mathsf{dead}\_s\\ \mathsf{block}\_x^d &\equiv \mathsf{dead}\_M \vee (\mathsf{read}(x, d) = \emptyset)\\ \mathsf{id} \mathsf{le}\_y^e &\equiv \mathsf{dead}\_M \vee (\mathsf{write}(y, e) = \emptyset) \end{aligned}$$

Here, cur <sup>s</sup> are boolean variables, aimed at reflecting the current state of the FSM.

Intuitively, Verbeek *et al.* propose to encode that input (output) channels of an FSM are blocked (idle) as follows. An input channel x is blocked for d if either the FSM has no transition which reads d from x or the FSM is dead. Likewise, an output channel y is idle for e if either the FSM has no transition which writes e to y or the FSM is dead. With the notion of dead FSM, Verbeek *et al.* intend to encode the existence of a state (a dead state, using the terminology of the authors), which can eventually be reached, and at the same time cannot be left anymore, since all outgoing transitions are dead. In such a situation, the FSM can neither read from its inputs nor write to its outputs.

#### *C. Life and death of state machines: a counter-example*

Unfortunately, there are xMAS networks with FSMs that are deadlock free according to these idle and block equations that do contain a deadlock. This is illustrated by the following example.

Example 3. Consider the state machine, depicted in Figure 3. It has two input channels x and y, connected to sources, and two output channels o and z, connected to sinks. All channels only transfer datum d. Initially, in s0, the FSM can either read d from channel x and produce d on channel o, and stay in s0, or it can read d from y *once* and produce d on z, and go to s1. In s1, the FSM never reads from y nor writes to o, and only reads from x, writes to z, and stays in s1.

According to the definition by Verbeek *et al.*, the FSM is not *dead*: channels o and z are not blocked, and since channel x is not idle, neither of the self-loops is dead. Consequently, neither s<sup>0</sup> nor s<sup>1</sup> is dead, and the FSM is not dead. However, once s<sup>1</sup> is reached, messages waiting on channel y will never be read, so y should be blocked.

Figure 3: Counterexample to method by Verbeek et al.

The example shows that, although channel y is dead for d, since block<sup>d</sup> y is false, this is not detected using the idle and block equations. The encoding from [19] is therefore unsound.

Generally, the issue lies in the definition of deadM. Even when none of the input channels are idle, and no output channel is blocked, a state machine can block an input channel. This happens, *e.g.*, when source states of transitions reading from a particular channel are reached only *finitely many times*. Output channels can become idle for similar reasons.

#### IV. IDLE AND BLOCK EQUATIONS FOR XMAS FSMS

We propose alternative idle and block equations for FSMs in the spirit of [12]. An input channel x of an FSM is dead, when eventually all transitions reading x become disabled. There are two possible causes for this. First, the source state of the transition can eventually never be reached anymore. Second, whenever the source state of the transition is current, the environment disables the transition since the output channel is blocked. We capture this intuition by saying that states that are eventually never reached again are idle, and transitions that are eventually never enabled are dead.

Definition 9 (Idle states and dead transitions). Consider FSM (S, s0, I, O, T). For s ∈ S and t ∈ T we define the following.

$$\begin{aligned} \mathsf{idle}(s) &:= \mathsf{FG} \neg cur(s) \\ \mathsf{dead}(t) &:= \mathsf{FG} \neg enabled(t) \end{aligned}$$

Formally, transitions eventually never become enabled along a path if and only if either the source state or the input channel of the transition is idle, or the output channel is blocked.

Lemma 2. *Let* M = (S, s0, I, O, T) *be an FSM in* N*. For all* t = s x(d)/y(e) −−−−−−→ s <sup>0</sup> ∈ T*, global states* ~s*, and paths* π ∈ Paths(~s)*,*

$$\pi \vdash \mathsf{FG} \neg enabled(t) \; \mathsf{i}\mathcal{f}\,\pi \vdash \mathsf{i}\mathbf{d}\mathbf{l}\mathbf{e}(s) \lor \mathsf{i}\mathbf{d}\mathbf{l}\mathbf{e}(x(d)) \lor \mathsf{l}\mathbf{l}\mathbf{o}\mathbf{c}\mathbf{k}(y).$$

*Proof sketch (for the full proof see [10]).* Fix an arbitrary transition t = s x(d)/y(e) −−−−−−→ s 0 , global state ~s, and path π ∈ Paths(~s). We prove both directions separately.

Due to the way the semantics of FSMs resolve nondeterminism, output channels of an FSM are never dead.

Lemma 3. *Given FSM* (S, s0, I, O, T) *in* N*, for all global states* ~s *and for channels* y ∈ O *and* e ∈ C(y)*, we have for all paths* π ∈ Paths(~s)*,* π 6|= dead(y(e))*.*

We now specify the idle and block equations for FSMs used in a SAT encoding. The equations refer to variables idle of incoming channels and block of outgoing channels that are defined in other components.

Definition 10 (Idle and block equations for FSMs). Consider an FSM M = (S, s0, I, O, T). For s ∈ S, x ∈ I, y ∈ O, d ∈ C(x), e ∈ C(y), and s x(d)/y(e) −−−−−−→ s <sup>0</sup> ∈ T we define the following equations.

$$\begin{aligned} \mathbf{dead}\_s \frac{\mathbf{z}^{(d)/\mathbf{y}(e)} \rhd}{\mathbf{idle}\_s \equiv \negcurlyeq\_{\operatorname{cder}\_s} \land \bigwedge\_{t \in \operatorname{in}(s)} \mathbf{dead}\_t} \\ \mathbf{idle}\_s \equiv \negcurlyeq\_{\operatorname{cder}\_s} \land \bigwedge\_{t \in \operatorname{in}(s)} \mathbf{dead}\_t \\ \mathbf{block}\_x^d \equiv \bigwedge\_{t \in \operatorname{read}(x,d)} \mathbf{dead}\_t \\ \mathbf{block}\_x \equiv \bigwedge\_{d \in C(x)} \mathbf{block}\_x^d \\ \mathbf{idle}\_y^e \equiv \bigwedge\_{t \in \operatorname{write}(y,e)} \mathbf{dead}\_t \\ \mathbf{idle}\_y \equiv \bigwedge\_{e \in C(y)} \mathbf{idle}\_y^e \end{aligned}$$

SAT(M) consists of the conjunction of all the idle and block equations for all states, transitions and channels in FSM M. Similarly we write SAT(N) for network N, which is the conjunction of all formulas for all the primitives of N, where for non-FSM components, the encoding from [12] is used.

We additionally use the invariants from [19] to reduce the number of false deadlocks. For example, P s∈S cur <sup>s</sup> = 1 dictates that the FSM is always in exactly one state.

The intuition behind the encoding is as follows. If a state is not current, and eventually none of its incoming transitions can ever become enabled, the state is effectively unreachable, thus the state is idle. In turn, a transition is dead if it ultimately never becomes enabled. This is the case if either its source state or its incoming channel is idle, or its outgoing channel is blocked. An input channel is blocked for a given datum if no transition will read that datum from the channel. Likewise an output channel is idle for a datum if that datum is never written to it. An output channel is idle if it is idle for all values, meaning that no value will ever be written to it. An input channel is blocked if it is blocked for all values. This follows from Lemma 1: a dead channel is blocked for all data.

We say assignment σ is *consistent* with path π and a set of components if for all input channels x, output channels y and data e of these components, σ(blockx) = > iff π |= block(x) and σ(idle<sup>e</sup> y ) = > iff π |= idle(y(e)).

We finally prove our idle and block equations are sound: if there is a channel that is dead for a particular value, then there is a satisfying assignment to the boolean equations showing this. We only consider input channels of FSMs, since output channels of FSMs cannot be dead as shown in Lemma 3.

Recall that a maximal path can either be finite or infinite, and in an infinite path in an xMAS network, the FSM can be stuck in a state locally. We construct assignments for each of these cases, and prove that each of the assignments is a satisfying assignment. We first construct assignment σ<sup>s</sup> for the case where a (fair) maximal path in a network containing the FSM is such that the FSM is stuck locally in state s.

Definition 11. Let M = (S, s0, I, O, T) be an FSM that appears in an xMAS network N, π ∈ Paths(M) and s ∈ S. Assignment σ<sup>s</sup> is defined as follows, where we write v := w if σ<sup>s</sup> assigns w to v. For states s <sup>0</sup> ∈ S, transitions t ∈ T, channels x ∈ I, y ∈ O, and d ∈ C(x), e ∈ C(y), let:

$$\begin{array}{c} \mathit{curr}\_{s'} := s = s' \\ \mathsf{block}\_{x}^{d} := \top \\ \mathsf{id}\mathbf{e}\_{y}^{d} := \top \end{array} \qquad \begin{array}{c} \mathsf{id}\mathbf{e}\_{s'} := s \neq s' \\ \mathsf{block}\_{x} := \top \\ \mathsf{id}\mathbf{e}\_{y} := \top \end{array} \qquad \begin{array}{c} \mathsf{d}\mathbf{e} \mathbf{a}\_{t} := \top \\ \mathsf{block}\_{y} := \top \\ \mathsf{id}\mathbf{e}\_{x}^{d} := \bot \end{array}$$

and σ<sup>s</sup> is consistent with π for all components other than M.

Whenever the FSM is stuck locally, σ<sup>s</sup> gives a satisfying assignment for the encoding to SAT.

Lemma 4. *Let* M = (S, s0, I, O, T) *be an FSM that appears in an xMAS network* N *and* s ∈ S*. If* π ∈ Paths(N) *is a* fair maximal path *such that either*

*then* σ<sup>s</sup> *is a satisfying assignment for* SAT(N)*.*

The proof of this lemma and Lemma 5 are omitted due to space restrictions. Details can be found in [10].

For a fair maximal path π on which the FSM is not stuck locally, we construct a satisfying assignment σ<sup>π</sup> based on π.

Definition 12. Let M = (S, s0, I, O, T) be an FSM that appears in an xMAS network N and π ∈ Paths(N). Assignment σ<sup>π</sup> is defined as follows. For states s <sup>0</sup> ∈ S, transitions t ∈ T, channels x ∈ I, y ∈ O, and d ∈ C(x), e ∈ C(y), let:

$$\begin{aligned} cur\_{s'} &:= s = s' \\ \mathsf{idle}\_{s'} &:= \forall 0 \le k \le n.\pi[i+k] \vdash \neg curv(s') \\ \mathsf{dead}\_{t} &:= \forall 0 \le k \le n.\pi[i+k] \vdash \neg enabled(t) \\ \mathsf{block}\_{x}^{d} &:= \forall t \in read(x,d).\forall 0 \le k \le n. \\ &\qquad \pi[i+k] \vdash \neg enabled(t) \\ \mathsf{block}\_{x} &:= \forall d \in C(x).\forall t \in read(x,d).\forall 0 \le k \le n. \\ &\qquad \pi[i+k] \vdash \neg enabled(t) \\ \mathsf{idle}\_{y}^{d} &:= \forall t \in write(y,e).\forall 0 \le k \le n. \\ &\qquad \pi[i+k] \vdash \neg enabled(t) \\ \mathsf{idle}\_{y} &:= \forall e \in C(y).\forall t \in write(y,e).\forall 0 \le k \le n. \\ &\qquad \pi[i+k] \vdash \neg enabled(t) \end{aligned}$$

and σ<sup>π</sup> is consistent with π for all components other than M.

Whenever the FSM is not stuck locally, σ<sup>π</sup> gives a satisfying assignment for the encoding to SAT.

Lemma 5. *Let* M = (S, s0, I, O, T) *be an FSM that appears in an xMAS network* N*. If* π ∈ Paths(N) *is an* infinite fair maximal paths *such that for all* s ∈ S*,* π |= GF cur (s) =⇒ W t∈out(s) enabled(t) *, the assignment* σ<sup>π</sup> *is a satisfying assignment for* SAT(N)*.*

We finally prove soundness of our encoding, assuming that idle and block equations for non-FSM components are sound.

Theorem 2. *Let* M = (S, s0, I, O, T) *be an FSM in xMAS network* N*. For all channels* x ∈ I *and data* d ∈ C(x)*, if there exists a fair maximal path* π ∈ Paths(N) *such that* π |= dead(x(d))*, then* SAT(N) ∧ ¬idle<sup>d</sup> <sup>x</sup> ∧ block<sup>x</sup> *is satisfiable.*

*Proof.* Fix arbitrary channel x ∈ I, and datum d ∈ C(x), and let π ∈ Paths(N) be a fair maximal path such that π |= dead(x(d)). We distinguish three cases:

According to Lemma 5, σ<sup>π</sup> is consistent with SAT(N). Note that since π |= dead(x(d)), π |= block(x(e)) for all e ∈ C(x), according to Lemma 1. Consider arbitrary e ∈ C(x), we show that the assignment satisfies block<sup>e</sup> x . From this and the definition it immediately follows that it satisfies blockx.

Let i be the index that signals the start of the loop of the lasso on π. Since π |= block(x(e)), π |= FG(¬x.trdy∨ x.data 6= e). By definition of enabled, this implies π |= FG(¬enabled(t)) for all t ∈ read(x, e). Hence, for all 0 ≤ k ≤ n, π[i+k] |= ¬enabled(t) for all t ∈ read(x, e). By definition of σπ, we then have block<sup>e</sup> <sup>x</sup> = >. Since this holds for all e, by definition also block<sup>x</sup> = >, and σ<sup>π</sup> is a satisfying assignment for SAT(N) ∧ ¬idle<sup>d</sup> <sup>x</sup> ∧ blockx.

We illustrate our approach using an example.

Example 4. Recall the FSM from Example 3. The environment guarantees idle<sup>x</sup> = idle<sup>y</sup> = block<sup>o</sup> = block<sup>z</sup> = ⊥.  This is witnessed by the following satisfying assignment for these equations, that also satisfies block<sup>y</sup> = >, and thus ¬idle<sup>y</sup> ∧ blocky.

$$\begin{array}{c} \mathit{curr}\_{s\_0} := \bot & \mathit{curr}\_{s\_1} := \top \\ \mathit{idle}\_{s\_0} := \top & \mathit{idle}\_{s\_1} := \bot \\ \mathsf{dead}\_{s\_0} \xrightarrow{x/s}\_{s\_1} := \top & \mathsf{dead}\_{s\_0} \xrightarrow{y/z}\_{s\_1} := \top \\ \mathsf{dead}\_{s\_1} \xrightarrow{x/z}\_{s\_1} := \bot \\ \mathsf{block}\_{s} := \bot & \mathsf{block}\_{s} := \top \\ \mathsf{idle}\_{o} := \top & \mathsf{idle}\_{z} := \bot \end{array}$$

#### V. EXPERIMENTS

We have implemented the idle and block equations described in Section IV. Given an xMAS model as input, our tool automatically generates a SAT problem that incorporates the idle and block equations [2]. The SAT problem is solved using Z3 [9] to verify liveness. Our tool can also generate an SMV model that encodes the xMAS network and its behaviour. This model uses idle and block equations as invariants. Reachability of a state in which a channel of the given xMAS model is checked using the NUXMV model-checker [5].

#### *A. Experimental setup*

We evaluate our implementation using two sets of models: one inspired by "go/no go" testing, the other inspired by power domains architectures. All models also have a version in which deadlocks have been introduced. A detailed description of the models can be found in [1].

*Go/no go models* are balanced binary trees of go/no go blocks. Each block has two binary inputs and one binary output, and consists of a pair of interconnected FSMs. The output of the block is ok if the data consumed from both input channels are ok, and it is nok otherwise.

 The output channels of two adjacent blocks on one level are used as input channels of a block on the next level in the tree.

Go/no go models with deadlocks are obtained by modifying one FSM in a go/no go block whose inputs are not connected to another block as follows. We add a new state with a selfloop reading ok from the first input channel i. We add a transition that reads nok from i from the initial state of the FSM to this new state. The new state is reachable, channel i is blocked for nok, and all output channels are idle.

*Power domains* are used to improve power efficiency of systems on chip. A power control architecture turns power domains on and off depending on the needs of an application. We model a dynamic power management policy that is an abstraction of industrial practice.

Our models consist of a number of power domains, each of which has a domain power controller. If the model has multiple power domains it also has a top power controller. Every power domain contains a number of device-controller pairs. In Figure 4a, we depict a device controller, which turns on its device (depicted in Figure 4b) if the device indicates activity (generated by the FSM depicted in Figure 4c). If a device shows no activity, its device controller requests to turn off the device, and the device can non-deterministically accept the request or decline it. A domain power controller powers on the domain when one of the devices in the domain shows activity. It powers off the domain when all device controllers in the power domain indicate their devices are turned off. The top power controller powers on if one of the domain power controllers indicates it needs power. It powers off if all domain power controllers indicate that all devices are turned off.

To obtain power domain models with a deadlock, one of the device controller FSMs is changed such that in its off state it expects to read act(0 ), and in its on state, it expects to read act(1 ), which leads to synchronisation issues and deadlocks.

All experiments were executed on a MacBook Pro 2015, 2,7GHz Intel Core i5, 16Gb RAM, running MacOS Catalina 10.15.4. For SAT solving, we use the Z3 solver, version 4.8.0 64-bit [9]. For reachability checks, we use NUXMV, version 2.0.0 64-bit [5]. Instructions to reproduce the experiments and the script used to obtain our results are available at [1].

#### *B. Results*

Table I: Experimental results

The times required for the experiments are reported in Table I. The *Model* column indicates the model that is evaluated. For go/no go models, the number in the name signifies the number of blocks. For power domain models, the first and second number in the name denote the number of power domains and device-controller pairs in every domain, respectively. *#FSMs* reports the number of FSMs in the model. In the *Live* column, ✓ indicates that the model is deadlock free, ✗ indicates it is not. For each instance, we list the result

Figure 4: Some of the power domain FSMs

Figure 5: Number of FSMs vs time for all experiments.

reported by the tool (*Res.*), where ✓ and ✗ represent absence and presence of deadlocks, respectively. Running time for each instance is reported in seconds.

For both sets of models, SAT and reachability correctly report absence and existence of deadlocks in all models. The largest go/no go models contain 126 FSMs. Liveness of the largest deadlock free go/no go model is proven using SAT in 7 seconds. Reachability analysis takes 1 minute 32 seconds for the same go/no go model. For the largest go/no go model with a deadlock, a deadlock is reported using SAT in 6 seconds. Using reachability it can be proven that a deadlock state is reachable in 3 minutes 41 seconds. As for the power domain experimental set, the largest models (both with and without deadlock) contain 1299 FSMs. For the largest model without a deadlock, SAT proves liveness in 9 minutes and 2 seconds. Analysis of the largest power domain model with a deadlock takes 8 minutes and 1 second using SAT. Reachability analysis for the power domain models with numbers of power domains larger than 30 was not possible in our case. This was caused by NUXMV exceeding the maximum allowed stack on MacOS.

#### *C. Discussion*

The results show that using our technique we can prove liveness of large xMAS models with FSMs. We plot the performance results on both sets of models in Figure 5. Note that we use the log-scale for the y-axis. In addition, we use deciseconds instead of seconds in order to avoid values less than 1 for the y-axis. The results show that both methods scale exponentially in the number of FSMs. However, using SAT for liveness verification significantly outperforms reachability for xMAS extended with FSMs. This is in line with our expectations, and aligns with results for standard xMAS [12].

Although we do not encounter false deadlocks in our experiments, the fact that our method is incomplete implies that finding false deadlocks using SAT is possible. If SAT reports a deadlock, it is not known if the deadlock is reachable or not. In that case, reachability analysis is necessary.

#### VI. CONCLUSIONS

We demonstrated that the approach to verify liveness of xMAS networks with FSMs proposed by Verbeek *et al.* [19] is unsound. We proposed new idle and block equations for xMAS networks containing FSMs, and proved their soundness. Our experimental evaluation shows that deadlock detection using satisfiability outperforms reachability analysis using symbolic model checking in NUXMV. In case deadlocks are found, the latter can, however, verify their reachability reasonably efficiently. Although our method is incomplete, this was not observed during the experiments.

As future work, we plan to investigate ways to make the method complete. In particular, an alternative encoding to SAT based on bounded model checking, could make the method complete provided an appropriate bound can be derived. Additionally, the FSMs presented in this paper always read from and write to exactly one channel. This restriction could be relaxed to read and write multiple channels on a single transition to enable more compact modeling of some FSMs.

#### REFERENCES

### Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration

Rohit Dureja<sup>∗</sup> , Jason Baumgartner† , Robert Kanzelman† , Mark Williams† and Kristin Y. Rozier<sup>∗</sup> <sup>∗</sup>Iowa State University, † IBM Corporation

*Abstract*—Industrial hardware verification tasks often require checking a large number of properties within a testbench. Verification tools often utilize parallelism in their solving orchestration 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 walltime, 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 highaffinity properties to minimize redundant work of applying identical strategies on individual properties with nearly-identical logic cones. In this paper, 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 a median 2.4 speedup yielding 18.1% more property solves, as demonstrated by extensive experiments.

#### I. INTRODUCTION

Practical hardware and software verification often mandates checking a large number of properties on a given design. For example, *functional verification* involves checking a suite of low-level assertions and higher-level encompassing properties. *Equivalence checking* compares pairwise equality of each output across two designs, yielding a distinct property per output. *Redundancy removal* requires proving many gate-equalities throughout a design, each comprising a distinct property. Redundancy removal is the core procedure of equivalence checking, and is widely-used to boost verification scalability.

Each property has a distinct minimal *cone of influence* (COI), or fan-in logic of the signals referenced in the property. Verification of a group of properties requires resources proportional to the collective COI size, which is often exponential (after lighter logic reductions). Each property adds distinct logic to the group's collective COI; *affinity* refers to the degree of common vs. distinct logic in the COI. *Atomic verification*<sup>1</sup> of a group of low-affinity properties is

Fig. 1. Parallel verification: property partitioning vs. strategy exploration.

thus often significantly slower than solving them one-at-atime. Conversely, atomic verification of a high-affinity group saves considerable verification resource, as the effort expended for one property can benefit the others without significantly slowing them down [1, 2]. Parallel verification resource can be optimized to leverage these facts using affinity-based *property partitioning* [3], where each parallel process, or *worker*, runs the same strategy on a different property group.

An alternate way to accelerate verification is by using a parallel portfolio (*strategy exploration*), where the same property group is concurrently verified using a different strategy per worker, as depicted in Fig. 1. However, portfolio approaches often degrade into highly-redundant work across processes, where similar algorithms address properties in nearly-identical order. Existing tools often independently use these modes in different contexts, particularly strategy exploration first running qualitatively-different strategies in available workers (e.g., BMC, IC3, interpolation) then padding differently-configured identical strategies in the remaining processes (e.g., IC3 with different heuristics). The latter yields increasingly-redundant CPU-time for diminishing gains in wall-time. These modes need not be mutually-exclusive: a strategy could partition within a worker, and partitioning could use different strategies for different groups. We explore the mutual optimization between property partitioning and strategy exploration, addressing the following challenges:

### *Property partitioning* →

P1 Some workers are not utilized if the number of highaffinity groups is less than available workers.

P2 Some workers finish their tasks and idle (no more partitions to dispatch) while others degrade wall-time solving large or difficult groups, or run on slower machines.

### *Strategy exploration* →

P3 Nearly-identical strategies verify the same properties concurrently yielding redundant computation; two or more workers would solve the same property at nearly the same time.

<sup>1</sup>*Atomic verification* refers to running a set of single-process verification engines (called a *strategy*) on a group of properties. *Serial verification* refers to beginning one atomic task after another finishes, using a single process. *Concurrent* or *parallel verification* refers to dispatching multiple atomic tasks on concurrently-running parallel processes.

P4 A worker gets stuck on the first difficult property inhibiting progress; easy properties go unexplored.

P5 When using a round-robin resource-constrained approach to avoid P4, a worker fails to solve a difficult property in the allocated time even after several repetitions.

*Contributions:* We optimize parallel verification using complementary *property partitioning* and *strategy exploration*, in terms of both wall- and CPU-time. (1) We present a scalable property partitioning algorithm (Sect. III-A), extending [3] to guarantee *complete* utilization of available processes with provable partition quality. (2) We propose parallel scheduling improvements (Sect. III-B), such as resource-constrained irredundant group iteration, incremental repetition, and group decomposition to dynamically cope with more-difficult groups or slower workers. (3) We address irredundant strategy exploration of a localization portfolio in a sequential redundancy removal framework (Sect. IV), which we have found to be the most-scalable strategy to prove non-inductive redundancies. (4) We additionally propose improvements to *semantic group partitioning* within localization (Sect. IV-C). To our knowledge, this is the first published approach to mutually-optimize property partitioning and strategy exploration within a multiproperty localization portfolio.

#### *A. Related Work*

Despite the prevalence of parallel verification tools and multi-property testbenches, little research has addressed mutual optimization of parallel partitioning and strategy exploration. Furthermore, most approaches optimize wall-time alone without considering CPU-time, treating additional CPUs as free horsepower to fill with slightly-modified strategies without attempting to minimize redundant computation.

Methods to group properties based on COI similarity are either computationally-prohibitive [1, 2, 4], or do not optimally utilize available parallel processes [3]. They may generate fewer groups than processes, or lose affinity guarantees when requiring *number of groups* as an algorithmic parameter.

Much prior work addresses ways to parallelize specific algorithms in a *single-property* context [5]–[7]. Other work incrementally reuses information between properties to accelerate specific algorithms [8]–[11]. These are complementary to our work, and can be used as strategies therein.

Much complementary research has addressed sequential redundancy removal, using scalability-boosting strategies including induction [12]–[14], simulation [15, 16], and synergistic transformation and verification algorithms [16, 17]. The benefit of parallelizing inductively-provable redundancies has been noted in [18, 19], though little work addresses parallelizing non-inductive redundancies. Localization is a powerful scalability boost to redundancy removal [14, 16, 20] and property checking [21]–[24]. Prior work is focused mostly upon single-property single-process contexts [21]–[24], or solely upon parallel property partitioning [3]. This work is complementary to ours: we extend state-of-the-art solutions for both, to mutually-optimized parallel verification.

#### II. PRELIMINARIES

The design under verification is represented as a *netlist* N, which is a tuple hhV, E , F where V, E is a directed graph with vertices V representing *gates*, and edges E ⊆ V × V representing interconnections between gates. Function F : V types assigns vertices to gate types: constants, primary inputs, combinational logic such as *AND* gates, and sequential logic such as *registers*. A *state* is a valuation to the registers. Certain gates are labeled as *properties*. The *fan-in* (*fan-out*) of gate u is the set of gates which may be reached by traversing edges backward (forward) from u. The fan-in of property p is called the *cone of influence* (COI) of p. Registers and inputs in the COI are called *support variables*. The number of support variables in the COI is its *size*. A *strongly connected component* (SCC) is a set of interconnected gates such that there is a non-empty directed path between every pair of gates in the same SCC. A *merge* of gate u onto gate v consists of moving the output edges of u onto v, then eliminating u from the netlist by treating u as a rename for v.

#### *A. Affinity Analysis*

Property grouping algorithms represent support variable information as a *Boolean bitvector* per property [25]. Every support variable in the netlist is indexed to a unique position in the bitvector, set to "1" if and only if the support variable is in the COI of the property. The length of such a bitvector is equal to the total number of support variables in the netlist, and all bitvectors have the same length. The COI size of the property is the number of bits set to "1". These bitvectors may be compared to determine relative property *affinity*. Properties p1, p<sup>2</sup> with bitvectors bv1, bv<sup>2</sup> respectively have

$$0 \le \text{affinity}(p\_1, p\_2) = 1 - \frac{\text{hamning}(bv\_1, bv\_2)}{\text{length}(bv\_1)} \le 1.00$$

where hamming(bv1, bv2) is the Hamming distance between bv<sup>1</sup> and bv2, and length(bv1) is the number of support variables in the netlist [3]. The *distance* between p1, p<sup>2</sup> equals the Hamming distance between their bitvectors, i.e., dist(p1, p2) = hamming(bv1, bv2). A *group* g is a set of properties, with a single property g ∗ therein representing its *center*. The *quality* Q(g) of a group is the minimum affinity between any property in g vs. its center g ∗ :

$$Q(g) = \min(\text{ affinity}(p, g^\*) \quad p \quad g^-)$$

It is desirable that property partitioning algorithms guarantee group quality to be greater than a specifiable threshold.

#### *B. High-Affinity Property Grouping*

Three-leveled grouping [3] (Fig. 2) utilizes support bitvectors of properties to generate high-affinity groups. The algorithm takes the desired grouping level (l) and affinity threshold (t). It groups properties based upon: a) *Level-1*: identical bitvectors (identical support variables); b) *Level-2*: common large SCCs (containing t% netlist support variables) in the COI; and c) *Level-3*: small Hamming distance between support bitvectors, scalably identified by equivalence-classing *mapped*

Fig. 2. Algorithm to group properties based on structural affinity [3].

bitvectors using threshold-aware mapping functions. Higher levels yield progressively fewer but larger groups.

Straightforward grouping approaches such as pairwise comparison are computationally prohibitive [25], requiring at least quadratic resource with respect to number of properties. Despite being conceptually a quadratic-resource algorithm, bitvector equivalence-classing [3] consumes near-linear runtime and memory in practice, enabling scalable online partitioning with provable quality bounds [3]. Bitvectors are computed during a linear sweep of the netlist, and have size proportional to the number of SCCs plus non-SCC support variables. SCC computation has linear runtime [26]. With efficient implementation, this entire process consumes a few seconds on netlists with millions of support variables and properties: e.g. computing bitvectors in topological netlist order, and garbage-collecting bitvectors as soon as all fanout references have been processed [25].

A priori knowledge of solvers may dictate the ideal grouping level. For example, BDD-based reachability is highly sensitive to COI size, and thus may prefer level=1. BMC may prefer level=3 with lower affinity. Localization may prefer level=1, =2, or =3 depending on subsequent solvers. In many contexts, the caller can set level=3 and allow Fig. 2 to determine group count and size, especially when using the techniques of Sect. III-B and Sect. IV-C to decompose difficult groups.

Theorem 1 ([3]). *Level-1 grouping generates property groups* G *such that* g G : Q(g) = 1.0*.*

Theorem 2 ([3]). *Given affinity* t*, level-2 grouping generates property groups* G *such that* g G : Q(g) ≥ t*.*

Theorem 3 ([3]). *Given affinity* t*, level-3 grouping generates property groups* G *such that* g G : Q(g) ≥ 3 ∗ t − 2*.*

Note that desired number of property groups is not an algorithmic parameter; affinity analysis determines the optimal number of groups respecting configurable quality bounds. For more details on leveled grouping, we refer the reader to [3].

#### III. GROUPING FOR PARALLEL VERIFICATION

Many organizations have large clusters of computers for load-balancing of tasks such as verification. The maximum number of available workers for a given task (n) is often known, e.g. the maximum number of organizational job submissions allowed per user, minus how many that user wishes to reserve for other tasks. Existing scalable grouping algorithms [3] may generate fewer high-affinity groups than n (P1). While partitioning a high-affinity group may yield redundant

Fig. 3. Property grouping guaranteed to generate at least min(n, P ) highaffinity groups for n parallel workers.

Fig. 4. Algorithm to subdivide high-affinity groups for n workers.

CPU-time (similar effort expended on nearly-identical COIs), it may benefit wall-time due to disparate difficulty of properties therein: e.g. one may be inductive, and another require deep sequential analysis. Traditional clustering algorithms can be configured to produce ≥ n groups, though are computationally prohibitive for online use and may not yield affinity guarantees if n does not align with the given netlist.

#### *A. Property Grouping Algorithm*

Fig. 3 shows our extension to leveled grouping [3] (Fig. 2), guaranteeing generation of at least min(n, P ) provableaffinity groups. Each property is returned as a singleton if there are fewer than n properties. Otherwise, grouping is performed in three levels that iteratively generate fewer, larger groups. Later levels are skipped if the number of generated groups becomes less than n at any level. The algorithm then rebalances as needed by fine-grained affinity analysis: subdividing large or lower-affinity groups to generate at least min(n, P ) property groups. As discussed in Sect. III-B, this procedure is beneficial even after initial partitioning to subdivide a difficult group into provably high-affinity subgroups.

The rebalancing algorithm is shown in Fig. 4. It subdivides groups based on the grouping level l<sup>c</sup> that generated fewer groups than n. For level-1, quality is already 100% so division is based on number of properties in the group (Fig. 5). Groups with the most properties are halved until at least min(n, P ) groups are generated. Finer-grained analysis may be integrated if desired, e.g. considering affinity of combinational gates in the combinational fan-in of these properties. Group rollback for higher levels is more intricate (Fig. 6), with the goal of *improving* group quality. A group with minimal quality is conservatively subdivided until at least min(n, P ) groups are generated. A minimal-quality group is split to yield smaller,

```
halve groups (Groups G, Workers n)
1: while G < n :
2: Group g = pick largest non-singleton group from G
3: G = (G g) halve group (g) # see below
halve group (Group g)
1: return first half of g, second half of g # split in half
```
Fig. 5. Algorithm for subdividing large level-1 groups in half.

rollback groups (Groups G, Netlist N, Level lc, Affinity t, Workers n) 1: while G < n : 2: Group g = pick minimal-quality non-singleton group from G 3: G = (G g) rollback group (g, N, lc, t) *# see below* rollback group(Group g, Netlist N, Level lc, Affinity t) 1: Groups G = singletons(g) *# split* g *to singletons* 2: grouping level 1 (G, N) *# level-1* 3: if G == 1 : G = halve group (g G) return G *#* G == *2* 4: else if G == 2 : return G *#* g *had two* 100% *quality subgroups* 5: rollback group level (G, N, t, 2) *# level-2* 6: if G == 2 : return G 7: if l<sup>c</sup> == 3 : rollback group level (G, N, t, 3) *# level-3* 8: return G *#* G == *2* rollback group level (Groups G, Netlist N, Affinity t, Level l) 1: Groups G<sup>c</sup> = G *# local copy of* G 2: Group g0, g<sup>1</sup> = *# temporary groups, initially empty* 3: if l == 2 : grouping level 2 (Gc, N, t) *# level-2* 4: else : grouping level 3 (Gc, N, t) *# level-3* 5: if G<sup>c</sup> == 1 : *#* G<sup>c</sup> *is one group containing all properties in* G 6: g<sup>0</sup> = g G containing center property g ∗ c 7: *# extract most-distant property into distinct subgroup* 8: g<sup>1</sup> = g G s.t. dist(g ∗ 0 , g ∗ ) == max( dist(g ∗ 0 , g ∗ i ) j 8g<sup>i</sup> <sup>G</sup> ) 9: for each group g G : *# merge groups to minimize distance* 10: if dist(g ∗ 0 , g ∗ ) ≤ dist(g ∗ 1 , g ∗ ) : add properties in g to g<sup>0</sup> 11: else : add properties in g to g<sup>1</sup> 12: <sup>G</sup> <sup>=</sup> <sup>g</sup>0, g<sup>1</sup> *# note* <sup>Q</sup>(g0), Q(g1) <sup>≥</sup> <sup>Q</sup>(gc)*, see Thm. 4* 13: else : <sup>G</sup> <sup>=</sup> <sup>G</sup><sup>c</sup> *#* <sup>G</sup>j ≥ *<sup>2</sup>*

Fig. 6. Algorithm for subdividing minimal-quality groups.

higher-quality subgroups. This process has negligible runtime, reuses precomputed support bitvectors and requires only a few milliseconds on the largest netlists.

The rebalancing procedure generates groups with quality bounds per Theorems 1, 2 and 3. Note that arbitrarily subdividing level-2,-3 groups without careful affinity consideration might violate affinity thresholds, because the quality of group g is measured with respect to its center property g ∗ . Assume that we generate subgroups g<sup>0</sup> and g<sup>1</sup> from g. If g ∗ is in g0, we trivially have Q(g ∗ 0 ) ≥ Q(g ∗ ) for any properties subgrouped with g ∗ . However, no such claim can be made about g1; its properties might have been nearer to g ∗ than to each other. It is thus desirable to subdivide the most-distant property g ∗ 1 from g ∗ to improve vs. risk degrading the resulting quality of both subgroups. Moreover, simply rolling back a higher level group to lower-level subgroups risks generating more groups than necessary, e.g., one level-2 group rolled back to ten level-1 groups. The algorithm in Fig. 3 generates *a minimal number* G of high-affinity groups with provable affinity bounds, where Gj ≥ min(n, P ).

Theorem 4. *Given a group* g*, the rollback group procedure*

*subdivides* g *into two disjoint subgroups* g<sup>0</sup> *and* g<sup>1</sup> *such that* Q(g0) ≥ Q(g) *and* Q(g1) ≥ Q(g)*.*

*Proof.* (Sketch) The algorithm returns two 100% affinity groups when properties in g generate at most two level-1 subgroups. Otherwise, the greatest-Hamming-distance property g ∗ 1 g from g's center property g ∗ is identified. Subgroup g<sup>0</sup> inherits g ∗ as its center, and g<sup>1</sup> inherits g ∗ 1 as its center. Remaining properties in g are added to g<sup>0</sup> vs. g<sup>1</sup> to minimize distance from g ∗ <sup>0</sup> vs. g ∗ 1 , ensuring provable quality bounds.

Corollary 4.1. *Given affinity* t *and level* l*, grouping for parallelism (Fig. 3) generates groups* G *such that* g G*: a)* Q(g) = 1.0 *if* l = 1*, b)* Q(g) ≥ t *if* l = 2*, and c)* Q(g) ≥ 3 ∗ t − 2 *if* l = 3*.*

*Proof.* The proof follows per Theorems 1, 2 and 3 when no rebalancing occurs. Otherwise, rebalancing divides group g in to smaller groups based on: (i) l = 1, level-1 subgroups are generated and Q(g) = 1.0 per Theorem 1; (ii) l = 2, levels-1 or 2 subgroups are generated and Q(g) ≥ t per Theorems 2 and 4; and (iii) l = 3, levels-1, 2 or 3 subgroups are generated and Q(g) ≥ 3 ∗ t − 2 per Theorems 3 and 4.

Theorem 5. *Given groups* G *over a set of properties* P*, and workers* n *with* G < n *and* Pj ≥ n*, rebalancing generates property groups* G<sup>0</sup> *such that* G0 <sup>=</sup> <sup>n</sup>*.*

*Proof.* Both halve group and rollback group subdivide a nonsingleton group g into exactly two subgroups, and iterate until G0 <sup>≥</sup> <sup>n</sup>. Therefore, the number of groups increases by exactly one in every iteration, unless all groups become singleton which cannot happen until G0 <sup>=</sup> <sup>P</sup>j ≥ <sup>n</sup>.

Corollary 5.1. *Given a set of properties* P *and* n *workers, grouping for parallelism (Fig. 3) generates groups* G *from* P *such that* Gj ≥ *min(*n*,* P *).*

*Proof.* The proof trivially holds when ≥n groups or Pj ≤ n singletons are generated without rebalancing. Otherwise, the proof holds per Theorem 5 when rebalancing occurs.

#### *B. Group Distribution Heuristics*

We propose three heuristics to optimally utilize parallel workers, used on-the-fly by a *manager* that dispatches property groups and dynamically adjusts based upon worker feedback. When partitioning is supported by an engine within a strategy (e.g. a localization engine [3]), there might be multiple managers partitioning an identical or overlapping set of properties. It is sometimes beneficial to use a hierarchy of managers: the *root* might use lower-affinity partitioning onto parallel strategies, with higher-affinity partitioning within a strategy.

Iteration order (I): Fig. 3 orders groups deterministically, and thus distributed managers within a strategy will likely verify common properties in the same order. This results in redundant CPU-time, where two or more strategies may solve the same property at nearly the same time (P3). The root manager could instead dispatch disjoint properties to different workers, though there are motivations for building

intelligence into distributed managers working on the entire property set, such as enabling incrementality and data sharing across properties [8]–[11]. To minimize redundant work, the manager may be augmented with options to iterate common groups in different orders: 1) smallest to largest COI (*forward*); 2) largest to smallest COI (*backward*); and 3) *random* to heuristically minimize concurrent solving of the same group while more groups than workers remain unsolved. If all properties are of comparable difficulty, running two identical strategies with opposite group ordering effectively halves walltime with almost no redundant CPU-time. This approach can yield superlinear irredundant speedup when different strategies are tailored for easier vs more-difficult properties: a lighter strategy can iterate *forward* heuristically addressing easier properties first (the heavier strategy would be slower for these), while the heavier strategy can iterate *backward* addressing more-difficult properties first (the lighter strategy might be unable to solve these).

Controlled repetition (R): Each worker solves groups one-ata-time. Encountering a difficult group inhibits overall progress (P4). Easier groups might follow, which when solved might speed-up incremental verification of the previous difficult group. Furthermore, solving easy properties sooner benefits other workers, allowing them to focus on fewer difficult groups. It is thus beneficial to impose time-limits per group within certain *fast* strategies. The manager must be capable of pruning already-solved properties (possibly solved by different workers), and repeating groups up to a configurable maximum allowed repetitions (to reduce redundant CPU-time). It may be beneficial to increase resource limits between repetitions, possibly after n repetitions with no progress. Engine incrementality is fairly important when imposing time-limits and repetition, to minimize redundant CPU-time.

Decomposition (D): Some groups are more difficult than others, either because they are large (e.g., many properties), or because individual properties therein are more difficult (e.g., having a very-deep counterexample). Some workers might be slower than others, possibly due to varying machine load. A common wall-time degradation occurs when fewer difficult groups than workers remain, and previously-active workers become idle (P2). This heuristic decomposes unsolved groups and dispatches them to idle workers, to accelerate convergence despite imposing some redundant CPU-time. Rather than redundantly dispatching an entire unsolved group, this

Fig. 8. Sequential equivalence checking uses redundancy removal to eliminate gate-equivalences between two logic designs. Each speculated gate-equality requires verifying a property called a *miter* (depicted as green box *=?*).

heuristic utilizes the algorithms of Fig. 5 and Fig. 6 to subdivide unsolved groups to smaller and higher-affinity groups, eventually becoming singletons. Smaller groups are easier for idle workers to redundantly solve (P5), benefiting but not preempting active workers (which might be on the verge of solves). The corresponding manager with decomposition is shown in Fig. 7. A group is *inactive* when no worker is currently verifying it. Solved properties and groups are discarded; groups with *unsolved* properties are subdivided and redundantly dispatched. Singleton groups are not redundantly dispatched, being *inactive* after the first dispatch.

#### IV. LOCALIZATION FOR REDUNDANCY REMOVAL

Industrial hardware designs are often rife with redundancy, e.g. to boost the performance of semiconductor devices, and to implement features such as error resilience, security, initialization logic and post-silicon observability. Verification testbenches yield additional netlist redundancies, due to *input constraints* restricting the set of stimulus applied to the design, and due to redundancies arising between the design and synthesized properties. Equivalence checking can be viewed as verifying a *composite netlist* comprising two designs as per Fig. 8. *Sequential redundancy removal* [12]–[14, 16]–[18, 27] (Fig. 9) is the process of proving that equivalence-classes of gates evaluate to equal or opposite values in all reachable states; each speculated redundancy entails solving a property called a *miter*. When a miter is proven, the corresponding redundant gates can be merged. This COI reduction is highly beneficial to verification scalability, and is the core procedure of sequential equivalence checking (SEC).

Various heuristics control the scope of equivalence-class candidates affecting runtime vs. reduction (Fig. 9 Step 1): e.g. whether to consider only registers vs. all gate types; whether to prune classes to reflect *corresponded signal names* or require per-class candidates spanning both designs in an equivalencechecking context (Fig. 8) [14, 20]. A *speculatively-reduced netlist* (Steps 2-3) accelerates verification of the miters. Techniques such as BMC and guided simulation are typically used to falsify miters; then induction proves the easier miters; and finally multi-engine strategies prove the difficult miters or find difficult counterexamples (Steps 4,5). Failed proofs (falsified miters or inconclusive results) cause a *refinement* of the equivalence classes to separate unproven miters' gates, then another expensive proof iteration is performed. Our goal is to minimize inconclusive proofs to achieve maximum netlist reduction with redundancy removal (Netlist N)

Fig. 9. Generic sequential redundancy removal framework [16].

minimal wall- *and CPU*-time, using a parallel localization portfolio. Note that even if a testbench has only a single property, redundancy removal will often create thousands of miters. The large number of miters often tremendously benefit from parallel processing, as noted for combinational redundancy removal [19] and induction [18]. These miters are distributed throughout the netlist, making affinity partitioning particularly beneficial. Since practical netlists comprise a diversity of logic, different miters benefit from different strategies.

The proof or counterexample of a property often only depends on a small subset of logic in its COI. *Localization* [21]– [24] is a powerful abstraction method to reduce COI size by replacing irrelevant gates by *cutpoints* or unconstrained primary inputs. Since cutpoints can simulate the behavior of the original gates and more, the abstracted netlist overapproximates the behavior of the original netlist: abstract proofs imply original proofs, but abstract counterexamples might be spurious. Abstraction *refinement* eliminates cutpoints deemed responsible for spurious counterexamples, reintroducing previously-eliminated logic. It is desirable that the abstract netlist be as small as possible to enable scalable verification, while being immune to spurious counterexamples.

Localization is often essential to solve non-inductive miters, leveraging speculative reduction to abstract nearly all logic except for differently-implemented yet functionally-equivalent logic *between* speculated equivalences [14, 16]. Without localization, the COI of a miter may be very large despite speculative reduction. This large COI size may choke even fairlyscalable provers such as IC3. While the benefits of localization for sequential redundancy removal are well-known [17], prior work considered only single-process miter verification, aside from use of a standard parallel model-checking portfolio to solve miters [20]. Ours is the first to optimize a parallel localization portfolio in this (or any multi-property) context, using property partitioning and irredundant scheduling procedures (Figs. 3 and 7), along with the following complementary strategies tailored for easier vs. difficult properties. Note that substrategies in either may be employed by the other.

#### *A. Fast-and-Lossy Localization*

*Fast-and-Lossy* localization (Fig. 10) attempts to quickly discharge easier property groups, using timeouts to skip diffi-

Fig. 10. *Fast-and-Lossy* localization with incremental repetition of highaffinity property groups.

cult groups. If the group is not solved within the allotted time, verification data (e.g., the current abstract netlist and achieved BMC depth) is saved for incremental reuse to accelerate later repetition. Skipped groups can be repeated as-is, or rebalanced (Fig. 7) after several repetitions of no progress. Note that repeating a group as-is may likely proceed further upon repetition, by incrementally skipping earlier processing and since a different worker might have solved some properties therein. *Fast-and-Lossy* localization uses counterexample-based refinement sometimes with quick proof-based abstraction (PBA), possibly yielding larger abstract netlists that are more-difficult to prove but with less time expended in BMC itself [23] for faster performance on easier groups. When ready to prove (i.e., no refinements occur for n consecutive BMC steps), abstracted groups are passed to a sequence of lighter reduction engines then IC3 [5, 28]) under a modest time-limit (e.g. ≤ 300s) which can be increased across repetitions (R).

#### *B. Aggressive Localization*

*Aggressive* localization (Fig. 11) is aimed at solving difficult properties, where *Fast-and-Lossy* may fail due to larger-thannecessary abstractions, insufficient reductions prior to IC3, or small group time-limits. *Aggressive* never repeats groups, so either imposes no time limit whatsoever, or a large time-limit as shown applied to semantically-partitioned (Sec. IV-C) subgroups but iterated and increased until the group is solved. *Aggressive* typically uses a hybrid of counterexample-based refinement and PBA run after every unsatisfiable BMC result, to yield smaller abstractions than the former alone to accelerate subsequent proofs at the expense of more runtime spent in BMC itself [23]. When ready to prove (i.e., no refinements occur for n consecutive BMC steps), abstracted groups are passed to a sequence of heavy reduction engines (including nested induction-only sequential redundancy removal across

Fig. 11. *Aggressive* localization with semantic partitioning, counterexampleand proof-based abstraction.

*all gates*, which might be too expensive to converge on large netlists before localization) followed by IC3 [5, 28]).

#### *C. Semantic Partitioning*

*Semantic partitioning* [3] refers to re-partitioning a group whose *unabstracted COI* was high-affinity, yielding subgroups of high affinity with respect to *abstract COI* as correlates to subsequent verification complexity. Abstract COI information is mined onto support bitvectors on a per-property basis as cutpoints are refined (Fig. 11 Step 4), considering minimized counterexamples for individual properties despite incrementally using the same BMC instance for the entire group. The group is partitioned into smaller, high-localizedaffinity subgroups (Step 7) before attempting to prove.

Improvements to semantic partitioning vs. [3]: Per-property abstract-COI bloat may arise during counterexample analysis, because the group must be mutually refined to be free of spurious counterexamples. Eager partitioning (as soon as any diverged abstract COI occurs) *could* circumvent this ambiguous bloat, though often severely hurts performance since intermediate abstract-COI differences often reconverge. In practice, lazy partitioning deferred until modest BMC time limits are exceeded is far superior (particularly since BMC often benefits from level=3 lower affinity), retaining highaffinity atomic verification benefits. Abstract-COI ambiguities can be largely corrected during proof analysis, by analyzing a distinct proof per property. Incremental data should be saved when semantically re-partitioning, to minimize restart penalty.

Difficult sub-groups are susceptible to delaying easier later sub-groups. Subgroups should be ordered as per (I) mode (Sect. III-B): *forward*, *backward*, and *random*, configured differently in parallel strategies for better portfolio performance with less redundant CPU-time. Subgroups are verified in the chosen order using controlled repetition (R) and large *Aggressive* time-limits (Steps 9–11). We recommend T ≥ 1h multiplying 2× at each iteration (Step 12) and overriding to *unlimited* when a single sub-group remains.

#### V. EXPERIMENTAL RESULTS

We evaluate our techniques within the post-induction proof strategy of a sequential redundancy removal framework (Fig. 9). To eliminate *noise* such as different counterexamples yielding different equivalence-classes (Step 5), we snapshot the speculatively-reduced netlist after ten minutes of induction, before the final iteration of a six-hour eight-process semiformal bug-hunting [29] and localization portfolio to eliminate most incorrect and easier [27] miters. The following experiments2 are run on these snapshotted netlists (pruning those with fewer miters than processes), yielding three benchmark sets. Set B1 (Fig. 12a) are the most-difficult 291 of 1822 proprietary SEC benchmarks, where initial equivalence classes comprise original properties and *name corresponded* register pairs. Set B2 (Fig. 12b) has 269 netlists derived from the former, including a large equivalence class for registers without name correlation. Set B3 has 72 netlists from the SINGLE property HWMCC 2017 benchmarks, comprising a large initial equivalence class of all registers. Our techniques are implemented within *RuleBase: Sixthsense Edition* [30].

#### *A. Localization Portfolio*

We select our localization portfolio (Table I) from extensive evaluation of 36 single-process localization configurations and 30 subsequent proof strategies, exploring options such as enabling vs. disabling PBA [23]; different levels of property grouping vs. no grouping [3]; enabling vs. disabling semantic partitioning (Sect. IV-C); and different policies for group iteration (I), repetition (R), and decomposition (D) (Sect. III-B). The best-performing collection is chosen, maximizing *complementary* unique solves. *Aggressive* localization (Sect. IV-B) primarily uses both counterexample- and proofbased abstraction, yielding smallest abstract netlists solved with a single-process heavy strategy of combinational rewriting; input elimination [31]–[33] which is especially powerful after localization due to inserted cutpoints; min-area retiming [34]; a nested induction-only gate-based sequential redundancy removal; then IC3. *Fast-and-Lossy* localization (Sect. IV-A) uses counterexample-based refinement mainly with no or lighter PBA for faster BMC, yielding larger abstract netlists solved using light combinational rewriting, input elimination, then IC3. The former is fastest for difficult properties; the latter for easier properties.

We compare four 6-process localization portfolios derived from Table I. The localization configuration and subsequent solving strategy of each process is identical across portfolios,

<sup>2</sup>Detailed results available at http://temporallogic.org/research/FMCAD20

TABLE I SIX-PROCESS COMPLEMENTARY LOCALIZATION PORTFOLIO.

except for adherence to the illustrated scheduling differences as discussed below. For greater portfolio value, each process includes localization configuration differences beyond the illustrated scheduling distinction in Table I. S1 only performs counterexample-based refinement; S2 and S3 also perform PBA. S2 vs. S3 perform hybrid counterexamplebased refinement with light PBA (modest time limit) after every unsatisfiable BMC step vs. only before the subsequent solving strategy, respectively. Abstract-netlist gates remaining after PBA are considered *committed* and cannot be eliminated in later PBA steps [21] in S2, but not S3. S3 utilizes a minimal unsatisfiable core to further reduce the abstract netlist. S4-S6 are identical to S1-S3, respectively, without imposed time-limits and modulo the above-mentioned post-localization solving strategy differences. To highlight our individual contributions, we compare four variants of this portfolio:

1) base: No property grouping or incremental repetition of properties; all processes iterate properties in forward order. This represents a standard state-of-the-art localization portfolio approach *without property grouping*, e.g., before [3].

2) base+g extends base with affinity property grouping, including semantic partitioning in one *Fast-and-Lossy* and one *Aggressive* strategy. This represents a state-of-the-art localization portfolio *with property grouping*, e.g., as per [3] though with our semantic refinement improvements of Sect. IV-C. 3) best-d extends base+g with incremental repetition (R) and irredundant iteration order (I), to reduce CPU-time. 4) best extends best-d with decomposition (D).

Processes S1-S6 are generic online localization strategies. Multi-property localization *without affinity-partitioning* generally yields poor/noncompetitive performance [3], eroding most of its scalability benefit, especially for difficult miters. (Recall that these benchmarks pre-filter easier miters, using induction and semi-formal bug-hunting.) Therefore, base and base+g are highly-competitive 6-process localization portfolios, for online "first-run-of-a-testbench." Industrial verification tools may use more processes for large testbenches, and may postprocess data from prior/ongoing runs to accelerate future results. This level of sophisticated benchmark-specific orchestration is valuable, though does not readily benefit "first-runof-a-testbench" and introduces noise in experiments hence are not used herein. We optimize runtime of a generic 6-process localization portfolio without per-benchmark customization.

#### *B. Experiment Setup*

Our experiments run on a computing grid with identical x86 Linux nodes. Each benchmark run uses a 6-process portfolio

Fig. 13. #Properties solved vs. wall-time for B1 and B2; 6-hour time limit.

Fig. 14. **best** vs. baselines for B1 (points below diagonal are in favor).

(Table I); each process S1-S6 runs on a single identical CPU core on the same host-machine. Each process eagerly cancels solved properties across all processes in that portfolio, to reduce redundant computation.

While most prior research and competitions focus solely upon optimizing wall-time, our techniques additionally benefit CPU-time. Traditionally, Fast-and-Lossy (unlike Aggressive) processes terminate early, leaving unsolved difficult properties. In these experiments, base and base+g augment Fast-and-Lossy processes to naively repeat identically-configured S1-S3 with identical resource limits per group (whereas best-d and best add incremental-repetition (R) with resource-doubling across repetitions), until all properties are solved or global timeout. This naive repetition is wasteful in practice, yielding highly-redundant CPU-time for marginal benefit. However, disabling naive repetition in these experiments yielded 3.2% fewer solves in base and base+g vs. best-d and best, which arguably unfairly penalized them as state-of-the-art solutions *before our contributions*. Therefore, S1-S6 in each portfolio continue working until all processes terminate, hence CPU-time is approximately 6× wall-time in these experiments.

#### *C. Proprietary Benchmarks*

Fig. 13 shows the number of properties solved vs. walltime for B1 and B2. best is the clear winner, solving 18.1% (15.3%) more properties in 17.2% (22.9%) less time for B1 (B2, respectively) compared to base. Affinity-grouping significantly improves performance of base+g over base. Level-3 grouping with our semantic partitioning improvements (Sect. IV-C) benefits *Aggressive*, atomically solving properties in fewer, larger high-abstract-affinity groups compared to level-1,-2. Incremental repetition and irredundant iteration allows best-d to solve 8.1% more properties than base+g, less-severely hindered by difficult groups. best yields additional solves through decomposition of difficult groups after five incremental repetitions of no progress, solving all properties in 4 vs. 6 benchmarks in B1 vs. B2 that time out with

Fig. 15. #Properties solved on B2 per process of Table I.

TABLE II UTILITY OF AGGRESSIVE STRATEGY PROCESSES IN A PORTFOLIO.

Fig. 16. #Properties solved vs. wall-time for **big**: (a) by all portfolios; (b) per process of Table I within best and best-d.

other portfolios. Fig. 14 details per-B1-benchmark runtimes of best, yielding a median speedup of 2.4× , 2.0× and 1.5× vs. base, base+g, and best-d, respectively.

Fig. 15 shows the distribution of properties solved per process (Table I) within these portfolios. The percentage solved by each *Fast-and-Lossy* (and *Aggressive*) process is nearly uniform in best, showing near-optimal irredundant work distribution. In contrast, without (I) and (R), base and base+g have highly-uneven distributions due largely to parallel processes addressing the same groups concurrently. While the number of solved (easier) miters is considerably larger with *Fast-and-Lossy*, we emphasize how critical the *Aggressive* solution of difficult miters is to the overall redundancy removal process. If any are left unsolved, Fig. 9 Step 5 will forgo attempting to merge the corresponding gates, thereby weakening netlist reductions, risking unsolved SEC, and hurting runtime by requiring yet another expensive proof iteration with refined equivalence classes [14] – where fanout miters often become more-difficult than those unsolved in prior iterations. Table II shows the number of properties solved by best, and a modified best portfolio with all *Fastand-Lossy* strategy processes where S4-S6 are identical to S1- S3 respectively, but without imposed time-limits and iterating groups in opposite order. Without *Aggressive* processes in the portfolio, modified best solves 10.9% (2.31%) fewer properties in 16.5% (11.51%) more time for B1 (B2).

To further highlight the value of decomposition (D), Fig. 16b illustrates an additional **big** benchmark containing 77728 properties partitioned into 9958 level-1 and level-2, and 2991 level-3 high-affinity groups. Fig. 16a shows the number of properties solved by each portfolio vs. time. best is 3.0× faster than base. Fig. 16b shows the number of properties solved by two *Fast-and-Lossy* processes of best and best-d; decomposition enables S2 and S3 in best to collectively solve 25.2% more properties than best-d.

#### *D. HWMCC Benchmarks*

Fig. 17 shows the number of properties solved by each portfolio for set B3. best is again the winner, solving 3054 more properties in less time than base. Incremental repetition and irredundant iteration is particularly

Fig. 17. #Solved vs. wall-time for B3.

beneficial in this set: several benchmarks have counterexamples that are discovered in earlier group repetitions, enabling *Aggressive* and later *Fast-and-Lossy* repetitions to direct resource upon more-difficult provable miters.

#### VI. CONCLUSIONS AND FUTURE WORK

We focus upon boosting the scalability of multi-property parallel verification, with application to sequential redundancy removal using a localization portfolio. Our contributions optimize both wall-time and CPU-time, orchestrating via complementary strategy exploration and property partitioning. (1) We extend scalable affinity-based property partitioning to guarantee *complete* utilization of available processes with provable partition affinities. (2) We propose improvements to the scheduling of parallel processes, such as resourceconstrained irredundant iteration, incremental repetition, and decomposition of difficult groups. (3) We deliver a carefullyoptimized localization portfolio, self-tailoring to irredundantly address a range of property difficulties through a synergistic balance of *Fast-and-Lossy* vs. *Aggressive* configurations. (4) We propose improvements to *semantic group partitioning* within localization, boosting scalability by enabling the BMC within localization to benefit from larger and slightly-lower affinity groups, then optimally sub-dividing those groups before solving the localized properties. To our knowledge, this is the first published approach to optimize both property partitioning and strategy exploration within a multi-property localization portfolio. Experiments confirm that this solution works well across large suites of benchmarks.

Note that our mutually-optimized partitioning vs. strategyexploration orchestration offers broad insights early in an ongoing verification-tool run, whereas traditional orchestration typically explores only easier (smaller-COI) properties or only a subset of strategies early in the run. Exploring how this insight may enable dynamic benchmark-specific customized orchestration *during* an ongoing run is a promising future direction, e.g. dynamically adjusting which strategy is used per process and partition. Exploring these techniques across a broader set of engines, and exploring incrementality of strategies across localization and equivalence-class refinements, are additional promising research directions.

#### ACKNOWLEDGMENTS

We thank the anonymous reviewers for their valuable feedback and suggestions. We thank Alexander Ivrii for assistance in implementing various localization features and for feedback on early drafts of this paper. We thank Raj Kumar Gajavelly for providing benchmarks and assistance with experimental evaluation. This work is partially supported by National Science Foundation CAREER Award CNS-1664356.

#### REFERENCES

### A Theoretical Framework for Symbolic Quick Error Detection

Florian Lonsing , Subhasish Mitra, and Clark Barrett Computer Science Department, Stanford University, Stanford, CA 94305, USA E-mail: {lonsing, subh<EMAIL_ADDRESS>
*Abstract*—Symbolic quick error detection (SQED) is a formal pre-silicon verification technique targeted at processor designs. It leverages bounded model checking (BMC) to check a design for counterexamples to a self-consistency property: given the instruction set architecture (ISA) of the design, executing an instruction sequence twice on the same inputs must always produce the same outputs. Self-consistency is a universal, implementation-independent property. Consequently, in contrast to traditional verification approaches that use implementationspecific assertions (often generated manually), SQED does not require a full formal design specification or manually-written properties. Case studies have shown that SQED is effective for commercial designs and that SQED substantially improves design productivity. However, until now there has been no formal characterization of its bug-finding capabilities. We aim to close this gap by laying a formal foundation for SQED. We use a transition-system processor model and define the notion of a bug using an abstract specification relation. We prove the soundness of SQED, i.e., that any bug reported by SQED is in fact a real bug in the processor. Importantly, this result holds regardless of what the actual specification relation is. We next describe conditions under which SQED is complete, that is, what kinds of bugs it is guaranteed to find. We show that for a large class of bugs, SQED can always find a trace exhibiting the bug. Ultimately, we prove full completeness of a variant of SQED that uses specialized state reset instructions. Our results enable a rigorous understanding of SQED and its bug-finding capabilities and give insights on how to optimize implementations of SQED in practice.

#### I. INTRODUCTION

Pre-silicon verification of HW designs given as models in a HW description language (e.g., Verilog) is a critical step in HW design. Due to the steadily increasing complexity of designs, it is crucial to detect logic design bugs before fabrication to avoid more difficult and costly debugging in post-silicon validation.

Formal techniques such as bounded model checking (BMC) [1] have an advantage over traditional pre-silicon verification techniques such as simulation in that they are exhaustive up to the BMC bound. Hence, formal techniques provide valuable guarantees about the correctness of a design under verification (DUV) with respect to the checked properties. However, in traditional assertion-based formal verification techniques, these properties are implementation-specific and must be written manually based on expert knowledge about the DUV. Moreover, it is a well-known, long-standing challenge that sets of manually-written, implementation-specific properties might be insufficient to detect all bugs present in a DUV [2]–[6].

This work was supported by the Defense Advanced Research Projects Agency, grant FA8650-18-2-7854.

Symbolic quick error detection (SQED) [7]–[10] is a formal pre-silicon verification technique targeted at processor designs. In sharp contrast to traditional formal approaches, SQED does not require manually-written properties or a formal specification of the DUV. Instead, it checks whether a self-consistency [11] property holds in the DUV. The self-consistency property employed by SQED is universal and implementation-independent. Each instruction in the instruction set architecture (ISA) of the DUV is interpreted as a function in a mathematical sense. The self-consistency check then amounts to checking whether the outputs produced by executing a particular instruction sequence match if the sequence is executed twice, assuming the inputs to the two sequences also match.

SQED leverages BMC to exhaustively explore all possible instruction sequences up to a certain length starting from a set of initial states. Several case studies have demonstrated that SQED is highly effective at producing short bug traces by finding counterexamples to self-consistency in a variety of processor designs, including industrial designs [9]. Moreover, SQED substantially increases verification productivity.

However, until now there has been no rigorous theoretical understanding of (A) whether counterexamples to self-consistency found by SQED always correspond to actual bugs in the DUV the *soundness* of SQED—and (B) whether for each bug in the DUV there exists a counterexample to self-consistency that SQED can find—the *completeness* of SQED. This paper makes significant progress towards closing this gap.

We model a processor as a transition system. This model abstracts away implementation-level details, yet is sufficiently precise to formalize the workings of SQED. To prove soundness and (conditional) completeness of SQED, we need to establish a correspondence between counterexamples to self-consistency and bugs in a DUV. In our formal model we achieve this correspondence by first defining the correctness of instruction executions by means of a general, abstract specification. A bug is then a violation of this specification. The abstract specification expresses the following general and natural property we expect to hold for actual DUVs: an instruction writes a correct output value into a destination location and does not modify any other locations.

As our main results, we prove soundness and conditional completeness of SQED. For soundness, we prove that if SQED reports a counterexample to the universal self-consistency property, then the processor has a bug. This result shows that SQED does not produce spurious counterexamples. Importantly, this

result holds regardless of the actual specification, confirming that SQED does not depend on such implementation-specific details. For completeness, we prove that if the processor has a bug then, under modest assumptions, there exists a counterexample to self-consistency that can be found by SQED. We also show that SQED can be made fully (unconditionally) complete with additional HW support in the form of specialized state reset instructions. Our results enable a rigorous understanding of SQED and its bug-finding capabilities in actual DUVs and provide insight on how to optimize implementations of SQED.

In the following, we first present an overview of SQED from a theoretical perspective (Section II). Then we define our transition system model of processors (Section III) and formalize the correctness of instruction executions in terms of an abstract specification relation (Section IV). After establishing a correspondence between the abstract specification and the self-consistency property employed by SQED (Section V), we prove soundness and (conditional) completeness of SQED (Section VI). We conclude with a discussion of related work and future research directions (Sections VII and VIII).

#### II. OVERVIEW OF SQED

We first informally introduce the basic concepts and terminology related to SQED. Fig. 1a shows an overview of the high-level workflow. Given a processor design P, i.e., the DUV, SQED is based on symbolic execution of instruction sequences using BMC. We assume that an *instruction* i = (op, l,(l , l<sup>00</sup>)) consists of an opcode op, an output location l, and a pair (l , l<sup>00</sup>) of input locations.<sup>1</sup> *Locations* are an abstraction used to represent registers and memory locations.

The self-consistency check is based on executing two instructions that should always produce the same result. The two instructions are called an *original* and a *duplicate instruction*, respectively. The duplicate instruction has the *same opcode* as the original one, i.e., it implements the same functionality, but it operates on different input and output locations. The locations on which the duplicate instruction operates are determined by an *arbitrary but fixed bijective function* L<sup>D</sup> : L<sup>O</sup> ! L<sup>D</sup> between two subsets LO, the *original locations*, and LD, the *duplicate locations*, that form a partition of the set L of all locations in P. An original instruction can only use locations in LO. An *instruction duplication function* Dup then maps any original instruction i<sup>O</sup> to its duplicate i<sup>D</sup> by copying the opcode and then applying L<sup>D</sup> to its locations.

Example 1. *Let* L = 0, . . . , 31 *be the identifiers of 32 registers of a processor* P*, and consider the partition* L<sup>O</sup> = 0, 1, . . . , 15 *and* L<sup>D</sup> = 16, 17, . . . , 31 *. Let* i<sup>O</sup> = (ADD, l12,(l4, l8)) *be an original register-type ADD instruction operating on registers* 4, 8*, and* 12*. Using* L<sup>D</sup> (k) = k + 16*, we obtain* Dup(iO) = i<sup>D</sup> = (ADD, l28,(l20, l24))*.*

*Consider a different partition* L<sup>O</sup> = 0, 2, 4, . . . , 30 *and* L<sup>D</sup> = 1, 3, 5, . . . , 31 *and function* L<sup>D</sup> (k) = k + 1*. For this function,* Dup(iO) = (ADD, l13,(l5, l9))*.*

Self-consistency checking is implemented using *QED tests*. A QED test is an instruction sequence i = i<sup>O</sup> :: i<sup>D</sup> consisting of a sequence i<sup>O</sup> of n original instructions followed by a corresponding sequence i<sup>D</sup> = Dup(iO) of n duplicate instructions (where operator "::" denotes concatenation). A QED test i is symbolically executed from a *QED-consistent state*, that is, a state where the value stored in each original location l is the same as the value stored in its corresponding duplicate location LD(l). The resulting final state after executing i should then also be QED-consistent. Fig. 1a illustrates the workflow. A QED test i *succeeds* if the final state that results from executing i is QED-consistent; otherwise it *fails*. Starting the execution in a QED-consistent state guarantees that original and duplicate instructions receive the same input values. Thus, if the final state is not QED-consistent, then this indicates that some pair of original and duplicate instructions behaved differently.

Example 2. *Consider Fig. 1b and the QED test* i = i<sup>O</sup> :: i<sup>D</sup> *consisting of one original instruction* i<sup>O</sup> *and its duplicate* Dup(iO) = i<sup>D</sup> *for some function* L<sup>D</sup> *. Suppose that* i *is executed in a QED-consistent state* s<sup>0</sup> *(denoted by* QEDcons(s0) *and* s0(LO) = s0(LD)*) and both* i<sup>O</sup> *and* i<sup>D</sup> *execute correctly. Instruction* i<sup>O</sup> *produces state* s1*, where the values at duplicate locations remain unchanged, i.e.,* s0(LD) = s1(LD)*, because* i<sup>O</sup> *operates on original locations only. When instruction* i<sup>D</sup> *is executed in state* s1*, it modifies only duplicate locations. The final state* s<sup>2</sup> *is QED-consistent (denoted by* QEDcons(s2) *and* s2(LO) = s2(LD)*), and thus QED test* i *succeeds.*

Example 3 (Bug Detection). *Consider processor* P *and* L<sup>O</sup> *and* L<sup>D</sup> *from Example 1. Let* iO,<sup>1</sup> = (ADD, l12,(l4, l15)) *and* iO,<sup>2</sup> = (MUL, l15,(l12, l12)) *be original register-type addition and multiplication instructions. Using* L<sup>D</sup> (k) = k+16*, we obtain* Dup(iO,1) = iD,<sup>1</sup> = (ADD, l28,(l20, l31)) *and* Dup(iO,2) = iD,<sup>2</sup> = (MUL, l31,(l28, l28))*. Assume that* P *has a bug that is triggered when two MUL instructions are executed in subsequent clock cycles, resulting in the corruption of the output location of the second MUL instruction.*<sup>2</sup> *Note that executing the QED test* i = iO,1, iO,<sup>2</sup> :: iD,1, iD,<sup>2</sup> *in a QED-consistent initial state produces a QED-consistent final state: the bug is not triggered by* i *because* iD,<sup>1</sup> *is executed between* iO,<sup>2</sup> *and* iD,2*. A slightly longer test* i = iO,2, iO,1, iO,<sup>2</sup> :: iD,2, iD,1, iD,<sup>2</sup> *does trigger the bug, however, because the subsequence* iO,2, iD,<sup>2</sup> *of two back-toback MULs causes the first duplicate instruction* iD,<sup>2</sup> *in* i *to produce an incorrect result at* l31*. This incorrect result then propagates through the next two instructions, resulting in a QED-inconsistent final state since the values at* l<sup>15</sup> *and* l31*, i.e., the output locations of* iO,<sup>2</sup> *and* iD,2*, differ.*

QED-consistency is the universal, implementation-independent property that is checked in SQED. In practice, the property must refer to some basic information about the design such as, e.g., symbolic register names, but this can be generated automatically from a high-level ISA description [10]. BMC

<sup>1</sup>This model is used for simplicity, but it could easily be extended to allow instructions with additional inputs or outputs.

<sup>2</sup>This scenario corresponds to a real bug in an out-of-order RISC-V design detected by SQED: https://github.com/ridecore/ridecore/issues/4.

Fig. 1. SQED workflow from a theoretical perspective (a) and illustration of executing the QED test i = i<sup>O</sup> :: i<sup>D</sup> in Example 2 (b).

is used to symbolically and exhaustively generate all possible QED tests up to a certain length 2n (the BMC bound). BMC ensures that SQED will find the shortest possible failing QED test first. The high-level workflow shown in Fig. 1a allows for flexibility in choosing the partition and mapping between original and duplicate locations. We rely on this flexibility for the results in this paper (Theorems 1 and 2). Current SQED implementations use a predefined partition and mapping, based on which BMC enumerates all possible QED tests. Extending implementations to have the BMC tool also choose a partition and mapping could be explored in future work.

We refer to related work [7], [9], [12] for case studies that demonstrate the effectiveness of BMC-based SQED on a variety of processor designs. The scalability of SQED in practice is determined by the scalability of the BMC tool being used. Thus, approaches for improving scalability of BMC can also be applied to SQED, e.g. abstraction, decomposition, and partial instantiation techniques [7].

#### III. INSTRUCTION AND PROCESSOR MODEL