S. Qin
From statecharts to verilog : a formal approach to hardware/software co-specification
Qin, S.; Chin, W.N.; He, J.; Qiu, Z.
Authors
W.N. Chin
J. He
Z. Qiu
Abstract
Hardware-Software co-specification is a critical phase in co-design. Our co-specification process starts with a high level graphical description in Statecharts and ends with an equivalent parallel composition of hardware and software descriptions in Verilog. In this paper, we first investigate the Statecharts formalism by providing it a formal syntax and a compositional operational semantics. Based on that, a semantics-preserving linking function is designed to compile specifications written in Statecharts into Verilog. The obtained Verilog specifications are then passed to a partitioning process to generate hardware and software sub-specifications, where the correctness is guaranteed by algebraic laws of Verilog.
Citation
Qin, S., Chin, W., He, J., & Qiu, Z. (2006). From statecharts to verilog : a formal approach to hardware/software co-specification. Innovations in Systems and Software Engineering, 2(1), 17-38. https://doi.org/10.1007/s11334-005-0020-2
Journal Article Type | Article |
---|---|
Publication Date | 2006-03 |
Deposit Date | Apr 23, 2008 |
Publicly Available Date | Dec 11, 2009 |
Journal | Innovations in Systems and Software Engineering |
Print ISSN | 1614-5046 |
Electronic ISSN | 1614-5054 |
Publisher | Springer |
Peer Reviewed | Peer Reviewed |
Volume | 2 |
Issue | 1 |
Pages | 17-38 |
DOI | https://doi.org/10.1007/s11334-005-0020-2 |
Keywords | Operational semantics, Homomorphism, Algebraic laws, Hardware/software partitioning. |
Public URL | https://durham-repository.worktribe.com/output/1599723 |
Files
Accepted Journal Article
(447 Kb)
PDF
You might also like
PTSC: probability, time and shared-variable concurrency
(2009)
Journal Article
Verifying BPEL-like Programs with Hoare Logic
(2008)
Journal Article
An Algebraic Hardware/Software Partitioning Algorithm
(2002)
Journal Article
Timed Automata Patterns
(2008)
Journal Article
Downloadable Citations
About Durham Research Online (DRO)
Administrator e-mail: dro.admin@durham.ac.uk
This application uses the following open-source libraries:
SheetJS Community Edition
Apache License Version 2.0 (http://www.apache.org/licenses/)
PDF.js
Apache License Version 2.0 (http://www.apache.org/licenses/)
Font Awesome
SIL OFL 1.1 (http://scripts.sil.org/OFL)
MIT License (http://opensource.org/licenses/mit-license.html)
CC BY 3.0 ( http://creativecommons.org/licenses/by/3.0/)
Powered by Worktribe © 2025
Advanced Search