Method for Formal Verification of Polymorphic Heterogeneous Multicore Processors
Amethod was developed to model polymorphic heterogeneous multicore processors at a high level of abstraction, and formally verify them. The Bahurupi polymorphic heterogeneous multi-core architecture allows the combination of multiple simple processor cores — which can be superscalar — in order to form a coalition that behaves like a wider superscalar processor. This is done at runtime under software directives, allowing the architecture to adapt to the needs of executed applications with high instruction level parallelism. Such coalitions of cores were found to have comparable or better performance than that of a wide superscalar processor with issue width equal to the sum of the issue widths of the simple cores in the coalition, while avoiding the complexity, reliability issues, and high power consumption of wide superscalar cores. All of these are highly desirable advantages of future microprocessors that will be optimized for aerospace applications.
The method is based on using suitable abstractions for the building blocks of a polymorphic heterogeneous multicore processor. The method is based on the formal verification method of correspondence checking by exploiting the property of positive equality. Suitable abstractions and invariant constraints were defined that are sufficient for the formal verification.
For test data, a high-level model of a polymorphic heterogeneous multicore processor was designed. The method enabled formal verification of polymorphic heterogeneous multicore processors with two, four, or more cores.
This work was done by Miroslav N. Velev and Ping Gao of Aries Design Automation for Glenn Research Center.
Inquiries concerning rights for the commercial use of this invention should be addressed to
NASA Glenn Research Center
Technology Transfer Office at This email address is being protected from spambots. You need JavaScript enabled to view it. .
Refer to LEW-19207-1.
Top Stories
INSIDERManned Systems
Turkey's KAAN Combat Aircraft Completes First Flight - Mobility Engineering...
INSIDERMaterials
FAA Expands Boeing 737 Investigation to Manufacturing and Production Lines -...
INSIDERImaging
New Video Card Enables Supersonic Vision System for NASA's X-59 Demonstrator -...
INSIDERManned Systems
Stratolaunch Approaches Hypersonic Speed in First Powered TA-1 Test Flight -...
INSIDERUnmanned Systems
Army Ends Future Attack and Reconnaissance Helicopter Development Program -...
ArticlesEnergy
Can Solid-State Batteries Commercialize by 2030? - Mobility Engineering...
Webcasts
AR/AI
From Data to Decision: How AI Enhances Warfighter Readiness
Energy
April Battery & Electrification Summit
Manufacturing & Prototyping
Tech Update: 3D Printing for Transportation in 2024
Test & Measurement
Building an Automotive EMC Test Plan
Manufacturing & Prototyping
The Moon and Beyond from a Thermal Perspective
Software
Mastering Software Complexity in Automotive: Is Release Possible...