The post has been translated automatically. Original language: Russian
When a new software or hardware verification tool appears, the question quickly arises: which languages should it work with? At first glance, the answer seems obvious — the more languages are supported, the better.
In practice, everything is more complicated. Each new language requires separate source code processing, support for its features, and constant compatibility checks. Therefore, for SJV, what is more important now is not the number of supported languages, but an understanding of where such a verification method is really needed.
Why did we start with SystemVerilog?
One of the areas where we use SJV is the development of the Memora8 processor. The hardware of such a project is naturally related to hardware description languages, so SystemVerilog became the first obvious candidate.
SystemVerilog is widely used to describe digital circuits and allows you to create quite complex modules: processors, memory controllers, interfaces, and other components. In such systems, there are many states and transitions between them, which means that there are enough tasks where ordinary tests may not be enough.
SJV does not replace SystemVerilog. The source module still describes how the device works, and SJV sets the properties that need to be checked.
For example, the memory module defines the logic of reading, writing, and access control. In SJV, you can write a separate rule that two processors should not simultaneously own the same memory area.
This approach allows you not to confuse the implementation of the device with the requirements for its behavior.
Do I need a regular Verilog?
Verilog appeared before SystemVerilog and is still used in many projects. Therefore, the natural question arises: is it necessary to add its support separately right away?
Technically, it looks reasonable. There is a large amount of existing code on Verilog, especially in long-running projects, educational developments, and small hardware modules.
But here it is important to distinguish the technical possibility from the actual need. If SJV users work primarily with SystemVerilog, separate Verilog support may not provide noticeable benefits at an early stage.
In addition, modern development tools often allow you to work with Verilog and SystemVerilog in the same project. Therefore, it makes sense to check first whether the lack of separate Verilog support really prevents SJV from being used in real-world tasks.
If such a request appears, adding appropriate source code processing would be the logical next step.
Why not add C, C++, and Rust at once?
After supporting the hardware description language, it's easy to continue the reasoning: if SJV describes states and transitions, why not use it for regular programs?
Theoretically, such a possibility exists. Requirements like "after calling a function, this value should not change" or "a resource cannot belong to two threads at the same time" are found not only in hardware.
But each language has its own memory model, rules for working with pointers, threads, exceptions, and external libraries. To test such a program correctly, it is not enough just to learn how to read its syntax.
It is necessary to determine exactly what each operation means from the point of view of the SJV model. The more complex the language, the more such rules will be required.
As a result, trying to support multiple languages at once may lead to the fact that most of the development will be spent on creating source code converters, rather than on the verification system itself.
SJV should not depend on a single language.
At the same time, one of the main ideas of SJV is precisely not to bind the description of the properties being checked to a specific implementation language.
Let's take a simple rule: "after the reset, the device should return to its initial state." It doesn't become different just because the device is written in SystemVerilog today, and tomorrow it will be implemented differently.
The same applies to many other properties. The system has states, valid transitions, and constraints that exist regardless of the syntax of the source code.
Therefore, SJV can be considered as a separate level of requirements description. And already a special part of the system must link these requirements to a specific implementation.
This theoretically allows you to add new languages without changing the way you write the properties being checked.
But versatility has a price.
Creating a tool that supports ten languages sounds more appealing than a tool for one language. However, for the user, the value is not determined by the number of items in the list of possibilities.
If SJV checks complex modules well on SystemVerilog and helps to find real errors, this is already a useful result. If it formally supports many languages, but only works with a small set of constructs for each one, such versatility may turn out to be rather a disadvantage.
Therefore, we consider the support of new languages as a consequence of real tasks, and not as an end in itself.
First, you need to find an area where the approach works particularly well. Then you can see if the same task occurs in other languages and projects.
What needs to be tested in practice
There are several open questions for us right now. How often do hardware developers need to check properties separately from the source code? Is SystemVerilog enough to get started? Are there any noticeable number of projects where separate Verilog support is required?
The question of programming languages is no less interesting. SJV may be useful not only for hardware, but also for system programming, where there are many explicit states, memory management, and strict restrictions.
However, the answer to this should not be a list of potential opportunities, but real projects.
Therefore, we are now trying to move away from specific tasks. If a system appears in a new language and the same verification method is really useful for it, this is a good argument in favor of a new support module.
It's better to have one language well than ten formally.
It's easy to fall into the trap of versatility early on. The developer wants to provide all possible options in advance, because architecturally they look logical.
But the new tool must first prove its usefulness in one understandable scenario. Only then does it become clear which capabilities are really needed, and which existed only in our assumptions.
Therefore, the immediate task of SJV is not to support as many languages as possible. It is more important to ensure that checking real projects on SystemVerilog is understandable, reproducible and really helps to find errors.
If this works out, adding other languages will no longer be an assumption about the future, but a response to a specific need.
Когда появляется новый инструмент проверки программ или аппаратуры, быстро возникает вопрос: с какими языками он должен работать? На первый взгляд ответ кажется очевидным — чем больше языков поддерживается, тем лучше.
На практике всё сложнее. Каждый новый язык требует отдельной обработки исходного кода, поддержки его особенностей и постоянной проверки совместимости. Поэтому для SJV сейчас важнее не количество поддерживаемых языков, а понимание того, где такой способ проверки действительно нужен.
Почему мы начали с SystemVerilog
Одно из направлений, где мы применяем SJV, — разработка процессора Memora8. Аппаратная часть такого проекта естественным образом связана с языками описания аппаратуры, поэтому первым очевидным кандидатом стал SystemVerilog.
SystemVerilog широко используется для описания цифровых схем и позволяет создавать достаточно сложные модули: процессоры, контроллеры памяти, интерфейсы и другие компоненты. В таких системах много состояний и переходов между ними, а значит, появляется достаточно задач, где обычных тестов может быть недостаточно.
SJV при этом не заменяет SystemVerilog. Исходный модуль по-прежнему описывает, как работает устройство, а SJV задаёт свойства, которые требуется проверить.
Например, модуль памяти определяет логику чтения, записи и управления доступом. В SJV можно отдельно записать правило, что два процессора не должны одновременно владеть одной и той же областью памяти.
Такой подход позволяет не смешивать реализацию устройства с требованиями к его поведению.
А нужен ли обычный Verilog
Verilog появился раньше SystemVerilog и до сих пор используется во множестве проектов. Поэтому возникает естественный вопрос: нужно ли сразу добавлять его поддержку отдельно?
Технически это выглядит разумно. Существует большое количество существующего кода на Verilog, особенно в давно развивающихся проектах, учебных разработках и небольших аппаратных модулях.
Но здесь важно отличать техническую возможность от реальной необходимости. Если пользователи SJV работают в основном с SystemVerilog, отдельная поддержка Verilog может не дать заметной пользы на раннем этапе.
Кроме того, современные средства разработки часто позволяют работать с Verilog и SystemVerilog в одном проекте. Поэтому сначала имеет смысл проверить, действительно ли отсутствие отдельной поддержки Verilog мешает использовать SJV в реальных задачах.
Если такой запрос появится, добавить соответствующую обработку исходного кода будет логичным следующим шагом.
Почему не добавить сразу C, C++ и Rust
После поддержки языка описания аппаратуры легко продолжить рассуждение: если SJV описывает состояния и переходы, почему бы не использовать его и для обычных программ?
Теоретически такая возможность существует. Требования вроде «после вызова функции это значение не должно измениться» или «ресурс не может одновременно принадлежать двум потокам» встречаются не только в аппаратуре.
Но у каждого языка есть собственная модель памяти, правила работы с указателями, потоками, исключениями и внешними библиотеками. Чтобы корректно проверять такую программу, недостаточно просто научиться читать её синтаксис.
Нужно точно определить, что означает каждая операция с точки зрения модели SJV. Чем сложнее язык, тем больше таких правил потребуется.
В результате попытка сразу поддержать несколько языков может привести к тому, что большая часть разработки уйдёт на создание преобразователей исходного кода, а не на саму систему проверки.
SJV не должен зависеть от одного языка
При этом одна из основных идей SJV состоит именно в том, чтобы не привязывать описание проверяемых свойств к конкретному языку реализации.
Возьмём простое правило: «после сброса устройство должно перейти в начальное состояние». Оно не становится другим только потому, что устройство сегодня написано на SystemVerilog, а завтра будет реализовано иначе.
То же относится и ко многим другим свойствам. У системы есть состояния, допустимые переходы и ограничения, которые существуют независимо от синтаксиса исходного кода.
Поэтому SJV можно рассматривать как отдельный уровень описания требований. А уже специальная часть системы должна связывать эти требования с конкретной реализацией.
Это позволяет теоретически добавлять новые языки без изменения самого способа записи проверяемых свойств.
Но универсальность имеет цену
Создать инструмент, который поддерживает десять языков, звучит привлекательнее, чем инструмент для одного языка. Однако для пользователя ценность определяется не количеством пунктов в списке возможностей.
Если SJV хорошо проверяет сложные модули на SystemVerilog и помогает находить реальные ошибки, это уже полезный результат. Если же он формально поддерживает множество языков, но для каждого работает только с небольшим набором конструкций, такая универсальность может оказаться скорее недостатком.
Поэтому мы рассматриваем поддержку новых языков как следствие реальных задач, а не как самоцель.
Сначала нужно найти область, где подход работает особенно хорошо. Затем можно смотреть, встречается ли та же задача в других языках и проектах.
Что нужно проверить на практике
Для нас сейчас есть несколько открытых вопросов. Насколько часто разработчикам аппаратуры требуется проверять свойства отдельно от исходного кода? Достаточно ли для начала SystemVerilog? Есть ли заметное количество проектов, где обязательна отдельная поддержка Verilog?
Не менее интересен вопрос о программных языках. Возможно, SJV окажется полезен не только для аппаратуры, но и для системного программирования, где много явных состояний, работы с памятью и строгих ограничений.
Однако ответ на это должен дать не список потенциальных возможностей, а реальные проекты.
Поэтому сейчас мы стараемся двигаться от конкретных задач. Если появляется система на новом языке и для неё действительно полезен тот же способ проверки, это хороший аргумент в пользу нового модуля поддержки.
Лучше один язык хорошо, чем десять формально
На раннем этапе легко попасть в ловушку универсальности. Разработчику хочется заранее предусмотреть все возможные варианты, потому что архитектурно они выглядят логичными.
Но новый инструмент сначала должен доказать свою полезность в одном понятном сценарии. Только после этого становится ясно, какие возможности действительно нужны, а какие существовали только в наших предположениях.
Поэтому ближайшая задача SJV — не поддержать как можно больше языков. Важнее добиться того, чтобы проверка реальных проектов на SystemVerilog была понятной, воспроизводимой и действительно помогала находить ошибки.
Если это получится, добавление других языков станет уже не предположением о будущем, а ответом на конкретную потребность.
Share
