Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 13

Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems

A Proof System for MDESL

, , ,

DOI: http://dx.doi.org/10.15439/2017F400

Citation: Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 13, pages 387–393 ()

Full text

Abstract. Hardware description language (HDL) Verilog has been standardized and widely used in industry. To describe the features such as event-driven computation, time and shared-variable concurrency of hardware, a Verilog-like language MDESL (multithreaded discrete event simulation language), has been introduced. In this paper, we put forward a proof system for MDESL which is based on the classical Hoare Logic (precondition, program, postcondition). To deal with the guard statement, we add a new element trace to Hoare triples. We extend the primitives of assertion to express the global time of current program, and interpret the triples so that it can verify both terminating and nonterminating computations. To verify a concurrent program, we use a merger method of the trace to combine the traces in our parallel rule. Finally, there is an example about using our proof system to verify the correctness of a program written by MDESL.

References

  1. IEEE, IEEE Standard Hardware Description Language based on the Verilog Hardware Description Laguage, Volume IEEE Standard 1364-1995. IEEE, 1995.
  2. IEEE, IEEE Standard Hardware Description Language based on the Verilog Hardware Description Laguage, Volume IEEE Standard 1364-2001. IEEE, 2001.
  3. N. Nissanke, Realtime Systems, Prentice Hall International Series in computer Science, 1997.
  4. Haase, V., Real-time Behavior of Programs, IEEE Transactions on Software Engineering SE-7,5 (Sept. 1981), 497-501.
  5. Zhu, H., Linking the Semantics of a Multithreaded Discrete Event Simulation Language, London South Bank University, 2005.
  6. Golze, U., VLSI Chip Design with the Hardware Description Language Verilog: An Introduction Based on a Large RISC Processor Design, Springer-Verlag New York, Inc. 1996.
  7. Gordon, M.J.C., The semantic challenge of Verilog HDL, In Proc. Tenth Annual IEEE Symposium on Logic in Computer Science, page 136-145. IEEE Computer Society Press, June 1995.
  8. Gordon, M.J.C., Relating event and trace semantics of hardware description languages, The Computer Journal, 45(1): 27-36, 2002.
  9. Apt, K.R., de Boer, F.S., Olderog, E., Verification of sequential and concurrent programs, Texts in Computer Science, Springer, 2009.
  10. Hoare, C.A.R., Communicating Sequential Processes, Prentice Hall International Series in Computer Science, 1985.
  11. Hooman, J., Extending hoare logic to real-time, Formal Aspects of Computing, 1994, 6(1):801-825.
  12. Park, S., Pfenning, F., Thrun, S., A probabilistic language based upon sampling functions, Acm Transactions on Programming Languages, 2004, 40.1(2004):171-182.
  13. Zhu, H., Qin, S., He, J., Bowen, J.P., PTSC: probaility, time and shared-variable concurrency, Innovations in Systems and Software Enginerring: A NASA Journal 5(4), 271-284(2009).
  14. Hoare, C. A. R., Algebra of concurrent programming, In: Meeting 52 of WG 2.3(2011).
  15. Hoare, C. A. R., He, J., Unifying Theories of programming, Prentice Hall International Series in Computer Science, 1998.