Home         Authors   Papers   Year of conference   Themes   Organizations        To MES conference

SoC protocols specification and validation: problems and solutions
Authors
	Pechenko I.S.
Date of publication
	2016
Abstract
	I. INTRODUCTION At first, let’s define an System on Chip. SoC is a complex integrated circuit that includes all the functional elements of a complete product on a single chip. The elements are usually a CPU, memory, several accelerating function units and some interfaces to peripheral devices. Today SoCs incorporate dozens of IP-blocks, complex reusable functional units. SoC design process can be divided into five development stages: planning, architecture definition, microarchitecture design, RTL coding and convergence. Nowadays most of system design validation activities take place only after RTL coding phase. One of the main reasons for it is the lack of complete, accurate and unambiguous architectural specifications. However, RTL is too low as an abstraction level to design and validate systems with millions of elements. In the last years, a big effort is spent on moving from RTL level to system level in SoC design and verification. A new method is needed for formal system description and further validation on the architecture or microarchitecture creation phases, both for hardware and software parts of the system. This new method will provide a possibility for system verification on the earliest stages of its design and will allow avoiding system specification errors, the most expensive errors for system designers. II. DESIGN PROCESS CHALLENGES At a high level of abstraction System on Chip can be viewed as a network of intercommunicating hardware and software components (IP-blocks). SoC architectural specification can be divided into two parts: structural specification and behavioral specification. The first one is a map of system components and a requirements specification for each of them. The second is a description of system behavior in different situations and protocols of IP-block intercommunication. In this work, we will address the challenges in behavioral SoC architecture specifications. Most of key "infrastructure" SoC protocols include the interaction of many components, both hardware and software. Examples of these protocols are reset, power management, security and other. Previously used methods of specification and verification of such protocols are loosing their effectiveness over the past years. There are several reasons for it: grooving the number of mistakes in SoC protocol specifications that implies the need for verification of such specifications, the key role of software in these protocols that implies the need for hardware and software co-verification etc. III. EXISTING SOLUTIONS Several solutions were suggested for the problems in SoC protocol specification. In [8] a process of creation and verification of SoC architectural formal models was described. Authors used models written on several formal languages including TLA+, Murφ and HOL. They worked with architect teams and created the models in parallel with architecture creation. In [9] authors describe their experience of applying formal methods for several complex system protocols including cache coherence protocol, sliding window protocol and other. In [2, 10] a possibility for bringing together UML diagrams and languages like SystemC and C++ for system architecture modelling was described. Authors also consider hardware and software co-verification using their models. IV. PROPOSED SOLUTION: IFLOW DIAGRAMS Here in this work a method for SoC protocols specification creation is described. Visual language called IFlow based on BPMN diagrams language is used for it. SoC protocol models described using IFlow should serve as a bridge between SoC architects, designers and validators. Let’s consider an IFlow diagram describing architecture of and SoC protocol. It can be presented as an oriented graph. Its nodes are tasks performed by SoC components that will be called “agents”. Edges of the graph can be of two types: control flows connecting sequential tasks performed by the same agent and messages connecting different agents. Let’s assume that text within a task is pseudocode that consists of a logical condition and a set of assignment operations on diagram variables and that text within a message or a control flow is a jump condition. It is easy to define a transition system S from this IFlow diagram. The definition of S consists of a set of state variables and a set of transition rules. The set of state variables is the set of diagram variables extended with the set of active messages with their status and the set of active control flows. The set of transition rules is inherited from the set of tasks. V. IFLOW DIAGRAMS VERIFICATION Translating the diagram into some formal model like the transition system S enables wide capabilities for the protocol analysis and verification. Two teams created two different approaches for IFlow diagram verification. One team [13] translated the transition system into Murφ and Promela models and used Murφ and Spin model checkers for their verification. Picture 2 shows an example of a toy security protocol of firmware load analyzed using this method. After protocol verification there were found a security issue that appears when two instances of the protocol run. The task sequence for the security violation is: 1, 2, 3, 4, 2`, 3`, 5, 7. The second team [14] designed a formalism called LSD (Live Sequence Diagrams) for IFlows diagram verification. This formalism is inherited from Petri nets and message sequence charts and combines features of these models. Both approaches bring good results: many mistakes in SoC protocol specifications were found that are very hard to catch “manually”, the quality of the architectural specifications grew dramatically. VI. CONCLUSION Existing process of SoC architectural specifications creation and usage has serious challenges. Here in this work we presented an approach for SoC architectural specifications creation using IFlow visual language derived from BPMN diagrams. Using IFlow diagrams allows creating accurate and unambiguous protocol specifications and further validating them by translation IFlow diagrams into formal models and using model checkers. Authors plan to continue their work on the approach. Main tasks are agreement on pseudocode syntax in diagram shapes and on assertions syntax for formal verification.
Keywords
	system on chip, design process, architecture, system level language, protocol, verification, BPMN, diagram, transition system.
Library reference
	Pechenko I.S. SoC protocols specification and validation: problems and solutions // Problems of Perspective Micro- and Nanoelectronic Systems Development - 2016. Proceedings / edited by A. Stempkovsky, Moscow, IPPM RAS, 2016. Part 2. P. 92-98.
URL of paper
	http://www.mes-conference.ru/data/year2016/pdf/D196.pdf