A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops

ABSTRACT

Due to the abstract and simple computation and communication mechanism in the synchronous computational model it is easy to simulate synchronous systems and to apply formal verification methods. In synchronous models, a local temporal refinement that increases the delay in a single computation block may affect the functionality of the entire model. To preserve the system's functionality after temporal refinements we provide a synchronization algorithm that applies also to models with nested feedback loops. The algorithm adds pure delay elements to the model in order to balance the delay caused by refinement and to assure concurrent data arrival at computation blocks. It is done so that the refined model stays latency equivalent to the original model. The advantages of our approach are that (a) we remain fully within the synchronous model of computation, (b) we preserve the functionality of the existing computation blocks, and (c) we do not require additional computation resources, wrapper circuits or schedulers.

REFERENCES

• 1: Samar Abdi , Daniel Gajski, Automatic generation of equivalent architecture model from functional specification, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996732]
• 2: Albert Benveniste , Benoît Caillaud , Paul Le Guernic, From Synchrony to Asynchrony, Proceedings of the 10th International Conference on Concurrency Theory, p.162-177, August 24-27, 1999
• 3: Gérard Berry , Michael Kishinevsky , Satnam Singh, System Level Design and Verification Using a Synchronous Language, Proceedings of the 2003 IEEE/ACM international conference on Computer-aided design, p.433, November 09-13, 2003 [doi>10.1109/ICCAD.2003.135]
• 4: Timothy J. Callahan , John Wawrzynek, Adapting software pipelining for reconfigurable computing, Proceedings of the 2000 international conference on Compilers, architecture, and synthesis for embedded systems, p.57-64, November 17-19, 2000, San Jose, California, United States [doi>10.1145/354880.354889]
• 5: L. Carloni, K. McMillan, and A. SangiovanniVincentelli. Theory of latency-insensitive design. IEEE Transactions on Computer-Aided Design, 20(9), 2001.
• 6: Luca P. Carloni , Alberto L. Sangiovanni-Vincentelli, A Framework for Modeling the Distributed Deployment of Synchronous Designs, Formal Methods in System Design, v.28 n.2, p.93-110, March 2006 [doi>10.1007/s10703-006-7842-x]
• 7: S. Edwards, L. Lavagno, E. A. Lee, and A. Sangiovanni-Vincentelli. Design of embedded systems: Formal models, validation, and synthesis. Proceedings of the IEEE, 85(3):366--390, March 1997.
• 8: Nicolas Halbwachs , Fabienne Lagnier , Christophe Ratel, Programming and Verifying Real-Time Systems by Means of the Synchronous Data-Flow Language LUSTRE, IEEE Transactions on Software Engineering, v.18 n.9, p.785-793, September 1992 [doi>10.1109/32.159839]
• 9: Shi-Yu Huang , Kwang-Ting Cheng , Kuang-Chien Chen, On Verifying the Correctness of Retimed Circuits, Proceedings of the 6th Great Lakes Symposium on VLSI, p.277, March 22-23, 1996
• 10: K. Keutzer, S. Malik, A. R. Newton, J. M. Rabaey, and A. Sangiovanni-Vincentelli. System-level design: Orthogonalization of concerns and platform-based design. IEEE Transaction on Computer-Aided Design of Integrated Circuits and Systems, 19(12):1523--1543, December 2000.
• 11: C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1):5--35, 1991.
• 12: Naresh Maheshwari , Sachin S. Sapatnekar, Minimum area retiming with equivalent initial states, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.216-219, November 09-13, 1997, San Jose, California, United States
• 13: Simin Nadjm-Tehrani , Jan-Erik Strömberg, Formal Verification of Dynamic Properties in an Aerospace Application, Formal Methods in System Design, v.14 n.2, p.135-169, March 1999 [doi>10.1023/A:1008651801000]
• 14: Dumitru Potop-Butucaru , Benoit Caillaud, Correct-by-Construction Asynchronous Implementation of Modular Synchronous Specifications, Proceedings of the Fifth International Conference on Application of Concurrency to System Design, p.48-57, June 07-09, 2005 [doi>10.1109/ACSD.2005.10]
• 15: M. Weinhardt and W. Luk. Pipeline vectorization. In IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pages 234--248, Feb 2001.

INDEX TERMS

Primary Classification:
  B. Hardware
  B.6 LOGIC DESIGN
      B.6.3 Design Aids

Additional Classification:
  J. Computer Applications
  J.6 COMPUTER-AIDED ENGINEERING
      Subjects: Computer-aided design (CAD)

General Terms:
Algorithms, Design

Keywords:
design refinement, synchronization, system design