Polynomial Formal Verification Drechsler, Rolf; Mahzoon, Alireza
2022 IEEE/ACM International Conference On Computer Aided Design (ICCAD),
10/2022
Conference Proceeding
Recently, a lot of effort has been put into developing formal verification approaches by both academic and industrial research. In practice, these techniques often give satisfying results for some ...types of circuits, while they fail for others. A major challenge in this domain is that the verification techniques suffer from unpredictability in their performance. The only way to overcome this challenge is the calculation of bounds for the space and time complexities. If a verification method has polynomial space and time complexities, scalability can be guaranteed.
In this tutorial paper, we review recent developments in formal verification techniques and give a comprehensive overview of Polynomial Formal Verification (PFV). In PFV, polynomial upper bounds for the run-time and memory needed during the entire verification task hold. Thus, correctness under resource constraints can be ensured. We discuss the importance and advantages of PFV in the design flow. Formal methods on the bit-level and the word-level, and their complexities when used to verify different types of circuits, like adders, multipliers, or ALUs are presented. The current status of this new research field and directions for future work are discussed.
Hardware verification requires a lot of effort. A recent study showed that on average, there are more verification engineers working on a project than design engineers. Hence, one of the biggest ...challenges in design and verification today is to find new ways to increase the productivity. For software development the agile methodology as an incremental approach has been proposed and is heavily used. Behavior Driven Development (BDD) as an agile technique additionally enables a direct link to natural language based testing. In this article, we show how BDD can be extended to make it viable for hardware design. In addition, we present a two-fold strategy which allows to specify textual acceptance tests and textual formal properties. Finally, this strategy is complemented by methods to generalize tests to properties, and to enhance design understanding by presenting debug and witness scenarios in natural language.
The identification of power-risky test patterns is a crucial task in the design phase of digital circuits. Excessive test power could lead to test failures due to IR-drop, noise, etc. This has to be ...avoided to prevent yield loss and chip damages. However, the accurate power simulation of all test patterns to identify power-risky patterns as well as to find critical areas within each pattern is not possible due to run time and resource constraints. An important task is therefore the selection of a subset of potentially power-risky patterns, which will be simulated in an accurate manner. In this paper, we propose an independent test pattern analysis methodology for the integration into an existing industrial design flow. The proposed test pattern analysis technique is a lightweight method based on the cell's Transient Power Activity (TPA) to identify potentially power-risky patterns. The method uses layout and power information to identify critical power activity areas using machine learning techniques. Experiments were performed on opensource benchmarks as well as on an industrial design. The results were correlated with commercial power and IR-drop simulation tools. The proposed methodology was found to be effective in terms of speed and localization of the critical areas for unsafe patterns.
Recently, the concept of Polynomial Formal Verification (PFV) has been introduced and successfully applied to several classes of functions, allowing complete verification under resource constraints. ...But so far, all studies were carried out for combinational circuits only. In this paper we show how the concept of PFV can be extended to sequential circuits. As a first case study we show for counters that PFV can be performed, even though they have an exponential number of states, i.e., they can be fully formally verified within polynomial upper bounds on run-time and memory requirement.
With ReRAM being a non-volative memory technology, which features low power consumption, high scalability and allows for in-memory computing, it is a promising candidate for future computer ...architectures. Approximate computing is a design paradigm, which aims at reducing the complexity of hardware by trading off accuracy for area and/or delay.
In this article, we introduce approximate computing techniques to in-memory computing. We extend existing compilation techniques for the
(PLiM) computer architecture, by adapting state-of-the-art approximate computing techniques for arithmetic circuits. We use Cartesian Genetic Programming for the generation of approximate circuits and evaluate them using a Symbolic Computer Algebra-based technique with respect to error-metrics. In our experiments, we show that we can outperform state-of-the-art handcrafted approximate adder designs.
"Debugging becomes more and more the bottleneck to chip design productivity, especially while developing modern complex integrated circuits and systems at the Electronic System Level (ESL). Today, ...debugging is still an unsystematic and lengthy process. Sure, a simple reporting of a failure is not enough, anymore. Rather, it becomes more and more important not only to find many errors early during development but also to provide efficient methods for their isolation. In ""Debugging at the Electronic System Level"" the state-of-the-art of modeling and verification of ESL designs is reviewed. There, a particular focus is taken onto SystemC. Then, a reasoning hierarchy is introduced. The hierarchy combines well-known debugging techniques with whole new techniques to improve the verification efficiency at ESL. The proposed systematic debugging approach is supported amongst others by static code analysis, debug patterns, dynamic program slicing, design visualization, property generation, and automatic failure isolation. All techniques were empirically evaluated using real-world industrial designs. Summarized, the introduced approach enables a systematic search for errors in ESL designs. Here, the debugging techniques improve and accelerate error detection, observation, and isolation as well as design understanding."
With the rapid growth in the size and complexity of digital circuits, the possibility of bug occurrence has significantly increased. In order to avoid the enormous financial loss due to the ...production of buggy circuits, using scalable formal verification methods is essential. The scalability of a verification method for a specific design is proven by showing that the method has polynomial space and time complexities. Unfortunately, not all verification methods have a polynomial complexity, particularly when it comes to the verification of large and complex designs. In this paper, we propose a divide-and-conquer strategy for Polynomial Formal Verification (PFV) of complex circuits. Instead of using a monolithic proof engine to verify the entire design, we break the verification task down into several problems, which can be solved in polynomial space and time using a hybrid proof engine. As a case study, we investigate the PFV of the ALU in a RISC-V processor using our divide-and-conquer strategy.
Quantum-dot cellular automata (QCA) are an emerging field-coupled nanotechnology with remarkable performance and energy efficiency. In order to enable the exploration of this technology, we propose a ...model for the logic synthesis of QCA circuits that, for the first time, considers and abstracts all main physical aspects-in particular, energy dissipation. To this end, we review in detail how energy is dissipated in QCA cells and present a corresponding environment that allows for the estimation of the energy dissipation with respect to any specific set of technology parameters. Based on that, we derive a model for logic synthesis. A case study confirms the accuracy of the proposed model and reveals that interconnections have a significant impact in this technology-motivating a more rigorous consideration. These findings eventually provide the basis for a new generation of synthesis approaches at the logic level that are explicitly dedicated to QCA systems.
The development of computing machines found great success in the last decades. But the ongoing miniaturization of integrated circuits will reach its limits in the near future. Shrinking transistor ...sizes and power dissipation are the major barriers in the development of smaller and more powerful circuits. Reversible logic provides an alternative that may overcome many of these problems in the future. For low-power design, reversible logic offers significant advantages since zero power dissipation will only be possible if computation is reversible. Furthermore, quantum computation profits from enhancements in this area, because every quantum circuit is inherently reversible and thus requires reversible descriptions. However, since reversible logic is subject to certain restrictions (e.g. fanout and feedback are not directly allowed), the design of reversible circuits significantly differs from the design of traditional circuits. Nearly all steps in the design flow (like synthesis, verification, or debugging) must be redeveloped so that they become applicable to reversible circuits as well. But research in reversible logic is still at the beginning. No continuous design flow exists so far. In Towards a Design Flow for Reversible Logic, contributions to a design flow for reversible logic are presented. This includes advanced methods for synthesis, optimization, verification, and debugging. Formal methods like Boolean satisfiability and decision diagrams are thereby exploited. By combining the techniques proposed in the book, it is possible to synthesize reversible circuits representing large functions. Optimization approaches ensure that the resulting circuits are of small cost. Finally, a method for equivalence checking and automatic debugging allows to verify the obtained results and helps to accelerate the search for bugs in case of errors in the design. Combining the respective approaches, a first design flow for reversible circuits of significant size results. TOC:1. Introduction.- 2. Preliminaries.- 3. Synthesis of Reversible Logic.- 4. Exact Synthesis of Reversible Logic.- 5. Embedding of Irreversible Functions.- 6. Optimization.- 7. Formal Veri¿cation and Debugging.- 8. Summary and Conclusions.- References.- Index.
PDF
