The post has been translated automatically. Original language: Russian
In the previous article, we got to the lowest level of the software chain.:
program
, the compiler
, operating system
↓
processorEven if the properties of the program, compiler, and operating system are proven, one last question remains.:
does the processor itself execute machine instructions correctly?
At first glance, it seems that the hardware can no longer be "proven" in the same way as the program.
But a digital processor is also a system of states and rules for the transition between them.
This means that a significant part of his behavior can be described formally.
First you need to determine what the processor should do.
The processor executes a set of machine instructions.
For example:
ADD
LOAD
STORE
JUMP
COMPAREFor each instruction, the expected behavior can be accurately described.
Simplified:
ADD R1, R2
before:
R1 = A
R2 = B
after:
R1 = A + BThis is already a formal specification of the instruction's behavior.
The same can be done for:
- registers;
- Memory;
- transitions;
- exceptions;
- interruptions;
- access rights;
- special processor states.
The entire architecture of commands can be considered as a set of rules.:
current status
+
manual
, next state
And inside the processor, everything is much more complicated.
A real processor rarely executes an instruction in just one action.
Inside there may be:
- instruction decoder;
- register file;
- arithmetic blocks;
- conveyor belt;
- cache;
- memory management unit;
- queues;
- exception handling;
- mechanisms of stopping and waking up.
For example, one instruction can go through several stages:
FETCH
↓
DECODE
↓
EXECUTE
↓
MEMORY
↓
WRITEBACKThe internal implementation can be complicated.
But externally, the result must still comply with the architectural specification.
This is what can be formally verified.
What does it mean to "verify the processor"?
The simplified task looks like this:
processor specification
↓
compare
, processor implementationIt is necessary to prove:
for all valid states and instructions, the implementation switches to a state conforming to the specification.
For example, if an instruction needs to increment a register by one:
R1 = 10
INC R1then after its execution it should work out:
R1 = 11Moreover, it is necessary to check not one example with the number 10, but all valid register values and all related processor states.
You can check more than just individual instructions.
Formal verification of the equipment allows you to set much more interesting properties.
For example:
The processor never writes
to a protected memory area
without the appropriate permission.or:
if the instruction has completed normally,
the result must be written
to the correct register.or:
after a reset, the processor always
switches to a certain state.You can check:
- correct decoding of instructions;
- operation of registers;
- memory accesses;
- privilege management;
- exceptions;
- interruptions;
- mutual blockages;
- forbidden states;
- compliance with protocols between blocks.
In other words, a processor can be viewed almost in the same way as a complex program.
Only instead of the program code, the digital logic is checked.
Where is the processor implementation located?
Prior to the manufacture of the chip, the processor exists as a digital description.
The simplified chain looks like this:
team architecture
↓
RTL
↓
logical elements
↓
Physical crystalRTL describes how registers and logic circuits change their state on each clock cycle.
At this level, the processor is still a mathematically described system.
Therefore, it is especially convenient to apply formal methods here.
You can check:
RTL
↓
does it match
↓
the formal specificationBut there is a problem of the number of states
Even a small processor has a huge state space.
If the processor contains:
32 registers × 64 bitsregisters alone already produce an astronomical number of combinations.
And there are also:
- memory;
- internal queues;
- cache;
- pipeline status;
- devices;
- interruptions.
It is impossible to sort through all the states directly.
Therefore, formal verification is not an ordinary complete search.
Mathematical methods are used that make it possible to reason about multiple states at once.
But the complexity still matters.
The more complex the processor, the more difficult the proof.
Does this mean that a simple processor is better?
Not necessarily in every way.
Complex architecture can give:
- greater productivity;
- deep conveyor;
- predicting transitions;
- parallel execution;
- complex caches.
But each new mechanism increases the number of internal states and interactions.
Therefore, an engineering compromise arises.:
maximum difficulty
↕
maximum verifiabilityIf the main goal of the system is not record performance, but the ability to strictly prove its properties, the processor architecture may be designed differently.
In other words, verifiability becomes an independent architectural requirement.
Is a proven processor already the end of the chain?
Not yet.
Suppose we have proved that the processor's RTL conforms to a formal specification.
Then RTL turns into logical elements.
The project is then placed on a chip.
After that, the physical device appears.
It turns out:
formal specification
↓
RTL
, logical scheme
↓
transistors
, physical processorAnd here there is a very important boundary.
Formally proven digital logic does not mean that a particular physical processor will never make a mistake.
It can be influenced by:
- manufacturing defects;
- Supply voltage;
- temperature;
- electromagnetic interference;
- aging;
- radiation;
- physical wear and tear.
Therefore, it is necessary to distinguish:
correctness of the design
and
the infallibility of a specific physical instance
The first can be proved mathematically to a large extent.
The second already applies to physics, production technology and reliability.
How far can you go then?
We already have an almost complete chain.:
program
, the compiler
, operating system
↓
command architecture
↓
processor
↓
digital logicFor each level, you can formulate properties and reduce the number of components that you simply have to trust.
It turns out to be a very interesting goal.:
not to prove the abstract "ideality of the computer", but to make the largest possible part of the computing system formally verifiable.
And then there's the last question of the series.:
is it possible to put all these levels together and build a fully verified computer?
В предыдущей статье мы дошли до самого нижнего уровня программной цепочки:
программа
↓
компилятор
↓
операционная система
↓
процессорДаже если свойства программы, компилятора и операционной системы доказаны, остаётся последний вопрос:
а правильно ли сам процессор выполняет машинные инструкции?
На первый взгляд кажется, что железо уже нельзя «доказать» так же, как программу.
Но цифровой процессор тоже является системой состояний и правил перехода между ними.
А значит, значительную часть его поведения можно описать формально.
Сначала нужно определить, что должен делать процессор
Процессор выполняет набор машинных инструкций.
Например:
ADD
LOAD
STORE
JUMP
COMPAREДля каждой инструкции можно точно описать ожидаемое поведение.
Упрощённо:
ADD R1, R2
до:
R1 = A
R2 = B
после:
R1 = A + BЭто уже формальная спецификация поведения инструкции.
То же самое можно сделать для:
- регистров;
- памяти;
- переходов;
- исключений;
- прерываний;
- прав доступа;
- специальных состояний процессора.
Вся архитектура команд может рассматриваться как набор правил:
текущее состояние
+
инструкция
↓
следующее состояниеА внутри процессора всё гораздо сложнее
Реальный процессор редко выполняет инструкцию буквально одним действием.
Внутри могут находиться:
- декодер инструкций;
- регистровый файл;
- арифметические блоки;
- конвейер;
- кэш;
- блок управления памятью;
- очереди;
- обработка исключений;
- механизмы остановки и пробуждения.
Например, одна инструкция может проходить несколько стадий:
FETCH
↓
DECODE
↓
EXECUTE
↓
MEMORY
↓
WRITEBACKВнутренняя реализация может быть сложной.
Но внешне результат всё равно должен соответствовать архитектурной спецификации.
Именно это можно проверять формально.
Что значит «верифицировать процессор»
Упрощённо задача выглядит так:
спецификация процессора
↓
сравнение
↑
реализация процессораНеобходимо доказать:
для всех допустимых состояний и инструкций реализация переходит в состояние, соответствующее спецификации.
Например, если инструкция должна увеличить регистр на единицу:
R1 = 10
INC R1то после её выполнения должно получиться:
R1 = 11Причём необходимо проверить не один пример с числом 10, а все допустимые значения регистра и все связанные состояния процессора.
Можно проверять не только отдельные инструкции
Формальная верификация аппаратуры позволяет задавать гораздо более интересные свойства.
Например:
процессор никогда не записывает
в защищённую область памяти
без соответствующего разрешенияили:
если инструкция завершилась нормально,
результат обязательно записан
в правильный регистрили:
после сброса процессор всегда
переходит в определённое состояниеМожно проверять:
- корректность декодирования инструкций;
- работу регистров;
- обращения к памяти;
- управление привилегиями;
- исключения;
- прерывания;
- взаимные блокировки;
- запрещённые состояния;
- соблюдение протоколов между блоками.
То есть процессор можно рассматривать почти так же, как сложную программу.
Только вместо программного кода проверяется цифровая логика.
Где находится реализация процессора
До изготовления микросхемы процессор существует как цифровое описание.
Упрощённая цепочка выглядит так:
архитектура команд
↓
RTL
↓
логические элементы
↓
физический кристаллRTL описывает, как регистры и логические схемы изменяют своё состояние на каждом такте.
На этом уровне процессор ещё является математически описываемой системой.
Поэтому именно здесь особенно удобно применять формальные методы.
Можно проверять:
RTL
↓
соответствует ли он
↓
формальной спецификацииНо есть проблема количества состояний
Даже небольшой процессор имеет огромное пространство состояний.
Если процессор содержит:
32 регистра × 64 битатолько регистры уже дают астрономическое число комбинаций.
А ещё существуют:
- память;
- внутренние очереди;
- кэш;
- состояние конвейера;
- устройства;
- прерывания.
Перебрать все состояния напрямую невозможно.
Поэтому формальная верификация не является обычным полным перебором.
Используются математические методы, позволяющие рассуждать сразу о множестве состояний.
Но сложность всё равно имеет значение.
Чем сложнее процессор, тем труднее доказательство.
Значит ли это, что простой процессор лучше?
Не обязательно во всех отношениях.
Сложная архитектура может дать:
- большую производительность;
- глубокий конвейер;
- предсказание переходов;
- параллельное исполнение;
- сложные кэши.
Но каждый новый механизм увеличивает количество внутренних состояний и взаимодействий.
Поэтому возникает инженерный компромисс:
максимальная сложность
↕
максимальная верифицируемостьЕсли основной целью системы является не рекордная производительность, а возможность строго доказать её свойства, архитектура процессора может проектироваться иначе.
То есть верифицируемость становится самостоятельным архитектурным требованием.
Доказанный процессор — это уже конец цепочки?
Пока нет.
Предположим, мы доказали, что RTL процессора соответствует формальной спецификации.
Дальше RTL превращается в логические элементы.
Затем проект размещается на кристалле.
После этого появляется физическое устройство.
Получается:
формальная спецификация
↓
RTL
↓
логическая схема
↓
транзисторы
↓
физический процессорИ здесь возникает очень важная граница.
Формально доказанная цифровая логика ещё не означает, что конкретный физический процессор никогда не ошибётся.
На него могут влиять:
- производственные дефекты;
- напряжение питания;
- температура;
- электромагнитные помехи;
- старение;
- радиация;
- физический износ.
Поэтому нужно различать:
правильность конструкции
и
безошибочность конкретного физического экземпляра
Первое можно в значительной степени доказывать математически.
Второе относится уже и к физике, технологии производства и надёжности.
Насколько далеко тогда можно зайти?
У нас уже появляется почти полная цепочка:
программа
↓
компилятор
↓
операционная система
↓
архитектура команд
↓
процессор
↓
цифровая логикаДля каждого уровня можно формулировать свойства и уменьшать количество компонентов, которым приходится просто доверять.
Получается очень интересная цель:
не доказать абстрактную «идеальность компьютера», а сделать максимально большую часть вычислительной системы формально проверяемой.
И тогда остаётся последний вопрос серии:
можно ли собрать все эти уровни вместе и построить полностью верифицированный компьютер?
Share
