есть свободные "модель чекеры" - единственная проблема - язык входной у них "левый" («Телесистемы»: Конференция 'Языки описания аппаратуры (VHDL и др.))

[an error occurred while processing this directive] есть свободные "модель чекеры" - единственная проблема - язык входной у них "левый"

(«Телесистемы»: Конференция 'Языки описания аппаратуры (VHDL и др.))

Отправлено yes 09 февраля 2006 г. 18:10
В ответ на: Кто пользуется формальной верификацией (model checking, equivalency check) ? отправлено <font color=gray>Shtirlits</font> 08 февраля 2006 г. 14:08

и ыщчо
http://nusmv.irst.itc.it/
http://www.cs.cmu.edu/~modelcheck/smv.html

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

Составить ответ ||| Конференция ||| Архив

Ответы

С SMV народ приспособился из VHDL->Verilog->SMV (+) — Shtirlits (09.02.2006 20:18 83.149.205.223, 391 байт, ссылка, картинка)
- я так понял, что для формальной верификации нужна полнота асертов — yes (10.02.2006 12:38 87.236.81.130, 631 байт)
  - А я разве не положил лиц. в известное место? Или ее оттуда того? — SM (10.02.2006 19:48 213.141.159.26, пустое)
    - Рядом с линуксячими файлами 2005 ничего не нашел (+) — Shtirlits (10.02.2006 20:11 83.149.205.223, 217 байт)
    - если можно - помогите/разъясните. лицензия оттуда имеет фичу с формалити, но ft_shell (вроде) оттудоваже требует другую фичу — yes (10.02.2006 19:59 87.236.81.130, пустое)
      - надеюсь, что это не только мне интересно : — yes   (10.02.2006 20:12 87.236.81.130, 422 байт)
        
        Ща. Погодите. Будет вам кофэ, и какава тоже будет. — SM   (10.02.2006 20:29 213.141.159.26, пустое)
        
        Кофэ с чаем, дыбанное именно из этой формалити (я сам удивился от изобилия урожая) найдете там. в кряксах. — SM   (10.02.2006 21:11 213.141.159.26, пустое)
        
        Небольшой сорри. Там поправка произошла мелкая - адын нюанс забыл. Смотреть там же. — SM   (10.02.2006 23:31 213.141.159.26, пустое)
        
        вопрос для общего развития - а что в этот src достаточно имя фичи записать и все? — yes   (13.02.2006 13:16 87.236.81.130, 39 байт)
        
        Естессно. — SM   (13.02.2006 17:05 213.141.159.26, пустое)
        
        УРА! Спасибо!!! — Shtirlits   (11.02.2006 00:53 83.149.205.223, пустое)
- А вот интересно - пара вопросов (+) — SM (10.02.2006 03:07 213.141.159.26, 518 байт)
  - Видать на VHDL уже написано, да и не совсем verilog в SMV (+) — Shtirlits (10.02.2006 09:18 83.149.205.223, 1110 байт, ссылка)
    - Про хватит ли чекеров (+) — SM (10.02.2006 11:02 213.141.159.26, 517 байт)

Перейти к списку ответов ||| Конференция ||| Архив ||| Главная страница ||| Содержание

E-mail: info@telesys.ru