Probabilistic verification of Boolean functions

We present a novel method for verifying the equivalence of two Boolean functions. Each function is hashed to an integer code by assigning random integer values to the input variables and evaluating an integer-valued transformation of the original function. The hash codes for two equivalent functions are always equal. Thus the equivalence of two functions can be verified with a very low probability of error, which arises from unlikely collisions between inequivalent functions. An upper bound, , on the probability of error is known a priori. The bound can be decreased exponentially by making multiple runs. Results indicate significant time and space advantages for this method over techniques that represent each function as a single OBDD. Some functions known to require space (and time) exponential in the number of input variables for these techniques require only polynomial resources using our method. Experimental results indicate that probabilistic verification can provide an attractive alternative for verifying functions too large to be handled using these OBDD-based techniques.     

Project verification and construction of superchip tests at the RTL level

Methods were proposed for project verification and directed design of the superchip tests represented in VHDL at the RTL level. The problem of test design and project verification was solved on the basis of the CNF-satisfiability of some system of Boolean functions.     

A novel formal verification approach for RTL hardware IP cores

We present a promising formal verification methodology based on the inductive approach using the imPROVE-HDL tool. This methodology is dedicated for RTL IPs or IP-based digital/logic hardware designs to prove the correctness of their temporal properties related to the control-dominated architecture model. Each temporal property can be checked through the IP interface where all properties have to be proved or disproved. We developed a new methodology to generate the appropriate environment of the IP interface according to the design context (master, slave, arbiter and decoder) before starting the verification of all properties one by one. When all temporal properties are verified, we generate some test sequences that contain a complex scenario to check the compatibility between all properties. We implemented our methodology to generate the appropriate environment and applied the inductive approach to verify various properties of two real IP designs using the imPROVE-HDL tool developed by TNI-Valiosys. The first design is an RTL IP-based digital hardware dedicated for real time video processing, where the second one performs an AHB to AHB Bridge. On these designs, we successfully proved few properties and discovered a design violation.     

The equivalence of Horn and network complexity for Boolean functions

Summary We propose in this paper a logical complexity measure — Horn complexity — for Boolean functions which measures the minimal length of quasi-Horn definitions of such functions by propositional formulae. The interest for this complexity measure comes on the one hand from the observation that the satisfiability problem for Horn formulae is in P, on the other hand from a strong connection to Cook's problem. We show the proposed Horn complexity to be polynomially equivalent to network complexity and therefore to Turing complexity for Boolean functions.A preliminary version of this work has appeared in the Proceedings of the 5^th Scandinavian Logic Symposium, edited by B. Mayoh and F. Jensen, Aalborg University Press, Aalborg 1979     

On affine (non)equivalence of Boolean functions

In this paper we construct a multiset S(f) of a Boolean function f consisting of the weights of the second derivatives of the function f with respect to all distinct two-dimensional subspaces of the domain. We refer to S(f) as the second derivative spectrum of f. The frequency distribution of the weights of these second derivatives is referred to as the weight distribution of the second derivative spectrum. It is demonstrated in this paper that this weight distribution can be used to distinguish affine nonequivalent Boolean functions. Given a Boolean function f on n variables we present an efficient algorithm having O(n2²ⁿ ) time complexity to compute S(f). Using this weight distribution we show that all the 6-variable affine nonequivalent bents can be distinguished. We study the subclass of partial-spreads type bent functions known as PS _ap type bents. Six different weight distributions are obtained from the set of PS _ap bents on 8-variables. Using the second derivative spectrum we show that there exist 6 and 8 variable bent functions which are not affine equivalent to rotation symmetric bent functions. Lastly we prove that no non-quadratic Kasami bent function is affine equivalent to Maiorana–MacFarland type bent functions.     

Lightweight and static verification of UML executable models

Executable models play a key role in many software development methods by facilitating the (semi)automatic implementation/execution of the software system under development. This is possible because executable models promote a complete and fine-grained specification of the system behaviour. In this context, where models are the basis of the whole development process, the quality of the models has a high impact on the final quality of software systems derived from them. Therefore, the existence of methods to verify the correctness of executable models is crucial. Otherwise, the quality of the executable models (and in turn the quality of the final system generated from them) will be compromised. In this paper a lightweight and static verification method to assess the correctness of executable models is proposed. This method allows us to check whether the operations defined as part of the behavioural model are able to be executed without breaking the integrity of the structural model and returns a meaningful feedback that helps repairing the detected inconsistencies.     

A UML-based static verification framework for security

Secure software engineering is a new research area that has been proposed to address security issues during the development of software systems. This new area of research advocates that security characteristics should be considered from the early stages of the software development life cycle and should not be added as another layer in the system on an ad-hoc basis after the system is built. In this paper, we describe a UML-based Static Verification Framework (USVF) to support the design and verification of secure software systems in early stages of the software development life-cycle taking into consideration security and general requirements of the software system. USVF performs static verification on UML models consisting of UML class and state machine diagrams extended by an action language. We present an operational semantics of UML models, define a property specification language designed to reason about temporal and general properties of UML state machines using the semantic domains of the former, and implement the model checking process by translating models and properties into Promela, the input language of the SPIN model checker. We show that the methodology can be applied to the verification of security properties by representing the main aspects of security, namely availability, integrity and confidentiality, in the USVF property specification language.     

A formal verification framework for static analysis

Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of-the-art static analyzers typically combine a range of complex techniques, make use of external tools, and evolve quickly. To formally verify such systems is not a realistic option. In this work, we propose a different approach whereby, instead of the tools, we formally verify the results of the tools. The central idea of such a formal verification framework for static analysis is the method-wise translation of the information about a program gathered during its static analysis into specification contracts that contain enough information for them to be verified automatically. We instantiate this framework with costa, a state-of-the-art static analysis system for sequential Java programs, for producing resource guarantees and KeY, a state-of-the-art verification tool, for formally verifying the correctness of such resource guarantees. Resource guarantees allow to be certain that programs will run within the indicated amount of resources, which may refer to memory consumption, number of instructions executed, etc. Our results show that the proposed tool cooperation can be used for automatically producing verified resource guarantees.     

Experience of improving the blast static verification tool

The BLAST static verification tool is one of the open-source verifiers of software written in C. The paper describes principles of BLAST implementation, the limitations revealed in the course of its practical use in the verification of the Linux operating system drivers, and an attempt to improve BLAST in the framework of the Linux Driver Verification (LDV) project [3].     

Using linux device drivers for static verification tools benchmarking

The Linux Driver Verification system is designed for static analysis of the source code of Linux kernel space device drivers. In this paper, we describe the architecture of the verification system, including the integration of third-party tools for static verification of C programs. We consider characteristics of the Linux drivers source code that are important from the viewpoint of verification algorithms and give examples of comparative analysis of different verification tools, as well as different versions and configurations of a given tool.     

Application of BDDs in Boolean matching techniques for formal logic combinational verification

Verifying that an implementation of a combinational circuit meets its golden specification is an important step in the design process. As inputs and outputs can be swapped by synthesis tools or by interaction of the designer, the correspondence between the inputs and the outputs of the synthesized circuit and the inputs and the outputs of the golden specification has to be restored before checking equivalence. In this paper, we review the main approaches to this isomorphism problem and show how to apply OBDDs in order to obtain efficient methods. Published online: 15 May 2001     

Enhanced equivalence checking: toward a solidarity of functional verification and manufacturing test generation

This article, from the Motorola (now Freescale) PowerPC design group, presents an interesting synergy among test, equivalence verification, and constraints. The authors use RTL, gate, and switch models of a design in two different flows one for test and one for functional verification to show that rectifying constraints and merging tests between the-two flows saves significant presilicon debug effort.     

VHDL RT级可测性检查和改进

在VHDL RT级综合的基础上，提出了在RT级进行电路可测性检查和改进方法。与一般的可测性分析方法不同，该文不是基于对电路的可控制性和可观察性的量化分析，而是通过检查和改进可测性不佳的局部设计，使得整体电路的可测性得到提升，达到高故障覆盖率。     

Reducing the verification cost of evolving product families using static analysis techniques

Software product line engineering enables proactive reuse among a set of related products through explicit modeling of commonalities and differences among them. Software product lines are intended to be used in a long period of time. As a result, they evolve over time, due to the changes in the requirements. Having several individual products in a software family, verification of the entire family may take a considerable effort. In this paper we aim to decrease this cost by reducing the number of verified products using static analysis techniques. Furthermore, to reduce model checking costs after product line evolution, we restrict the number of products that should be re-verified by reusing the previous verification result. All proposed techniques are based on static analysis of the product family model with respect to the property and can be automated. To show the effectiveness of these techniques we apply them on a set of case studies and present the results.     

Boolean sets and most general solutions of Boolean equations

The aim of this paper is twofold. First we determine the most general form of the subsumptive general solution of a Boolean equation (Theorem 1 and Theorem 2). Then we discuss several characterizations of Boolean sets, meaning sets of zeros of Boolean functions, and prove that every Boolean transformation X=Φ(T) is the parametric general solution of a certain Boolean equation.     

Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges

We present a combination of approaches for the verification of event-condition-action (ECA) systems. The analyzed ECA systems range from structurally simple to structurally complex systems. We address the verification of reachability properties and behavioral properties. Reachability properties are represented by assertions in the program and we determine statically whether an assertion holds for all execution paths. Behavioral properties are represented as linear temporal logic formulas specifying the input/output behavior of the program. Our approach assumes a finite state space. We compare a symbolic analysis with an exhaustive state space exploration and discuss the trade-offs between the approaches in terms of the number of computed states and run-time behavior. All variants compute a state transition graph which can also be passed to an LTL verifier. The variants have a different impact on the number of computed states in the state transition graph which in turn impacts the run-time and memory consumption of subsequent phases. We evaluate the different analysis variants with the RERS benchmarks.     

基于RTL8019的ARM和PC机间的TCP/IP通信

介绍以太网控制芯片RTL8019AS的初始化;介绍EasyARM2210控制RTL8019AS实现与PC机通信的硬件设计方案;为实现EasyARM2210和PC机的通信,采用C语言编写程序实现相互通信,并进行了实验结果验证。证明通过网络能够良好通信。     

完全RTL的故障数目预测及故障覆盖率计算

在超大规模集成电路设计过程中,门级故障仿真通常因仿真速度太慢而不能满足市场需求,因此近年来寄存器传输级(RTL)故障仿真成了一个研究热点．已有的RTL的故障模型和故障仿真方法在计算系统的故障覆盖率时,对故障数目或者加权系数的计算需要将RTL设计综合到门级．文中在信号位宽和运算符类型的基础上,提出了一种在RTL预测故障数的手段,并由此得到完全RTL的故障覆盖率计算方法．实验结果证明了该方法的有效性．