Zobrazeno 1 - 10
of 15
pro vyhledávání: '"Ghiath Al-Sammane"'
Publikováno v:
Formal Aspects of Computing. 25:971-991
In this paper we propose an automatic methodology to verify the soundness of model checking reduction techniques. The idea is to use the consistency of the specifications to verify if the reduced model is faithful to the original one. The user provid
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a5641ee1ba811a4ab6d2adf768811e6d
https://doi.org/10.1007/s00165-012-0223-x
https://doi.org/10.1007/s00165-012-0223-x
Publikováno v:
Journal of Computer Science and Technology. 24:76-95
In this paper, we provide a necessary infrastructure to define an abstract state exploration in the HOL theorem prover. Our infrastructure is based on a deep embedding of the Multiway Decision Graphs (MDGs) theory in HOL. MDGs generalize Reduced Orde
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8b63d9aa2da1e93ab7257a903400f99f
https://doi.org/10.1007/s11390-009-9205-8
https://doi.org/10.1007/s11390-009-9205-8
Publikováno v:
Computational Intelligence in Analog and Mixed-Signal (AMS) and Radio-Frequency (RF) Circuit Design ISBN: 9783319198712
This chapter proposes a complementary formal-based solution to the verification of analog and mixed-signal (AMS) designs. The authors use symbolic computation to model and verify AMS designs through the application of induction-based model checking.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7880402c829741b97981556f4aac5ce4
https://doi.org/10.1007/978-3-319-19872-9_5
https://doi.org/10.1007/978-3-319-19872-9_5
Publikováno v:
Revue internationale de génie électrique. 5:241-252
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::070f1c3f0705e81216091cd66d783e22
https://doi.org/10.3166/rige.5.241-252
https://doi.org/10.3166/rige.5.241-252
Autor:
Rajeev Narayanan, Naeem Abbasi, Sofiène Tahar, Mohamed H. Zaki, Zhiwei Wang, Ghiath Al Sammane
Publikováno v:
2009 IEEE 15th International Mixed-Signals, Sensors, and Systems Test Workshop.
Analog and mixed signal (AMS) circuits play an important role in today's System on Chip design. They pose, however, many challenges in the verification of the overall system due to their complex behavior. Among many developed verification techniques,
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::daa7c9a0b216ebff6897740c30254a03
https://doi.org/10.1109/ims3tw.2009.5158695
https://doi.org/10.1109/ims3tw.2009.5158695
Publikováno v:
SAC
In this paper, all the necessary infrastructure is provided to define a state exploration approach within the HOL theorem prover. While related work has tackled the same problem by representing primitive Binary Decision Diagram (BDD) operations as in
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::be5a305c2c86ad48b02b8b2f9ef184dd
https://doi.org/10.1145/1363686.1363774
https://doi.org/10.1145/1363686.1363774
Publikováno v:
2007 IEEE Northeast Workshop on Circuits and Systems.
Digital communication systems such as MODEM (modulation-demodulation) and M-PSK require the application of carrier synchronization in phase and frequency. The key role of this DCS depends largely on the numerically controlled oscillator (NCO) and the
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::2c6dc7ce1d53697128dd88da0835448d
https://doi.org/10.1109/newcas.2007.4487971
https://doi.org/10.1109/newcas.2007.4487971
Publikováno v:
Electronic Workshops in Computing.
Multiway Decision Graphs (MDGs) represent and manipulate a subset of first-order logic formulae suitable for model checking of large data path circuits. Due to the presence of abstract variables, existing reduction algorithms that is defined on symbo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7bb77f6e7a6f4be855a5d326affce283
https://doi.org/10.14236/ewic/vecos2007.9
https://doi.org/10.14236/ewic/vecos2007.9
Publikováno v:
2007 Design, Automation & Test in Europe Conference & Exhibition.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6c85d995e34064156577bf536fe4ceba
https://doi.org/10.1109/date.2007.364599
https://doi.org/10.1109/date.2007.364599
Publikováno v:
Computational Science – ICCS 2007 ISBN: 9783540725855
International Conference on Computational Science (2)
International Conference on Computational Science (2)
In this paper, we show how symbolic algebra in Mathematica can be used to formally verify analog and mixed signal designs. The verification methodology is based on combining induction and constraints solving to generate correctness for the system wit
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6f2fc08e1bf4761aa09b26d2e1064a45
https://doi.org/10.1007/978-3-540-72586-2_37
https://doi.org/10.1007/978-3-540-72586-2_37