Binary decision diagrams in theory and practice
R Drechsler, D Sieling - International Journal on Software Tools for …, 2001 - Springer
Decision diagrams (DDs) are the state-of-the-art data structure in VLSI CAD and have been
successfully applied in many other fields. DDs are widely used and are also integrated in …
successfully applied in many other fields. DDs are widely used and are also integrated in …
Model checking
EM Clarke - Foundations of Software Technology and Theoretical …, 1997 - Springer
Abstract Model checking is an automatic technique for verifying finite-state reactive systems,
such as sequential circuit designs and communication protocols. Specifications are …
such as sequential circuit designs and communication protocols. Specifications are …
Formal verification in hardware design: a survey
C Kern, MR Greenstreet - ACM Transactions on Design Automation of …, 1999 - dl.acm.org
In recent years, formal methods have emerged as an alternative approach to ensuring the
quality and correctness of hardware designs, overcoming some of the limitations of …
quality and correctness of hardware designs, overcoming some of the limitations of …
[图书][B] Binary decision diagrams: theory and implementation
R Drechsler, B Becker - 2013 - books.google.com
For someone with a hammer the whole world looks like a nail. Within the last 10-13 years
Binar· y Decision Diagmms (BDDs) have become the state-of-the-art data structure in VLSI …
Binar· y Decision Diagmms (BDDs) have become the state-of-the-art data structure in VLSI …
Binary decision diagrams and beyond: Enabling technologies for formal verification
RE Bryant - Proceedings of IEEE International Conference on …, 1995 - ieeexplore.ieee.org
Ordered Binary Decision Diagrams (OBDDs) have found widespread use in CAD
applications such as formal verification, logic synthesis, and test generation. OBDDs …
applications such as formal verification, logic synthesis, and test generation. OBDDs …
[图书][B] Decision diagram techniques for micro-and nanoelectronic design handbook
SN Yanushkevich, DM Miller, VP Shmerko… - 2018 - taylorfrancis.com
Decision diagram (DD) techniques are very popular in the electronic design automation
(EDA) of integrated circuits, and for good reason. They can accurately simulate logic design …
(EDA) of integrated circuits, and for good reason. They can accurately simulate logic design …
ACL2 theorems about commercial microprocessors
B Brock, M Kaufmann, JS Moore - … on Formal Methods in Computer-Aided …, 1996 - Springer
ACL2 is a mechanized mathematical logic intended for use in specifying and proving
properties of computing machines. In two independent projects, industrial engineers have …
properties of computing machines. In two independent projects, industrial engineers have …
Checking equivalence for partial implementations
C Scholl, B Becker - Proceedings of the 38th Annual Design Automation …, 2001 - dl.acm.org
We consider the problem of checking whether a partial implementation can (still) be
extended to a complete design which is equivalent to a given full specification. Several …
extended to a complete design which is equivalent to a given full specification. Several …
Combinations of model checking and theorem proving
TE Uribe - International Workshop on Frontiers of Combining …, 2000 - Springer
The two main approaches to the formal verification of reactive systems are based,
respectively, on model checking (algorithmic verification) and theorem proving (deductive …
respectively, on model checking (algorithmic verification) and theorem proving (deductive …
[图书][B] Spectral interpretation of decision diagrams
RS Stanković, JT Astola - 2003 - Springer
DDs are derived by the reduction of decision trees (DTs)[195, 196]. The reduction of a DT
into a DD for a given function f is possible due to some particular properties of f that assure …
into a DD for a given function f is possible due to some particular properties of f that assure …