INDUCTION-ORIENTED VERIFICATION OF REPLICATED ARCHITECTURES DESCRIBED IN VHDL

This paper is concerned with the application of theorem proving techniques to the formal proof of hardware. More precisely, we aim at providing a methodology for applying provers like Nqthm or Acl2 to the formal verification of parameterized replicated circuits. Nqthm (the Boyer–Moore theorem prover) and its successor Acl2 are induction-based systems; their formalisms are respectively a simplified Lisp-like language and Common Lisp. Hence, the circuits we consider must be given a purely functional representation. Moreover, our work puts the emphasis on the integration of formal proof techniques in CAD (Computer Aided Design) environments which support Hardware Description Languages in which replication is expressed by iteration. Therefore, we associate with the iterative statement of the VHDL language a functional semantics that guarantees an easy translation from VHDL to Nqthm/Acl2 while simplifying the subsequent inductive proofs. The approach has been successfully applied to one-dimensional as well as two-dimensional structures.

Download Full-text

A hierarchical approach to digital design using computer-aided design and hardware description languages

FIE'99 Frontiers in Education. 29th Annual Frontiers in Education Conference. Designing the Future of Science and Engineering Education. Conference Proceedings (IEEE Cat. No.99CH37011 ◽

10.1109/fie.1999.840442 ◽

2003 ◽

Cited By ~ 6

Author(s):

W. Kleinfelder ◽

D. Gray ◽

G. Dudevoir

Keyword(s):

Computer Aided Design ◽

Digital Design ◽

Hardware Description Languages ◽

Hierarchical Approach ◽

Computer Aided ◽

Hardware Description ◽

Description Languages ◽

Aided Design

Download Full-text

Invariant-Based Safety Assessment of FPGA Projects: Conception and Technique

Computers ◽

10.3390/computers10100125 ◽

2021 ◽

Vol 10 (10) ◽

pp. 125

Author(s):

Vyacheslav Kharchenko ◽

Oleg Illiashenko ◽

Vladimir Sklyar

Keyword(s):

Computer Aided Design ◽

Safety Assessment ◽

Theoretical Research ◽

Systems Software ◽

Field Programmable ◽

Information Management Systems ◽

Programmable Gate Arrays ◽

Hardware Description ◽

Description Languages ◽

Aided Design

This paper describes a proposed method and technology of safety assessment of projects based on field programmable gate arrays (FPGA). Safety assessment is based on special invariants, e.g., properties which remain unchanged when a specified transformation is applied. A classification and examples of FPGA project invariants are provided. In the paper, two types of invariants are described. The first type of invariants used for such assessment are those which are versatile since they reflect the unchanged properties of FPGA projects, hardware description languages, etc. These invariants can be replenished as experience gained in project implementation accumulates. The second type of invariants is formed based on an analysis of the specifics of a particular FPGA project and reflects the features of the tasks to be solved, the algorithms that are implemented, the hardware FPGA chips used, and the computer-aided design tools, etc. The paper contains a description of the overall conception and particular stages of FPGA projects invariant-based safety assessment. As examples for solving some tasks (using of invariants and defect injections), the paper contains several algorithms written in the VHSIC hardware description language (VHDL). The paper summarizes the results obtained during several years of practical and theoretical research. It can be of practical use for engineers and researchers in the field of quality, reliability, and security of embedded systems, software and information management systems for critical and business applications.

Download Full-text