Your browser does not support JavaScript!

Encoding of processor instruction sets with explicit concurrency control

Encoding of processor instruction sets with explicit concurrency control

For access to this article, please select a purchase option:

Buy article PDF
(plus tax if applicable)
Buy Knowledge Pack
10 articles for $120.00
(plus taxes if applicable)

IET members benefit from discounts to all IET publications and free access to E&T Magazine. If you are an IET member, log in to your account and the discounts will automatically be applied.

Learn more about IET membership 

Recommend Title Publication to library

You must fill out fields marked with: *

Librarian details
Your details
Why are you recommending this title?
Select reason:
IET Computers & Digital Techniques — Recommend this title to your library

Thank you

Your recommendation has been sent to your librarian.

There is a critical need for design automation in microarchitectural modelling and synthesis. One of the areas which lacks the necessary automation support is synthesis of instruction codes targeting various design optimality criteria. This paper aims to fill this gap by providing a set of formal methods and a software tool for synthesis of instruction codes given the description of a processor as a set of instructions. The method is based on the conditional partial order graph (CPOG) model, which is a formalism for efficient specification and synthesis of microcontrollers. It describes a system as a functional composition of its behavioural scenarios, or instructions, each of them being a partial order of events. In order to distinguish instructions within a CPOG they are given different encodings represented with Boolean vectors. Size and latency of the final microcontroller significantly depends on the chosen encodings, thus efficient synthesis of instruction codes is essential. The paper shows that the CPOG model is a very convenient formalism for efficient representation of processor instruction sets. It provides a ground for a concise formulation of several encoding problems, which are reducible to the Boolean satisfiability (SAT) problem and can be efficiently solved by modern SAT solvers.


    1. 1)
      • Lee, J., Choi, K., Dutt, N.: `Efficient instruction encoding for automatic instruction set design of configurable asips', Proc. Int. Conf. on Computer-Aided Design (ICCAD), 2002.
    2. 2)
      • Alomary, A., Nakata, T., Honma, Y., Sato, J., Hikichi, N., Imai, M.: `PEAS-I: A hardware/software co-design system for ASIPs', Proc. European Design Automation Conf. (EURO-DAC), 1993.
    3. 3)
      • I. Wegener . (1987) The complexity of boolean functions.
    4. 4)
      • Ranjan, D., Tang, D., Malik, S.: `A comparative study of 2QBF algorithms', Proc. Seventh Int. Conf. on Theory and Applications of Satisfiability Testing (SAT’04), 2004.
    5. 5)
      • MSP430x4xx Family User's Guide.
    6. 6)
      • Zhao, Q., Mesman, B., Basten, T.: `Practical instruction set design and compiler retargetability using static resource models', Proc. Design, Automation and Test in Europe (DATE), 2002.
    7. 7)
    8. 8)
    9. 9)
      • Nohl, A., Greive, V., Braun, G.: `Instruction encoding synthesis for architecture exploration using hierarchical processor models', Proc. 40th Annual Design Automation Conf. (DAC), ACM, 2003, p. 262–267.
    10. 10)
      • G. Birkhoff . (1967) Lattice theory.
    11. 11)
      • J. Cortadella , M. Kishinevsky , A. Kondratyev , L. Lavagno , A. Yakovlev , K. Itoh , T. Lee , T. Sakurai , D. Schmitt-Landsiedel . (2002) Logic synthesis of asynchronous controllers and interfaces, Advanced microelectronics.
    12. 12)
      • G. De Micheli . (1994) Synthesis and optimization of digital circuits.
    13. 13)
      • Mokhov, A., Sokolov, D., Rykunov, M., Yakovlev, A.: `Formal modelling and transformations of processor instruction sets', Technical report, 2011.
    14. 14)
      • D. Sokolov , I. Poliakov , A. Yakovlev . Analysis of static data flow structures. Fundam. Inform. , 4 , 581 - 610
    15. 15)
      • H.H. Aiken , G.M. Hopper . The automatic sequence controlled calculator.
    16. 16)
      • T.H. Cormen , C.E. Leiserson , R.L. Rivest , C. Stein . (2009) Introduction to algorithms.
    17. 17)
      • P. Mishra , N. Dutt , L. Sheffer , L. Lavagno , G. Martin . (2006) Processor modelling and design tools, EDA for IC systems design, verification, and testing.
    18. 18)
      • Mokhov, A.: `Conditional partial order graphs', 2009, PhD, Newcastle University.
    19. 19)
      • A.W. Burks , H.H. Goldstein , J. von Neumann . Preliminary discussion of the logical design of an electronic computing instrument.
    20. 20)
      • S.I. Baranov . (1994) Logic synthesis for control automata.

Related content

This is a required field
Please enter a valid email address