Перейти к содержанию
    

не нашёл ничего толкового

посмотрел на FTP и поискал в форуме и не нашёл ничего толкового.

не освещены вообще такие программы как

 

eCheck

Formality

Conformal

 

кто пробовал поделитесь впечатлением.

 

PS:Может у кого-то есть и сами программы.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

также можно добавить сюда каденсовские

static checker

formal checker

 

ходили тут люди синопсиса и каденца и вели рассказы какие замечательные тулы - все сами делают...

 

но есть у меня сомнения, так как скорее всего эти формальные чекеры память и ресурсы жрут страшно ими проверять можно только что-то маленькое...

 

а по поводу другой фишки - автогенерация тестбенчей из рандомайзнутых воздействий - тоже не понятно - покрытие после этой рандомизации надо наверно самому смотреть, из автоматических методов видится только перебор

 

если кто знает чего - расскажите

 

static checker есть в линуксном дистрибутиве IUS (с ftp) - только лицензии нету

а на formal checker - только дока (мутная как и для 1-го)

 

в sold-е вроде новом вообще только на formality дока - а на статический/формальный анализ я так и не понял какой тул

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

вот еще есть официально бесплатный тул from Cadence Berkeley Laboratories (типа идея та же что и formal check)

 

но сразу понять что к чему у меня не вышло и вроде бы там язык не совсем (совсем не) PSL

 

http://embedded.eecs.berkeley.edu/Alumni/kenmcmil/smv/

 

хотя никому это наверно и не интересно.........

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

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 мегабайтам.

В общем, я счастлив. Когда несложный последовательный алгоритм нужно превратить в параллельный или еще какай-то вроде небольшой, но головоломный блок пишется пишется, очень утомительно тестировать.

Наконец-то компьютеры доросли до того, чтобы думать.

Поделиться сообщением


Ссылка на сообщение
Поделиться на другие сайты

Присоединяйтесь к обсуждению

Вы можете написать сейчас и зарегистрироваться позже. Если у вас есть аккаунт, авторизуйтесь, чтобы опубликовать от имени своего аккаунта.

Гость
Ответить в этой теме...

×   Вставлено с форматированием.   Вставить как обычный текст

  Разрешено использовать не более 75 эмодзи.

×   Ваша ссылка была автоматически встроена.   Отображать как обычную ссылку

×   Ваш предыдущий контент был восстановлен.   Очистить редактор

×   Вы не можете вставлять изображения напрямую. Загружайте или вставляйте изображения по ссылке.

×
×
  • Создать...