Abstract
We propose in this paper an algebraic approach to hardware/software partitioning in Verilog HDL. We explore a collection of algebraic laws for Verilog programs, from which we design a set of syntax-based algebraic rules to conduct hardware/software partitioning. The co-specification language and the target hardware and software description languages are specific subsets of Verilog, which brings forth our successful verification for the correctness of the partitioning process by algebra of Verilog. Facilitated by Verilog’s rich features, we have also successfully studied hw/sw partitioning for environment-driven systems.
The work is partially supported by NNSFC under grant Nos. 60173003 and 69983001.
Work as a Research Fellow at Singapore-MIT Alliance, National University of Singapore starting from July 15, 2002. Email: smaqs@nus.edu.sg
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
M. Gordon, “The Semantic Challenge of VERILOG HDL”, In the proc. of Tenth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 136–145, 1995.
M. Gordon, “Relating Event and Trace Semantics of Hardware Description Languages”, The Computer Journal, pp. 27–36, Vol. 45, No. 1, 2002.
He J., “An Algebraic Approach to the Verilog Programming”, will appear in the proc. of Lisbon Workshop, 2002.
He J., I. Page and J. Bowen, “A Provable Hardware Implementation of Occam”, LNCS 711, pp. 693–703, 1993.
He J. and J. Bowen, “Specification, Verification and Prototyping of an Optimised Compiler”, Formal Aspect of Computing 6, pp. 643–658, 1994.
He J. et al, “Provably Correct Systems”, LNCS 863, pp. 288–335, 1994.
He J. and Zhu H., “Formalising Verilog”, in the proc. of ICECS 2000, IEEE Computer Society Press, pp. 412–415, Lebanon, Dec. 2000.
C.A.R. Hoare and He J., Unifying Theories of Programming, Prentice Hall, 1998.
IEEE Computer Society, IEEE Standard Hardware Description Language Based on the VERILOG Hardware Description Language (IEEE std 1364-1995), 1995.
J. Iyoda and He J., “Towards an Algebraic Synthesis of Verilog”, in the proc of ERSA’2001, Las Vegas, USA, 2001.
I. Page and W. Luk, “Compiling Occam into FPGAs”, in FPGAs, eds., W. Moore and W. Luk, pp. 271–283, Abingdon EE&CS books, 1991.
Qin S., “An Algebraic Approach to Hardware/Software Partitioning in Hardware/Software Co-Design”, Ph.D thesis, School of Mathematical Sciences, Peking University, March, 2002.
S. Qin and J. He, “Partitioning Program into Hardware and Software”, in the proc of APSEC 2001, IEEE Computer Society Press, pp. 309–316, Macau, 4–7 Dec., 2001.
Qin S., He J., Qiu Z. and Zhang N., “Hardware/Software Partitioning in Verilog”, Research Report 2002-33, School of Mathematical Sciences, http://www.math.pku.edu.cn/printdoc/182.ps.
A. Sampaio, An Algebraic Approach to Compiler Design, World Scientific, 1997.
L. Silva, A. Sampaio and E. Barros, “A Normal Form Reduction Strategy for Hardware/software Partitioning”, Formal Methods Europe (FME) 97, LNCS 1313, pp. 624–643, 1997.
Zhu H., J. Bowen and He J., “From Operational Semantics to Denotational Semantics for Verilog”, in the proc. of CHARME 2001, LNCS 2144, pp. 449–464.
Zhu H., J. Bowen and He J., “Deriving Operational Semantics from Denotational Semantics for Verilog”, in the proc. of APSEC 2001, IEEE Computer Society Press, pp. 177–184, Macau, 4–7 Dec., 2001.
Zhu H. and He J., “A DC-based Semantics for Verilog”, in the proc. of the International Conference on Software: Theory and Practice (ICS2000), pp. 421–432, Beijing, Aug. 21–24, 2000.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Qin, S., He, J., Qiu, Z., Zhang, N. (2002). Hardware/Software Partitioning in Verilog. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_19
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_19
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive