Andrey Mokhov
Victor Khomenko
Abstract
One of the difficulties in designing modern hardware systems is the necessity for comprehending and dealing with a very large number of system configurations, operational modes, and behavioural scenarios. It is often infeasible to consider and specify each individual mode explicitly, and one needs methodologies and tools to exploit similarities between the individual modes and work with groups of modes rather than individual ones. The modes and groups of modes have to be managed in a compositional way: the specification of the system should be composed from specifications of its blocks. This includes both structural and behavioural composition. Furthermore, one should be able to transform and optimise the specifications in a formal way.
In this article, we propose a new formalism, called parameterised graphs. It extends the existing conditional partial order graphs (CPOGs) formalism in several ways. First, it deals with general graphs rather than just partial orders. Moreover, it is fully compositional. To achieve this, we introduce an algebra of parameterised graphs by specifying the equivalence relation by a set of axioms, which is proved to be sound, minimal, and complete. This allows one to manipulate the specifications as algebraic expressions using the rules of this algebra. We demonstrate the usefulness of the developed formalism on several case studies coming from the area of microelectronics design.
- M. Bauderon and B. Courcelle. 1987. Graph expressions and graph rewritings. Math. Syst. Theory 20, 1 (1987), 83--127.Google Scholar
Cross Ref
- E. Best, R. Devillers, and M. Koutny. 2001. Petri Net Algebra. Monographs in Theoretical Computer Science, Springer. Google ScholarDigital Library
- A. Bizjak and A. Bauer. 2011. Alg User Manual. http://hg.andrej.com/alg/.Google Scholar
- B. A. Carré. 1971. An algebra for network routing problems. IMA J. Appl. Math. 7, 3 (1971), 273--294.Google ScholarCross Ref
- C. D'Alessandro, D. Shang, A. Bystrov, A. Yakovlev, and O. Maevsky. 2006. Multiple-rail phase-encoding for NoC. In Proceedings of the International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC). 107--116. Google ScholarDigital Library
- G. de Micheli. 1994. Synthesis and Optimization of Digital Circuits. McGraw-Hill Higher Education. Google ScholarDigital Library
- D. Eppstein. 1992. Parallel recognition of series-parallel graphs. Inform. Computat. 98, 1 (1992), 41--55. Google ScholarDigital Library
- F. Gadducci and R. Heckel. 1998. An inductive view of graph transformation. In Recent Trends in Algebraic Development Techniques. Lecture Notes in Computer Science, vol. 137, Springer, 223--237. Google ScholarDigital Library
- F. Gécseg. 1974. Composition of automata. In Automata, Languages and Programming. Lecture Notes in Computer Science, vol. 14, Springer, 351--363. Google ScholarDigital Library
- C. A. R. Hoare. 1978. Communicating sequential processes. Commun. ACM 21, 8 (1978), 666--677. Google ScholarDigital Library
- ITRS. 2011. International Technology Roadmap for Semiconductors: Design. http://www.itrs.net/Links/2011ITRS/2011Chapters/2011Design.pdf.Google Scholar
- M. B. Josephs and J. T. Udding. 1993. An overview of DI algebra. In Proceedings of the 26th Hawaii International Conference on System Sciences. Vol. 1, 329--338.Google Scholar
- R. McConnell and F. de Montgolfier. 2005. Linear-time modular decomposition of directed graphs. Discrete Appl. Math. 145, 2 (2005), 198--209. Google ScholarDigital Library
- R. Milner. 1982. A Calculus of Communicating Systems. Lecture Notes in Computer Science, vol. 92, Springer. Google ScholarDigital Library
- R. Milner, J. Parrow, and D. Walker. 1992. A calculus of mobile processes, Part I. Inform. Comput. 100, 1 (1992), 1--40. Google ScholarDigital Library
- A. Mokhov. 2012. An algebra of switching networks. Technical Report NCL-EEE-MSD-TR-2012-178. Newcastle University.Google Scholar
- A. Mokhov, A. Alekseyev, and A. Yakovlev. 2011a. Encoding of processor instruction sets with explicit concurrency control. IET Comput. Digital Techniques 5, 6 (2011), 427--439.Google ScholarCross Ref
- A. Mokhov, V. Khomenko, A. Alekseyev, and A. Yakovlev. 2011b. Algebra of parametrised graphs. Technical Report CS-TR-1307. School of Computing Science, Newcastle University. http://www.cs.ncl.ac.uk/publications/trs/papers/1307.pdf.Google Scholar
- A. Mokhov and A. Yakovlev. 2010. Conditional partial order graphs: Model, synthesis and application. IEEE Trans. Comput. 59, 11 (2010), 1480--1493. Google ScholarDigital Library
- C. E. Shannon. 1938. A symbolic analysis of relay and switching circuits. Trans. Amer. Institute Electr. Eng. 57 (1938), 713--723.Google ScholarCross Ref
- Texas Instruments. 2013. MSP430x4xx Family User's Guide. http://www.ti.com/lit/ug/slau056l/slau056l.pdf.Google Scholar
Index Terms
- Algebra of Parameterised Graphs
Recommendations
Algebra of Parameterised Graphs
ACSD '12: Proceedings of the 2012 12th International Conference on Application of Concurrency to System DesignOne of the difficulties in designing modern hardware systems is the necessity to comprehend and to deal with a very large number of system configurations, operational modes, and behavioural scenarios. It is often infeasible to consider and specify each ...
Taut distance-regular graphs and the subconstituent algebra
We consider a bipartite distance-regular graph @C with diameter D>=4 and valency k>=3. Let X denote the vertex set of @C and fix x@__ __X. Let @C"2^2 denote the graph with vertex set X@__ __={y@__ __X|@__ __(x,y)=2}, and edge set R@__ __={yz|y,z@__ __X@_...
Using Event-B to construct instruction set architectures
AbstractThe instruction set architecture (ISA) of a computing machine is the definition of the binary instructions, registers, and memory space visible to an executable binary image. ISAs are typically implemented in hardware as microprocessors, but also ...
Comments