Advertisement

Design and Implementation of Priority Queuing Mechanism on FPGA Using Concurrent Periodic EFSMs and Parametric Model Checking

  • Tomoya Kitani
  • Yoshifumi Takamoto
  • Isao Naka
  • Keiichi Yasumoto
  • Akio Nakata
  • Teruo Higashino
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2778)

Abstract

In this paper, we propose a design and implementation method for priority queuing mechanisms on FPGAs. First, we describe behavior of WFQ (weighted fair queuing) with several parameters in a model called concurrent periodic EFSMs. Then, we derive a parameter condition for the concurrent EFSMs to execute their transitions without deadlocks in the specified time period repeatedly under the specified temporal constraints, using parametric model checking technique. From the derived parameter condition, we can decide adequate parameter values satisfying the condition, considering total costs of components. Based on the proposed method, high-reliable and high-performance WFQ circuits for gigabit networks can be synthesized on FPGAs.

Keywords

Model Check Implementation Method Computation Tree Logic Time Automaton Circuit Size 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: HYTECH: A Model Checker for Hybrid Systems. International Journal on Software Tools for Technology Transfer 1(1-1), 110–122 (1997)CrossRefGoogle Scholar
  2. 2.
    I.S.O.: Information Processing System, Open Systems Interconnection LOTOS. ISO 8807 (1989)Google Scholar
  3. 3.
    Katagiri, H., Kirimura, M., Yasumoto, K., Higashino, T., Taniguchi, K.: Hardware Implementation of Concurrent Periodic EFSMs. In: Proc. of Joint Intl. Conf. on 13th Formal Description Techniques and 20th Protocol Specification, Testing, and Verification (FORTE/PSTV2000), pp. 285–300 (2000)Google Scholar
  4. 4.
    Nakata, A., Higashino, T.: Deriving Parameter Conditions for Periodic Timed Automata Satisfying Real-Time Temporal Logic Formulas. In: Proc. of 21st IFIP Int’l Conf. on Formal Techniques for Networked and Distributed Systems (FORTE2001), pp. 151–166 (2001)Google Scholar
  5. 5.
    Parekh, A., Gallager, B.: A Generalized Processor Sharing Approach to Flow Control in Integrated Services Networks—The Single Node Case —. IEEE/ACM Trans. on Networking 1(3), 344–357 (1993)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Tomoya Kitani
    • 1
  • Yoshifumi Takamoto
    • 1
  • Isao Naka
    • 2
  • Keiichi Yasumoto
    • 3
  • Akio Nakata
    • 1
  • Teruo Higashino
    • 1
  1. 1.Graduate School of Information Science and TechnologyOsaka UniversityJapan
  2. 2.Dept. of TourismOsaka Seikei UniversityJapan
  3. 3.Nara Institute of Science and TechnologyGraduate School of Information ScienceJapan

Personalised recommendations