--- _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:10.1109/ICCAD.1999.810700' apa: 'Henzinger, T. A., Liu, X., Qadeer, S., & 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. https://doi.org/10.1109/ICCAD.1999.810700' chicago: Henzinger, Thomas A, Xiaojun Liu, Shaz Qadeer, and Sriram Rajamani. “Formal Specification and Verification of a Dataflow Processor Array,” 494–99. IEEE, 1999. https://doi.org/10.1109/ICCAD.1999.810700. 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. Formal Specification and Verification of a Dataflow Processor Array. IEEE, 1999, pp. 494–99, doi:10.1109/ICCAD.1999.810700. 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' ...