Микроэлектроника, 2019, T. 48, № 5, стр. 371-378

ВВЕДЕНИЕ

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

В связи с вышеизложенным математической моделью внешнего поведения проектируемой цифровой системы может служить семейство стационарных динамических систем, что впервые предложено в [1].

Будем использовать приведенное в [2] определение динамической системы в виде

где T – множество моментов времени, в общем случае действительная полуось {t|t ≥ 0}; X – множество внутренних состояний; U – множество мгновенных значений входных воздействий, называемое также множеством входных состояний; Ω – множество отображений ω: T → U – допустимых входных воздействий; Y – множество мгновенных значений выходных воздействий, называемое также множеством выходных состояний; Γ – множество отображений γ: T → Y – возможных выходных воздействий; φ: T × T × X × Ω → X – переходная функция состояния, значениями которой служат внутренние состояния x(t) = φ(t, τ, x, ω), x(t) ∈ X, в которых оказывается система в момент времени t, t ∈ T, если в начальный момент времени τ, τ ∈ T, она была в начальном состоянии x(τ) ∈ X и если на нее действовало входное воздействие ω ∈ Ω; η: T × X → Y – выходное отображение, определяющее выходные воздействия y(t) = η(t, x(t)).

Динамическая система является стационарной, если ее реакция на заданный отрезок входного воздействия при условии, что система находится в заданном внутреннем состоянии, не зависит от начального момента времени [2]. В частности, переходная функция принимает вид φ: T × X × Ω → X, ее значениями служат состояния x(t) = φ(t, x, ω), где x – состояние системы в момент t = 0, выходное отображение η: X → Y не зависит от времени.

В приведенном определении динамической системы каждому внутреннему состоянию x однозначно соответствует мгновенное значение выходного воздействия y. Более удобным для нас является использование выходного отображения в виде η: X → Y, предложенное в [3]. Такой вид выходного отображения не искажает приведенного выше определения стационарной динамической системы и позволяет получить в качестве частного случая последней конечный автомат Мили.

МОДЕЛЬ ВНЕШНЕГО ПОВЕДЕНИЯ ЦИФРОВОЙ СИСТЕМЫ

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

1. Конечное множество терминальных переменных P, описывающих внешние линии и шины цифровой системы. Переменная p ∈ P всегда имеет одно из значений конечного множества ${{{\mathbf{Z}}}_{p}},$ причем ${{{\mathbf{Z}}}_{p}} = {\mathbf{Z}}_{p}^{*} \times {\text{DI}}{{{\text{R}}}_{p}},$ где ${\mathbf{Z}}_{p}^{*}\quad$ – множество логических значений переменной p, в частности, для шины из n линий имеется 2ⁿ значений или 2ⁿ + 1 значений, если шина имеет состояние с высоким выходным сопротивлением; $\quad{\text{DI}}{{{\text{R}}}_{p}}$ – множество направлений передачи сигнала. В множестве P можно выделить три непересекающихся подмножества: ${\mathbf{P}}{\text{'}} = \quad\left\{ {p{\text{|DI}}{{{\text{R}}}_{p}} = \left\{ 1 \right\}} \right\};$ ${\mathbf{P}}{\text{''}} = \left\{ {p{\text{|DI}}{{{\text{R}}}_{p}} = \left\{ 0 \right\}} \right\};$ P''' = $\left\{ {p{\text{|DI}}{{{\text{R}}}_{p}} = \left\{ {0.1} \right\}} \right\},$ причем P = $P{\text{'}} \cup {\mathbf{P}}{\text{''}} \cup {\;}\quad{\mathbf{P}}{\text{'''}}{\text{.}}$ Терминальные переменные подмножеств ${\mathbf{P}}{\text{',}}$ описывают входные, выходные и двунаправленные шины и линии цифровой системы соответственно; направление передачи ${\text{di}}{{{\text{r}}}_{p}}$ = 1 указывает на входной, а ${\text{di}}{{{\text{r}}}_{p}}$ = 0 – на выходной сигнал. Состояние шины или линии p с высоким выходным сопротивлением представляется значением из множества ${\mathbf{Z}}_{p}^{{}}$ при ${\text{di}}{{{\text{r}}}_{p}}$ = 0.

Множество мгновенных значений терминальных переменных, то есть внешних состояний цифровой системы, есть Q = $\prod\nolimits_{p \in {\mathbf{P}}} {{{{\mathbf{Z}}}_{p}}} .$

2. Множество моментов времени T = $\left\{ {t{\text{|}}t \geqslant 0} \right\}.$

3. Множество Ψ допустимых взаимодействий с внешней средой, каждое из которых есть отображение ψ: [0, t) → Q, t ∈ T. Каждое ψ может быть представлено как конечное множество отображений ${{\psi }_{p}}{\text{:}}$ [0, t) → $\quad{{{\mathbf{Z}}}_{p}},$ p ∈ P, t ∈ T.

Отличие допустимых взаимодействий друг от друга может быть обусловлено:

− различной длительностью взаимодействий;

− различной последовательностью функций, выполняемых цифровой системой в зависимости от внешних сигналов;

− различной последовательностью появления ряда входных или выходных сигналов, если эта последовательность безразлична, при выполнении одной и той же последовательности функций; наличием безразличных входных событий (переключений сигналов), не оказывающих влияния на функционирование цифровой системы;

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

Таким образом, внешнее поведение семейства стационарных динамических систем, являющихся математической моделью цифровой системы, при известных T, P, $\left\{ {{{{\mathbf{Z}}}_{p}}{\text{|}}p \in {\mathbf{P}}} \right\}$ задается множеством допустимых взаимодействий Ψ.

МОДЕЛЬ ДОПУСТИМЫХ ВЗАИМОДЕЙСТВИЙ ЦИФРОВОЙ СИСТЕМЫ

Рассмотрим подробнее задание допустимых взаимодействий ψ: [0, t) → Q. Событием по переменной p назовем изменение переменной p со значения ${{z}_{1}}$ ∈ ${{{\mathbf{Z}}}_{p}}$ на значение ${{z}_{2}}$ ∈ ${{{\mathbf{Z}}}_{p}}$ в момент времени t. Обозначим такое событие $\chi _{{p,{{z}_{1}},{{z}_{2}}\quad}}^{t}.$

В цифровых системах для каждого конечного временного интервала количество событий по терминальным переменным, то есть количество изменений их значений, конечно. В связи с этим любое допустимое взаимодействие ψ ∈ Ψ может быть представлено в виде вектора ($z_{{{{p}_{1}},\quad \ldots ,}}^{{\text{н }}}z_{{{{p}_{k}}}}^{{\text{н }}}$) начальных значений переменных ${{p}_{1}},$…,${{p}_{k}}$ (k – мощность множества Р) в момент времени t = 0 и последовательности событий по переменным множества Р с конечным числом событий за любой конечный интервал времени:

где ${{t}_{1}}$ ≤ ${{t}_{2}}$ ≤ ${{t}_{3}}$ ≤ … – упорядоченная последовательность времен событий;

${{p}_{{{{i}_{1}}\quad}}},$ ${{p}_{{{{i}_{2}}}}},\quad{{p}_{{{{i}_{3}}}}},$ … – переменные, принадлежащие множеству P;

${{z}_{{{{j}_{{1\quad}}}}}},$ ${{z}_{{{{j}_{{3\quad}}}}}},$ ${{z}_{{{{j}_{{5\quad}}}}}},$ … – значения переменных непосредственно перед событием;

${{z}_{{{{j}_{{2\quad}}}}}},$ ${{z}_{{{{j}_{{4\quad}}}}}},$ ${{z}_{{{{j}_{{6\quad}}}}}},$ … – значения переменных непосредственно после события,

причем при выделении из (1) начального значения любой терминальной переменной ${{p}_{{i\quad}}}$ и подпоследовательности событий по этой переменной получаем отображение ${{\psi }_{{{{p}_{i}}}}}{\text{:}}$[0, t) → ${{{\mathbf{Z}}}_{{{{p}_{i}}}}},$ которое имеет вид:

где $z_{{{{p}_{i}}}}^{{\text{н }}}$ – начальные значения переменной ${{p}_{i}};$

${{\tau }_{1}} < {{\tau }_{2}} < {{\tau }_{{3\quad}}} < \ldots $ – упорядоченная последовательность времен событий по данной переменной;

${{z}_{1}},$ ${{z}_{2}},\,\,{{z}_{3}},$ … – значения переменной ${{p}_{{i\quad}}}$ из множества ${{{\mathbf{Z}}}_{{{{p}_{i}}}}}.$

Представим последовательность (1) в виде двух подпоследовательностей: последовательности входных для цифровой системы событий – входного воздействия

где $z_{{{{p}_{1}},\quad \ldots ,}}^{{\text{н }}}z_{{{{p}_{n}}}}^{{\text{н }}}$ – начальные значения переменных множества причем для переменных множества логические значения задаются только в том случае, если в начальный момент времени у них ${\text{di}}{{{\text{r}}}_{p}}$ = 1; в противном случае для них достаточно задания направления передачи ${\text{di}}{{{\text{r}}}_{p}}$ = 0;

n – количество переменных множества

$\chi _{{{{p}_{{{{i}_{1}}}}},{{z}_{{{{j}_{1}}}}},{{z}_{{{{j}_{2}}}}}\quad}}^{{'{{t}_{1}}}},$ $\chi _{{{{p}_{{{{i}_{2}}}}},{{z}_{{{{j}_{3}}}}},{{z}_{{{{j}_{4}}}}}\quad}}^{{'{{t}_{2}}}},$ $\chi _{{{{p}_{{{{i}_{3}}}}},{{z}_{{{{j}_{5}}}}},{{z}_{{{{j}_{6}}}}}\quad}}^{{'{{t}_{3}}}}\,\,...$ – события по переменным множества ${\mathbf{P}}{\text{'}},$ а также события по переменным множества ${\mathbf{P}}{\text{''',}}$ для которых начальное, конечное или оба значения в событии имеет ${\text{di}}{{{\text{r}}}_{p}}$ = 1;

${{t}_{1}}$ ≤ ${{t}_{2}}$ ≤ ${{t}_{3}}$ ≤ … – упорядоченная последовательность времен входных событий, и последовательности выходных событий – выходного воздействия

где $z_{{{{p}_{1}},\quad \ldots ,}}^{{\text{н }}}z_{{{{p}_{m}}}}^{{\text{н }}}$ – начальные значения переменных множества причем для переменных множества логические значения задаются только в том случае, если в начальный момент времени у них ${\text{di}}{{{\text{r}}}_{p}}$ = 0; в противном случае для них достаточно задания направления передачи ${\text{di}}{{{\text{r}}}_{p}}$ = 1;

m – количество переменных множества

– события по переменным множества ${\mathbf{P}}{\text{'',}}$ а также события по переменным множества ${\mathbf{P}}{\text{''',}}$ для которых начальное, конечное или оба значения в событии имею ${\text{di}}{{{\text{r}}}_{p}}$ = 0;

${{t}_{1}}$ ≤ ${{t}_{2}}$ ≤ ${{t}_{3}}$ ≤ … – упорядоченная последовательность времен выходных событий.

Полученные входное ω и выходное γ воздействия могут содержать одинаковые события $\chi _{{{{p}_{i}},{{z}_{{{{j}_{1}}}}},{{z}_{{{{j}_{2}}}}}\quad}}^{t}$ по переменным множества если одно из значений ${{z}_{{{{j}_{1}}}}},$ ${{z}_{{{{j}_{2}}}}}$ имеет ${\text{di}}{{{\text{r}}}_{p}}$ = 1, а другое ${\text{di}}{{{\text{r}}}_{p}}$ = 0.

Входное воздействие есть

U – множество мгновенных значений входных воздействий, называемое также множеством входных состояний; состояние переменной p ∈ равное 0, указывает на передачу сигнала на выход и не определяет логического значения переменной.

Выходное воздействие есть

Y – множество мгновенных значений выходных воздействий, называемое также множеством выходных состояний; состояние переменной p ∈ P, равное 1, указывает на передачу сигнала на вход и не определяет логического значения переменной.

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

Выделим из последовательности событий (1) – взаимодействия ψ – последовательность выходных событий, которые по заданному протоколу обмена обуславливают моменты времени входных событий. Назовем переменные, по которым происходят эти выходные события, переменными управления обменом ${{{\mathbf{P}}}^{{\text{o}}}},$ Выделенную из (1) подпоследовательность событий вместе с начальными значениями переменных управления обменом назовем выходным воздействием управления обменом

где $z_{{{{p}_{1}},\quad \ldots ,}}^{{\text{н }}}z_{{{{p}_{q}}}}^{{\text{н }}}$ – начальные значения переменных множества ${{{\mathbf{P}}}^{{\text{о }}}};$

q – мощность множества ${{{\mathbf{P}}}^{{\text{о }}}};$

– события по переменным множества ${{{\mathbf{P}}}^{{\text{о }}}};$

${{t}_{1}}$ ≤ ${{t}_{2}}$ ≤ ${{t}_{3}}$ ≤ … – упорядоченная последовательность времен выходных событий управления обменом.

Выходное воздействие управления обменом есть

${{{\mathbf{Y}}}^{{\text{о }}}}$ – множество мгновенных значений выходных воздействий управления обменом.

Объединим подпоследовательности событий входного воздействия ω (2) и выходного воздействия обмена ${{\gamma }^{{\text{o}}}}$ (4) одного и того же ψ и вместе с начальными значениями соответствующих переменных назовем полученную подпоследовательность событий входным взаимодействием

где

– входные события и выходные события управления обменом; ${{t}_{1}}$ ≤ ${{t}_{2}}$ ≤ ${{t}_{3}}$ ≤ … – упорядоченная последовательность времен событий входного взаимодействия.

Входное взаимодействие есть μ: [0, t) → U × ${{{\mathbf{Y}}}^{{\text{o}}}},$ t ∈ T.

В дальнейшем в качестве аргументов функционирования цифровых систем будем использовать входные взаимодействия, что дает возможность рассматривать режимы работы, инициируемые как внешними входными сигналами, так и самими цифровыми системами. В простейшем случае, когда подача сигналов на проектируемую систему не зависит от ее выходных сигналов, множество выходных переменных управления обменом ${{{\mathbf{P}}}^{{\text{o}}}}$ пусто и входное взаимодействие μ совпадает с входным воздействием ω.

При известных T, P, $\left\{ {{{{\mathbf{Z}}}_{p}}{\text{|}}p \in {\mathbf{P}}} \right\}$ каждое допустимое взаимодействие ψ описанным выше образом определяет входное ω и выходное γ воздействия, выходное воздействие управления обменом ${{\gamma }^{{\text{o}}}}$ и входное взаимодействие ω на общем интервале времени [0, t). Тогда множество допустимых взаимодействий Ψ задает множество входных воздействий Ω, выходных воздействий Γ, выходных воздействий управления обменом ${{\Gamma }^{{\text{о }}}}$ и входных взаимодействий Μ. Кроме того, на Ω × Γ, Ω × ${{\Gamma }^{{\text{о }}}}$ и Μ × Γ определены отношения b, b' и b'' соответственно: (ω, γ) ∈ b, если ω и γ образуют допустимое взаимодействие ψ ∈ Ψ; (ω, γ⁰) ∈ b', если ω и γ⁰ образуют входное взаимодействие μ ∈ Μ; (μ, γ) ∈ b'', если μ и γ образуют допустимое взаимодействие ψ ∈ Ψ. Множество допустимых взаимодействий может быть задано как Ψ = (Ω, Γ, b) или как Ψ = = (Μ, Γ, b''); множество входных взаимодействий – как Μ = (Ω, Γ^о, b').

Каждому допустимому входному взаимодействию μ соответствует непустое множество выходных воздействий ${{\Gamma }_{\mu }}$ = {γ|b''(μ, γ)}. Все элементы $\gamma \in {{\Gamma }_{\mu }}$ различаются только моментами времени выходных событий в допустимых пределах и, возможно, значениями выходных переменных на определенных отрезках времени, если эти значения безразличны. При известных T, P, $\left\{ {{{{\mathbf{Z}}}_{p}}{\text{|}}p \in {\mathbf{P}}} \right\}$ множество допустимых взаимодействий

причем при μ ∈ Μ, ${{\Gamma }_{\mu }} \ne \emptyset .$

УЧЕТ ПОСЛЕДОВАТЕЛЬНОСТИ ВЫПОЛНЯЕМЫХ ФУНКЦИЙ И ВРЕМЕННЫХ ОГРАНИЧЕНИЙ В МОДЕЛИ ДОПУСТИМЫХ ВЗАИМОДЕЙСТВИЙ

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

Обозначим через f конечную последовательность функций, а через F в общем случае счетное множество конечных последовательностей f. Каждая последовательность функций f, начинающаяся с момента времени t = 0 (например, включения питания), задается по крайней мере одним входным взаимодействием ${{\mu }^{f}} \in M.$ Этот факт следует из того, что M содержит все допустимые входные взаимодействия для любой допустимой последовательности функций цифровой системы.

В большинстве случаев одни и те же функции могут выполняться цифровой системой с различными наборами данных, что обуславливает задание различными μ одной и той же последовательности функций f. В связи с тем, что для различных экземпляров цифровой системы задержки выходных событий управления обменом относительно входных событий различаются в определенных пределах, а также в связи с допустимостью варьирования моментов времени входных событий относительно друг друга и относительно выходных событий управления обменом, множество Μ содержит континуальное подмножество ${{M}^{f}} \subset M$ входных взаимодействиий, каждое из которых вызывает выполнение цифровой системой конечной последовательности функций f. Множество входных взаимодействий может быть представлено в виде

Входное взаимодействие μ ∈ ${{M}^{f}}$ содержит конечное множество событий

где n – количество событий в μ.

Множество ${{M}^{f}}$ содержит также входные взаимодействия, времена событий в которых (событий множества (8)) различаются в определенных пределах. Ограничения на эти различия могут быть заданы в виде:

где $t_{{{\text{min}}}}^{{l,m}},$ – минимально и максимально допустимые промежутки времени между l-м и m-м событиями;

C – конечное множество пар событий множества (8), для которых заданы временные ограничения.

Входное взаимодействие μ множества ${{M}^{f}}$ кроме событий (8) может содержать на определенных интервалах времени безразличные события, не влияющие на функционирование цифровой системы. Пригодный для практики метод задания всего класса ${{M}^{f}}$ должен быть рассмотрен отдельно, а сейчас отметим, что в множестве ограничений (9) фигурируют времена существенных событий, то есть событий множества (8).

Выделим в C все пары (l, m), для которых t_m есть время выходного события управления обменом, в множество C_out, а все пары (l, m), для которых t_m есть время входного события, в множество C_in. Тогда ограничения на моменты времени выходных событий обмена есть

а ограничения на моменты времени входных событий

Рассмотрим пространство G = = $\prod\nolimits_{{{C}_{{{\text{out}}}}}} {\left\{ {\left. {{{t}_{m}} - {{t}_{l}}} \right|{{t}_{m}} - {{t}_{l}} \geqslant 0} \right\}} .$ Каждая точка g ∈ G определяет конкретные значения задержек выходных событий управления обменом. В пространстве G выделим область G_f ∈ G, для всех точек которой выполняются ограничения (10). Область G_f определяет задержки выходных событий управления обменом, допустимые по техническому заданию. Если техническое задание непротиворечиво, а мы рассматриваем именно такой случай, то G_f ≠ ∅.

Для любой точки g ∈ G_f в связи с допустимостью таких задержек выходных событий управления обменом существует непустое множество входных взаимодействий $M_{g}^{f},$ обеспечивающих выполнение системой последовательности функций f.

где $M_{g}^{f}$ – множество входных взаимодействий, обеспечивающих выполнение цифровой системой конечной последовательности функций f при фиксированных задержках выходных событий управления обменом, определяемых g ∈ G_f.

Таким образом, множество допустимых входных взаимодействий представимо в виде

Структура множества входных взаимодействий (12) вместе с представлением множества взаимодействий (6) позволяют сформулировать задачу отладки цифровых систем на этапе проектирования в терминах теории динамических систем.

ЗАДАЧА ОТЛАДКИ В ТЕРМИНАХ ТЕОРИИ ДИНАМИЧЕСКИХ СИСТЕМ

Пусть техническим заданием определено требуемое поведение цифровой системы в виде (T,P,{Z_p|p ∈ P},Μ,{Γ_μ|μ ∈ Μ}), то есть для каждого допустимого входного взаимодействия μ определено непустое множество возможных выходных воздействий Γ_μ. Задано также множество конечных последовательностей выполняемых цифровой системой функций F, причем $M = \bigcup\nolimits_{f \in {\mathbf{F}}} {{{M}^{f}}} ;$ ${{M}^{{f{\kern 1pt} {\text{'}}}}} \cap {{M}^{{f{\kern 1pt} '{\text{'}}}}} = \emptyset $ при f  ' ≠ f  ". Кроме того, для любого f

В свою очередь спроектированная цифровая система задается в виде принципиальной схемы Sc технических средств и текста программно или микропрограммного обеспечения Sf, то есть в виде пары (Sc, Sf).

Схема технических средств

где Bl – конечный комплект цифровых блоков; Nt – конечное множество узлов принципиальной схемы; Р – множество переменных в терминальных узлах (шинах и линиях) схемы, P $ \in $ У; Zp – конечное множество значений переменной р. Причем Zp = ${\mathbf{Z}}_{p}^{*} \times {\text{DI}}{{{\text{R}}}_{p}},$ где ${\mathbf{Z}}_{p}^{*}$ – множество логических значений, ${\text{DI}}{{{\text{R}}}_{p}}$ – множество направлений передачи сигнала. Для входных шин и линий ${\text{DI}}{{{\text{R}}}_{p}}$ = {1}, для выходных ${\text{DI}}{{{\text{R}}}_{p}}$ = {0}, для двунаправленных ${\text{DI}}{{{\text{R}}}_{p}}$ = {0.1}; $\xi $ – отображение множества выводов цифровых блоков в множество узлов.

В (13) для всех переменных p, описывающих шины из нескольких линий, под узлом у понимается соединение нескольких шин с одинаковым количеством линий, что физически соответствует количеству узлов, равному количеству линий в шинах.

Программное или микропрограммное обеспечение

где Mc – конечное множество ячеек памяти, хранящих программу или микропрограмму; ${{z}_{c}}$ – состояние ячейки памяти c.

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

Спроектированную цифровую систему в целом можно представить как

Спроектированная цифровая система (Sc, Sf), представленная в виде (14), определяет некоторое семейство M стационарных динамических систем, которое может быть задано своим внешним поведением в виде (6), (7). Будем обозначать множество входных взаимодействий и выходных воздействий семейства динамических систем M как Μ_M и Γ_M соответственно, а множество возможных выходных воздействий для заданного входного взаимодействия μ как ${{\Gamma }_{{\mu {\text{M}}}}}.$ При сравнении внешнего поведения спроектированной цифровой системы с требуемым по техническому заданию будем считать, что в обоих случаях используются одинаковые T, P,{Z_p|p ∈ P}.

Цифровая система может быть спроектирована таким образом (хотя это является ошибкой), что при каких-то допустимых сочетаниях задержек блоков, в какие-то интервалы времени на одном или нескольких выходах логические сигналы будут не определены. Дополним множество значений переменных множеств P'' и P''' значением u (неопределенный сигнал) следующим образом:

Тогда и в случае отсутствия в какие-то интервалы времени определенных логических сигналов на выходах цифровой системы выходные воздействия представимы в виде (3), если вместо {Z_p|p ∈ P} использовать {$\widetilde {{\mathbf{Z}}p}$|p ∈ P}. Множество возможных выходных воздействий при известном μ, рассматриваемых в алфавитах $\widetilde {{\mathbf{Z}}p}$ будем обозначать $\widetilde {{{\Gamma }_{{\mu {\text{M}}}}}}.{\;}$ При этом для каждого μ ∈ Μ_M существует непустое множество $\widetilde {{{\Gamma }_{{\mu {\text{M}}}}}},$ состоящее из выходных воздействий, соответствующих различным сочетаниям задержек блоков цифровой системы. Выходные воздействия управления обменом по-прежнему будут рассматриваться в алфавитах Z_p. В случае, если в какой-то последовательности событий логическое значение выходной переменной управления обменом p ∈ P^о не определено, будем считать, что такая последовательность входным взаимодействием не является.

Пусть пара (Sc, Sf) определяет

а также F_M, такое, что

Обозначим через τ вектор задержек множества блоков, входящих в схему технических средств цифровой системы, а через $\Im $ множество векторов возможных задержек блоков системы. Каждому τ ∈ $\Im $ соответствуют свои задержки выходных событий управления обменом. Следовательно, существует отображение a_f: $\Im $ → G. Если при каких-либо значениях задержек, то есть при каком-либо τ ∈ $\Im $, логическое значение выходной переменной, участвующей во входном взаимодействии, не определено, то a_f(τ) не существует. Таким образом, отображение a_f в общем случае является частичным.

Для того, чтобы при любых возможных сочетаниях задержек блоков выполнялись ограничения (12), необходимо, чтобы при

Для каждого τ ∈ $\Im $ существует свое множество допустимых входных взаимодействий

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

Кроме того, при правильном проектировании цифровой системы $\widetilde {{{\Gamma }_{{\mu {\text{M}}}}}} \subset {{\Gamma }_{\mu }}$ для всех μ ∈ Μ ∩ Μ_M, где Μ ∩ Μ_M = $\bigcup\nolimits_{f \in {\mathbf{F}}} {\bigcup\nolimits_{{\text{t}} \in {\text{T}}} {M_{{{\text{a}}f\left( {\text{t}} \right)}}^{f}} } .$ Выполнение этого соотношения в качестве необходимого условия требует, чтобы выходные воздействия γ, где γ ∈ $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}},$ не содержали значения u (не определено) какой-либо переменной.

Задача отладки проекта цифровой системы может быть сформулирована следующим образом.

Доказать, что

В случае, если это неверно, внести в (Sc, Sf) такие исправления, чтобы соотношения (15)–(17) выполнялись.

ПОДЗАДАЧИ ОТЛАДКИ ЦИФРОВЫХ СИСТЕМ

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

1) проверить включение F_M ⊇ F;

2) выбрать такое конечное множество подмножеств входных взаимодействий ${{{\mathbf{M}}}^{{{{f}_{j}}}}},\,\,j = 1,...,n,$ что:

а) из того, что при t ∈ $\Im $ ${{а }_{{{{f}_{j}}}}}$(t) ∈ ${{{\mathbf{G}}}_{{{{f}_{j}}}}},$ ${\mathbf{M}}_{{t{\text{M}}}}^{{{{f}_{j}}}}$ ⊇ ${\mathbf{M}}_{{{\text{a}}f\left( {\text{t}} \right)}}^{{{{f}_{j}}}}$ для всех j следует, что при t ∈ $\Im $ a_f(t) ∈ G_f и ${\mathbf{M}}_{{t{\text{M}}}}^{f}$ ⊇ ⊇ ${\mathbf{M}}_{{{\text{a}}f\left( {\text{t}} \right)}}^{f}$ для всех f ∈ F;

б) из того, что $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}} \subset {{{\mathbf{\Gamma }}}_{\mu }}$ для μ ∈ $\bigcup\nolimits_{{\text{t}} \in \Im } {{\mathbf{M}}_{{{\text{a}}{{f}_{j}}({\text{t}})}}^{{{{f}_{j}}}}} $ и всех j, следует, что $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}} \subset {{{\mathbf{\Gamma }}}_{\mu }}$ для всех μ ∈ ∈ $\bigcup\nolimits_{f \in {\mathbf{F}}} {\bigcup\nolimits_{{\text{t}} \in \Im } {{\mathbf{M}}_{{{\text{a}}{{f}_{j}}({\text{t}})}}^{{{{f}_{j}}}}} } ;$

3) проверить соотношения ${{а }_{{{{f}_{j}}}}}$(t) ∈ ${{{\mathbf{G}}}_{{{{f}_{j}}}}}$ и ${\mathbf{M}}_{{t{\text{M}}}}^{{{{f}_{j}}}}$ ⊇ ⊇ ${\mathbf{M}}_{{{\text{a}}{{f}_{j}}\left( {\text{t}} \right)}}^{{{{f}_{j}}}}$ при τ ∈ $\Im $ и j = 1,…, n;

4) проверить соотношения $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}} \subset {{{\mathbf{\Gamma }}}_{\mu }}$ при μ ∈ ∈ $\bigcup\nolimits_{{\text{t}} \in \Im } {{\text{M}}_{{{\text{a}}{{f}_{j}}\left( {\text{t}} \right)}}^{{{{f}_{j}}}}} $ для j = 1,…, n;

5) при невыполнении условий, проверяемых в пп. 1, 3, 4 иметь возможность локализовать ошибки в (Sc, Sf) и исправить их, а затем повторить указанные действия.

Подзадача 2 решается путем представления технического задания в виде формальной спецификации, по которой осуществляется выбор конечного числа ${{{\mathbf{{\rm M}}}}^{{{{f}_{j}}}}},\,\,j = 1, \ldots ,\,\,n,$ исходя из требуемого внешнего поведения цифровой системы.

Практическое решение подзадачи 1 основывается на проверке внутренних состояния цифровой системы, в которые последняя приходит после выполнения различных функций. При отладке эта подзадача решается во время моделирования цифровой системы на выбранном уровне.

Решения подзадачи 3 заключается в проверке появления выходных сигналов управления обменом и соблюдения ограничений на моменты переключений сигналов вида (9) во входных взаимодействиях при всех возможных сочетаниях задержек. Такая проверка должна проводиться для всех подмножеств входных взаимодействий ${{{\mathbf{{\rm M}}}}^{{{{f}_{k}}}}},{\;}k = 1, \ldots ,{\;}n.$

Подзадача 3 представляет собой задачу верификации временных диаграмм работы цифровой системы и осуществляется путем моделирования схемы с учетом разброса задержек блоков [4].

Для решения подзадачи 4 осуществляется проверка включений $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}} \subset {{{\mathbf{\Gamma }}}_{\mu }}$ для μ ∈ $\bigcup\nolimits_{{\text{t}} \in \Im } {{\text{M}}_{{{\text{a}}{{f}_{j}}\left( {\text{t}} \right)}}^{{{{f}_{j}}}}} $ и конечного множества j осуществляется путем подачи на вход объекта отладки отладочных тестов и анализа получаемых реакций.

Наиболее полным решением подзадачи 4 является путь формального доказательства. При этом в наиболее общем случае необходимо осуществить символическое вычисление $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}}$ одновременно для всех μ ∈ $\bigcup\nolimits_{{\text{t}} \in \Im } {{\text{M}}_{{{\text{a}}f\left( {\text{t}} \right)}}^{f}} ,$ а полученное $\widetilde {{{{\mathbf{\Gamma }}}_{{\mu {\text{M}}}}}}$ сравнить с ${{{\mathbf{\Gamma }}}_{\mu }},$ заданным формальной спецификацией также символически. Отладочным тестом в этом случае являлось бы все множество $\bigcup\nolimits_{{\text{t}} \in \Im } {{\text{M}}_{{{\text{a}}f\left( {\text{t}} \right)}}^{f}} = {\mathbf{M}}_{{\text{M}}}^{f} \cap {{{\mathbf{M}}}^{f}}.$ При таком подходе, назовем его полным символическим тестированием, необходимо проводить одновременное символическое вычисление как моментов времени выходных событий с учетом диапазонов задержек блоков, так и логических значений сигналов. Теоретически это возможно путем символического моделирования логики работы цифровой системы с нарастающей неопределенностью моментов времени событий.

ЗАКЛЮЧЕНИЕ

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

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