26 / 37 · Теория
Отладка счётчика и минимальные контрпримеры
Спроектируйте короткие тесты, различающие ошибки reset, enable и перехода через границу.
Уроки доступны бесплатно. Запишитесь, чтобы сохранять прогресс.
Правильный итог не гарантирует правильного порядка
Окончание счёта в 0 не доказывает правильность reset и циклического перехода: постоянно нулевая схема даёт тот же итог. Нужны точки наблюдения, отдельно выявляющие увеличение, хранение, сбросСброс возвращает состояние к заданному начальному значению. Нужно определить, синхронен он или асинхронен и имеет ли приоритет над другими управляющими сигналами. Подробнее и переход через границу.
Намеренно столкните два управления
| Ситуация | Проверяемое требование |
|---|---|
| reset=1, enable=0 | Не скрывает ли enable сброс |
| reset=1, enable=1 | Приоритет reset над увеличением |
| count=M-1, enable=0 | Нет ли ошибочного возврата во время остановки |
| count=M-1, enable=1 | Точный возврат из M-1 в 0 |
| Смена reset между фронтами | Синхронный reset действует на следующем фронте |
Ошибку приоритета трудно найти, проверяя каждое управление отдельно.
Каждый столбец — запись наблюдения одного положительного фронтаПоложительный фронт — момент перехода такта из 0 в 1. Его следует отличать от уровня, означающего весь интервал CLK=1. Подробнее. Входы показаны непосредственно перед фронтом, состояния со словом «после» в имени — сразу после обновления. Выравнивание столбцов обозначает порядок выборок, а не физическую задержку распространенияЗадержка распространения — время от изменения входа до установления правильного выхода. Логическая эквивалентность выражений и их временные характеристики — разные вопросы. Подробнее.
Начально count=5. Неверная схема проверяет reset только внутри enable, поэтому на первом фронте сохраняет 5. Даже при одинаковом итоге первое расхождение выявляет дефект.
Показать данные диаграммы
| Сигнал | Диаграмма | Значения шины |
|---|---|---|
| фронт | 234 | E0 → E1 → E2 |
| reset | 101 | |
| enable | 01. | |
| верный результат после | 234 | 0 → 1 → 0 |
| ошибочный результат после | 234 | 5 → 6 → 0 |
Запустите эталонный modulo-8 из 101. Выберите enable=0, reset=1 и продвиньте такт. Правильное значение — 000; RTL со сбросом внутри enable сохранит 101. После снятия reset также различайте хранение при enable=0 и увеличение при enable=1.
Синхронный сброс приоритетнее enable. При enable=0 сохранённое значение удерживается. q=101; q_next = (q + 1) mod 8
Поиск первого расхождения с эталоном
Эта функциональная модель предполагает нормальные состояния 0–M-1. Восстановление вне диапазона добавляется отдельной политикой. На каждом фронте вычисляйте ожидание и сравнивайте с фактом. Вход и состояние непосредственно перед первым ошибочным фронтом — минимальная отправная точка поиска причины.
Если сбой возник через 1000 циклов, сократите ненужные участки и попробуйте воспроизвести его за 3–5 фронтов. После исправления RTL оставьте минимальный контрпример в регрессионном тесте. Пересматривайте изменённые спецификацию и код отдельно, чтобы не внести одно неверное условие одновременно в проект и тест.
Попробуйте сами
Неверный код поместил reset внутрь if(en) begin if(rst) ... end. Какие начальное состояние и входы выявят проблему самой короткой последовательностью?
Прочитать объяснение
Возьмите ненулевое начальное состояние и один положительный фронт с rst=1, en=0. При приоритете reset должно получиться 0, а неверная схема сохранит старое. Начальное 0 скрыло бы ошибку.