Методология измерения покрытия в структурном состоянии взаимного соединения
Изобретение относится к способам и устройствам проверки правильности структуры протокола. Технический результат заключается в повышении точности проверки правильности реализации протокола. Пространство покрытия состояний для структуры генерируется и сохраняется в базе данных. Во время моделирования встречающиеся состояния пространства покрытия маркируются. Из этого можно определить встретившиеся и не встретившиеся состояния. На основе не встретившихся состояний разрабатывается целевая тестовая последовательность, чтобы наметить по меньшей мере некоторые из состояний, не встретившихся во время предыдущего моделирования. Эту обратную связь из моделирования для обновления типовой тестовой последовательности по не встретившимся во время моделирования состояниям пространства покрытия можно рекурсивно повторять, пока не будет достигнуто адекватного подтверждения правильности. 4 н. и 15 з.п. ф-лы, 4 ил.
Область техники, к которой относится изобретение
Данное изобретение относится к области компьютерных систем, а в частности к методологии проверки правильности протоколов.
Уровень техники
Успех в обработке полупроводников и логическом проектировании позволили увеличить количество логических элементов, которые могут присутствовать в устройствах на интегральных микросхемах. Помимо этого компьютерные системы развились до такой степени, что вмещают много различных функций, таких как традиционные компьютерные системы, системы хранения медийных данных, развлекательные центры, воспроизведение аудиосигналов, воспроизведение видеосигналов, серверы и т.п. Дополнительно высокопроизводительные протоколы разработаны для переноса информации по всей компьютерной системе для этих более быстрых и более расширенных функциональных возможностей. В качестве примера, структура Intel's Quickpath включает в себя структуру протокола для высокоскоростного последовательного двухточечного многоуровневого протокола взаимосвязи с кэшем, способную передавать данные на высоких скоростях. Однако по мере того как эти более развитые протоколы продолжают эволюционировать, сложность каждого уровня в структуре протокола также возрастает.
Традиционно проверка правильности структуры протокола для гарантирования правильной работы включает в себя ручную идентификацию поворотных случаев, т.е. предельных рабочих точек или состояний. Эти поворотные случаи вызываются в системе, чтобы проверить правильность работы реализации протокола. В качестве альтернативы или иногда в дополнение к поворотным случаям случайные рабочие переменные / состояния изменяются, чтобы случайным образом проверить правильность структуры протокола.
Однако эти параметры и переменные становятся чрезвычайно большими по количеству по мере увеличения сложности. Например, в сложном протоколе с множеством агентов число потенциальных состояний растет по экспоненте. В результате человеку становится труднее не терять из виду пространство покрытия для этих потенциальных состояний. Помимо того нынешние способы проверки правильности зачастую не способны проследить, какие из большого числа состояний проверяются. Вследствие этого становится еще труднее получить точный доверенный уровень во всей проверенной структуре.
Краткое описание чертежей
Настоящее изобретение иллюстрируется посредством примера и не предназначено для ограничения сопровождающими чертежами.
Фиг.1 иллюстрирует вариант осуществления системы, содержащей различные межсоединения для связывания компонентов системы вместе.
Фиг.2 иллюстрирует вариант осуществления носителя данных для сохранения базы данных покрытия для конфигурации структуры.
Фиг.3 иллюстрирует вариант осуществления блок-схемы алгоритма для способа, который гарантирует проверенное покрытие для структуры.
Фиг.4 иллюстрирует вариант осуществления блок-схемы алгоритма для другого способа, который гарантирует проверенное покрытие для структуры межсоединений.
Подробное описание
В нижеследующем описании многочисленные конкретные детали изложены посредством примеров конкретных структур протоколов, конкретных рабочих переменных / параметров протоколов, конкретных моделей, конкретных этапов проверки правильности и т.п., чтобы обеспечить полное понимание настоящего изобретения. Специалисту будет, однако, ясно, что эти детали не обязательны для практической реализации настоящего изобретения. В других случаях общеизвестные составляющие или способы, такие как протоколы / воплощение межсоединений, разработка / содержание формальных моделей межсоединений, конкретные запросы и прочие конкретные подробности работы не описаны подробно, чтобы избежать ненужного затемнения настоящего изобретения.
Описанные здесь способ и устройство предназначены для обеспечения стратегии проверки правильности, чтобы реально и эффективно проверять правильность реализации сложного протокола. Конкретно проверка правильности протоколов межсоединений в первую очередь обсуждается в применении к взаимосвязанному с кэшем протоколу межсоединений, таких как высокоскоростное двухточечное межсоединение, в том числе протокол взаимосвязи с кэшем, по существу привязанный к спецификации Intel's Quickpath, чтобы проиллюстрировать методологию проверки правильности. Однако описанные здесь способы и устройства не ограничены так, что они могут быть реализованы по любому протоколу или во взаимосвязи с любым протоколом, структурным уровнем межсоединений или иной системой множества агентов / параметров.
На фиг.1 иллюстрируется вариант осуществления множества междсоединений для связывания компонентов системы. Как показано, изображена часть традиционной многопроцессорной системы. Однако описанная здесь методология проверки правильности может быть использована в любой системе, такой как компьютерные системы с единственным процессором, серверы, встроенные системы, мобильные системы и прочие системы с множеством электрических агентов.
В одном варианте осуществления концентратор 125 напоминает набор микросхем. Часто набор микросхем содержит два интегральных схемных устройства, таких как концентратор контроллера памяти (МСН) и концентратор контроллера межсоединений (ICH). В одном варианте осуществления концентратор 125 представляет собой МСН, связывающий процессоры 106, 111, 116 и 121 с памятью 130, однако концентратор 125 может включать в себя любую интегральную схему для облегчения передачи данных между процессорами и другими системными устройствами.
Память 130, как показано, включает в себя системную память для хранения кода, данных и другой информации, к которой можно обращаться во время работы. Пример системной памяти включает в себя динамическое оперативно запоминающее устройство (ДОЗУ) (DRAM). Однако для системной памяти может быть использована любая память, такая как память с двойной скоростью передачи данных (DDR), синхронное динамическое ОЗУ (SDRAM), буферизованная память и другие известные устройства памяти. Помимо этого память 130 не ограничена системной памятью и может включать в себя другие известные устройства памяти, такие как устройство флэш-памяти.
Процессорные гнезда 105, 110, 115 и 120 предназначены для соединения процессоров 106, 111, 116 и 121 с монтажной платой, такой как печатная плата (РСВ) или материнская плата. Часто используется гнездо и соответствующая технология упаковки, такая как матрица площадочных выводов (LGA), матрица штырьковых выводов (PGA), матрица шариковых выводов (BGA) или иная известная гнездовая технология. Процессоры 106, 111, 116 и 121 зачастую именуются физическими процессорами, но могут включать в себя любой вид процессорного элемента, такой как микропроцессор, встроенный процессор, многоядерный процессор, многопоточный процессор или сигнальный процессор.
Межсоединение 126, как показано, связывает процессоры 106, 111, 116 и 121 с концентратором 125, зачастую межсоединение именуется внешней шиной (FSB). Хотя проверка правильности обсуждается в отношении межсоединения 126 и его протоколов, отметим, что обсуждаемая здесь методология проверки правильности может использоваться на любом межсоединении, таком как межсоединение ввода-вывода, шина памяти или иная линия, связывающая вместе агенты, которые воплощают любое число и вид протокола передачи данных. Физически межсоединение 126 может использовать параллельную шину, последовательную шину, многоточечную шину, двухточечную шину, шину логики приемопередатчика Ганнинга (GTL), шину GTL+, шину двойной скорости передачи данных (DDR), дифференциальную шину или иной известный физический слой / воплощение межсоединения. В качестве конкретного иллюстративного варианта осуществления межсоединение 126 включает в себя высокоскоростное последовательное двухточечное межсоединение.
В одном варианте осуществления межсоединение 126 включает в себя многоуровневую стековую структуру протокола. Примерные уровни структуры межсоединений включают в себя физический уровень для обеспечения физического электрического соединения между устройствами, канальный уровень для содействия упорядочению транзакций / запросов / пакетов и уровень транзакций для реализации различных видов транзакций / запросов / пакетов. Эти уровни являются общими в структуре межсоединений, такой как межсоединение периферийных компонентов (PCI) Express. Однако и другие уровни или протоколы могут присутствовать как часть структуры межсоединений. Например, структура межсоединений, по существу привязанная к спецификации Intel's Quickpath, включает в себя различные протоколы транзакций и передачи данных, такие как протокол взаимосвязи с кэшем.
Как указано выше, проверка правильности протоколов для межсоединений может включать в себя любое межсоединение в платформе, такое как шина ввода-вывода (I/O), шина межсоединений периферийных элементов (PCI) или PCI Express, либо шину памяти, такую как шина 127 памяти. Общие примеры физической шины памяти для соединения концентратора 125 с памятью 130 включают в себя шину на основе DDR, шину на основе оперативно запоминающего устройства (ОЗУ) или любую иную известную шину памяти или другую шину, приспособленную для шины памяти. Каждый вид шины может быть связан со своими протоколами передачи данных, подлежащими проверке правильности.
Далее, методология проверки правильности для протоколов не ограничена протоколами межсоединений традиционной настольной компьютерной системы. Например, сетевые протоколы, протоколы беспроводного доступа и другие сложные протоколы передачи данных могут проверяться на правильность аналогичным образом. Поэтому относится ли проверка правильности к физическому соединению, протоколу межсоединений или иному протоколу, цель этой проверки правильности можно назвать структурой, объектом проверки правильности или целью проверки правильности.
На фиг.2 иллюстрируется вариант осуществления базы данных покрытия для пространства покрытия возможных состояний структуры, подлежащей проверке на правильность. Отметим, что, как установлено выше, использование термина «структура, подлежащая проверке на правильность» может относиться к подлежащей проверке на правильность структуре протокола, такого как подлежащий проверке правильности протокол взаимосвязи с кэшем, другие подлежащие проверке правильности протоколы, подлежащее проверке правильности физическое межсоединение или к проверке правильности их комбинации.
В одном варианте осуществления база 2001 данных хранится на носителе 200 памяти. Носитель памяти включает в себя любое устройство хранения, способное сохранять электронную информацию, такое как диск, дисковод, память, накопитель на магнитной ленте, внешний блок памяти, временная память, энергозависимая память, энергонезависимая память, другие устройства хранения, или доступный для машины / машиночитаемый носитель. Отметим, что доступный для машины носитель может включать в себя несущее колебание или иную среду электронной передачи данных, которая несет или передает информацию, такую как информация, хранящаяся в базе 201 данных, от носителя данных в компьютерную систему, к которой осуществляется доступ.
В одном варианте осуществления база данных пространства покрытия для структуры включает в себя множество состояний для структуры, такой как структура протокола, которые могут встретиться в процессе работы. В качестве примера, база данных покрытия включает в себя все потенциальные состояния воплощения структуры, такой как ограниченная конфигурацией модель структуры. Однако в другом примере база данных покрытия включает в себя сокращенный набор возможных состояний воплощения структуры.
Например, предположим, что формальная модель уровня протокола межсоединения приспособлена к модели конкретного протокола реализации для межсоединения. Здесь, когда меняются переменные / параметры для достижения различных состояний в конкретном протоколе реализации, каждый набор переменных может иметь потенциально симметричный набор переменных, дающий симметричные состояния. В результате в данном примере только одно симметричное состояние сохраняется в базе 201 данных, образуя симметрично сокращенный набор состояний межсоединений, который в общем случае может именоваться пространством покрытия.
В качестве сверхупрощенного примера пространства покрытия для проверки правильности адаптирована формальная модель для протокола взаимосвязи с кэшем взаимосвязанного с кэшем межсоединения на основе ограничений конфигурации, таких как число агентов протокола, тип агентов протокола и т.п. Пространство покрытия для проверки правильности протокола взаимосвязи с кэшем включает в себя всевозможные состояния на основе изменяемых параметров агентов для каждого из агентов протокола и (или) для изменяемых глобальных параметров для протокола взаимосвязи.
Однако для сложных протоколов или межсоединений число параметров потенциально возрастает до значительного числа. Например, может присутствовать 100 или более параметров для конкретной реализации протокола. Следовательно, каждая комбинация различных значений для каждого параметра потенциально приводит к чрезвычайно большому числу возможных состояний, даже для конкретного воплощения протокола.
В одном варианте осуществления состоянием именуется моментальный снимок состояний параметров, устройств, агентов и (или) других компонентов проверяемого объекта. Состоянием может также именоваться структурное состояние структуры или проверяемого объекта. В качестве другого примера, состояние определяется комбинацией значений параметров в моментальном снимке состояния. Следовательно, если для структуры идентифицируют сотню параметров, то каждая комбинация различных значений для этой сотни параметров потенциально дает различные состояния.
Поскольку состоянием зачастую именуют большое число параметров для сложного протокола, сверхупрощенный иллюстративный пример состояния для протокола взаимосвязи с кэшем включает в себя один процессор, имеющий строку кэша в совместно используемом взаимосвязанном состоянии, два процессора, имеющие строку кэша в недостоверном состоянии, и в один из процессоров принимается разведчик. Здесь имеется множество агентов протокола, множество строк кэша во множестве состояний, и запрос / сообщение принимается в конкретном месте назначения. Поэтому в данном простом отдельно взятом примере имеется всего несколько параметров. В качестве другого иллюстративного примера транзакция записи, несущая полезные данные, потенциально приводит к множеству состояний, т.к. могут изменяться другие параметры, такие как место назначения записи, состояние строк кэша, связанных в подлежащей записи полезной нагрузкой, трафик межсоединений, отклики записи от других агентов и т.п.
Поэтому в одном варианте осуществления параметром именуется любой элемент в протоколе, физической логике, устройстве агенте или глобальном состоянии / переменной, которые могут изменяться или помещаться в различные состояния. В качестве конкретного примера, при проверке правильности протокола взаимосвязи с кэшем параметр для агента кэширования включает в себя отклик кэша на разведчик. Здесь одно значение параметра отклика кэша включает в себя направление разведанной строки кэша в запрашивающее устройство, а второе значение параметра отклика кэша включает в себя запись строки кэша в собственный узел. Другие общие параметры протокола взаимосвязи включают в себя различные типы агентов, откликов агентов, откликов устройств, откликов межсоединений, откликов сообщений, типов откликов, других откликов на конкретные действия, мест назначений откликов, сообщений, типов сообщений, мест назначения сообщений, запросов, типов запросов, мест назначения запросов, типов кэшей, состояний кэшей, местоположений кэшей, состояний регистра и т.п.
Однако, поскольку любая структура, такая как физическое межсоединение, протокол передачи данных или иной протокол могут быть объектом проверки правильности, параметр может охватывать большое разнообразие переменных. Неисчерпывающий иллюстративный перечень потенциальных связанных с протоколом параметров включает в себя несколько агентов протокола, тип агента протокола, тип реализации кэша для агента, несколько агентов протокола разных типов, вид агента протокола, состояние агента протокола, состояние схемы или конечного автомата в агенте протокола или на шине, идентификатор агента, число запросов протокола, типа запроса, источник запроса, место назначения запроса, состояние запроса, указанная операция, источник операции, указанный адрес, состояние местоположения адреса, полезные данные, состояние агента протокола, состояние кэша, состояние строки кэша и параметр физического состояния прокола, такой как состояние напряжения, частоты, мощности или иной физический атрибут протокола.
Когда должен быть проверен физический уровень межсоединения, немногие примеры физических параметров межсоединения включают в себя напряжение, частоту, период, расширенный спектр, дрожание, шум и т.п., тогда как остальные параметры включают в себя состояние связанных с межсоединением конечных автоматов, типы агентов, состояния агентов, состояния схемы ввода-вывода в агентах и т.п. Однако любой переменный элемент в структуре можно рассматривать как параметр.
Поскольку пространства покрытия возрастают экспоненциально и человеку в одном варианте осуществления становится трудно их осмыслить, база 201 данных хранит пространство покрытия возможных состояний для структуры / реализации межсоединений. Как показано, каждый ввод базы 201 данных, такой как вводы 250-257, представляет возможное состояние реализации межсоединений. Поэтому ссылка на ввод 250 синонимична обсуждению состояния 250 со значениями параметров, как определено в поле 210. Здесь поле 210 значений параметров ввода 250 должно сохранять несколько значений для связанных параметров, соответствующих состоянию 250.
В одном варианте осуществления поле 210 значений параметров разделено на множество полей 211, 212, 213 и 214. В качестве примера, предположим, что база 201 данных должна сохранять пространство покрытий для реализации протокола взаимосвязи, имеющего три агента протокола. Здесь поля 211-213 соответствуют каждому из трех агентов протокола. В каждом поле каждое числовое значение, которое может быть логически рассмотрено как подполе, заранее определено или связано с соответствующим параметром.
Например, в поле 211 для первого агента первое численное значение поля 211 определяет тип агента, второе численное значение определяет, находится ли первый агент в собственном узле, третье численное значение определяет состояние строки кэша и т.д. Отметим, что отклик на конкретный запрос / действие, такой как отклик на разведку / считывание, потенциально имеет много вариантов. Например, отклик с четырьмя различными откликами потенциально представлен двумя двоичными битами с четырьмя возможными комбинациями, т.е. один, два, три и четыре, и каждая из этих комбинаций представляет возможный отклик.
Далее, поле 214 может быть полем глобального параметра, включающим в себя глобальные параметры для всех агентов. Например, глобальный отклик кэша на разведчика может быть направлен в собственный узел, и, как таковое, значение параметра в поле 214 представляет этот отклик кэша. Вышеприведенные примеры являются вполне иллюстративными, т.к. любое число агентов и любое число параметров, такое как десятки, сотни или тысячи, может быть представлено в поле 210 в любом виде. Помимо этого любой вышеприведенный способ представления разнообразных элементов может быть использован в поле 210.
В другом варианте осуществления поле 210 хранит множество последовательных значений, и заранее установленная структура численных значений в поле 210 связывает каждое значение параметра с соответствующим параметром. В качестве примера первое число в поле 210 представляет число всех агентов, второе число представляет число кэшированных агентов, третье число представляет отклик первым агентом на запрос, четвертое число представляет отклик вторым агентом на запрос и т.д. Как видно, здесь вместо прерывания параметров агентом параметры перечисляются последовательно. Однако в базе 201 данных может быть использована любая конструктивная реализация или форма представления параметров.
По мере возрастания сложности межсоединений и увеличения числа переменных / параметров число состояний, подлежащих хранению в базе 201 данных, также сильно возрастает. Поэтому в одном варианте осуществления каждый ввод включает в себя поле 205 признакового идентификатора для однозначного идентифицирования каждого ввода. Например, численные значения параметров, которые хранятся в поле 210, определяют состояние 250, т.е. ввод 250, а признаковый идентификатор 205 для ввода 250 основан на численных значениях, хранящихся в поле 210 ввода 250.
В качестве первого примера, численные значения объединяются с применением математического алгоритма, чтобы получить соответствующий признаковый идентификатор. Поэтому если в поле 210 параметра содержится сотня численных значений, то сотня значений или некоторая ее часть объединяются в каждом вводе 250-257, чтобы получить однозначные признаковые идентификаторы 205 для каждого ввода 250-257. Отметим, что по мере изменения параметров по различным численным значениям признаковый идентификатор будет меняться на основе изменения значений параметра в полях 210. Например, когда признак для параметра разведчика изменяется от первого отклика, который, предположим, представлен как 0, ко второму отклику, который, предположим, представлен как 1, признаковый идентификатор тоже изменяется на основе математической комбинации численных значений параметра. Для объединения численных значений параметра в признаковый идентификатор можно использовать любой алгоритм.
В одном варианте осуществления каждый ввод 250-257 включает в себя также маркирующее поле 215. Маркирующее поле 215 при хранении первого значения, такого как немаркированное значение, представляет, что соответствующее состояние не встретилось во время моделирования. Например, когда маркирующее поле 215 не маркировано, ввод 250, т.е. состояние 250, не встретилось во время моделирования. В противоположность этому, когда маркирующее поле 215 ввода 250 обновляется на маркированное значение, состояние 250 встретилось во время моделирования. Поэтому за счет маркирования во время моделирования можно позже определить, какие состояния посещены / встретились во время моделирования, а какие состояния не встретились.
Вследствие этого пространство покрытия для объекта проверки, такого как протокол, физическое межсоединение, другой уровень или структура, генерируется и потенциально используется для проверки правильности. В одном варианте осуществления база 201 данных генерируется и подается на или носителе данных посредством носителя данных для последующей проверки правильности. Здесь любой уровень реализации для объекта проверки может быть определен для генерирования пространства покрытия, т.е. возможных состояний, хранимых в базе 201 данных.
Например, формальный режим структуры межсоединений может фильтроваться для конкретной модели реализации. В зависимости от ограничений конкретной модели реализации число состояний в базе 201 данных изменяется. Например, если первая модель лишь определяет число агентов протокола, то пространство покрытия может быть чрезмерно большим, т.к. многие другие параметры могут при этом изменяться. В противоположность этому, если модель определяет число агентов, типы агентов, межсоединение агентов, некоторые ограничения протокола, пространство покрытия можно сократить. Помимо этого, когда исполняется программа проверки модели для исследования возможных состояний объекта проверки, то либо полный набор, либо сокращенный набор состояний сохраняется во вводы базы 201 данных. Базу 201 данных можно затем предоставить пользователю, такому как потребитель, чтобы дать возможность проверки правильности протокола, межсоединения или иного объекта проверки. Методология проверки правильности для проверки правильности структуры межсоединений с использованием базы данных, аналогичной базе 201 данных, обсуждается ниже.
На фиг.3 показан вариант осуществления блок-схемы алгоритма для способа обеспечения покрытия структурных состояний во время проверки правильности структуры, такой как структура протокола, структура физического межсоединения, структура протокола межсоединения или иная структурная система. Хотя блок-схемы алгоритмов на фиг.3-4 иллюстрируются как практически последовательные и в конкретном порядке, любая из операций может выполняться параллельно или и другом порядке. Например, маркирование в операции 430 часто имеет место во время моделирования 425, но может также иметь место после моделирования. Далее, моделирование типовой тестовой последовательности может выполняться параллельно или полностью отдельно от операций 405-415.
Отметим также, что любая из операций может выполняться как результат исполнения кода из доступного для машины или машиночитаемого носителя. Доступный для машины или машиночитаемый носитель, такой как изделие промышленного производства, обсуждается подробнее ниже. Поэтому компилятор, синтаксический анализатор или иной исполняемый код при его исполнении может вводить команды, операции, вызов функции или прочие исполняемые коды или структуры для выполнения операций, иллюстрируемых в следующих цепочках операций. Далее, в одном варианте осуществления каждая из цепочек операций, обсуждаемых со ссылкой на фиг.3 и 4, может быть автоматизирована. В одном варианте осуществления автоматизация включает в себя исполнение сценариев, анализаторов или иного кода для выполнения задачи(задач) в цепочке операций. Кроме того, основной код или другой код может сам вызывать или обусловливать следующую подлежащую выполнению цепочку операций, которая также может быть автоматизирована.
В операции 300 определяют возможные состояния для объекта проверки, такого как структура межсоединений, структура протокола или другая известная цель проверки правильности состояния или переменной. Как установлено выше, в одном варианте осуществления возможные состояния именуются состояниями структуры, которые могут встретиться во время работы. Здесь возможными состояниями именуются моментальные снимки параметров, переменных, состояний схем и конечных автоматов, а также любой иной обсуждаемый или известный параметр.
Например, комбинация конкретных значений идентифицированных параметров для структуры межсоединений может привести к единственному состоянию структуры межсоединений. Для иллюстрации в протоколе взаимодействия упрощенное примерное состояние включает в себя три агента протокола, причем один агент хранит строку кэша в собственном состоянии, а два агента хранят ее в неверном состоянии, глобальный отклик на разведчика для записи в собственный узел, и разведчик принимается. Здесь протокол взаимодействия находится в конкретном состоянии. Заметим, однако, что когда другие, не перечисленные переменные / параметры включены и изменяются, эти конкретные параметры по существу образуют запрос. Этот запрос может логически просматривать пространство поднабора возможных состояний, т.е. состояний с конкретными параметрами из вышеперечисленных с другими изменяемыми параметрами.
В одном варианте осуществления формальная модель структуры межсоединений фильтруется или приспосабливается к конкретной модели реализации. Здесь формальная модель может воплощать в себе спецификацию структуры / протокола, такую как полная формальная модель ограничений для подлежащего воплощению протокола взаимодействия. В одном варианте осуществления формальная модель включает в себя формальную модель протокола взаимодействия, которая по существу привязана к спецификации Intel's Quickpath. Однако формальная модель может включать в себя любое моделирование протокола, структуры, межсоединения, уровня межсоединения или иной объект проверки. В одном варианте осуществления база 201 данных предназначена для хранения пространства покрытия состояний для формальной модели.
Однако в полной спецификации может использоваться конкретная реализация структуры межсоединений. В результате формальную модель можно фильтровать, приспосабливать и (или) модифицировать на основе конкретных ограничений конфигурации конкретного воплощения. Например, в протоколе взаимодействия могут быть конкретизированы несколько агентов, а также тип агентов или иная информация. Когда конкретная модель воплощения получена, программа проверки модели или иной инструмент исполняется для определения пространства покрытия возможных состояний для структуры межсоединений. Как установлено выше, пространство покрытия может включать в себя все возможные состояния для модели воплощения или сокращенного набора возможных состояний, такого как симметрично сокращенный набор состояний.
Затем, в операциях 305-310 типовая тестовая последовательность загружается и исполняется для моделирования. В одном варианте осуществления среда моделирования включает в себя среду моделирования уровня регистровых передач (RTL). В качестве примера, среда RTL создается для моделирования работы структуры во время работы. Типовая тестовая последовательность возбуждает / моделирует обычные действия, которые могут иметь место для выделения различных маршрутов и состояний протокола взаимосвязи. Например, конкретные известные затрудненные транзакции или конфигурации могут быть включены в типовую тестовую последовательность для проверки того, что протокол не отказывает во время работы. Типовая тестовая последовательность может также включать в себя произвольные случаи, трафик или активность, чтобы обеспечить случайную проверку правильности состояний протокола. Отметим, что такое же моделирование типовой тестовой последовательности можно использовать для любого объекта проверки, такого как уровень физического соединения или иной протокол.
В операции 315 обратная связь на основе множества из нескольких возможных состояний, не встречающихся во время исполнения / моделирования типовой тестовой последовательности, обеспечивается для формирования целевой тестовой последовательности. Здесь в операции 316 определяют возможные состояния структуры, которые не встречались и не посещались во время моделирования. В одном варианте осуществления для этого определения используется база данных, аналогичная базе 201 данных по фиг.2. Как установлено выше, база данных может хранить пространство покрытия возможных состояний, которыми могут быть все возможные состояния объекта проверки или некоторый сокращенный их поднабор.
В качестве примера, состояния, встречающиеся во время моделирования, маркируются в базе данных. Отметим, что признаковый идентификатор базы 201 данных может использоваться для индексации в базу данных и маркировки правильного ввода. Поэтому когда моделирование завершено, все посещавшиеся состояния маркируют в базе 201 данных. В результате любое возможное состояние, хранящееся в базе 201 данных не маркированным, определяется, чтобы быть не встретившимся во время моделирования.
В операции 317 определяется целевая тестовая последовательность для не встретившихся целевых возможных состояний. В одном варианте осуществления база данных запрашивается для определения не встретившихся состояний. Например, когда большое пространство состояний, т.е. некоторая комбинация параметров, что то же самое, не встречается, оно часто именуется как дыра или зазор. В качестве примера предположим, что состояние, где первый процессор хранит строку в совместно используемом состоянии, второй процессор хранит строку в совместно используемом состоянии и разведчик принимается из третьего процессора, никогда не встречается. Отметим, что база данных с сотней параметров, имеющая только эти три параметра постоянными, будет логически создавать большое число не встречающихся состояний, т.е. каждое состояние, которое включает в себя эти параметры и изменяет остальные 97. Иными словами, получается очень большая дыра или зазор, т.к. большое число состояний с аналогичными параметрами не встречалось во время моделирования, чтобы гарантировать должную работу.
Поэтому в одном варианте осуществления информация состояния заводится назад в формальный режим или иную модель, чтобы определить маршрут, получающийся из начального состояния к не встретившемуся состоянию. Иными словами, определяется, что должно произойти в структуре для достижения этого не встретившегося состояния. Данная информация затем используется для построения целевой тестовой последовательности, которая потенциально вызывает маршрут в моделировании для достижения не встретившихся состояний или некоторой их части.
Здесь типовая тестовая последовательность может быть модифицирована вышеупомянутой маршрутной информацией или иной информацией к целевым не встретившимся состояниям. Однако целевая тестовая последовательность не должна намечать все из возможных не встретившихся состояний. На деле в чрезвычайно сложном межсоединении с таким большим количеством возможных состояний может быть чрезвычайно трудно наметить каждое возможное состояние. Следовательно, цель может состоять только в достижении доверительного уровня, т.е. части подтвержденных состояний, а не обнаружения всех состояний. Отметим, что может также иметь место цель доверительного уровня частичной дыры / зазора, чтобы гарантировать, что по меньшей мере для некоторых состояний в числе дыр / зазоров подтверждена правильность. В результате некий пользовательский анализ или анализ посредством программы может определить поднабор возможных не встретившихся состояний, чтобы наметить покрытие дыр, зазоров или поворотных случаев для проверки правильности.
Как установлено выше, целевая тестовая последовательность, при ее исполнении, предназначена для того, чтобы вызвать или смоделировать возможные состояния структуры, не встретившиеся во время исполнения / моделирования типовой тестовой последовательности. Далее, поднабор возможных не встретившихся состояний может быть грамотно выбран физическим пользователем либо посредством исполнения кода для целевых зазоров, дыр, поворотных случаев, идентифицированных трудных состояний или иных возможных состояний.
В операции 310 целевая тестовая последовательность исполняется / моделируется аналогично типовой тестовой последовательности. Здесь вновь встретившиеся состояния могут также маркироваться в базе данных. Далее, петля 315 обратной связи может повторяться рекурсивно, чтобы далее намечать другие еще не встретившиеся возможные состояния, или чтобы повторно намечать возможные состояния, которые были ранее намечены, но не встретились во время моделирования.
На фиг.4 показан конкретный сверхупрощенный иллюстративный вариант осуществления блок-схемы алгоритма для методологии / стратегии, чтобы обеспечить эффективное моделирование проверки правильности покрытия структуры. В операциях 405-417 формальную модель фильтруют на основе ограничений конфигурации конкретного варианта осуществления структуры, запускают проверочную программу модели для исследования пространства покрытия возможных состояний для отфильтрованной конкретной модели реализации, и это пространство покрытия сохраняют в базе 417 данных.
Отметим исходя из вышесказанного, что пространство покрытия может включать в себя все возможные состояния структуры для объекта структуры / проверки или сокращенный набор состояний, такой как симметрично сокращенный набор состояний. Кроме того, база 417 данных может содержать базу 201 данных по фиг.2, в которой ввод базы данных соответствует состоянию структуры пространства покрытия. Здесь каждый ввод включает в себя по меньшей мере множество значений параметров для параметров структуры, которые определяют состояние структуры, соответствующее этому вводу, признаковый идентификатор, который основан на множестве значений параметров, и маркирующее поле.
Здесь проверка правильности и моделирование могут выполняться параллельно, непосредственно после генерирования базы данных, либо позже. Например, компания, обеспечивающая спецификацию или модель для структуры, такой как структура протокола, может в дополнение к ней или альтернативно предоставить базу данных из операции 417 потребителю, чтобы обеспечить эффективные моделирование и проверку правильности межсоединения. Типовая тестовая последовательность и другие коды / сценарии также могут быть предоставлены.
Тем не менее, после того как база данных создана и (или) предоставлена, в операции 425 моделируют типовую тестовую последовательность из операции 420. В иллюстрируемом варианте осуществления выполняют моделирование уровня регистровых передач (RTL). Однако для моделирования работы структуры можно использовать любой язык, код, имитатор или иной известный инструмент моделирования / проверки правильности. Либо во время моделирования, либо после моделирования встретившиеся состояния структуры маркируют в операции 430 в базе данных операции 417. Как установлено выше, признаковый идентификатор для каждого состояния / ввода может быть использован для индексации в базу 417 данных. Отметим, что вместо этого можно использовать любой другой ключ, такой как исходный ключ базы данных, для индексации в базу данных.
Здесь возможные состояния пространства покрытия, хранящиеся в базе данных немаркированными, определяют в операции 435 как не встретившиеся / не посещенные во время моделирования в операции 425. На основе этого определения целевая тестовая последовательность разрабатывается / определяется в операции 440, чтобы наметить возможные состояния пространства покрытия, не встретившиеся во время моделирования. Как установлено выше, зазоры и дыры, а также другие состояния могут намечаться с помощью автоматизированного программного обеспечения и подаваться назад в модель для определения маршрутов / информации, чтобы наметить эти состояния. Отметим, что не все из возможных не встретившихся состояний могут быть намечены, т.к. намеченные состояния могут быть грамотно выбраны, чтобы охватить поворотные состояния, известные проблематичные состояния и зазоры / дыры в покрытии состояний, а также некоторое число случайным образом встретившихся состояний, чтобы обеспечить дополнительное покрытие. Целевую тестовую последовательность используют затем в операции 425 моделирования, и маркируют вводы / состояния базы данных, которые встречаются вновь. Этот процесс может выполняться рекурсивно до тех пор, пока не будет достигнуто адекватного покрытия проверки правильности для возможных состояний.
Поэтому, как видно из вышеприведенного, здесь описана эффективная и автоматическая методология проверки правильности для сложной структуры, такой как сложные протоколы, сложные межсоединения и прочие сложные объекты проверки. Раньше протоколы и межсоединения были менее сложными, позволяя пользователю постигать пространство покрытия и обеспечивать адекватные тестовые последовательности, чтобы гарантировать достоверность во время проверки правильности. Однако при использовании базы данных для хранения пространства покрытия состояний структуры сложную структуру стало возможным постичь в электронном формате. Далее, за счет маркировки состояний, встречающихся во время моделирования, число встречающихся и не встретившихся состояний также стало возможным постичь. На основе этого можно разработать целевую тестовую последовательность, чтобы гарантировать, что достигается адекватная проверка правильности пространства покрытия. В результате можно не только постичь уровень достоверности при проверке правильности структуры, но можно также достичь его, рекурсивно намечая непромоделированные состояния.
Как используется здесь, «значение» включает в себя любое известное представление числа, состояния, логического состояния или двоичного логического состояния. Зачастую, использование логических уровней, булевых переменных или логических значений именуется также единицами и нулями, которые просто представляют двоичные логические состояния. Например, 1 относится к высокому логическому уровню, а 0 относится к низкому логическому уровню. В одном варианте осуществления ячейка памяти, такая как транзисторная ячейка или ячейка флэш-памяти, может оказаться способна хранить единственное логическое значение или множество логических значений. Однако в компьютерных системах использованы и другие представления значений. Например, десятичное число десять может быть также представлено как двоичное значение 1010 и шестнадцатеричная буква А. Поэтому значение включает в себя любое представление информации, способное храниться в компьютерной системе.
Кроме того, состояния могут быть представлены значениями или частями значений. В качестве примера, первое значение, такое как логическая единица, может представлять состояние по умолчанию или начальное состояние, тогда как второе значение, такое как логический ноль, может представлять состояние не по умолчанию. Помимо этого термины «сброс» и «установка» в одном варианте осуществления относятся к значению или состоянию по умолчанию и обновленному значению или состоянию, соответственно. Например, значение по умолчанию потенциально включает в себя высокое логическое значение, т.е. сброс, тогда как обновленное значение потенциально включает в себя низкое логическое значение, т.е. установку. Отметим, что любую комбинацию значений можно использовать для представления любого числа состояний.
Изложенные выше варианты способов, аппаратного обеспечения, программного обеспечения, встроенного программного обеспечения или кода могут быть реализованы командами или кодом, хранящимися на доступном для машин или машиночитаемом носителе, которые являются исполнимыми элементами обработки. Доступный для машины / машиночитаемый носитель включает в себя любой механизм, который обеспечивает (т.е. сохраняет и (или) передает) информацию в виде, считываемом машиной, такой как компьютер или электронная система. Например, доступный для машины носитель включает в себя оперативное запоминающее устройство (ОЗУ) (RAM), такое как статическое ОЗУ (SRAM) или динамическое ОЗУ (DRAM); ПЗУ (КОМ); магнитный или оптический носитель данных, устройства флэш-памяти; электрическое запоминающее устройство, оптические запоминающие устройства, акустические запоминающие устройства или иной вид устройства запоминания распространяемого сигнала (к примеру, несущие колебания, инфракрасные сигналы, цифровые сигналы) и т.п. Например, машина может обращаться к носителю данных посредством приема распространяемого сигнала, такого как несущие колебания, из среды, способной хранить информацию, подлежащую передаче на распространяемом сигнале.
Ссылка по всему данному описанию на «один вариант осуществления» или «вариант осуществления» означает, что конкретный признак, структура или характеристика, описанная в связи с этим вариантом осуществления, включена в по меньшей мере один вариант осуществления настоящего изобретения. Таким образом, появления выражений «в одном варианте осуществления» или «в варианте осуществления» в разных местах по всему данному описанию не обязательно относятся к одному и тому же варианту осуществления. Далее, частные признаки, структуры или характеристики могут комбинироваться любым подходящим образом в одном или нескольких вариантах осуществления.
Выше дано подробное описание со ссылкой на конкретные примерные варианты осуществления. Однако очевидно, что различные модификации и изменения могут быть сделаны в нем без отхода от более широких сущности и объема изобретения, как изложено в приложенной формуле изобретения. Описание и чертежи следует, соответственно, рассматривать в иллюстративном смысле, а не в ограничительном смысле. Далее, вышеуказанное использование варианта осуществления или других примерных языков не обязательно относится к одному и тому же варианту осуществления или тому же самому примеру, но может относиться к разным и отличным вариантам осуществления, а также потенциально к одному и тому же варианту осуществления.
1. Машиночитаемый носитель, включающий в себя программный код для обеспечения покрытия эффективной проверки правильности структуры протокола, который при исполнении в машине заставляет эту машину выполнять операции, в которых:
определяют первое число состояний, хранящихся в ссылочной базе данных для реализации протокола, которые не встречаются во время моделирования типовой тестовой последовательности для реализации протокола;
разрабатывают целевую тестовую последовательность при моделировании для реализации протокола, чтобы наметить множество из первого числа состояний, которые не посещаются во время моделирования типовой тестовой последовательности,
осуществляют проверку правильности реализации различных протоколов моделированием тестовой последовательности возможных состояний структуры протокола и проверку подтвержденной части состояний доверительного уровня структуры протокола.
2. Машиночитаемый носитель по п.1, в котором этап определения первого числа состояний, хранящихся в ссылочной базе данных для реализации протокола, которые не посещаются во время моделирования типовой тестовой последовательности для реализации протокола, содержит этапы, на которых:
маркируют второе число состояний, хранящихся в ссылочной базе данных, которые посещаются во время моделирования типовой тестовой последовательности;
определяют, что первое число состояний, хранящихся в ссылочной базе данных для реализации протокола, не встречаются во время моделирования типовой тестовой последовательности в ответ на первое число состояний, не промаркированное после маркировки второго числа состояний во время моделирования типовой тестовой последовательности.
3. Машиночитаемый носитель по п.2, в котором этап разработки целевой тестовой последовательности моделирования при моделировании реализации протокола, чтобы наметить множество из первого числа состояний, которые не посещаются во время моделирования типовой тестовой последовательности, содержит этапы, на которых:
идентифицируют множество из первого числа состояний, которые не посещаются во время моделирования типовой тестовой последовательности;
определяют множество маршрутов от начального состояния к множеству из первого числа состояний, которые не встречаются во время моделирования типовой тестовой последовательности; и
строят множество маршрутов в целевой тестовой последовательности моделирования при моделировании для реализации протокола, чтобы наметить множество из первого числа состояний.
4. Машиночитаемый носитель по п.3, в котором этап идентифицирования множества из первого числа состояний, которые не встречаются во время моделирования типовой тестовой последовательности, происходит в ответ на автоматический запрос ссылочной базы данных.
5. Машиночитаемый носитель по п.2, в котором программный код, который при исполнении машиной заставляет далее эту машину выполнять операции, в которых:
моделируют целевую тестовую последовательность моделирования; и маркируют множество из первого числа состояний, хранящихся в ссылочной базе данных, которые посещаются во время моделирования целевой тестовой последовательности моделирования.
6. Машиночитаемый носитель, включающий в себя программный код для обеспечения покрытия эффективной проверки правильности структуры протокола, который при исполнении машиной заставляет эту машину выполнять операции, в которых:
определяют пространство покрытия возможных состояний для объекта проверки на основе множества параметров для этого объекта проверки;
вычисляют соответствующий признаковый идентификатор для возможного состояния в пространстве покрытия возможных состояний на основе множества соответствующих значений, которые соответствуют множеству параметров для возможного состояния,
осуществляют проверку правильности реализации различных протоколов с использованием моделирования для тестовой последовательности возможных состояний структуры протокола, при моделировании с подтвержденной частью состояний доверительного уровня структуры протокола; и
сохраняют соответствующий признаковый идентификатор и множество соответствующих значений для возможного состояния во вводе базы данных.
7. Машиночитаемый носитель по п.6, в котором объект проверки выбран из группы, состоящей из протокола передачи данных, сетевого протокола, протокола беспроводной связи, протокола взаимосвязи, протокола межсоединений и структуры физических межсоединений.
8. Машиночитаемый носитель по п.6, в котором этап определения пространства покрытия возможных состояний для объекта проверки на основе множества параметров содержит этапы, на которых:
приспосабливают формальную модель объекта проверки на основе множества ограничений конфигурации для объекта проверки;
исполняют программу проверки модели для исследования всех возможных состояний для объекта проверки посредством изменения множества параметров для формирования пространства покрытия множества состояний.
9. Машиночитаемый носитель по п.6, в котором этап вычисления соответствующего признакового идентификатора для возможного состояния в пространстве покрытия возможных состояний на основе множества соответствующих значений, которые соответствуют множеству параметров для возможного состояния, содержит этап, на котором комбинируют множество соответствующих значений с помощью алгоритма для получения соответствующего признакового идентификатора.
10. Машиночитаемый носитель по п.6, содержащий далее этапы, на которых:
моделируют типовую тестовую последовательность для объекта проверки;
маркируют ввод базы данных, связанный с возможным состоянием, в ответ на обнаружение этого возможного состояния во время моделирования типовой тестовой последовательности для объекта проверки; и
обеспечивают целевую тестовую последовательность при моделировании объекта проверки, чтобы наметить это возможное состояние в ответ на ввод из базы данных, не промаркированный после моделирования типовой тестовой последовательности.
11. Способ для обеспечения покрытия эффективной проверки правильности структуры протокола, содержащий этапы, на которых:
определяют множество возможных состояний структуры протокола;
вычисляют идентификатор для каждого из возможных состояний на основе численных параметров для каждого из множества возможных состояний;
осуществляют проверку правильности реализации различных протоколов моделированием тестовой последовательности возможных состояний структуры протокола и проверку подтвержденной части состояний доверительного уровня структуры протокола; и
сохраняют в базе данных этот идентификатор для каждого из множества возможных состояний и численные параметры для каждого из множества возможных состояний.
12. Способ по п.11, в котором этап определения множества возможных состояний структуры протокола содержит этапы, на которых фильтруют формальную модель на основе множества ограничений для формирования модели реализации для структуры протокола, и выполняют программу проверки модели на этой модели реализации, чтобы определить множество возможных состояний для этой структуры протокола.
13. Способ по п.11, в котором этап определения множества возможных состояний структуры протокола содержит этапы, на которых фильтруют формальную модель на основе множества ограничений конфигурации, чтобы сформировать модель реализации для этой структуры протокола, выполняют программу проверки модели на этой модели реализации, чтобы определить все возможные состояния этой структуры протокола, и сокращают множество симметричных состояний всех из возможных состояний, чтобы определить множество возможных состояний.
14. Способ по п.11, в котором этап вычисления идентификатора для каждого из возможных состояний на основе численных параметров для каждого из множества возможных состояний содержит этап, на котором комбинируют численные параметры для каждого из множества возможных состояний с использованием заранее заданного математического алгоритма, чтобы вычислить идентификатор для каждого из множества возможных состояний.
15. Способ для обеспечения покрытия эффективной проверки правильности структуры протокола, содержащий этапы, на которых:
определяют число возможных состояний для структуры протокола;
исполняют типовую тестовую последовательность для моделирования работы этой структуры протокола;
обеспечивают обратную связь на основе множества из числа возможных состояний, не встретившихся во время исполнения типовой тестовой последовательности, чтобы сформировать целевую тестовую последовательность, предназначенную при ее исполнении, чтобы наметить множество из числа возможных состояний, не встретившихся во время исполнения типовой тестовой последовательности, и
осуществляют проверку правильности реализации различных протоколов моделированием тестовой последовательности возможных состояний структуры протокола и проверку подтвержденной части состояний доверительного уровня структуры протокола.
16. Способ по п.15, в котором структура протокола включает в себя структуру протокола, подлежащую выбору из группы, состоящей из структуры протокола передачи данных межсоединений, структуры протокола взаимосвязи с кэшем, структуры протокола сетевой передачи данных и структуры протокола беспроводной передачи данных.
17. Способ по п.15, в котором этап определения числа возможных состояний структуры протокола содержит этапы, на которых:
фильтруют формальную модель для этой структуры протокола для конкретной модели реализации этой структуры протокола на основе множества ограничений конфигурации; и
исполняют программу проверки модели, чтобы определить число возможных состояний конкретной модели для реализации этой структуры протокола.
18. Способ по п.15, содержащий далее этап, на котором: сохраняют представление каждого из числа возможных состояний во вводе базы данных, причем каждый ввод базы данных предназначен для включения поля параметра для хранения множества численных значений, связанных с множеством параметров, которые определяют одно возможное состояние из числа возможных состояний, связанных с этим вводом, поле признакового идентификатора для хранения признакового идентификатора на основе множества численных значений и маркирующее поле при обновлении на маркированное значение для индикации возможного состояния, встретившегося во время исполнения типовой тестовой последовательности.
19. Способ по п.18, в котором этап обеспечения обратной связи на основе множества из числа возможных состояний, не встретившихся во время исполнения типовой тестовой последовательности, чтобы сформировать целевую тестовую последовательность, предназначенную при ее исполнении, чтобы наметить множество из числа возможных состояний, не встретившихся во время исполнения типовой тесовой последовательности, содержит этапы, на которых:
обновляют маркирующее поле каждого ввода базы данных на маркированное значение в ответ на обнаружение этого возможного состояния из числа состояний во время исполнения типовой тестовой последовательности;
определяют множество из числа не встретившихся возможных состояний на основе маркирующего поля, связанного с каждым из множества из числа возможных состояний, хранящего немаркированное значение; и
модифицируют типовую тестовую последовательность, чтобы сформировать целевую тестовую последовательность.
