This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Specification and Validation of Control-Intensive IC's in hopCP
June 1994 (vol. 20 no. 6)
pp. 405-423

Control-intensive IC's pose a significant challenge to the users of formal methods in designing hardware. These IC's have to support a wide variety of requirements including synchronous and asynchronous operations, polling and interrupt driven modes of operation, multiple concurrent threads of execution, nontrivial computational requirements, and programmability. We illustrate the use of formal methods in the design of a control-intensive IC called the "Intel 8251" Universal Synchronous/Asynchronous Receiver/Transmitter (USART), using our hardware description language "hopCP". A feature of hopCP is that it supports communication via asynchronous ports in addition to synchronous message passing. Asynchronous ports are distributed shared variables writable by exactly one process. We show the usefulness of this combination of communication constructs. We outline algorithms to determine safe usages of asynchronous ports, and also to discover other static properties of the specification. We discuss a compiled-code concurrent functional simulator called CFSIM, as well as the use of concurrent testers for driving CFSIM. The use of a semantically well-specified and simple language, and the associated analysis/simulation tools helps conquer the complexity of specifying and validating control-intensive IC's.

[1] V. Akella and G. Gopalakrishnan, "hopCP: A concurrent Hardware Description Language,"Tech. Rep. UUCS-91-021, Department of Computer Science, University of Utah, Oct. 1991.
[2] V. Akella and G. Gopalakrishnan, "CFSIM: Static Analysis Techniques for the Synthesis of Efficient Asynchronous Circuits,"Tech. Rep. UUCS-91-018, Department of Computer Science, University of Utah, Oct. 1991.
[3] V. Akella and G. Gopalakrishnan, "CFSIM: A Compiled-Code Concurrent Functional Simulator for VLSI Systems,"Tech. Rep. UUCS-TR-92-002, Department of Computer Science, University of Utah, Jan. 1992. To appear in International Journal in Computer Simulation, 1994.
[4] V. Akella and G. Gopalakrishnan, "SHILPA: A High-Level Synthesis System for Self-Timed Circuits", inInt. Conf. on Computer-aided Design. ICCAD 92, Nov. 1992, p. 587-591.
[5] A. Appel and D. MacQueen, "A Standard ML compiler," inFunct. Programming Lang. and Comp. Archit.Sept. 1987.
[6] A. W. Appel,Compiling with Continuations, Cambridge Univ. Press, 1992. ISBN 0-521-41695-7.
[7] K. R. Apt and E. R. Olderog,Verification of Sequ. and Concurrent Prog., Springer-Verlag, 1991, ISBN 0-387-97532-2.
[8] M. R. Barbacci, "Instruction set processor specifications (ISPS): The notation and its applications,"IEEE Trans. on Comput. C-30, 1 Jan. 1981, pp.24-40.
[9] R. S. Boyer and J. S. Moore,A Computational Logic, Academic Press, 1979.
[10] E. Brunvand,Translating Concurrent Communicating Programs into Asynchronous Circuits. PhD thesis, Carnegie Mellon University, Nov. 1991.
[11] A. Charlesworth, "The multi-way rendezvous,"ACM Trans. Programming Languages Syst., vol. 9, no. 2, pp. 350-366, July 1987.
[12] R. Cleveland, J. Parrow and B. Steffen, "The concurrency workbench: A semantics based tool for the verification of concurrent systems,"Tech. Rep. ECS-LFCS-89-83, Laboratory for Foundations of Computer Science, Univ of Edinburgh, Aug. 1989.
[13] D. L. Dill,Trace Theory for Automatic Hierarhical Verification of Speed-Independent Circuits. Cambridge, MA: MIT Press, 1988.
[14] D. L. Dill, S. M. Nowick and R. F. Sproull, "Specification and automatic verification of self-timed queues,"Formal Methods in Syst. Des. I.1 July, 1992, pp. 29-62.
[15] J. C. Ebergen, "Translating programs into delay-insensitive circuits," CWI Tract 56, Centre for Mathematics and Computing Science, Amsterdam, 1989.
[16] G. Gopalakrishnan and R. Fujimoto, "Design and verification of the rollback chip using hop: A case study of formal methods applied to hardware design,Tech. Rep. UU-CS-TR-91-015, University of Utah, Department of Computer Science, 1991.
[17] G. Gopalakrishnan and L. Josephson, "Towards amalgamating the synchronous and asynchronous styles," InTAU 93: Timing Aspects of VLSI, Malente, Germany, ACM, Sept. 1993.
[18] G. Gopalakrishnan, N. Michell, E. Brunvand and S. M. Nowick, "A correctness criterion for asynchronous circuit verification and optimization,"IEEE Trans. Computer-Aided Des., 1992,Accepted for Publication,.
[19] M. J. Gordon, "Mechanizing programming logics in higher order logic," in1988 Banff Hardware Verification Workshop, Banff, June 1988, G. Birtwistle and P. A. Subrahmanyam, Eds.
[20] A. Hall, "Seven myths of formal methods,"IEEE Software, 9 Sept. 1990.
[21] Z. Har'El and R. P. Kurshan, "Software for analytical development of communication protocols,"AT&T Tech. J.Jan. 1990.
[22] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[23] Intel. 8251A Programmable Communication Interface. inIntel Micro-processor and Peripheral Handbook, 1986, pp. 6.1226-6.138.
[24] S.D. Johnson,Synthesis of Digital Designs From Recursion Equations, MIT Press, Cambridge, Mass., 1984.
[25] D. Ku and G. De Micheli,HardwareC: A Language for Hardware Design, tech. rpt. CSL-TR-90-419, Computer System Lab., Stanford Univ., Aug. 1990 (Version 2.0).
[26] L. Lamport, "A simple approach to specifying concurrent systems,"Commun. ACM, vol. 32, pp. 32-45, 1989.
[27] L. Logrippo, A. Obaid, J. P. Braind, and M. C. Fehri, "An interpreter for LOTOS, A specification language for distributed systems,"Software--Practice and Exper., vol. 18, pp. 365-385, Apr. 1988.
[28] I. Page and W. Luk, "Compiling Occam into field-programmable gate arrays," Int. Workshop on Field Programmable Logic and Applic., September, 1991, Oxford University, UK.
[29] A. J. Martinet al., "The design of an asynchronous microprocessor," inAdvanced Research in VLSI, Proceedings of the Decennial Caltech Conference on VLSI, C. L. Seitz, Ed., Mar. 1989, pp. 351-373.
[30] K.L. McMillian,Symbolic Model Checking, Kluwer Academic Press, Boston, 1993.
[31] M. C. McFarlandet al., "High level synthesis of digital systems,"Proc. IEEE, Feb. 1990.
[32] M. David,Compiling Occam into Silicon. Developments in Concurrency and Communication Addison-Wesley, 1990.
[33] R. Nalumasu and G. Gopalakrishnan. "Verifying an asynchronous wave-front crossbar arbiter using smv, 1993,"Class Project Notes, CS 611, Available upon request from ratan@cs.utah.edu.
[34] Occam Programming Manual, INMUS Ltd., Prentice-Hall International, 1984.
[35] T. Y. C. Leung and R. R. Muntz, "Query processing for temporal databases," inProc. Int. Conf. Data Engineering, pp. 200-208, 1990.
[36] R. Milner,Communication and Concurrency. Englewood Cliffs, NJ: Prentice-Hall International, 1989.
[37] F. U. Rosenberger, C. E. Molnar, T. J. Chaney and Ting-Pein Fang, "Q-modules: internally clocked delay-insensitive modules,"IEEE Trans. Comp. 37,9 Sept. 1988, pp. 1005-1018.
[38] M. Sheeran, "Design of regular hardware structures using higher order functions," inProc. of the Funct. Prog. and Comput. Architecture Conf., Sept. 1985, Springer-Verlag, LNCS 201. Nancy, France.
[39] M. Srivas and M. Bickford, "Formal verification of a pipelined micro-processor,"IEEE Software, 9 Sept. 1990.
[40] E. Sternheim, R. Singh, and Y. Trivedi,Digital Design with Verilog HDL, Automata Publishing, Cupertino, Calif., 1990.
[41] I. Sutherland, "Micropipelines,"Communications of the ACMJune, 1989.The 1988 ACM Turing Award Lecture.
[42] D. Thomas et al.,Algorithmic and Register-Transfer-Level Synthesis: The System Architect's Workbench, Kluwer Academic Publishers, Boston, 1990.
[43] D.E. Thomas and P.R. Moorby,The Verilog Hardware Description Language, Kluwer Academic Publishers, Boston, 1991.
[44] VHDL Language Reference Manual, Aug. 1985.Intermetrics Rep. IR-MD-045-2; See also IEEE Des. and Test. Apr., 1986.

Index Terms:
microprocessor chips; message passing; specification languages; formal specification; digital simulation; formal verification; control-intensive integrated circuits; hopCP; validation; specification; formal methods; hardware design; synchronous operations; asynchronous operations; polling; interrupt; multiple concurrent threads; computational requirements; Intel 8251; Universal Synchronous/Asynchronous Receiver/Transmitter; USART; hardware description language; synchronous message passing; distributed shared variables; asynchronous ports; compiled-code concurrent functional simulator; CFSIM
Citation:
V. Akella, G. Gopalakrishnan, "Specification and Validation of Control-Intensive IC's in hopCP," IEEE Transactions on Software Engineering, vol. 20, no. 6, pp. 405-423, June 1994, doi:10.1109/32.295890
Usage of this product signifies your acceptance of the Terms of Use.