Даниэль Дж. Сорин Младший профессор Факультет Электротехники и вычислительной техники и информатики университет Дьюка Оригинал: Verification-Aware Microarchitecture Наша цель заключается в разработке микроархитектуры таким...

dan sorin of engineering

Даниэль Дж. Сорин

Младший профессор
Факультет
Электротехники и вычислительной техники и информатики
университет Дьюка

Оригинал: Verification-Aware Microarchitecture

Наша цель заключается в разработке микроархитектуры таким образом, что они могут быть более легко проверяется с существующими формальными методологии проверки. Проверка в настоящее время потребляет большинство ресурсов в развитии нового процессора, а еще современные процессоры по-прежнему поставляется клиентам с десятками открытых впоследствии и документально дизайн ошибок. Вместо разработки процессор для работы, энергоэффективность, надежность и т.д., а затем, когда дизайн завершения, “бросить его на стене” в группе по проверке, наша цель заключается в лечении проверки усилия в качестве первого класса дизайн ограничение. В частности, мы изучаем, как проектировать процессоры, такие, что они более склонны к формальной верификации, в частности, с проверкой модели.

Публикации

Daniel J. Sorin, Opeoluwa Matthews, and Meng Zhang.  “Architecting Dynamic Power Management to be Formally Verifiable.”  Design Automation Conference (DAC), June 2014.
Meng Zhang, Jesse D. Bingham, John Erickson, and Daniel J. Sorin.  “PVCoherence: Designing Flat Coherence Protocols for Scalable Verification.”  20th International Symposium on High Performance Computer Architecture (HPCA), February 2014.  Best Paper Award
Opeoluwa Matthews, Meng Zhang, and Daniel J. Sorin. “Scalably Verifiable Dynamic Power Management.”  20th International Symposium on High Performance Computer Architecture (HPCA), February 2014.
Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. “Fractal Consistency: Architecting the Memory System to Facilitate Verification.” Computer Architecture Letters, volume 9, number 2, July-December 2010.
Meng Zhang, Alvin R. Lebeck, and Daniel J. Sorin. “Fractal Coherence: Scalably Verifiable Cache Coherence. To appear in 43rd International Symposium on Microarchitecture (MICRO), December 2010.
Meng Zhang, Anita Lungu, and Daniel J. Sorin. “Analyzing Formal Verification and Testing Efforts of Different Fault Tolerance Mechanisms.” 24th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, October 2009.
Anita Lungu, Pradip Bose, Alper Buyuktosunoglu and Daniel J. Sorin. “Dynamic Power Gating with Quality Guarantees.” International Symposium on Low Power Electronics and Design (ISLPED), August 2009.
Anita Lungu, Pradip Bose, Daniel J. Sorin, Steven German and Geert Janssen. “Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification.” Seventh ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2009.
Anita Lungu, Pradip Bose, Daniel J. Sorin, Steven German, and Geert Janssen. “Multicore Power Management: Ensuring Robustness via Early-Stage Formal Verification.” 3rd Workshop on Dependable Architectures (WDA-3), November 2008.
Anita Lungu and Daniel J. Sorin. “Verification-Aware Microprocessor Design.” Sixteenth International Conference on Parallel Architectures and Compilation Techniques (PACT), September 2007.

Группа

Профессор Даниэль Дж Сорин , доцент кафедры электротехники и вычислительной техники и информатики

Анита Лунгу

Опелува (Лува) Мэттьюс

Мэн Чжан

Финансирование и поддержка

Национальный научный фонд предоставить CCF-0811290