Zobrazeno 1 - 10
of 42
pro vyhledávání: '"James H. Kukula"'
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783540425410
CHARME
CHARME
Model checking is the process of verifying whether a model of a concurrent system satisfies a specified temporal property. Symbolic algorithms based on Binary Decision Diagrams (BDDs) have significantly increased the size of the models that can be ve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::74107dea88bd9f7d907de959f7183f0c
Publikováno v:
Theory and Applications of Satisfiability Testing ISBN: 9783540208518
SAT
SAT
A tree decomposition of a hypergraph is a construction that captures the graph’s topological structure. Every tree decomposition has an associated tree width, which can be viewed as a measure of how tree-like the original hypergraph is. Tree decomp
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::4cc541052d51765f7835ccd7c4b3189e
https://doi.org/10.1007/978-3-540-24605-3_24
https://doi.org/10.1007/978-3-540-24605-3_24
Autor:
Robert Damiano, James H. Kukula
Publikováno v:
DAC
Procedures for Boolean satisfiability most commonly work with Conjunctive Normal Form. Powerful SAT techniques based on implications and conflicts can be retained when the usual CNF clauses are replaced with BDDs. BDDs provide more powerful implicati
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f28938a4993bdf7af9c0f9a68e641ca6
https://doi.org/10.1145/775832.776039
https://doi.org/10.1145/775832.776039
Publikováno v:
ICCAD
Circuits can be simplified for combinational equivalence checking by transforming internal functions, while preserving their ranges. In this paper, we investigate how to effiectively apply the idea to improve equivalence checking. We propose new heur
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a89e9780aeed28288479cd130866f319
https://doi.org/10.1145/774572.774650
https://doi.org/10.1145/774572.774650
Publikováno v:
Formal Methods in Computer-Aided Design ISBN: 9783540001164
FMCAD
FMCAD
We introduce a SAT based automatic abstraction refinement framework for model checking systems with several thousand state variables in the cone of influence of the specification. The abstract model is constructed by designating a large number of sta
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8259c3803014f416ca0b7dfa0c75209d
https://doi.org/10.1007/3-540-36126-x_3
https://doi.org/10.1007/3-540-36126-x_3
Publikováno v:
Computer Aided Verification ISBN: 9783540439974
CAV
CAV
We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase 'hides' the logic of various variables, hence considering them as inputs. This type of abstraction may lead to 'spuriou
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e9b38047b7303d4126fae1eed9d5feec
https://doi.org/10.1007/3-540-45657-0_20
https://doi.org/10.1007/3-540-45657-0_20
Publikováno v:
Formal Methods in Computer-Aided Design ISBN: 9783540001164
FMCAD
FMCAD
We describe a new method to simplify combinational circuits while preserving the set of all possible values (that is, the range) on the outputs. This method is performed iteratively and on the fly while building BDDs of the circuits. The method is co
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::3e638ae183fae9e05541c2b945ff5baf
https://doi.org/10.1007/3-540-36126-x_4
https://doi.org/10.1007/3-540-36126-x_4
Publikováno v:
DAC
Image computation is the key step in fixpoint computations that are extensively used in model checking. Two techniques have been used for this step: one based on conjunction of the terms of the transition relation, and the other based on recursive ca
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c09eabb39cf6f6af3c372042ebc7551a
https://doi.org/10.1145/337292.337305
https://doi.org/10.1145/337292.337305
Autor:
James H. Kukula, Thomas R. Shiple
Publikováno v:
Computer Aided Verification ISBN: 9783540677703
CAV
CAV
Given a Free BDD for the characteristic function of an input-output relation T(x, y), we show how to construct a combinational logic circuit satisfying that relation. Such relations occur as environmental constraints for module specifications, as par
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c0f3d437758f2e73f3e71fd6b41af3a4
https://doi.org/10.1007/10722167_12
https://doi.org/10.1007/10722167_12
Publikováno v:
Formal Methods in Computer-Aided Design ISBN: 9783540651918
FMCAD
FMCAD
BDD-based implicit state enumeration usually fails for systems with wide numeric datapaths. It may be possible to take advantage of higher level structure in designs to improve efficiency. By treating the integer variables as atomic types, rather tha
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::99f0aec156bdaf1ed6314bc26f2b2b8b
https://doi.org/10.1007/3-540-49519-3_30
https://doi.org/10.1007/3-540-49519-3_30