Formal Verification of a Pipelined Cryptographic Circuit Using Equivalence Checking and Completion Functions

2007 ◽  
Author(s):  
Chiu Hong Lam ◽  
Mark D. Aagaard
Keyword(s):  
Formal Verification ◽  
Equivalence Checking ◽  
Completion Functions

scholarly journals Fast equivalence -- checking for quantum circuits

2010 ◽  
Vol 10 (9&10) ◽  
pp. 721-734
Author(s):  
Shigeru Yamashita ◽  
Igor L. Markov
Keyword(s):  
Formal Verification ◽  
Quantum Algorithms ◽  
Quantum Circuits ◽  
Equivalence Checking ◽  
Sat Solvers ◽  
Reversible Circuits ◽  
Verification Tools ◽  
Verification Methodology ◽  
Verification Techniques ◽  
Factoring Algorithm

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.

Industrial Experience with Formal Verification (Industrielle Erfahrungen mit Formaler Verifikation)

2001 ◽  
Vol 43 (1) ◽  
Author(s):  
Michael Payer
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Equivalence Checking ◽  
Functional Equivalence ◽  
Design Environment ◽  
Popular Method ◽  
The Past ◽  
Formal Equivalence ◽  
Functional Simulation ◽  
Low Coverage

In recent years, Formal Verification has become an increasingly popular method to verify the functional equivalence of different design views. Just recently, designers also start to speak about Model Checking, a methodology that allows to analyze functional properties of a design. In the past both, equivalence checking and property checking, have been carried out with functional simulation; with today′s designs of several 100K or even Mio. gates this is not feasible anymore. The main reasons are the unsatisfactory runtime and the low coverage of this approach. In this paper, I will report experiences with Formal Equivalence Verification in an industrial design environment.

scholarly journals Token-Aware Completion Functions for Elastic Processor Verification

2009 ◽  
Vol 2009 ◽  
pp. 1-5 ◽  
Author(s):  
Sudarshan K. Srinivasan ◽  
Koushik Sarker ◽  
Rajendra S. Katti
Keyword(s):  
Formal Verification ◽  
Systematic Approach ◽  
Data Flow ◽  
Instruction Set ◽  
Model Data ◽  
Instruction Set Architecture ◽  
Processor Verification ◽  
Elastic Systems ◽  
Processor Designs ◽  
Completion Functions

We develop a formal verification procedure to check that elastic pipelined processor designs correctly implement their instruction set architecture (ISA) specifications. The notion of correctness we use is based on refinement. Refinement proofs are based on refinement maps, which—in the context of this problem—are functions that map elastic processor states to states of the ISA specification model. Data flow in elastic architectures is complicated by the insertion of any number of buffers in any place in the design, making it hard to construct refinement maps for elastic systems in a systematic manner. We introduce token-aware completion functions, which incorporate a mechanism to track the flow of data in elastic pipelines, as a highly automated and systematic approach to construct refinement maps. We demonstrate the efficiency of the overall verification procedure based on token-aware completion functions using six elastic pipelined processor models based on the DLX architecture.

A New Verification Method of Digital Circuits Based on Cone-Oriented Partitioning and Decision Diagrams

2010 ◽  
Vol 29-32 ◽  
pp. 1040-1045
Author(s):  
Zhong Liang Pan ◽  
Ling Chen
Keyword(s):  
Formal Verification ◽  
Circuit Design ◽  
Digital Circuits ◽  
Experimental Results ◽  
Equivalence Checking ◽  
Decision Diagrams ◽  
Circuit Partitioning ◽  
Circuit Verification ◽  
Verification Method ◽  
Signal Line

The formal verification is able to check whether the implementation of a circuit design is functionally equivalent to an earlier version described at the same level of abstraction, it can show the correctness of a circuit design. A new circuit verification method based on cone-oriented circuit partitioning and decision diagrams is presented in this paper. First of all, the structure level of every signal line in a circuit is computed. Secondly, the circuit is partitioned into a lot of cone structures. The multiple-valued decision diagram corresponding to every cone structure is generated. The verification procedure is to compare the equivalence of the multiple-valued decision diagrams of two types of cone structures. Experimental results on a lot of benchmark circuits show the method presented in this paper can effectively perform the equivalence checking of circuits.

Formal verification of code motion techniques using data-flow-driven equivalence checking

2012 ◽  
Vol 17 (3) ◽  
pp. 1-37 ◽  
Author(s):  
Chandan Karfa ◽  
Chittaranjan Mandal ◽  
Dipankar Sarkar
Keyword(s):  
Formal Verification ◽  
Data Flow ◽  
Equivalence Checking ◽  
Using Data ◽  
Code Motion

Formal Verification for Nonlinear Analog Systems: Approaches to Model and Equivalence Checking

2006 ◽  
pp. 205-245 ◽  
Author(s):  
Walter Hartong ◽  
Ralf Klausen ◽  
Lars Hedrich
Keyword(s):  
Formal Verification ◽  
Equivalence Checking ◽  
Systems Approaches ◽  
Analog Systems ◽  
Nonlinear Analog
Sign in / Sign up

Export Citation Format

Share Document