На такой квантизации уже сильно падает качество. UD-Q4_K_XL - ещё норм, но если ниже, то очень заметна разница.
И по поводу скорости. 10-20 токенов на генерации терпимо, но низкая скорость на промпте - это прям грустно, особенно когда делается сжатие контекста. А на 80к это часто надо делать.
Всё ж надо пару, а лучше тройку 3090, чтобы cpu разгрузить. И контекст побольше. Но это моё ИМХО, не настаиваю.
Базовый синтез RTL, ограниченную проверку (BMC) с использованием SMT-решателя Z3. Подходит для небольших дизайнов и простых assert/assume.
Yosys+SBY - не только BMC и не только Z3. Там в полной мере поддерживается k-induction prove, и кроме Z3 там ещё десяток солверов, в т.ч. встроенный прямо в Yosys, который используется в EQY - LEC на базе Yosys.
А что касается простых assert/assume, то на них (плюс liveness) можно реализовать всё, что есть в SVA. Только текста больше получится.
Так что опенсорс не так плох как может показаться.
Отсутствие поддержки SVA - это печально, но при желании можно обойтись immediate assertions. Больше писанины, но оно работает, народ использует (в т.ч. и я).
Пока не понятно какую гипотезу необходимо доказать
Вот эту:
Это не так должно работать.
Должно работать в пайплайне из трёх агентов и RAG? Охотно верю, но хочется реальной проверки, а не просто слов. Мне вот чатгпт после разбора статьи предложил вариант пайплайна из 10 пунктов. Но это из разряда "Да, вы совершенно правы...".
Про то, что там в статье за гипотеза - это надо у Юрия спросить. Я там чёт не нашел упоминаний RAG, Каммингса и Харриса (кроме списка литературы).
Но могу из своего опыта привести пример. И использованием современных средств ИИ-разработки - спецификации, планирования, ревью на всех этапах, мультиагентной системы, функциональных тестов и формальных проверок (с помощью Yosys и SBY, кстати) - ИИ не смог написать FWFT FIFO на блочной памяти (с латентностью чтения и некоторыми дополнительными условиями). Точнее смог в конце концов, но с моей помощью.
Архитектурная задача на одном агенте с галлюцинирующей моделью не решается
Решите с несколькими. Тут-то ситуация простая - есть задача и есть неудачные попытки её решения. Если вы уверены, что её решали неправильно, покажите правильное решение (решение, а не рассуждения о том, как правильно).
Настольный ПК из б/у комплектующих совсем не то же самое, что сервер для 24x7 работы в ДЦ
Так про "сервер для 24x7 работы в ДЦ" никто кроме вас не говорил. Локального кодового агента вполне можно запускать на компьютере с двумя БУ видеокартами с Авито, работающего в серверной через дверь (у меня вообще в сарае стоит). И работать, кстати, он будет без проблем 24х7.
Сравните с VexRiscv. По моим тестам у него лучшее отношение производительности к площади.
Для использования 75-омного кабеля можно попробовать поставить терминаторы на 75 Ом (можно просто резистор в разъём воткнуть).
На такой квантизации уже сильно падает качество. UD-Q4_K_XL - ещё норм, но если ниже, то очень заметна разница.
И по поводу скорости. 10-20 токенов на генерации терпимо, но низкая скорость на промпте - это прям грустно, особенно когда делается сжатие контекста. А на 80к это часто надо делать.
Всё ж надо пару, а лучше тройку 3090, чтобы cpu разгрузить. И контекст побольше. Но это моё ИМХО, не настаиваю.
Выложили https://huggingface.co/collections/Qwen/qwen36
Какой сетап?
На днях в режиме планирования:
И создал :)
Yosys+SBY - не только BMC и не только Z3. Там в полной мере поддерживается k-induction prove, и кроме Z3 там ещё десяток солверов, в т.ч. встроенный прямо в Yosys, который используется в EQY - LEC на базе Yosys.
А что касается простых assert/assume, то на них (плюс liveness) можно реализовать всё, что есть в SVA. Только текста больше получится.
Так что опенсорс не так плох как может показаться.
Отсутствие поддержки SVA - это печально, но при желании можно обойтись immediate assertions. Больше писанины, но оно работает, народ использует (в т.ч. и я).
Я ничего не утверждаю. Это вы утверждаете, что решит. Но пока кроме утверждений ничего не видно.
Я пробовал с Клодом, GPT, GLM, Qwen и с некоторыми локальными моделями. Gemini не пробовал.
Вот эту:
Должно работать в пайплайне из трёх агентов и RAG? Охотно верю, но хочется реальной проверки, а не просто слов. Мне вот чатгпт после разбора статьи предложил вариант пайплайна из 10 пунктов. Но это из разряда "Да, вы совершенно правы...".
Про то, что там в статье за гипотеза - это надо у Юрия спросить. Я там чёт не нашел упоминаний RAG, Каммингса и Харриса (кроме списка литературы).
Но могу из своего опыта привести пример. И использованием современных средств ИИ-разработки - спецификации, планирования, ревью на всех этапах, мультиагентной системы, функциональных тестов и формальных проверок (с помощью Yosys и SBY, кстати) - ИИ не смог написать FWFT FIFO на блочной памяти (с латентностью чтения и некоторыми дополнительными условиями). Точнее смог в конце концов, но с моей помощью.
В тексте есть ссылки на статью и на задание. Не понимаю, что ещё нужно.
Решите с несколькими. Тут-то ситуация простая - есть задача и есть неудачные попытки её решения. Если вы уверены, что её решали неправильно, покажите правильное решение (решение, а не рассуждения о том, как правильно).
Покажите как. Решите задачу из статьи с помощью своего пайплайна.
В то время там был Synplify, сейчас только ADS.
PangoMicro недавно добавила экспериментальную поддержку подмножества VHDL-93 в свой синтезатор. Если это "отлично", то ок.
А вы вставляйте "шум" только в участки, где большая громкость.
Так про "сервер для 24x7 работы в ДЦ" никто кроме вас не говорил. Локального кодового агента вполне можно запускать на компьютере с двумя БУ видеокартами с Авито, работающего в серверной через дверь (у меня вообще в сарае стоит). И работать, кстати, он будет без проблем 24х7.
За $1500 можно собрать свой сервер для комфортного инферинга glm-4.7-flash.
Так душно, что даже отвечать сил нет.