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: |

On Telegram’s website, it says that Pavel Durov “supports Telegram financially and ideologically while Nikolai (Duvov)’s input is technological.” Currently, the Telegram team is based in Dubai, having moved around from Berlin, London and Singapore after departing Russia. Meanwhile, the company which owns Telegram is registered in the British Virgin Islands. "We as Ukrainians believe that the truth is on our side, whether it's truth that you're proclaiming about the war and everything else, why would you want to hide it?," he said. That hurt tech stocks. For the past few weeks, the 10-year yield has traded between 1.72% and 2%, as traders moved into the bond for safety when Russia headlines were ugly—and out of it when headlines improved. Now, the yield is touching its pandemic-era high. If the yield breaks above that level, that could signal that it’s on a sustainable path higher. Higher long-dated bond yields make future profits less valuable—and many tech companies are valued on the basis of profits forecast for many years in the future. The Russian invasion of Ukraine has been a driving force in markets for the past few weeks. At this point, however, Durov had already been working on Telegram with his brother, and further planned a mobile-first social network with an explicit focus on anti-censorship. Later in April, he told TechCrunch that he had left Russia and had “no plans to go back,” saying that the nation was currently “incompatible with internet business at the moment.” He added later that he was looking for a country that matched his libertarian ideals to base his next startup.
from hk


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