Specification and Verification of Hardware Circuits

Organisation:	Centre for Efficiency-Oriented Languages, University College Cork (IRELAND)
Method:	muCRL
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Hardware Design.
Period:	2007-2009
Size:	n/a
Description:	The validation of hardware circuits by simulation or prototype testing is both costly and time-consuming. This case study examines how a computer science based approach based on a process algebra can be applied to the specification and verification of hardware circuits that are asynchronous or combinatorial. Such an approach can be applied much earlier in the design cycle, saving time, and reducing both risk and cost. Two benchmark circuits, an asynchronous arbiter and a hazardous circuit, were analysed. The asynchronous arbiter was described in muCRL, linearised, and its state space was generated. Analysis with CADP showed it to be deadlock-free and satisfying liveness properties.
Conclusions:	This case study demonstrates that process algebraic languages, when used in combination with a comprehensive verification toolset such as CADP, are an efficient and effective means of formally specifying and verifing hardware circuits that are asynchronous or combinatorial.
Publications:	[Man-07] K.L. Man. "Specification and Analysis of Hardware Systems Using Timed Process Algebras". World Scientific and Engineering Academy and Society Transactions on Electronics, Issue 4, volume 4, April 2007. Available on line at: http://www.worldses.org/journals/electronics/electronics-april2007.htm or from the CADP Web site: PDF or PostScript [Man-09] K.L. Man. "muCRL: A Computer Science based Approach for Specification and Verification of Hardware Circuits". Proceedings of the International SoC Design Conference ISOCC'08, I-387-I-390. IEEE, November 2009. Available on-line at: http://ieeexplore.ieee.org/xpl/freeabs_all.jsp?arnumber=4815653&tag=1 or from the CADP Web site: PDF or PostScript
Contact:	K.L. Man Centre for Efficiency-Oriented Languages (CEOL) Department of Computer Science University College Cork Ireland Email: [email protected]
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page