Zobrazeno 1 - 10
of 10
pro vyhledávání: '"Marco Murciano"'
Publikováno v:
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 29:382-395
Interpolant-based model checking has been shown to be effective on large verification instances, as it efficiently combines automated abstraction and reachability fixed-point checks. On the other hand, methods based on variable quantification have pr
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b97fd068a6474b388aadb22b3c67798b
https://doi.org/10.1109/tcad.2010.2041847
https://doi.org/10.1109/tcad.2010.2041847
Publikováno v:
ACM Transactions on Design Automation of Electronic Systems. 15:1-34
Hardware synthesis is the process by which system-level, Register Transfer (RT)-level, or behavioral descriptions can be turned into real implementations, in terms of logic gates. Scheduling is one of the most time-consuming steps in the overall desi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dd6dbf36b3a35f4116b8414e4b940705
https://doi.org/10.1145/1698759.1698762
https://doi.org/10.1145/1698759.1698762
Publikováno v:
Journal of Electronic Testing. 26:261-278
This paper introduces an approach to effectively exploit incremental SAT in order to search for multiple equivalence-preserving transformations of combinational circuits. Typical applications, such as redundancy removal with observability and externa
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::e884a51e1b1088d1f93107dc586ff8e0
https://doi.org/10.1007/s10836-010-5144-0
https://doi.org/10.1007/s10836-010-5144-0
The design of complex embedded systems deployed in safety-critical or mission-critical applications mandates the availability of methods to validate the system dependability across the whole design flow. In this article we introduce a fault injection
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4eb98573c8928ee59bff2cde0b4e1b06
http://hdl.handle.net/11583/2261409
http://hdl.handle.net/11583/2261409
Publikováno v:
HLDVT
This paper introduces an approach to effectively exploit incremental SAT in order to search for multiple equivalencepreserving transformations of combinational circuits.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::731c975bbe14f51437a091695a259b51
http://hdl.handle.net/11583/2279205
http://hdl.handle.net/11583/2279205
Publikováno v:
FMCAD
Interpolant-based model checking has been shown effective on large verification instances, as it efficiently combines automated abstraction and fixed-point checks. On the other hand, methods based on variable quantification have proved their ability
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c506f5386c29fdf4922b082d359c82bd
https://doi.org/10.1109/fmcad.2008.ecp.30
https://doi.org/10.1109/fmcad.2008.ecp.30
SAT--based Unbounded Model Checking based on Craig Interpolants is often able to overcome BDDs and other SAT--based techniques on large verification instances. Based on refutation proofs generated by SAT solvers, interpolants provide compact circuit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::c23a35eed54ec584bc52728975bea25f
http://hdl.handle.net/11583/1848729
http://hdl.handle.net/11583/1848729
Autor:
Marco Murciano, Massimo Violante
Publikováno v:
HLDVT
The design of complex embedded systems deployed in safety-critical or mission-critical applications mandate the availability of methods for validating the system dependability across the whole design flow. In this paper we introduce a fault-injection
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fc52b9a2ac726b2cd065146a70d5025f
http://hdl.handle.net/11583/1852789
http://hdl.handle.net/11583/1852789
Autor:
Marco Murciano, Gianpiero Cabodi
Publikováno v:
Formal Methods for Hardware Verification ISBN: 9783540343042
SFM
SFM
This chapter overviewes Binary Decision Diagrams (BDDs) and their application in Formal Hardware Verification. BDDs are first described as a representation formalism for Boolean functions. BDDs are directed acyclic graphs, deriving their efficiency f
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::fc6639fb0df9e28da3871bbea85f321a
https://doi.org/10.1007/11757283_4
https://doi.org/10.1007/11757283_4
Publikováno v:
ICCAD
This paper addresses SAT-based Unbounded Model Checking based on Craig Interpolants. This recently introduced methodology is often able to outperform BDDs and other SAT-based techniques on large verification instances. Based on refutation proofs gene
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a9f3df564d10d984e4253defa8c2a7f6
https://doi.org/10.1145/1233501.1233661
https://doi.org/10.1145/1233501.1233661