Zobrazeno 1 - 10
of 25
pro vyhledávání: '"Ziyad Hanna"'
Autor:
Roberto Sebastiani, Zurab Khasidashvili, Amit Palti, Roberto Bruttomesso, Marco Bozzano, Alessandro Cimatti, Anders Franzén, Ziyad Hanna
Publikováno v:
Electronic Notes in Theoretical Computer Science. 144(2):3-14
Formal checking at Register-Transfer Level (RTL) is currently a fundamental step in the design of hardware circuits. Most tools for formal checking, however, work at the boolean level, which is not expressive enough to capture the abstract, high leve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5c5d67e65236ec3df31c67e9e0c96e34
Publikováno v:
Electronic Notes in Theoretical Computer Science. 128(3):75-90
We describe the design and implementation of a highly optimized, multithreaded algorithm for the propositional satisfiability problem. The algorithm is based on the Davis-Putnam-Logemann-Loveland sequential algorithm, but includes many of the optimiz
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::91f1fb921a3fd004dc03f5a6358d8305
Publikováno v:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 22:1042-1048
Design automation problems can often be encoded in propositional logic, and solved by applying propositional logic proof methods. Unfortunately, there exists no single proof method with adequate performance for all problems of interest. It is, theref
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::646086377dd3e05a92020c455d58fba7
https://doi.org/10.1109/tcad.2003.814959
https://doi.org/10.1109/tcad.2003.814959
Autor:
Ziyad Hanna, Zurab Khasidashvili
Publikováno v:
Electronic Notes in Theoretical Computer Science. 89:593-607
The BDD- and SAT-based model checking and verification methods normally require an initial state. Here we are concerned with sequential hardware verification, where an initial state must be one of the reset states. In practice, a reset state is not a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::be792525eeac94cfc5499b6af58cd60f
https://doi.org/10.1016/s1571-0661(05)82545-9
https://doi.org/10.1016/s1571-0661(05)82545-9
Autor:
Ziyad Hanna
Publikováno v:
2014 Formal Methods in Computer-Aided Design (FMCAD).
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::68428bb6a0ce26bd581bf15f4bf810cd
https://doi.org/10.1109/fmcad.2014.6987583
https://doi.org/10.1109/fmcad.2014.6987583
Autor:
Ziyad Hanna
Publikováno v:
Proceedings of the 45th annual Design Automation Conference.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2ded870a7723035d90dc30e1ffb142ef
https://doi.org/10.1145/3255523
https://doi.org/10.1145/3255523
Autor:
Roberto Bruttomesso, Amit Palti, Alexander Nadel, Alberto Griggio, Anders Franzén, Ziyad Hanna, Alessandro Cimatti, Roberto Sebastiani
Publikováno v:
Computer Aided Verification ISBN: 9783540733676
CAV
CAV
Rarely verification problems originate from bit-level descriptions. Yet, most of the verification technologies are based on bit blasting, i.e., reduction to boolean reasoning. In this paper we advocate reasoning at higher level of abstraction, within
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6742f6200c69855d0fc09deee55a5c89
https://doi.org/10.1007/978-3-540-73368-3_54
https://doi.org/10.1007/978-3-540-73368-3_54
Autor:
Ziyad Hanna
Publikováno v:
Computer Science – Theory and Applications ISBN: 9783540745099
CSR
CSR
Moore's Law continues to drive a severe increase in the number of transistors that can be integrated onto a single microprocessor chip. Computer architects and designers continue to look for ways to take advantage from it to produce ever more complex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5b0746d274c5d0a61c91a7023e0d05ea
https://doi.org/10.1007/978-3-540-74510-5_5
https://doi.org/10.1007/978-3-540-74510-5_5
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2007 ISBN: 9783540727873
SAT
SAT
We show that modern conflict-driven SAT solvers implicitly build and prune a decision tree whose nodes are associated with flipped variables. Practical usefulness of conflict-driven learning schemes, like 1UIP or AllUIP, depends on their ability to g
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::36be2989e1ec09c0e950a0c4ae85839c
https://doi.org/10.1007/978-3-540-72788-0_27
https://doi.org/10.1007/978-3-540-72788-0_27