Exploring formal verification methodology for FPGA-based digital systems.

We perform formal verification of quantum circuits by integrating several techniques specialized to particular classes of circuits. Our verification methodology is based on the new notion of a reversible miter that allows one to leverage existing techniques for simplification of quantum circuits. For reversible circuits which arise as runtime bottlenecks of key quantum algorithms, we develop several verification techniques and empirically compare them. We also combine existing quantum verification tools with the use of SAT-solvers. Experiments with circuits for Shor's number-factoring algorithm, containing thousands of gates, show improvements in efficiency by four orders of magnitude.

Download Full-text

A Formal Verification Methodology for DDD Mode Pacemaker Control Programs

Journal of Electrical and Computer Engineering ◽

10.1155/2015/939028 ◽

2015 ◽

Vol 2015 ◽

pp. 1-10 ◽

Cited By ~ 5

Author(s):

Sana Shuja ◽

Sudarshan K. Srinivasan ◽

Shaista Jabeen ◽

Dharmakeerthi Nawarathna

Keyword(s):

Formal Verification ◽

Control Program ◽

Formal Specifications ◽

Object Code ◽

Correctness Proof ◽

Safety Critical ◽

Control Programs ◽

Control Functions ◽

Verification Process ◽

Verification Methodology

Pacemakers are safety-critical devices whose faulty behaviors can cause harm or even death. Often these faulty behaviors are caused due to bugs in programs used for digital control of pacemakers. We present a formal verification methodology that can be used to check the correctness of object code programs that implement the safety-critical control functions of DDD mode pacemakers. Our methodology is based on the theory of Well-Founded Equivalence Bisimulation (WEB) refinement, where both formal specifications and implementation are treated as transition systems. We develop a simple and general formal specification for DDD mode pacemakers. We also develop correctness proof obligations that can be applied to validate object code programs used for pacemaker control. Using our methodology, we were able to verify a control program with millions of transitions against the simple specification with only 10 transitions. Our method also found several bugs during the verification process.

Download Full-text

Dependent types and formal synthesis

Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences ◽

10.1098/rsta.1992.0029 ◽

1992 ◽

Vol 339 (1652) ◽

pp. 121-135 ◽

Cited By ~ 2

Keyword(s):

Formal Verification ◽

Effective Means ◽

Order Logic ◽

Digital Systems ◽

Heuristic Methods ◽

Dependent Types ◽

Higher Order Logic ◽

Type Checking ◽

Formal Synthesis ◽

Starting Point

The relative advantages offered by the use of dependent types (rather than polymorphic ones) in a higher-order logic used for reasoning about digital systems are explored. Dependent types and subtypes are shown to provide an effective means of expressing the bounded, parametrized types typically encountered in this field. Heuristic methods can be used to minimize problems arising from the loss of decidable type-checking. A second topic discussed is formal synthesis, an approach to design in which the activities of behavioural synthesis and of formal verification are combined. The starting point is a behavioural specification, the end result is a specification of an implementation together with a proof of its correctness.

Download Full-text