61 |
Dominator-based Algorithms in Logic Synthesis and VerificationKrenz-Bååth, René January 2007 (has links)
Today's EDA (Electronic Design Automation) industry faces enormous challenges. Their primary cause is the tremendous increase of the complexity of modern digital designs. Graph algorithms are widely applied to solve various EDA problems. In particular, graph dominators, which provide information about the origin and the end of reconverging paths in a circuit graph, proved to be useful in various CAD (Computer Aided Design) applications such as equivalence checking, ATPG, technology mapping, and power optimization. This thesis provides a study on graph dominators in logic synthesis and verification. The thesis contributes a set of algorithms for computing dominators in circuit graphs. An algorithm is proposed for finding absolute dominators in circuit graphs. The achieved speedup of three orders of magnitude on several designs enables the computation of absolute dominators in large industrial designs in a few seconds. Moreover, the computation of single-vertex dominators in large multiple-output circuit graphs is considerably improved. The proposed algorithm reduces the overall runtime by efficiently recognizing and re-using isomorphic structures in dominator trees rooted at different outputs of the circuit graph. Finally, common multiple-vertex dominators are introduced. The algorithm to compute them is faster and finds more multiple-vertex dominators than previous approaches. The thesis also proposes new dominator-based algorithms in the area of decomposition and combinational equivalence checking. A structural decomposition technique is introduced, which finds all simple-disjoint decompositions of a Boolean function which are reflected in the circuit graph. The experimental results demonstrate that the proposed technique outperforms state-of-the-art functional decomposition techniques. Finally, an approach to check the equivalence of two Boolean functions probabilistically is investigated. The proposed algorithm partitions the equivalence check employing dominators in the circuit graph. The experimental results confirm that, in comparison to traditional BDD-based equivalence checking methods, the memory consumption is considerably reduced by using the proposed technique. / QC 20100804
|
62 |
Design, Implementation, and Formal Verification of On-demand Connection Establishment Scheme for TCP Module of MPICH2 LibraryMuthukrishnan, Sankara Subbiah 2012 August 1900 (has links)
Message Passing Interface (MPI) is a standard library interface for writing parallel programs. The MPI specification is broadly used for solving engineering and scientific problems on parallel computers, and MPICH2 is a popular MPI implementation developed at Argonne National Laboratory. The scalability of MPI implementations is very important for building high performance parallel computing applications. The initial TCP (Transmission Control Protocol) network module developed for Nemesis communication sub-system in the MPICH2 library, however, was not scalable in how it established connections: pairwise connections between all of an application's processes were established during the initialization of the application (the library call to MPI_Init), regardless of whether the connections were eventually needed or not.
In this work, we have developed a new TCP network module for Nemesis that establishes connections on-demand. The on-demand connection establishment scheme is designed to improve the scalability of the TCP network module in MPICH2 library, aiming to reduce the initialization time and the use of operating system resources of MPI applications. Our performance benchmark results show that MPI_Init in the on-demand connection establishment scheme becomes a fast constant time operation, and the additional cost of establishing connections later is negligible.
The on-demand connection establishment between two processes, especially when two processes attempt to connect to each other simultaneously, is a complex task due to race-conditions and thus prone to hard-to-reproduce defects. To assure ourselves of the correctness of the TCP network module, we modeled its design using the SPIN model checker, and verified safety and liveness properties stated as Linear Temporal Logic claims.
|
63 |
Reasoning About Staged ProgramsJanuary 2010 (has links)
This thesis establishes formal equational properties of multi-stage
calculi and related proof techniques that support analyses of staged
programs. A key promise of staging is to make programs efficient
without destroying clarity, thereby reducing the likelihood of bugs.
However, few publications rigorously verify that their staged
programs indeed behave as intended. In fact, little is known about
how staged programs can be verified, or what correctness issues
staging introduces. To solve this problem, I show a reduction of
the correctness of a staged program to that of an unstaged program.
This reduction not only clarifies the effects of staging on program
behavior but also eases verification, as unstaged programs are more
susceptible to existing reasoning techniques. I also demonstrate
that important single-stage reasoning techniques apply to staged
programs. These techniques are useful for establishing side
conditions for the reduction and for discovering or validating
further reasoning principles. / NSF grant CCF-0747431
|
64 |
Efficient Verification of Bit-Level Pipelined Machines Using RefinementSrinivasan, Sudarshan Kumar 24 August 2007 (has links)
Functional verification is a critical problem facing the semiconductor
industry: hardware designs are extremely complex and highly optimized,
and even a single bug in deployed systems can cost more than $10
billion. We focus on the verification of pipelining, a key
optimization that appears extensively in hardware systems such as
microprocessors, multicore systems, and cache coherence protocols.
Existing techniques for verifying pipelined machines either consume
excessive amounts of time, effort, and resources, or are not
applicable at the bit-level, the level of abstraction at which
commercial systems are designed and functionally verified.
We present a highly automated, efficient, compositional, and scalable
refinement-based approach for the verification of bit-level pipelined
machines. Our contributions include:
(1) A complete compositional reasoning framework based on refinement.
Our notion of refinement guarantees that pipelined machines satisfy
the same safety and liveness properties as their instruction set
architectures.
In addition, our compositional framework can be used to decompose
correctness proofs into smaller, more manageable pieces, leading to
drastic reductions in verification times and a high-degree of
scalability.
(2) The development of ACL2-SMT, a verification system that integrates
the popular ACL2 theorem prover (winner of the 2005 ACM Software
System Award) with decision procedures. ACL2-SMT allows us to
seamlessly take advantage of the two main approaches to hardware
verification: theorem proving and decision procedures.
(3) A proof methodology based on our compositional reasoning framework
and ACL2-SMT that allows us to reduce the bit-level verification
problem to a sequence of highly automated proof steps.
(4) A collection of general-purpose refinement maps, functions that
relate pipelined machine states to instruction set architecture
states. These refinement maps provide more flexibility and lead to
increased verification efficiency.
The effectiveness of our approach is demonstrated by verifying various
pipelined machine models, including a bit-level, Intel XScale inspired
processor that implements 593 instructions and includes features such
as branch prediction, precise exceptions, and predicated instruction
execution.
|
65 |
Model Checking Of Apoptosis Signaling Pathways In Lung CancersParlak, Mehtap Ayfer 01 October 2011 (has links) (PDF)
Model checking is a formal verification technique which is widely used in different
areas for automated verification and analysis. In this study, we applied a Model
Checking method to a biological system. Firstly we constructed a single-cell,
Boolean network model for the signaling pathways of apoptosis (programmed cell
death) in lung cancers by combining the intrinsic and extrinsic Apoptosis pathways,
p53 signaling pathway and p53 - DAP Kinase pathway in Lung cancers. We
translated this model to the NuSMV input language. Then we converted known
experimental results to CTL properties and checked the conformance of our model
with respect to biological experimental results. We examined the dynamics of the
apoptosis in lung cancer using NuSMV symbolic model checker and identified the
relationship between apoptosis and lung cancer. Finally we generalized the whole
process by introducing translation rules and CTL property patterns for biological
queries so that model checking any signaling pathway can be automated.
|
66 |
Graph dominators in logic synthesis and verificationKrenz, René January 2004 (has links)
<p>This work focuses on the usage of dominators in circuit graphs in order to reduce the complexity of synthesis and verification tasks. One of the contributions of this thesis is a new algorithm for computing multiple-vertex dominators in circuit graphs. Previous algorithms, based on single-vertex dominators suffer from their rare appearance in many circuits. The presented approach searches efficiently for multiple-vertex dominators in circuit graphs. It finds dominator relations, where algorithms for computing single-vertex dominators fail. Another contribution of this thesis is the application of dominators for combinational equivalence checking based on the arithmetic transform. Previous algorithms rely on representations providing an explicit or implicit disjoint function cover, which is usually excessive in memory requirements. The new algorithm allows a partitioned evaluation of the arithmetic transform directly on the circuit graph using dominator relations. The results show that the algorithm brings significant improvements in memory consumption for many benchmarks. Proper cuts are used in many areas of VLSI. They provide cut points, where a given problem can be split into two disjoint sub-problems. The algorithm proposed in this thesis efficiently detects proper cuts in a circuit graph and is based on a novel concept of a reduced dominator tree. The runtime of the algorithm is less than 0.4 seconds for the largest benchmark circuit. The final contribution of this thesis is the application of the proper cut algorithm as a structural method to decompose a Boolean function, represented by a circuit graph. In combination with a functional approach, it outperforms previous methods, which rely on functional decomposition only.</p>
|
67 |
A Compositional Approach to Asynchronous Design Verification with Automated State Space ReductionAhrens, Jared 23 February 2007 (has links)
Model checking is the most effective means of verifying the correctness of asynchronous designs, and state space exploration is central to model checking. Although model checking can achieve very high verification coverage, the high degree of concurrency in asynchronous designs often leads to state explosion during state space exploration. To inhibit this explosion, our approach builds on the ideas of compositional verification. In our approach, a design modeled in a high level description is partitioned into a set of parallel components. Before state space exploration, each component is paired with an over-approximated environment to decouple it from the rest of the design. Then, a global state transition graph is constructed by reducing and incrementally composing component state transition graphs. We take great care during reduction and composition to preserve all failures found during the initial state space exploration of each component. To further reduce complexity, interface constraints are automatically derived for the over-approximated environment of each component. We prove that our approach is conservative in that false positive results are never produced. The effectiveness of our approach is demonstrated by the experimental results of several case studies showing that our approach can verify designs that cannot be handled by traditional at approaches. The experiments also show that constraints can reduce the size of the global state transition graph and prevent some false failures.
|
68 |
A verified framework for symbolic execution in the ACL2 theorem proverSwords, Sol Otis 11 February 2011 (has links)
Mechanized theorem proving is a promising means of formally
establishing facts about complex systems. However, in applying
theorem proving methodologies to industrial-scale hardware and
software systems, a large amount of user interaction is required in
order to prove useful properties. In practice, the human user tasked
with such a verification must gain a deep understanding of the system
to be verified, and prove numerous lemmas in order to allow the
theorem proving program to approach a proof of the desired fact.
Furthermore, proofs that fail during this process are a source of
confusion: the proof may either fail because the conjecture was false,
or because the prover required more help from the user in order to
reach the desired conclusion.
We have implemented a symbolic execution framework inside the ACL2
theorem prover in order to help address these issues on certain
problem domains. Our framework introduces a proof strategy that
applies bit-level symbolic execution using BDDs to finite-domain
problems. This proof strategy is a fully verified decision procedure
for such problems, and on many useful problem domains its capacity
vastly exceeds that of exhaustive testing. Our framework also
produces counterexamples for conjectures that it determines to be
false.
Our framework seeks to reduce the amount of necessary user interaction
in proving theorems about industrial-scale hardware and software
systems. By increasing the automation available in the prover, we
allow the user to complete useful proofs while understanding less of
the detailed implementation of the system. Furthermore, by producing
counterexamples for falsified conjectures, our framework reduces the
time spent by the user in trying to determine why a proof failed. / text
|
69 |
Automatic verification of cryptographic protocols : privacy-type propertiesCheval, Vincent 03 December 2012 (has links) (PDF)
Many tools have been developed to automatically verify security properties on cryptographic protocols. But until recently, most tools focused on trace properties (or reachability properties) such as authentication and secrecy. However, many security properties cannot be expressed as trace properties, but can be written as equivalence properties. Privacy, unlinkability, and strong secrecy are typical examples of equivalence properties. Intuitively, two protocols P, Q are equivalent if an adversary can not distinguish P from Q by interacting with these processes. In the literature, several notions of equivalence were studied, e.g. trace equivalence or a stronger one, observational equivalence. However, it is often very difficult to prove by hand any of these equivalences, hence the need for efficient and automatic tools. We first worked on an approach that rely on constraint solving techniques and that is well suited for bounded number of sessions. We provided a new algorithm for deciding the trace equivalence between processes that may contain negative tests and non-determinism. We applied our results on concrete examples such as anonymity of the Private Authentication protocol and the E-passport protocol. We also investigated composition results. More precisely, we focused on parallel composition under shared secrets. We showed that under certain conditions on the protocols, the privacy type properties are preserved under parallel composition and under shared secrets. We applied our result on the e-passport protocol. At last this work presents an extension of the automatic protocol verifier ProVerif in order to prove more observational equivalences. This extension have been implemented in ProVerif and allows us to automatically prove anonymity in the private authentication protocol.
|
70 |
Formal verification of secured routing protocolsArnaud, Mathilde 13 December 2011 (has links) (PDF)
With the development of digital networks, such as Internet, communication protocols are omnipresent. Digital devices have to interact with each other in order to perform the numerous and complex tasks we have come to expect as commonplace, such as using a mobile phone, sending or receiving electronic mail, making purchases online and so on. In such applications, security is important. For instance, in the case of an online purchase, the right amount of money has to be paid without leaking the buyer personal information to outside parties. Communication protocols are the rules that govern these interactions. In order to make sure that they guarantee a certainlevel of security, it is desirable to analyze them. Doing so manually or by testing them is not enough, as attacks can be quite subtle. Some protocols have been used for years before an attack was discovered. Because of their increasing ubiquity in many important applications, e.g. electronic commerce, a very important research challenge consists in developing methods and verification tools to increase our trust on security protocols, and so on the applications that rely on them. For example, more than 28 billion Euros were spent in France using Internet transactions, and the number is growing. Moreover, new types of protocols are continuously appearing in order to face new technological and societal challenges, e.g. electronic voting, electronic passport to name a few.
|
Page generated in 0.1244 seconds