Кто пользуется формальной верификацией (model checking, equivalency check) ? («Телесистемы»: Конференция «Языки описания аппаратуры (VHDL и др.))

[an error occurred while processing this directive] Кто пользуется формальной верификацией (model checking, equivalency check) ?

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

Отправлено Shtirlits 08 февраля 2006 г. 14:08

Какими продуктами именитых и не очень фирм довелось пользоваться?
Что достойного внимания есть среди opensource ?

Смотрю на formality от synopsys и на список по ссылке.
Еще есть echeck от www.prover.com, с виду они не против дать demo, но не дают.

А что еще существует и есть?

http://vl.fmnet.info/

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

Ответы

есть свободные "модель чекеры" - единственная проблема - язык входной у них "левый" — yes (09.02.2006 18:10 87.236.81.130, 85 байт, ссылка)
- С 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 байт)
Пользуюсь formality, а также (этой просто постоянно) встроенной в команду "compile" DC (+) — SM (09.02.2006 01:36 213.141.159.26, 594 байт)
- интересно, что у DC возможно генерация несовпадающего нетлиста... я предполагал, что formality для — yes (09.02.2006 18:06 87.236.81.130, 186 байт)
  - Хе-хе. В DC... А уж сколько после BG такой лажи наблюдалось... Все не безглючны. — SM (09.02.2006 18:32 213.141.159.26, пустое)
    - Да, несовпадающий мне сгенерил 2000.05. А в 2004.06 такого пока не было. Но теперь зато верифицирую вот. — SM (09.02.2006 18:33 213.141.159.26, пустое)
- про formality вопрос (+) — Shtirlits (09.02.2006 09:19 83.149.205.223, 56 байт)
  - Под FC4. Конечно удалось. — SM (09.02.2006 14:09 213.141.159.26, пустое)
    - в известном месте есть еще static check (в IUS5.3) каденсовский, а лицензии нет - если умеете :) и интересно — yes (09.02.2006 18:16 87.236.81.130, пустое)
      - Вах. Я везде про IUS спрашивал, а он оказывается там есть!!!!! Сделаем, сделаем. — SM (09.02.2006 18:31 213.141.159.26, пустое)
        
        срочно спешу извинится - напутал. для линуха там еще ldv5.1 (со статик чеком), а ius5.3 для винды — yes (09.02.2006 18:48 87.236.81.130, 49 байт)

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

E-mail: info@telesys.ru

Ответы

Отправка ответа