Altifigence Academy

12 / 37 · Теория

Проверка MUX: полный перебор и свойства

Проверяйте покрытие комбинационных входов и хранение раздельно, минимизируйте контрпримеры.

Что считать правильным

Однобитные a, b и sel дают восемь комбинаций. При таком размере полный перебор эффективен. Для MUXМультиплексор — комбинационная схема, соединяющая один из нескольких входов с выходом по сигналу выбора. Соответствие битов выбора и номеров входов должно быть задано явно. Подробнее ширины W простой полный перебор с селектором требует 22W+12^{2W+1} наборов, поэтому уже небольшое увеличение ширины требует другой стратегии.

Правило выбора каждого из W выходных битов:

∀i∈{0,…,W−1},yi=s‾ai+sbi\forall i\in\{0,\ldots,W-1\},\quad y_i=\overline s a_i+s b_i

Подбирайте воздействия под класс ошибок

Проверяемый дефектПолезный вход или наблюдение
Перепутаны a/bРазные a и b, сравнение sel=0 и 1
Обратный порядок битовWalking-one с единственной единицей
Залипание stuck-atВсе нули, все единицы, чередующиеся биты
Неверный фронт храненияСмена входа между фронтами, проверка хранения q
Ошибка задержки на циклРазные ожидания на последовательных фронтах

Большое число тестов само по себе не означает хорошую проверку. Нужно уметь объяснить, какой дефект они обнаруживают.

Ниже выбраны только случаи с разными a и b. Каждый столбец — один тестовый вектор. Ошибочное выражение выбора даёт значение, противоположное expected, во всех четырёх столбцах.

Четыре комбинации для обнаружения инверсии выбора
Показать данные диаграммы
Данные диаграммы: каждый символ — один интервал; точка сохраняет предыдущее состояние; p — один тактовый цикл.
СигналДиаграммаЗначения шины
a0.1.
b1.0.
sel0101
ожидаемое01.0
перепутанный выбор10.1

Эталон должен быть независим от реализации

Копирование кода DUT может воспроизвести одну ошибку дважды. Формируйте ожидания по таблице истинностиТаблица истинности перечисляет все возможные комбинации входов и выход для каждой из них. Изменения во времени проверяют отдельно по временным диаграммам. Подробнее спецификации или индексному выбору; для q отдельно отслеживайте захваченное состояние. При mismatch сократите воздействие до самой короткой последовательности, сохраняющей ошибку, и объясните причину.

Вместо одного конечного состояния записывайте фактическое значение, ожидание и вход в каждой точке наблюдения. Это позволяет различить «симуляция выполнилась» и «спецификация соблюдена».

Попробуйте сами

Для 8-битного MUX оба значения селектора проверены только с a=0x00, b=0xFF. Обнаружит ли это обратный порядок выходных битов?

Прочитать объяснение

Нет. 0x00 и 0xFF не меняются при развороте битов. Нужны позиционные шаблоны вроде 0x01 и 0x02 и сравнение каждого выходного бита.

Выбор действует в этом браузере. Его можно изменить внизу страницы.