ЭлектроКот - ТехноБлог

В продолжение предыдущего поста. Вспомнил, как называется этот open-source формальный инструмент - Kepler-formal. Еще недавно одним из заметных пробелов open-source EDA был полноценный инструмент для Equivalence Checking (как LEC так и SEQ), а теперь появился и такой инструмент. Почему вообще SEC настолько полезен в реальной разработке? Например, у нас есть уже верифицированный блок, но после timing analysis обнаружилась проблема. Мы вносим RTL-изменения, чтобы исправить критический путь: переписываем часть логики, добавляем или переносим регистры. После этого возникает вопрос, а не сломали ли мы при этом функциональность блока? Конечно, можно снова прогонять весь regression set, но это долго и не всегда дает достаточную уверенность. SEC позволяет формально проверить, что старая и новая реализации сохраняют требуемое функциональное поведение. Особенно интересно, что такие инструменты постепенно появляются и в open source. Коммерческим решениям пока, конечно, есть куда расти в плане возможностей и зрелости, но сам факт появления подобных инструментов - хороший показатель развития open-source EDA. Пост написал, осталось на досуге посмотреть насколько вообще тул работоспособен🥲 Но я уверен кто-то из читателей поделится фидбеком👀

Сегодняшние книги. Для будущей разработки аналогов этих программ.

https://youtu.be/92DLCvAS7Ms

https://youtu.be/iQdY-bcgjEA

Чет я угорел, и решил подкаст друга послушать как в 2005 году 😁😁😁 Зато умею теперь делать сервер подкастов для Тигры / iTunes 7

Председатель FreeCAD Association и один из старейших разработчиков проекта решил «отойти от сопровождения FreeCAD» из-за несогласия с использованием ИИ в проекте. «Я почти 20 лет входил в основную команду, но теперь проект движется в направлении, с которым я не хочу работать», - заявил председатель FreeCAD Йорик ван Хавр. Говоря об ИИ, он отметил: «Я считаю эти инструменты крайне вредными для FOSS-проекта вроде FreeCAD. Серьёзные экологические последствия, проблемы с авторскими правами, этические вопросы и, прежде всего, попытки крупнейших технологических корпораций навязать своё влияние проекту, который создавался как безопасная альтернатива им, – всё это то, от чего, на мой взгляд, мы должны защищать проект». https://forum.freecad.org/viewtopic.php?t=106653 @linuxos_tg

Проект Debian готовится провести голосование по общей резолюции, которая официально запретит использование ИИ и LLM при работе над любыми компонентами Debian Linux. Предложение предусматривает исключение для сторонних апстрим-проектов, не относящихся напрямую…

Проект Debian готовится провести голосование по общей резолюции, которая официально запретит использование ИИ и LLM при работе над любыми компонентами Debian Linux. Предложение предусматривает исключение для сторонних апстрим-проектов, не относящихся напрямую к Debian, которым будет разрешено продолжать использовать LLM. Благодаря этому исключению использование ИИ останется допустимым, например, при разработке ядра Linux, где сейчас около 10% новых патчей написаны с помощью ИИ. https://debian.org/vote/2026/vote_002 @linuxos_tg