Telegram Group & Telegram Channel
Рандомизация в Verilator

Тут оказывается у верилятора сподвижки в рандомизации случились.

Если сжать всю историю до нескольких предложений, то

▫️ Первым заходом в рандомизацию было использование API-вызовов библиотеки CRAVE. Решение как оказалось было не совсем подходящим - слишком громоздкий и универсальный инструмент, который сильно усложняет сборку самого верилятора.
▫️Далее пошел заход через SMT-LIB2 - SV констрейны конвертируются в Lisp-подобное описание, которое идёт в рантайме на вход любому (почти) из популярных SMT-решателей, установленных в системе. Далее остается лишь забрать выхлоп и разложить по переменным.

Именно последний подход начали пиарить в недавних статье и докладе про текущие дела верилятора. Хотя PR на Github находился еще в работе, да и судя по комментариям мистер Снайдер похоже не сильно был воодушевлен таким подходом.

Однако, работу довели до мержа в мастер, и теперь по умолчанию верилятор пытается использовать z3, как бэкэнд для рандомизации.

Рандомизация работает, я проверил. Однако надо убедиться что решатель есть в системе, иначе в рантайме будет сюрприз

%Warning: Subprocess command `z3 --in' failed: exit status 127


Но сама рандомизация пока еще довольно слабая - можно глянуть в оригинальном PR, что ограничений пока довольно много.

#verilator
@positiveslack



group-telegram.com/positiveslack/302
Create:
Last Update:

Рандомизация в Verilator

Тут оказывается у верилятора сподвижки в рандомизации случились.

Если сжать всю историю до нескольких предложений, то

▫️ Первым заходом в рандомизацию было использование API-вызовов библиотеки CRAVE. Решение как оказалось было не совсем подходящим - слишком громоздкий и универсальный инструмент, который сильно усложняет сборку самого верилятора.
▫️Далее пошел заход через SMT-LIB2 - SV констрейны конвертируются в Lisp-подобное описание, которое идёт в рантайме на вход любому (почти) из популярных SMT-решателей, установленных в системе. Далее остается лишь забрать выхлоп и разложить по переменным.

Именно последний подход начали пиарить в недавних статье и докладе про текущие дела верилятора. Хотя PR на Github находился еще в работе, да и судя по комментариям мистер Снайдер похоже не сильно был воодушевлен таким подходом.

Однако, работу довели до мержа в мастер, и теперь по умолчанию верилятор пытается использовать z3, как бэкэнд для рандомизации.

Рандомизация работает, я проверил. Однако надо убедиться что решатель есть в системе, иначе в рантайме будет сюрприз

%Warning: Subprocess command `z3 --in' failed: exit status 127


Но сама рандомизация пока еще довольно слабая - можно глянуть в оригинальном PR, что ограничений пока довольно много.

#verilator
@positiveslack

BY позитивслэк


Warning: Undefined variable $i in /var/www/group-telegram/post.php on line 260

Share with your friend now:
group-telegram.com/positiveslack/302

View MORE
Open in Telegram


Telegram | DID YOU KNOW?

Date: |

"And that set off kind of a battle royale for control of the platform that Durov eventually lost," said Nathalie Maréchal of the Washington advocacy group Ranking Digital Rights. For example, WhatsApp restricted the number of times a user could forward something, and developed automated systems that detect and flag objectionable content. Overall, extreme levels of fear in the market seems to have morphed into something more resembling concern. For example, the Cboe Volatility Index fell from its 2022 peak of 36, which it hit Monday, to around 30 on Friday, a sign of easing tensions. Meanwhile, while the price of WTI crude oil slipped from Sunday’s multiyear high $130 of barrel to $109 a pop. Markets have been expecting heavy restrictions on Russian oil, some of which the U.S. has already imposed, and that would reduce the global supply and bring about even more burdensome inflation. Russians and Ukrainians are both prolific users of Telegram. They rely on the app for channels that act as newsfeeds, group chats (both public and private), and one-to-one communication. Since the Russian invasion of Ukraine, Telegram has remained an important lifeline for both Russians and Ukrainians, as a way of staying aware of the latest news and keeping in touch with loved ones. Telegram does offer end-to-end encrypted communications through Secret Chats, but this is not the default setting. Standard conversations use the MTProto method, enabling server-client encryption but with them stored on the server for ease-of-access. This makes using Telegram across multiple devices simple, but also means that the regular Telegram chats you’re having with folks are not as secure as you may believe.
from us


Telegram позитивслэк
FROM American