VLSI designs often show regular structures, where issues like temporal and spatial recursivity, and bidirectionality play a central role. This document introduces the modelling of a class of regular VLSI circiuts, namely iterative systolic arrays, in a particular second-order logic, and presents fully automatic verification of pipeline properties for an example from the literature.
Paper itself:
- compressed file (for previewing)
Cross links:
- more reports
- Lehrstuhlübersicht der Fakultät für Mathematik und Informatik
- Fakultät für Mathematik und Informatik
- Universität Passau
Ulrike Peiker, Martin Griebl