2011 | OriginalPaper | Buchkapitel
Exploiting Abstraction for Efficient Formal Verification of DSPs with Arrays of Reconfigurable Functional Units
verfasst von : Miroslav N. Velev, Ping Gao
Erschienen in: Formal Methods and Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We compare two approaches for efficient formal verification of the integration of pipelined processor cores with arrays of reconfigurable functional units. The processors are modeled at a high level of abstraction, using a subset of Verilog, in a way that allows us to exploit the property of Positive Equality that results in significant simplifications of the solution space, and orders of magnitude speedup relative to previous methods. The presented techniques allow us to formally verify the integration of pipelined processors, including complex Digital Signal Processors (DSPs), with arrays of reconfigurable functional units of any size, where the reconfigurable functional units have any design, and for any topology of the connections between them. Such architectures are becoming increasingly used because of their much higher performance and reduced power consumption relative to conventional processors. One of the compared two approaches, which abstracts the entire array of reconfigurable functional units, results in at least 3 orders of magnitude speedup relative to the other approach that models the exact number of reconfigurable functional units and abstracts the design of each and the network that connects them, such that the speedup is increasing with the size of the array. To the best of our knowledge, this is the first work on automatic formal verification of pipelined processors with arrays of reconfigurable functional units.