---
_id: '4480'
abstract:
- lang: eng
  text: 'We describe the formal specification and verification of the VGI parallel
    DSP chip [1], which contains 64 compute processors with ~30K gates in each processor.
    Our effort coincided in time with the “informal” verification stage of the chip.
    By interacting with the designers, we produced an abstract but executable specification
    of the design which embodies the programmer''s view of the system. Given the size
    of the design, an automatic check that even one of the 64 processors satisfies
    its specification is well beyond the scope of current verification tools. However,
    the check can be decomposed using assume-guarantee reasoning. For VGI, the implementation
    and specification operate at different time scales: several steps of the implementation
    correspond to a single step in the specification. We generalized both the assume-guarantee
    method and our model checker MOCHA to allow compositional verification for such
    applications. We used our proof rule to decompose the verification problem of
    the VGI chip into smaller proof obligations that were discharged automatically
    by MOCHA. Using our formal approach, we uncovered and fixed subtle bugs that were
    unknown to the designers.'
article_processing_charge: No
author:
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Xiaojun
  full_name: Liu, Xiaojun
  last_name: Liu
- first_name: Shaz
  full_name: Qadeer, Shaz
  last_name: Qadeer
- first_name: Sriram
  full_name: Rajamani, Sriram
  last_name: Rajamani
citation:
  ama: 'Henzinger TA, Liu X, Qadeer S, Rajamani S. Formal specification and verification
    of a dataflow processor array. In: IEEE; 1999:494-499. doi:<a href="https://doi.org/10.1109/ICCAD.1999.810700">10.1109/ICCAD.1999.810700</a>'
  apa: 'Henzinger, T. A., Liu, X., Qadeer, S., &#38; Rajamani, S. (1999). Formal specification
    and verification of a dataflow processor array (pp. 494–499). Presented at the
    ICCAD: Computer-Aided Design, San Jose, CA, United States of America: IEEE. <a
    href="https://doi.org/10.1109/ICCAD.1999.810700">https://doi.org/10.1109/ICCAD.1999.810700</a>'
  chicago: Henzinger, Thomas A, Xiaojun Liu, Shaz Qadeer, and Sriram Rajamani. “Formal
    Specification and Verification of a Dataflow Processor Array,” 494–99. IEEE, 1999.
    <a href="https://doi.org/10.1109/ICCAD.1999.810700">https://doi.org/10.1109/ICCAD.1999.810700</a>.
  ieee: 'T. A. Henzinger, X. Liu, S. Qadeer, and S. Rajamani, “Formal specification
    and verification of a dataflow processor array,” presented at the ICCAD: Computer-Aided
    Design, San Jose, CA, United States of America, 1999, pp. 494–499.'
  ista: 'Henzinger TA, Liu X, Qadeer S, Rajamani S. 1999. Formal specification and
    verification of a dataflow processor array. ICCAD: Computer-Aided Design, 494–499.'
  mla: Henzinger, Thomas A., et al. <i>Formal Specification and Verification of a
    Dataflow Processor Array</i>. IEEE, 1999, pp. 494–99, doi:<a href="https://doi.org/10.1109/ICCAD.1999.810700">10.1109/ICCAD.1999.810700</a>.
  short: T.A. Henzinger, X. Liu, S. Qadeer, S. Rajamani, in:, IEEE, 1999, pp. 494–499.
conference:
  end_date: 1999-11-11
  location: San Jose, CA, United States of America
  name: 'ICCAD: Computer-Aided Design'
  start_date: 1999-11-07
date_created: 2018-12-11T12:09:04Z
date_published: 1999-01-01T00:00:00Z
date_updated: 2022-09-05T14:48:48Z
day: '01'
doi: 10.1109/ICCAD.1999.810700
extern: '1'
language:
- iso: eng
month: '01'
oa_version: None
page: 494 - 499
publication_identifier:
  issn:
  - 1092-3152
publication_status: published
publisher: IEEE
publist_id: '246'
quality_controlled: '1'
scopus_import: '1'
status: public
title: Formal specification and verification of a dataflow processor array
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '1999'
...