Verification Using Prolog

1. Masahiro Fujita, Hidehiko Tanaka, Tohru Moto-Oka: Temporal Logic Based Hardware Description and Its Verification with Prolog. New Generation Computing 2(1): 195-203 (1983)
2. Circuit Verification in Prolog
3. Oxford System written in Prolog
4. M. E. Leeser. Reasoning about the function and timing of integrated circuits with Prolog and Temporal Logic. Technical Report 126, University of Cambridge Computer Laboratory, 1987.

BDD-Based Approaches

1. CS/EE 649 - Real-Time Hardware Verification. Handouts.
2. Randal Bryant on BDDs and Verification

INDUSTRIAL CONFERENCES

1. HESDC '97 Program Overview. Industrial conference in Validation, verification, etc.

RESEARCH GROUPS

1. Excellent Resources including Software from Oxford
   
   
2. Vis (Verification Interaction with Synthesis)
3. Oxford University Computing Laboratory list of formal methods resources
4. Formal Methods Around The World
5. Carnegie-Mellon University CSD: Formal Methods Research
6. NASA Langley Formal Methods Program
7. Formal Methods at CSL, SRI International

   GERMANY

8. Hardware Verification Group, University of Karlsruhe, Germany
   Formal Verification of Combinational Circuits

   STANFORD

   Stanford CS Dept. Verification Group Papers

   Publications of Prof.Dill and his group at Stanford

   MILITARY

   The Larch/VHDL Methodology for Hardware Verification

   SRC's Larch Home Page.

HOL

1. HOL PRIMER FROM UTAH
2. On the Comparison of HOL and Boyer-Moore for Formal Hardware Verification
3. The HOL System
4. HOL Tutorial
5. Demonstration Code for Hardware Verification in HOL
6. HOL

BIBLIOGRAPHIES

1. Isabelle
2. Mizar
3. Automated Deduction
4. Hardware Verification and Formal Methods
5. Logical Frameworks
6. Computer Algebra
7. Logic Programming
8. Prolog
9. LISP
10. Big bibliography of JACM and others
11. Computer Science bibliography collection
12. Mathematics bibliography collection
13. List of computer science bibliographies
14. Bibliographies collection

UNIVERSITY COURSES ON VERIFICATION.

1. BRICS notes on various systems and ideas at the recent Autumn School on Verification.
2. Mike Gordon, Cambridge. Course in Verification
3. Computational Modelling of Mathematical Reasoning, Alan Bundy and Alan Smaill See links, good.
4. Formal Hardware Verification by Symbolic Simulation
5. VLSIhoo?! Worldwide VLSI/IC/Microprocessor R&D Repository
6. Coverage-Based Microprocessor Verification
7. Shui-Kai Chin, Syracuse, Course in Hardware Verification
8. Adnan Aziz, U Texas, Course in Hardware Verification
9. Alan Hu, UBC, Course in Hardware Verification
10. Thomas Kropf, U Karlsruhe (in German), Course in Hardware Verification
11. Robert K. Brayton, UC Berkeley, Course in Hardware Verification, Logic Desing oriented.
12. John Harrison, Cambridge, Functional programming course, Hardware Verification.

BENCHMARKS

1. Benchmarks from Germany

FREE SOFTWARE

1. Some relevant software that could be used as part of a verification course. Page with all other software.
2. Page with VIS software for verification.
   VIS (Verification Interacting with Synthesis) is a system for formal verification,
   synthesis, and simulation of finite state systems.
   It has been developed jointly at the University
   of California at Berkeley, the University of Colorado at Boulder, and the University of Texas, Austin.
   
   VIS is able to synthesize finite state systems and/or
   verify properties of such systems, which have been specified
   hierarchically as a collection of interacting finite state machines.
   VIS provides the following features:
   Simulation of logic circuits (proof of concept only).
   Formal "implementation" verification of combinational and sequential circuits (proof of concept only).
   State-of-the-art formal "design" verification using fair CTL model checking and language emptiness.
   Logic synthesis via hierarchy restructuring and a path to and from SIS.
   
   Each of these can be executed interactively from any point in the design hierarchy.
   A Verilog HDL front end, vl2mv, is also provided,
   which compiles a subset of Verilog into an intermediate format BLIF-MV.
3. From Goethe University in Germany: The C@S Verfication System

COMMERCIAL VERIFICATION COMPANIES

SYNOPSYS: Formality Tool and others.

1. Formality Tool from Synopsys, introduction.
2. Synopsys Tools
3. Success Story of using Synopsys Formality
4. Models from Synopys

CHRYSALIS CORPORATION

1. Chrysalis tools Information and links.
2. Chrysalis tools and Competition. Win $1,000.00 .

ABSTRACT HARDWARE LIMITED

1. Abstract Hardware Limited (for CheckOff-E and CheckOff-M tools)

HARDWARE VERIFICATION MARKET AND INTEL BUG

1. Hardware Verification Market
2. Intel Bug
3. OOps! Another Intel Bug. November 7, 1997, Web Resource, C|Net reported the discovery of a programming error in the standard Pentium processor.

CO-DESIGN

1. Co-Design
2. INSYDE
3. Provably Correct Hardware/Software Co-design
4. Cornell Co-Design

FORMAL METHODS

1. World-Wide LOTOS
2. Circal (CIRcuit CALculus)
3. Verimag
4. CADP

VHDL, HARDWARE SPECIFICATION AND VERIFICATION

1. VHDL User Forum
2. VHDL-93 Formatter/Parser (in Prolog)
3. Ruby
4. Rainbow

Digital FPGAs and CPLDs

1. GENERAL INFORMATION: http://www.optimagic.com/companies.html
   all companies.
2. Use of Xilinx.
3. Altera UP1 Educational board
4. ATMEL.
5. Lattice
6. Motorola.

Digital Design Tools

1. Xilinx.
2. Aldec Alliance for Xilinx.
3. Altera.
4. ORCAD
5. Mentor
6. Summit. Visual HDL for VHDL on Windows.
7. Cypress. VHDL book.
8. Free Demo from Motorola.
9. Lattice Semiconductor.

Reconfigurable FPGA Computers

1. DEC PERLE-1.
2. http://www.irisa.fr/EXTERNE/bibli/pi/pi810.html
3. http://www.ai.mit.edu/projects/transit/rcgp/chapter1.4.3.html
4. http://www.iro.umontreal.ca/~cloutier/FPGA/fpga.html
5. http://www.io.com/~guccione/bib/fccm94.html
6. PAMETTE. http://www.optimagic.com/boards.html
   http://africa.cern.ch/digital-at-cern/joint-project/pcipamv1/pci-presentation-951017.html
7. XPUTER. Xputers Page
8. SPLASH.
9. Other. http://www.ee.pdx.edu/~mperkows/RECONFIGURABLE/=index-RECONFIGURABLE.html

Analog and Mixed FPGAs

1. IMP. IMP EPAC FPAA in Switched-capacitor Technology with bandwidth of 150kHz.
2. Motorola.
   Motorola MPAA020 in Switched-capacitor Technology with bandwidth of 200kHz.
   Motorola FPAA Contact Information
3. Review of Motorola's chip.
4. Zetex. Zetex TRAC in Continuous-time Technology, Bipolar with bandwith 4MHz.
5. Universities.
   1. Portland State University. FPAAs of Analogix.
   2. University of Toronto. Lee-Gulak (1995) Continuous-time CMOS 125kHz
      
   3. University of Toronto FPAA Bibliography.
   4. University of Toronto General Information on FPAAs.
   5. Look to all University of Toronto General FPAA Pages - a lot of useful information there.
   
   
6. Mixed Programmable Devices and Boards. Rapid Retargeting and Reconfigurable Logic Engines. A Solution to Electronic Systems Obsolescence by Dr. Gary L. Fitzhugh VisiCom Laboratories, Inc.
7. Mixed Analog-Digital FPGAs.
8. Mixed Design Editorial:

IBM CENTER ALMADEN