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.