More Web Proxy on the site http://driver.im/

Article

Free access

Symbolic simulation for functional verification with ADLIB and SDL

Author:

W. E. CoryAuthors Info & Claims

DAC '81: Proceedings of the 18th Design Automation Conference

Pages 82 - 89

Published: 29 June 1981 Publication History

Abstract

The basic verification problem addressed in this paper is to determine the consistency of two digital design descriptions. This is done by symbolically simulating each description and comparing the results. This approach is complicated by the presence of different levels of abstraction and asynchronous timing.

This paper motivates interest in this problem and provides background information on verification, ADLIB, and SDL. It then discusses approaches for dealing with the problems encountered in the symbolic simulation of ADLIB/SDL descriptions.

References

[1]

D. Brand "Algebraic Simulation between Parallel Programs," IBM Research Report RC 7206, Yorktown Heights, N.Y., 39 pp., June 1978

[2]

W.C. Carter, H.A. Ellozy, W.H. Joyner Jr., and G.B. Leeman Jr. "Techniques for Microprogram Validation," IBM Research Report RC 6361, Yorktown Heights, N.Y., 19 pp., Jan. 1977

[3]

W.C. Carter, W.H. Joyner Jr., and D. Brand "Microprogram Verification Considered Necessary," Proc. National Computer Conference, pp. 657-664, 1978

[4]

W.C. Carter, W.H. Joyner Jr., and D. Brand "Symbolic Simulation for Correct Machine Design," Proc. 16th Design Automation Conference, San Diego, pp. 280-286, 1979

Digital Library

[5]

W.E. Cory and W.M. vanCleemput "Developments in Verification of Design Correctness: A Tutorial", Proc. 17th Design Automation Conference, Minneapolis, pp. 156-164, 1980

Digital Library

[6]

J.A. Darringer "The Application of Program Verification Techniques to Hardware Verification," Proc. 16th Design Automation Conference, San Diego, pp. 375-381, 1979

Digital Library

[7]

C.J. Evangelisti, G. Goertzel, and H. Ofek "LCD - Language for Computer Design (Revised)," IBM Research Report RC 6244, Yorktown Heights, N.Y., 32 pp., Oct. 1976

[8]

C.J. Evangelisti, G. Goertzel, and H. Ofek "Designing with LCD - Language for Computer Design," Proc. Fourteenth Design Automation Conference, New Orleans, pp. 369-376, 1977

Digital Library

[9]

D.D. Hill "ADLIB: A Modular, Strongly-Typed Computer Design Language," Proc. Fourth Intl. Symposium on Computer Hardware Description Languages, Palo Alto, pp. 75-81, 1979

[10]

D.D. Hill "Language and Environment for Multi-Level Simulation" Technical Report No. 185, Stanford University, Dept. of Electrical Engineering, Ph.D. thesis, 170 pp., March 1980

[11]

S.L. Hantler and J.C. King "An Introduction to Proving the Correctness of Programs," ACM Computing Surveys, vol. 8, no. 3, pp. 331-353, Sept. 1976

Digital Library

[12]

D.D. Hill and W.M. vanCleemput "SABLE: A Tool for Generating Structured, Multi-level Simulations," Proc. Sixteenth Design Automation Conference, San Diego, pp. 272-279, June 1979

Digital Library

[13]

K. Jensen and N. Wirth Pascal User Manual and Report, Second Edition, New York: Springer-Verlag, 1979

Digital Library

[14]

J. King "Symbolic Execution and Program Testing," IBM Research Report RC 5082, Yorktown Heights, N.Y., Oct. 1974

[15]

N. Kawato, T. Saito, F. Maruyama, and T. Uehara "Design and Verification of Large-Scale Computers by Using DDL," Proc. 16th Design Automation Conference, San Diego, pp. 360-366, 1979

Digital Library

[16]

G.B. Leeman Jr., W.H. Joyner Jr., and W.C. Carter "An Automated Proof of Microprogram Correctness," IBM Research Report RC 6587, Yorktown Heights, N.Y., 33 pp., June 1977

[17]

S. Leinwand and T. Lamdan "Design Verification Based on Functional Abstraction," Proc. 16th Design Automation Conference, San Diego, pp. 353-359, 1979

Digital Library

[18]

H. Ofek, J.D. Lesser, C.J. Evangelisti, and G. Goertzel "Structured Design Verification of Sequential Machines," IBM Research Report RC 7037, Yorktown Heights, N.Y., 20 pp., March 1978

[19]

J.P. Roth "Verify: An Algorithm to Verify a Computer Design" IBM Technical Disclosure Bulletin, vol. 15, no. 8, pp. 2646-2648, Jan. 1973

[20]

J.P. Roth "Generation and Verification of Hardware Designs at High Level," IBM Research Report RC 5779, Yorktown Heights, N.Y., 16 pp., Nov. 1975

[21]

J.P. Roth "Hardware Verification," IEEE Trans. Computers, vol. C-26, no. 12, pp. 1292-1294, Dec. 1977

[22]

W.M. vanCleemput "A Structural Design Language for Computer Aided Design of Digital Systems" Stanford University, Computer Systems Laboratory, Technical Report No. 136, 27 pp., April 1977

Digital Library

[23]

D. van-Mierop "An Experiment in Automatic Verification of Microcode" Univ. of Southern California, Information Sciences Institute, Microver note #31, 21 pp., June 1979

Cited By

Chen CParker APaulin P(1994)A hybrid numeric/symbolic program for checking functional and timing compatibility of synthesized designsProceedings of the 7th international symposium on High-level synthesis10.5555/254208.254245(112-117)Online publication date: 20-May-1994
https://dl.acm.org/doi/10.5555/254208.254245
Feldbusch FKumar RAmbler TJess JDe Man H(1991)Verification of synthesized circuits at register transfer level with flow graphsProceedings of the conference on European design automation10.5555/951513.951518(22-26)Online publication date: 25-Feb-1991
https://dl.acm.org/doi/10.5555/951513.951518
Bryant RSmith R(1991)Symbolic simulation—techniques and applicationsProceedings of the 27th ACM/IEEE Design Automation Conference10.1145/123186.128296(517-521)Online publication date: 3-Jan-1991
https://dl.acm.org/doi/10.1145/123186.128296
Show More Cited By

Index Terms

Symbolic simulation for functional verification with ADLIB and SDL

Recommendations

Formal verification of high-level data-flow synthesis designs using relational modeling and symbolic computation

This paper presents a formal verification methodology of high-level data-flow synthesis process. Typically, given a data-flow description, the high-level data-flow synthesis tools perform high-level restructuring and data-flow transformations to produce ...
Formal semantics, modular specification, and symbolic verification of product-line behaviour

Formal techniques for specifying and verifying Software Product Lines (SPL) are actively studied. While the foundations of this domain recently made significant progress with the introduction of Featured Transition Systems (FTSs) and associated ...
A Functional Approach to Module Verification

The purpose of this paper is to develop a method for designing and verifying data abstractions using the functional approach. Before doing so, the existing techniques for designing and verifying procedure and data abstractions will be surveyed briefly. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '81: Proceedings of the 18th Design Automation Conference

June 1981

899 pages

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE-CS\DATC: IEEE Computer Society

Publisher

IEEE Press

Publication History

Published: 29 June 1981

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
155
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)4

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chen CParker APaulin P(1994)A hybrid numeric/symbolic program for checking functional and timing compatibility of synthesized designsProceedings of the 7th international symposium on High-level synthesis10.5555/254208.254245(112-117)Online publication date: 20-May-1994
https://dl.acm.org/doi/10.5555/254208.254245
Feldbusch FKumar RAmbler TJess JDe Man H(1991)Verification of synthesized circuits at register transfer level with flow graphsProceedings of the conference on European design automation10.5555/951513.951518(22-26)Online publication date: 25-Feb-1991
https://dl.acm.org/doi/10.5555/951513.951518
Bryant RSmith R(1991)Symbolic simulation—techniques and applicationsProceedings of the 27th ACM/IEEE Design Automation Conference10.1145/123186.128296(517-521)Online publication date: 3-Jan-1991
https://dl.acm.org/doi/10.1145/123186.128296
Ishiura NTakahashi MYajima SThomas D(1989)Time-symbolic simulation for accurate timing verification of asynchronous behavior of logic circuitsProceedings of the 26th ACM/IEEE Design Automation Conference10.1145/74382.74465(497-502)Online publication date: 1-Jun-1989
https://dl.acm.org/doi/10.1145/74382.74465
Lathrop RKirk ROfek HO'Neill L(1985)An extensible object-oriented mixed-mod functional simulation systemProceedings of the 22nd ACM/IEEE Design Automation Conference10.5555/317825.317956(630-636)Online publication date: 1-Jun-1985
https://dl.acm.org/doi/10.5555/317825.317956
Rosenberg JBoyer DDallen JDaniel SPoirier CPoulton JRogers DWeste NRadke COfek HShaklee DLosleben PNash JPistilli PLambert PPreas BLerman H(1983)A vertically integrated VLSI design environmentProceedings of the 20th Design Automation Conference10.5555/800032.800637(31-38)Online publication date: 27-Jun-1983
https://dl.acm.org/doi/10.5555/800032.800637

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents