A Multiple-Valued Logic Approach to the Design and Verification of Hardware Circuits
| Autor: | Amnon Rosenmann |
|---|---|
| Rok vydání: | 2015 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science B.5.2 Theoretical computer science B.7.2 Logic Computer science I.6.3 Applied Mathematics Degree of truth Computation 010102 general mathematics Binary number Initialization 02 engineering and technology 01 natural sciences 020202 computer hardware & architecture Logic in Computer Science (cs.LO) 0202 electrical engineering electronic engineering information engineering Canonical form Boolean expression Hardware circuits 0101 mathematics Equivalence (formal languages) |
| DOI: | 10.48550/arxiv.1502.05748 |
| Popis: | We present a novel approach, which is based on multiple-valued logic (MVL), to the verification and analysis of digital hardware designs, which extends the common ternary or quaternary approaches for simulations. The simulations which are performed in the more informative MVL setting reveal details which are either invisible or harder to detect through binary or ternary simulations. In equivalence verification, detecting different behavior under MVL simulations may lead to the discovery of a genuine binary nonequivalence or to a qualitative gap between two designs. The value of a variable in a simulation may hold information about its degree of truth and its "place of birth" and "date of birth." Applications include equivalence verification, initialization, assertions generation and verification, partial control on the flow of data by prioritizing and block-oriented simulations. Much of the paper is devoted to theoretical aspects behind the MVL approach, including the reason for choosing a specific algebra for computations, and the introduction of the verification complexity of a Boolean expression. Two basic algorithms are presented. Comment: 34 pages, 4 figures |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|