Abstract Symbolic Machine Learning Prover (SMLP)is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a grey-box approach: SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system’s response. SMLP has been applied in industrial setting at Intel for analyzing and optimizing hardware designs at the analog level. SMLP is a general purpose tool and can be applied to any system that can be sampled and modeled by machine learning models.

Application domains of Bayesian optimization include optimizing black-box functions or very complex functions. The functions we are interested in describe complex real-world systems applied in industrial settings. Even though they do have explicit representations, standard optimization techniques fail to provide validated solutions and correctness guarantees for them. In this paper we present a combination of Bayesian optimization and SMT-based constraint solving to achieve safe and stable solutions with optimality guarantees.

Combining machine learning with constraint solving and formal methods is an interesting new direction in research with a wide range of safety critical applications.Our focus in this work is on analyzing Neural Networks with Rectified Linear Activation Function (NN-ReLU).The existing, very recent research works in this direction describe multiple approaches to satisfiability checking for constraints on NN-ReLU output.Here we extend this line of work in two orthogonal directions: We propose an algorithm for finding configurations of NN-ReLU that are (1) safe and (2) stable.We assume that the inputs of the NN-ReLU are divided into existentially and universally quantified variables, where the former represent the parameters for configuring the NN-ReLU and the latter represent (possibly constrained) free inputs.We are looking for (1) values of the configuration parameters for which the NN-ReLU output satisfies a given constraint for any legal values of the input variables (the safety requirement); and (2) such that the entire family of configurations with configuration variable values close to a safe configuration is also safe (the stability requirement).To our knowledge this is the first work that proposes SMT-based algorithms for searching safe and stable configuration parameters for systems modelled using neural networks.We experimentally evaluate our algorithm on NN-ReLUs trained on a set of real-life datasets originating from an industrial CAD application at Intel.

We propose a supervised learning algorithm whose aim is to derive features that explain the response variable better than the original features. Moreover, when there is a meaning for positive vs negative samples, our aim is to derive features that explain the positive samples, or subsets of positive samples that have the same root-cause. Each derived feature represents a single or multi-dimensional subspace of the feature space, where each dimension is specified as a feature-range pair for numeric features, and as a feature-level pair for categorical features. Unlike most Rule Learning and Subgroup Discovery algorithms, the response variable can be numeric, and our algorithm does not require a discretization of the response. The algorithm has been applied successfully to numerous real-life root-causing tasks in chip design, manufacturing, and validation, at Intel.

In current SoCs, key infrastructure capabilities are distributed across many components and involve tight software, firmware, and hardware interaction. Examples include resets, power management, security, and more. The architectural complexity of these features often results in specification errors that when found quite late in the product life cycle are very costly to fix. This means that we have to find ways to analyze the architectural specification and not only the implementation. To address these issues, we describe a framework called iPave that supports the following capabilities: (1) A common, formal system-level specification serving as a contract between different design teams; (2) Specification analysis with focus on cross-component assumptions and dependencies; and (3) A method to reuse the specification as a global checker to assure that the implementation is compliant with the specification across all validation platforms (simulation, emulation, silicon). At the front end of this framework we have an intuitive visual formalism, iFlow, which makes it easy for architects to specify system-level protocols, while at the back end we have a new logical formalism, called Logic Sequence Diagrams (LSDs), which enables formal compliance checking across different validation platforms.

Symbolic Trajectory Evaluation is an industrial-strength verification method, based on symbolic simulation and abstraction, that has been highly successful in data path verification, especially microprocessor execution units. These correctness results are typically obtained under certain assumptions about how the verified hardware block's inputs are driven, as well as assumptions about the values of these inputs. For correct overall operation, the hardware environment within which the verified block resides is expected to satisfy these assumptions. We describe a translation of these proof assumptions into System Verilog Assertions. These are then used as checkers in dynamic validation of the hardware environment within which blocks verified by Symbolic Trajectory Evaluation operate. The result is a pragmatic assume-guarantee method that increases the quality and confidence in verification results, requires little or no modification to the Symbolic Trajectory Evaluation proofs, and leverages pre-existing dynamic validation infrastructure.

We propose an equivalence checking theory in a wider-than-usual sense. The theory shows how to combine Formal Equivalence Checking (FEC) of specification and implementation models with Assertion Based Verification (ABV) of the specification model, and with Reboot Sequence Checking (RSC) on both models, to ensure that the implementation model has the intended logic functionality. Here, FEC is performed to ensure that the input-output behavior of the models coincides in post-reboot states. ABV ensures that the specification model has the intended logic functionality captured by temporal assertions. RSC ensures deterministic behavior of the models after reboot. We propose a flexible compositional theory for FEC, an abstraction method for ABV, and a scalable algorithm for RSC, enabling performance of all three activities in a modular, compositional manner, and largely independently: FEC and ABV are performed without knowing the actual reboot sequence (and the respective initial states) of the two models; and FEC, ABV and RSC have the same observables.

We propose a new method for equivalence checking of RTL and schematic descriptions of memories using translation into first-order logic. Our method is based on a powerful abstraction of memories and address decoders within them. We propose two ways of axiomatizing some of the bit-vector operations, decoders, and memories. The first axiomatization uses an algebra of operations on bit-vectors. The second axiomatization considers a bit-vector as a unary relation and memory as a relation of larger arity. For some designs, including real-life designs, the second axiomatization results in a first-order problem falling into a known decidable fragment of first-order logic and suitable for solving by modern first-order provers. Equivalence of real-life memories can be verified in seconds with our approach.

Automatic synchronization (or reset) of sequential synchronous circuits is considered one of the most challenging tasks in the domain of formal sequential equivalence verification of hardware designs. Earlier attempts were based on Binary Decision Diagrams (BDDs) or classical reachability analysis, which by nature suffer from capacity limitations. A previous attempt to attack this problem using non-BDD based techniques was essentially a collection of heuristics aimed at toggling of the latches, and it is not guaranteed that a synchronization sequence will be computed if it exists. In this paper we present a novel approach for computing reset sequences (and reset states) in order to perform sequential hardware equivalence verification between circuit models. This approach is based on the dual-rail modeling of circuits and utilizes efficient SAT-based engines for Bounded Model Checking (BMC). It is implemented in Intel's sequential verification tool, Seqver, and has been proven to be highly successful in proving the equivalence of complex industrial designs. The synchronization method described in this paper can be used in many other CAD applications, including formal property verification, automatic test generation, and power estimation.

We introduce a finer concept of a hardware machine, where the set of post-reboot operation states is explicitly a part of the FSM definition. We formalize an ad-hoc flow of combinational equivalence verification of hardware, the way it was performed over the years in the industry. We define a concept of post-reboot bisimulation, which better suits the hardware machines, and show that a right form of combinational equivalence is in fact a form of post-reboot bisimulation. Further, we show that alignability equivalence is a form of post-reboot bisimulation, too, and the latter is a refinement of alignability in the context of compositional hardware verification. We find that post-reboot bisimulation has important advantages over alignability also in the wider context of formal hardware verification, where equivalence verification is combined with formal property verification and with validation of a reboot sequence. As a result, we propose a more comprehensive, compositional, and fully-formal framework for hardware verification. Our results are extendible to other forms of labeled transition systems and adaptable to other forms of bisimulation used to model and verify complex hardware and software systems

This paper addresses the problem of formal equivalence verification of hardware designs. Traditional methods and tools which perform equivalence verification are commonly based on combinational equivalence verification (CEV) methods. We however present a novel method and tool (Seqver) for performing sequential equivalence verification (SEV). The theory behind Seqver is based on the alignability theory, however in this paper we present a refinement to that theory: strong alignability, which introduces a concept of automatic model synchronization to the verification process. Automatic synchronization (reset) of sequential synchronous circuits is considered as one of the most challenging tasks in the domain of sequential equivalence verification. Earlier attempts were based on BDDs or classical reachability analysis, which by nature suffer from capacity limitations. Seqver is empowered with hybrid verification engines which combine state of the art SAT and BDD based engines for performing synchronization and verification. Seqver is widely used today in Intel for formally verifying leading next generation CPU designs.

We are interested in sequential hardware equivalence (or alignability equivalence) verification of synchronous sequential circuits as stated in C. Pixley (1992). To cope with large industrial designs, the circuits must be divided into smaller subcircuits and verified separately. Furthermore, in order to succeed in verifying the subcircuits, design constraints must be added to the subcircuits. These constraints mimic "essential" behavior of the subcircuit environment. In this work, we extend the classical alignability theory in the presence of design constraints, and prove a compositionality result allowing inferring alignability of the circuits from alignability of the subcircuits. As a result, we build a divide and conquer framework for alignability verification. This framework is successfully used on Intel designs.

In orthogonal expression reduction systems, a common generalization of term rewriting and λ-calculus, we extend the concepts of normalization and needed reduction by considering, instead of the set of normal forms, a set S of 'results'. When S satisfies some simple axioms which we call stability, we prove the corresponding generalizations of some fundamental theorems: the existence of needed redexes, that needed reduction is normalizing, the existence of minimal normalizing reductions, and the optimality theorem.

Some λ-terms exhibit the following alternation property: whenever a redex having the shape (λx.P) (λy.Q) is created in a reduction path starting with the contraction of M N, then either λx appears in M and λy in N, or λx appears in N and λy in M. In this paper, we investigate the alternation property and we establish its relevance in the context of typed calculi. In particular, we prove that the alternation property implies normalization. To this aim, we use a simple technique based on labels. The intended meaning of the labelling is to give information about the minimal number of contractions needed by a variable to be substituted during the reduction process. Further, we apply this result to obtain new normalization proofs for Curry's simply typed lambda calculus and, similarly, for terms typable with intersection types.