Zobrazeno 1 - 10
of 37
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
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
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
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,
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
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
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
Publikováno v:
2007 Design, Automation & Test in Europe Conference & Exhibition.
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