VERIFY - A PROGRAM FOR PROVING CORRECTNESS OF DIGITAL HARDWARE DESIGNS

被引:37
作者
BARROW, HG
机构
[1] Fairchild Lab for Artificial, Intelligence Research, Palo Alto,, CA, USA, Fairchild Lab for Artificial Intelligence Research, Palo Alto, CA, USA
关键词
COMPUTER PROGRAMMING - COMPUTERS; MICROPROCESSOR - Computer Aided Design - LOGIC CIRCUITS - Computer Aided Design - SYSTEMS SCIENCE AND CYBERNETICS - Artificial Intelligence;
D O I
10.1016/0004-3702(84)90044-4
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
VERIFY is a PROLOG program that attempts to prove the correctness of a digital design. It does so by showing that the behavior inferred from the interconnection of its parts and their behaviors is equivalent to the specified behavior. It has successfully verified large designs involving many thousands of transistors.
引用
收藏
页码:437 / 491
页数:55
相关论文
共 33 条
  • [1] Boyer R.S., 1979, COMPUTATIONAL LOGIC
  • [2] BUNDY A, 1979, 6TH P INT JOINT C AR
  • [3] Clocksin W. F., 1981, Programming in Prolog
  • [4] Dahl O.-J, 1972, STRUCTURED PROGRAMMI
  • [5] DAVIS R, 1983, AUG P NAT C ART INT
  • [6] FATEMAN RJ, 1972, THESIS MIT CAMBRIDGE
  • [7] Floyd R.W., 1967, Proc. Symp. Appl. Math., V19, P19, DOI DOI 10.1090/PSAPM/019/0224860
  • [8] FOSTER MJ, 1981, VLSI SYSTEMS COMPUTA, P203
  • [9] FUJITA M, 1983, 6TH IFIP COMP HARDW, P103
  • [10] GABRIEL JR, 1983, ANLMCSTM10