This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Abstract Model of Behavior for Hardware Descriptions
July 1983 (vol. 32 no. 7)
pp. 621-637
M.C. McFarland, Department of Computer Science, Boston College
As part of our research on the Carnegie-Mellon University Design Automation System, we have been investigating methods for proving that the system produces correct designs from correct specifications. We have developed a mathematical model for the behavior of hardware descriptions, which we have used to prove that some of the optimizing transformations used in the design system preserve behavioral equivalence. The model, which is based on regular expressions modified by predicates to show data dependence, goes beyond the usual computational models used in program verification, in that it takes into account the proper sequencing of those "events" which represent interactions with the environment. This paper presents the model, shows how it can be used to represent the behavior of descriptions in an ISP-like hardware description language, and gives an example proof of a transformation.
Index Terms:
verification, Computer-aided design, formal semantics, hardware description languages, models of behavior, optimization of hardware, transformations on hardware descriptions
Citation:
M.C. McFarland, A.C. Parker, "An Abstract Model of Behavior for Hardware Descriptions," IEEE Transactions on Computers, vol. 32, no. 7, pp. 621-637, July 1983, doi:10.1109/TC.1983.1676294
Usage of this product signifies your acceptance of the Terms of Use.