KA_ru 0 7 января, 2006 Опубликовано 7 января, 2006 · Жалоба посмотрел на FTP и поискал в форуме и не нашёл ничего толкового. не освещены вообще такие программы как eCheck Formality Conformal кто пробовал поделитесь впечатлением. PS:Может у кого-то есть и сами программы. Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
RVlad 0 12 января, 2006 Опубликовано 12 января, 2006 · Жалоба Formality Эта программа пробегала (на FTP), но к ней нет лицензии. :( Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
edward77 0 13 января, 2006 Опубликовано 13 января, 2006 · Жалоба чего нет, того нет..... Я даже топик открык по этому вопросу, но безрезультатно Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
yes 3 2 февраля, 2006 Опубликовано 2 февраля, 2006 · Жалоба также можно добавить сюда каденсовские static checker formal checker ходили тут люди синопсиса и каденца и вели рассказы какие замечательные тулы - все сами делают... но есть у меня сомнения, так как скорее всего эти формальные чекеры память и ресурсы жрут страшно ими проверять можно только что-то маленькое... а по поводу другой фишки - автогенерация тестбенчей из рандомайзнутых воздействий - тоже не понятно - покрытие после этой рандомизации надо наверно самому смотреть, из автоматических методов видится только перебор если кто знает чего - расскажите static checker есть в линуксном дистрибутиве IUS (с ftp) - только лицензии нету а на formal checker - только дока (мутная как и для 1-го) в sold-е вроде новом вообще только на formality дока - а на статический/формальный анализ я так и не понял какой тул Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
yes 3 8 февраля, 2006 Опубликовано 8 февраля, 2006 · Жалоба вот еще есть официально бесплатный тул from Cadence Berkeley Laboratories (типа идея та же что и formal check) но сразу понять что к чему у меня не вышло и вроде бы там язык не совсем (совсем не) PSL http://embedded.eecs.berkeley.edu/Alumni/kenmcmil/smv/ хотя никому это наверно и не интересно......... Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться
Shtirlits 0 1 апреля, 2006 Опубликовано 1 апреля, 2006 · Жалоба http://embedded.eecs.berkeley.edu/Alumni/kenmcmil/smv/ хотя никому это наверно и не интересно......... Подниму эту тему повыше. Есть, как минимум, 3 разных языка SMV: 1. CMU SMV (http://emc.cs.cmu.edu/) из которого вырос проект cadence и NuSMV 2. NuSMV (http://nusmv.irst.itc.it/) 3. Cadence SMV Последнее время активно пытаюсь работать с Cadence SMV. Сам язык местами приятный, нравится больше, чем первые два. Описание языка неполное, многое узнаешь из tutorial-а и примеров. Препроцессор от C, о чем ни слова в документации. Синхронные схемы с одним тактовым сигналом система позволяет моделировать. Есть компилятор с урезанного verilog (synchronous verilog). Если запустить трассировку, потом перезагрузить исходный текст и запустить трассировку снова - вываливается. Ну и плевать, это вообще не очень и нужно. Удалось кое-что написать для обучения: Поставил себе задачу сделать схему, которая получает на каждом такте 1 байт из потока и должна находить в потоке определенную последовательность. Найдя ее, схема должна поднимать выход на один такт. Написал модель (определение, что значит последовательность встретилась) и реализацию на smv, доказал, что '1' на выходе реализации бывает тогда и только тогда, когда встретилась такая последовательность. При доказательстве нашел ошибку в реализации, которую легко бы сделал и в реальной задаче. Усложнил задачу. Теперь схема получает по 2 байта за такт и выдает 2 бита результата. Написал и доказал. Тоже нашел ошибку. Написал реализацию на урезанном, но синтезируемом verilog-е. Скомпилировал в SVM и доказал, что сигналы на ее выходе эквивалентны модели. Солвер думает примерно полминуты-минуту на 2.2GHz opteron, памяти жрет к 300 мегабайтам. В общем, я счастлив. Когда несложный последовательный алгоритм нужно превратить в параллельный или еще какай-то вроде небольшой, но головоломный блок пишется пишется, очень утомительно тестировать. Наконец-то компьютеры доросли до того, чтобы думать. Цитата Поделиться сообщением Ссылка на сообщение Поделиться на другие сайты Поделиться