INDUSTRIAL CONFERENCES

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

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

    IBM CENTER ALMADEN

    Formal verification made easy Formal verification made easy, paper

    OTHER

    DC MetaData for: Polynomial Formal Verification of Multipliers
    Polynomial Formal Verification of Multipliers. by    M. Keim, M. Martin, B. Becker, R. Drechsler, P. Molitor. Formal Verification of Programs (CMU/SEI-CM-020)

    Design EXPLORE--Interactive Formal Verification Design EXPLORE. TM. Interactive Formal Verification Software. OVERVIEW. Chrysalis

    Chrysalis Design VERIFYer Formal Verification Datasheet Formal Equivalence Checking Software. The only. Complete, Accurate, Independent,Formal Design Solution. Download Data Sheet in PDF..

    Chrysalis Educational Services: Formal Verification
    Chrysalis Educational Services. Chrysalis training helps you quickly use our formal verification tools to speed up verification and increase the quality

    Chrysalis: the formal verification company
    Chrysalis supplies software products that use formal methods to automate the design of advanced digital integrated circuits.

    Chrysalis Debuts Design VERIFYer 2 Formal Verification Software
    Chrysalis Advances Formal Verification For Complex ASICs and Microprocessors. Partners drive development of capabilities to verify RTL and transistor.

    Formal Verification - A Viable Alternative toSimulation? Anders Nordstrom. Norther Telecom Ltd. Telecom Microelectronics Centre. Ottowa, Ontario Canada...

    Nortel Taps Chrysalis for Formal Verification
    Nortel Taps Chrysalis for Formal Verification. High-performance telecommunications ASICs to be checked with Design VERIFYer.

    QED Adopts Chrysalis' Formal Verification Software

    Chrysalis Announces Design EXPLORE Interactive Formal Verification Tool

    DEC Selects Chrysalis' Formal Verification Software
    CHRYSALIS SYMBOLIC DESIGN ANNOUNCES DIGITAL EQUIPMENT CORPORATION'S SELECTION OF CHRYSALIS FORMAL VERIFICATION.

    Chrysalis: the formal verification company
    Chrysalis supplies software products that use formal methods to automate the design of advanced digital integrated circuits.

    Leading Formal Verification with Superior Synthesis Alternative
    nbsp; AMBIT AND CHRYSALIS PARTNER FOR HIGH-END, HIGH-PERFORMANCE ASIC DESIGN. Links Leading Formal Verification with Superior Synthesis Alternative Chrysalis White Paper - Formal Verification for ASIC and IC Design EDA Today 11-95 - Chrysalis' formal verification for ASICs and micros
    An article from the EDA Today Summary Report Vol. 1, No. 11, November 1995. Chrysalis advances formal verification for complex ASICs and microprocessors.

    SYNOPSYS

    Synopsys Formal Verification -- Formality
    Synopsys Formality -- Formal verification tool for million-gate design

    AMBIT DEVELOPMENT PROCESS INCORPORATES INDEPENDENT FORMAL VERIFICATION FROM CH

    SYNOPSYS FORMALITY

    Synopsys Launches Formality, Formal Verification Tool
    Synopsys Launches Formality, Industry's First Formal Verification Tool for Million-Gate Designs.

    ASIC DESIGN VS. VERIFICATION

    (08.95) ASIC Design: Benchmarking Forum: Design Solutions: Formal verification

    (10.95) Technology Directions: ASICs, ICs & System Design: Formal verification

    (05.97) ASICs/DESIGN TOOLS: VHDL support for formal verification (62:0.17)

    FPGA DESIGN VS. VERIFICATION

    A Highly Parallel FPGA-Based Machine and its Formal Verification

    ELECTRONIC NEWS

    >January 20, 1997 Electronic News

    PRAXIS

    Praxis Critical Systems: SPARK

    VARIOUS

    ACM Computing Surveys: Position Statement, Gerard J. Holzmann

    Prototyping
    Prototyping. Another New Company Showing up at DAC. Dataquest DAC Presentation. Ready For Prime Time? 4/95. Resurgence in Prototyping.

    MIL-STD 490-A SPECIFICATION PRACTICES

    CHRYSALIS

    TITLE
    CHRYSALIS EXPANDS FIELD ORGANIZATION. Formal verification leader initiates international operations, appoints VP, North American Sales

    Chrysalis: the Formal Design Company
    Chrysalis supplies software products that use formal methods to automate the design of advanced digital integrated circuits.

    ASIC

    ASIC'95 Conference Information

    Viewlogic - The Year 2001

    VARIOUS

    Notes1
    I. Course Introduction A. Review of COSC 236 Topics 1. Characterization of Field of Computer Science.

    Research Report 1995
    Laboratory for Applied Logic. Research Report. 1994-1995. Computer Science Home Page. Univ. of Idaho Home Page. Jim Alves-Foss, LAL Director
    Giampaolo Bella's Dissertation

    Research in VLSI Design Automation

    Arpa Project Summary: Highly Assured and Fault-Tolerant Security in Distribute
    SRI International Computer Science Laboratory and AT&T Laboratories. Arpa Project Summary: Highly Assured and Fault-Tolerant Security in Distributed..

    LIDOS BibTeX Database File ec-95_a42009-29.bib
    German Research Center for Artificial Intelligence GmbH.

    Faculty Publications
    Electrical Engineering and Computer Sciences Faculty Publications (1994-1995)

    Grand Unification Theory List of EDA- and Design-Related Software
    EDA- and Design-Related Software. This is the list of software for the Electronic Design Automation brief of grand-unification-theory. Comments

    DAC'96 - Design Methodology Sessions

    Undergraduate Supplemental Calendar 1997/98

    Design Tools Sessions
    34TH DAC DESIGN TOOLS SESSIONS.

    No Title
    TO: Design Sciences STAB Design Sciences Mentors Design Sciences PIs FROM: Justin E. Harlow, III Program Manager DATE:
    No Title
    The Infeasibility of Quantifying the Reliability of Life-Critical Real-Time Software Butler, Ricky W. Finelli, George B.

    Events Archive: IEEE CS Eurom Digital System Design workshop cfp (fwd)

    Cover Story - December 1997
    Design Automation. Readers Speak Out on DSM: Part 2. Our three-part report on readers' experiences with deep-submicron design continues.

    Anya's Home Page
    Anna Pogosyants. Former Graduate student (PhD candidate, Advisor: Nancy Lynch) In memory of Anna (Anya), a UROP (Undergraduate Research Opportunities

    Kljaich, J.
    The Petri Nets Bibliography:

    International Computer Science Institute Talks

    CALL FOR PARTICIPATION *** SYSTEM LEVEL DESIGN WORKSHOP DFW

    Opening Remarks

    LIDOS BibTeX Database File co-94_a43162-99.bib

    190. COSC4422
    Formal Verification
    Dipartimento di Scienze dell'Informazione. Formal Verification. The aim of formal verification is to prove that a program/circuit is correct

    The Formal Verification Technology Used for the AAMP5 and AAMP-FV

    (10.95) ASIC Design: Special Report: Using formal verification.

    Formal Verification Group
    Design Automation Section, Eindhoven University of Technology. Welcome to the pages of the Formal Verification Group of the Design Automation Section.

    Formal Verification Using a Network of Workstations

    Formal Verification of Embedded Systems based on CFSM Networks

    Trans. Computers: Abstract: Formal Verification Using Edge-Valued Binary Decis Yung-Te Lai, Massoud Pedram, and Sarma B.K. Vrudhula.

    Introduction to Formal Verification
    Introduction to Formal Verification. Applying Formal Methods to Spacecraft Sub-systems.

    Efficient Formal Verification Using Transition Hierarchies

    Computer Engineering Research Center: UT Austin

    No Title
    Date: Tue, 31 Mar 92 20:19:44 CST From: Robert S. Boyer.

    June 9, 1997 Electronic News
    From Page One of Electronic News: June 9, 1997 Issue. DESIGN AUTOMATION CONFERENCE. Verification Enigma - Direction To Take. By Judy Erkanat

    Architecture Design
    Next: Outline of Our Up: Introduction Previous: Advancement of CAD. Architecture Design. Processors are used not only for personal computers
    archive: Formal Verification Opportunities at National Semiconductor
    Formal Verification Opportunities at National Semiconductor. Joseph Lu (jlu@berlioz.nsc.com) Thu, 5 Jun 1997

    Formal Verification of Communication Protocols
    Formal Verification of Communication Protocols. James F. Leathrum, Jr., Rasha M.B.E. Morsi, and Thomas E. Leathrum.

    PAMPAS_WP1_ANNEX - Simulation and Formal Verification and Validation
    Simulation and Formal Verification and Validation. GEODE includes a powerful simulation and validation tool.

    Subject: Postdoc Position in Formal Verification

    Formal Verification of the K5 Divide Program - Abstract

    Towards a Formal Verification of a Distributed System and its Applications

    Chrysalis White Paper - What is Formal Verification

    HP saves months with Design VERIFYer formal verification software
    Customer Success Story.
    IBM Microelectronics Supports Chrysalis Formal Verification For ASIC Design Flow.

    NP-Tools, Formal Verification of Complex Systems
    NP-Tools, Formal Verification of Complex Systems. Description. NP-Tools is a computer based set of tools for modelling and formally verifying systems.

    Sun Mircosystems Selects Chrysalis for Formal Verification
    SUN MICROSYSTEMS SELECTS CHRYSALIS FOR FORMAL VERIFICATION.

    Formal Verification of Real-Time Kernels

    Chrysalis: the formal verification company
    Chrysalis supplies software products that use formal methods to automate the design of advanced digital integrated circuits.

    Reetz, R.; Kropf, T.: Principles of formal verification tools for VHDL
    Formal Verification
    Symbolic Methods for Formal Hardware Verification. Funding. Research in formal hardware verification at CMU.

    Chrysalis the Formal Verification
    Chrysalis supplies software products that use formal methods to automate the design of advanced digital integrated circuits.

    Specification, Formal Verification and Implementation of Tasks and Mission : Application to the Distribution of Empty Vehicles in the Praxitele Project. S. Abdou, M. Parent and B. Espiau

    A Scalable Formal Verification Methodology for Pipelined Microprocessors Jeremy Levitt and Kunle Olukotun. Computer Systems Laboratory, Stanford...

    Formal Verification
    Formal Verification. RuleBase is a symbolic model checking tool, developed by the IBM Haifa Research Laboratory.

    The Formal Verification of the Fairisle ATM Switching Element

    Annals: Abstract: Mathematics, Technology, and Trust: Formal Verification, Com
    Mathematics, Technology, and Trust: Formal Verification, Computer Security, and the U.S. Military. Donald Mackenzie and Garrel Pottinger.
    (8.97) DESIGN TRENDS: Formal verification heads for mainstream (20:1.5)
    August, 1997. Home - Editorial

    Formal Verification of Reactive Systems
    My main interest is in the area of Formal Verification of Reactive Systems.

    (06.97) ASICs/DESIGN TOOLS: Adding to formal verification (75:0.25)
    June, 1997. Home - Editorial - June, 1997

    concurrency-1994: Surveys on formal verification?
    Surveys on formal verification? Hans van der Schoot (vdschoot@csi.uottawa.ca) Fri, 3 Jun 1994

    Simulation vs formal verification
    Next: Limitations to verification Up: Uses and limitations Previous: Simulation. Simulation vs formal verification. It is instructive to compare.

    Formal Verification
    Theoretical Computer Science. Formal Specification and Verification of Real-Time Systems. Automated Verification of Object-Oriented Systems. System-Level.

    Ph.D. scholarship in Formal Verification

    Spin - Formal Verification
    Spin is a general tool for verifying the correctness of distributed software (designs) in a rigorous and mostly automated fashion.

    Formal Verification Support for HLS

    Formal Verification
    Formal Verification. Mathematically proves correctness. Shows implementation satisfies properties required by specification. Guarantees complete coverage..

    Formal Verification of Interfaces

    Formal Verification
    nbsp; Formal Verification Research. Computer Engineering Research Center The University of Texas at Austin.

    Interfacing System Description Language to Formal Verification Wendell Baker ( wbaker@eecs.berkeley.edu) PostScript (contains all figures)

    Formal Verification of Transformations for Peephole Optimization
    University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence.

    SPIN - Formal Verification
    THE MODEL CHECKER SPIN. We modified the original document to describe the customization of the SPIN package here at CNUCE.

    Formal Verification
    Prof. Ben-Avi] Formal Verification.   Introduction.   Motivation for Formal Verification.

    Interfacing System Description Language to Formal Verification
    Interfacing System Description Languages to Formal Verification. Wendell Baker

    Formal Verification of Transformations for Peephole Optimization
    University of Ulm, Faculty of Computer Science, Dept. of Artificial Intelligence. up: Our Papers. Formal Verification of Transformations for Peephole...

    SPIN - Formal Verification
    THE MODEL CHECKER SPIN. We modified the original document to describe the customization of the SPIN package here at CNUCE.

    Formal Verification
    Prof. Ben-Avi] Formal Verification.   Introduction.   Motivation for Formal Verification.
    Structured formal verification
    Structured formal verification. Alfons Geser, Wolfgang Küchlin: fragment of the IBM 390 Clock Chip

    Formal Verification of Concurrent Program using the Larch Prover
    Formal Verification of Concurrent Program using the Larch Prover. Boutheina Chetali. In TACAS, pages 174--186. Abstract: This paper describes, by means of.

    The Formal Verification of Hardware Timing
    Document Archive. The Formal Verification of Hardware Timing George J. Milne. Tech Report No. RR-88-05 (formally HDV-02-88). University of Strathclyde.

    Formal Verification of the K5 Divide Program
    Formal Verification of the K5 Divide Program. author affiliations. colloquia anouncement. abstract. technical report explaining how the proof works.

    VARIOUS

    FORVERTIS
    D:\WINNT\Profiles\Administrator\Desktop\QC\html\geninsp.html
    1 Abstract. This document describes the routines for inspecting various types of documents and code. Inspecting documents and code will remove faults.

    DAC Harriet Feature - June 1997
  10. ELLA