Последнюю неделю бьюсь над задачей верификации процессорного ядра (RISC архитектура (load/store), 6 ступенчатый конвейер команд, только целочисленная математика). Задача для меня совсем новая (раньше делал только математику и коммуникационные контроллеры), поэтому не знаю даже с какой стороны подойти.

Пока родилась следующая структура: Есть эталонная модель на SystemC (потактовая, тоже с конвейерными регистрами, но вместо логики обычные C++ методы).
На эталонной модели и верифицируемой RTL-модели прогоняется набор тестовых программ и на каждом такте сверяется содержимое конвейерных регистров. После прогона получаем список команд (а также номер такта и название конвейерного регистра), на которых обнаружены ошибки.

Может ли кто-нибудь поделиться опытом, как на практике верифицируют процессоры и покритиковать мой подход?

Я бы просто сверял что получилось, с тем что хотелось. Ну к примеру после mov ax,bx убедился бы что в ax==bx. Хотя процессоры не писал. Можно глянуть "у взрослых".
http://www.opensparc.net/opensparc-t2/download.html

Я делал процессорные ядра.
Что могу сказать?
на самом деле когда нет обратной записи или перезагрузки конвейера, то все довольно прозрачно.
вся хитрость начинается именно в том случае, когда появляются команды типа SKIP, JMP, CALL. Ну и обратные команды возвратов. Надо проверять, когда идут подряд две "атомные" операции, например комбинации пропусков и переходов... обратной записи и переходов.
Что касается методологии тестирования, то постарайтесь достать мой "Краткий Курс HDL", раздел о тестировании... Или закажите диск... Или читайте файлы на сайте у Ментора...
На самом деле, эта тема для меня довольна интересна.
Если будут вопросы - пишите письмом..
Моя методика такова: сначала я делал сам процессор, потом к нему софт симулятор+ассемблер+формирователь дампа. Это все есть в моих статьях..
Сейчас не могу писать больше, т.к. через 40 минут иду читать вебинар "Про Ethernet"... Приходите слушать... Я о вебинаре сделал отдельный пост..
Удачи...

Есть вариант проверки в "железе":

Подсоедините к Вашему процессору например UART для того чтобы была двунаправленная связь с ПК, и также неплохо бы подсоединить к процессору внешнюю оперативную память (SRAM или DDR или DDR2). Напишите программу для своего процессора, а результаты обработки выдавайте на ПК. Желательно написать несколько таких программ, которые охватывали б различные комбинации команд (чем больше, тем лучше) для процессора. Напишите программу для ПК которая будет верифицировать приходящие данные с Вашего процессора и выдавать команды для Вашего процессора.
Например задачами для Вашего процессора могут быть:
- сортировка(различные ее варианты) N(исходя из размера оперативной памяти) значений;
- математический расчет (например нахождение минимума/максимума какой-то функции);
- фурье/вейлет преобразование;

Еще бы неплохо бы его зациклить - производить N раз вычислений - для проверки возможных зависаний и тому подобных вещей.

Кроме того, неплохо бы проверить работу Вашего процессора на различных тактовых частотах, для нахождения максимальной частоты, на которой Ваш процессор устойчиво работает (правильно производит все вычисления).

ЗЫ Если программа для Вашего процессора пишется на ассемблере - желательно написать компилятор для языка верхнего уровння (С, С++).

ЗЫ ЗЫ Это только мое субъективное видение.

Как Ваш процессор программируется?

Еще надо проверить прерывания/многопоточность и тп - м/б и логические ошибки (на верхнем уровне). У меня, кстати, прерывание реализовано, как аппаратное переключение задачи - проще/лучше делать прерывания через многопоточность, чем многопоточность через прерывания.

И сколько примерно на Спартане/Циклоне ЛУТ/МГц получается для ядра?

Это как? На каждое прерывание/поток по своему набору регистров, конвейеров и всего того что к нему прилагается?

Извиняюсь, я не совсем правильно сформулировал тему, имеется ввиду функциональная верификация.



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

Еще раз извиняюсь, я не правильно сформулировал тему. Предложенный вами метод вообще плохо подходит для верификации: хотя он и позволяет обнаружить наличие жуков, но понять где их искать будет очень сложно.

На данный момент никак. Программа зашивается как ROM прямо в прошивке для FPGA.


Ну у меня все просто: прерывание это просто команда безусловного перехода с сохранением адреса возврата.


3700 Лутов на Spartan 3AN (XC700AN, Spartan-3AN Starter Kit). Ядро без памяти гоняет на 80 МГц. При подключении памяти все падает до 38 МГц, поэтому сейчас думаю о создании MMU, пока смотрю литературу.



Недавно слушал лекцию парня из OneSpin (http://www.onespin-solutions.com/) про формальную верификацию. Нахожусь под впечатлением, жаль что САПРЫ для формальной верификации (OneSpin 360, Mentor 0-in, Cadence Incisive formal) не доступны широкому кругу студентов
Идея примерно следующая:
1) Весь дизайн покрывается спецификацией на темпоральной логике (обычно SystemVerilog Assertions). Спецификация состоит из множества высказываний примерно следующего содержания: "Если в поле КОД_ОПЕРАЦИИ находится ADD, а в регистрах-операндах находятся A и B, то через 4 такта в регистре результата будет A+B, а во влаге OF будет значение переноса в старший разряд"
2) САПР статически вычисляет coverage, если он не достаточен, возвращаемся к пункту 1 и покрываем спеками недостающие области.
3) Дальше запускается SAT-solver (программа решающая задачу булевой выполнимости наших спеков на верифицируемом RTL коде)
4) Если где-то есть жуки, САПР выводит список контр-примеров: к примеру "Команда ADD не корректно выполняется на значениях операндов -123 и -123"

Что именно дублируется - зависит от архитектуры. Сам конвейер, например, дублировать не нужно. Указатели, программный счетчик, и тп - дублируются. У меня большой регистровый файл (1К слов) на памяти - можно и аппаратно, и софтово (без потери производительности) разграничить память потоков. Софтово даже лучше - железо проще, тактовая выше - для каждого прерывания/потока компилятор создает свои статические переменные (доступны и глобальные). В целом получается проще, чем для "классического" прерывания.


Какой памяти, внешней, или внутренней?


А "правильность" самой спецификации кто гарантировать будет? Важно не пропустить ошибку, а как локализировать - вопрос религии/бизнеса, имхо.

Ну, более высокоуровневое описание того же алгоритма менее подвержено ошибкам.


К тому же в идеальном случае верификацией не следует заниматься разработчикам. А "две головы" все-таки лучше, чем одна. 

Если компилятор (gcc) уже портирован, то у него полно тестов. Более чем нормальная вертификация.


Где-то про аппаратную многозадачность, я уже слышал. И далеко не раз.

Multithreading. Есть у всех быстрых современных процессоров.

Но не на аппаратном уровне. На программном: прыгнули, все регистры выгрузили в стек, переключились, загрузили новый указатель стека, загрузили регистры из нового стека итд.

Да, примерно так. SVA гораздо легче для восприятия чем RTL, да и вряд ли два разных человека могут ошибиться в одном и том же месте.


Основной плюс формальной верификации в том, что она дает 100% покрытие по тем блокам на которые написана спека. Верификация путем логической
симуляции никогда не даст 100% покрытия по двум причинам:
1) Время симуляции будет стремиться к вечности;
2) Невозможно написать такую программу, которая покрыла бы все возможные состояния/ исключительные ситуации/форматы данных и.т.п.

Тем не менее, вернемся к верификации путем симуляции:
Как создавать тестовые вектора (программы) во общем то понятно: либо сделать кросс-компилятор, либо генератор случайных команд.

Меня больше беспокоит вопрос создания эталонной модели: В простейшем случае, в качестве эталона можно использовать симулятор системы команд (Instruction Set Simulator),
он же Архитектурная модель (System Architecture Model). Это такая штука, которая эмулирует работу процессора с точностью до команды. Как правило, ISS'ы есть
в каждой нормальной среде разработки для микроконтроллеров, к примеру, в Keil. Если мы верифицируем мультитактную модель процессора, т.е. простейшую реализацию процессора
без конвейера команд, то все отлично: всегда есть такое состояние, когда процессор завершил выполнение одной команды, но еще не начал исполнять другую. Далее сравниваем состояние регистров
в RTL и ISS, если есть расхождения, то сразу ясно, на какой команде возникает ошибка.

Далее рассмотрим реализацию процессора с конвейером команд: куча команд выполняется параллельно, данные летают во все стороны (работают всякие forwarding'и, stall'ы c пузырями, отлавливаются конфликты
по управлению). Выловить завершение исполнения отдельной команды невозможно: т.е. сравнить выполнение каждой команды в ISS и в RTL мы не можем. В лучшем случае можно ловить циклы записи в память и сравнивать передаваемые данные. Но для RISC процессоров с тучей регистров, такой подход плохо подходит: обращение к памяти происходит редко. Если мы и отловим жука, то продебажить его будет очень тяжело.


Внутренней. Block Ram

Simultaneous Multi-Threading для повышения производительности - там все на аппаратном уровне, и никаких лишних копирований.


Для навороченного ядра исполняемые инструкции могут вообще не совпадать со входными(оптимизация обращений к памяти, например). Так что просто проверять контрольные точки программы(результат), имхо. Обнаружили ошибку - посеять дополнительные точки. Либо детально описывать все нюансы RTL-поведения(SVA) - на порядок больше работы(за ту-же зарплату).


Тогда советую пересмотреть архитектуру(если проц не для ASIC) и/или HDL-описание(избегать "case"-стиля описания АЛУ и др блоков) - кэши/MMU и тп призваны оптимизировать обращения к внешней памяти FPGA.


У меня все проще, некоторыми идеями аппаратной многопоточности воспользовался только для организации прерываний и выполнения фоновых задач, не для повышения производительности.

Не, косяк был все-таки в памяти, оказалось что я случайно поставил в визарде distributed ram вместо block для памяти данных, в итоге он мне растащил память по всей микросхеме *_*. Исправил, теперь имею 80 МГц. Я пока таймингом всерьез не занимался, думаю много что удастся причесать. Пока строю планы на будущее, делать что-то буду уже после сессии.


Да, no silver bullet, к сожалению.

Попытаюсь еще порыться в литературе, если обнаружу что-нибудь интересное - отпишусь.