Synchronization after design refinements with sensitive delay elements

ABSTRACT

The synchronous computational model with its simple computation and communication mechanism makes it easy to describe, simulate and formally verify synchronous embedded systems at a high level of abstraction. In synchronous models, a local refinement increasing the delay in a single computation block may affect the functionality of the entire model. We provide a synchronization algorithm that preserves the system's functionality after design refinements, by using additional synchronization delays and making some delays sensitive to their input values. The refined and synchronized model stays latency equivalent to the original model. The advantages of our approach are the following: (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, specific communication protocols, wrapper circuits around computation blocks 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: 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]
• 5: Mario R. Casu , Luca Macchiarulo, A new approach to latency insensitive design, Proceedings of the 41st annual conference on Design automation, June 07-11, 2004, San Diego, CA, USA [doi>10.1145/996566.996725]
• 6: 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.
• 7: 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]
• 8: 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.
• 9: C. E. Leiserson and J. B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1):5--35, 1991.
• 10: 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
• 11: 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]
• 12: 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]
• 13: Tarvo Raudvere , Ingo Sander , Axel Jantsch, A synchronization algorithm for local temporal refinements in perfectly synchronous models with nested feedback loops, Proceedings of the 17th ACM Great Lakes symposium on VLSI, March 11-13, 2007, Stresa-Lago Maggiore, Italy [doi>10.1145/1228784.1228869]
• 14: The SMV model checker. online {available} http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/.
• 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