Цитата(Poluektovich @ Nov 14 2016, 14:33)
НИИСИ использовали Jasper для проверки connectivity на системном уровне, регистрового пространства.
см JasperGold Applications Approach for Verification Workflow of SRISA Project
Да, мы видели такое приложение (APP как они его называют). Но на мой скромный взгляд это самое тривиальное из того что можно доказать формально, собственно поэтому вопросов к работоспособности и масштабируемости именно этого приложения практически нет. А вот случаи посложнее, типа доказательства соответствия RTL реализации заданному протоколу для всех возможных воздействий, такой уверенности пока не вселяли. Подозреваю, что там есть множество ограничений.
Более того, приложение проверки коннективити, насколько я понял (если не прав - поправьте), использует сторонний файл с описанием требуемой карты связности (который создаётся ручками). В таком случае от двойной ошибки и в списке связности и в RTL вызванной непониманием особенностей взаимодействия блоков страховки все равно нет. Ещё один момент — текущий уровень автоматизации создания систем. Многие блоки сейчас поставляются с IP-XACT (
ссылка_ip_xact) описанием, в котором, в том числе возможно функциональное объединение пинов в интерфейсы, которые на системном уровне подключаются друг у другу автоматически. Современные средства сборки СнК позволяют задавать каркас будущей системы, её карту памяти и теоретически такая система в части связности должна быть корректна от рождения. Во всяком случае серьёзных проблем именно с картой памяти или подключением стандартных интерфейсов в таких системах я не помню. Т.е. приложение то рабочее, но не самое эффектное с точки зрения влияния формалки на маршрут верификации.
На прошедшей в 2016 году конференции МЭС была целая секция посвящённая функциональной верификации, на которой в том числе обсуждались и теоретические аспекты формальной верификации (
МЭС. расписание секции функциональной верификации). Один из орг выводов — русскоязычного сообщества верификаторов пока нет, а в силу скорости развития этого направления лучше держаться вместе.
Данный форум — это площадка для живого обсуждения практических вопросов и обмена материалами и мнениями. Кроме того мы создали на FaceBook группу с пафосным названием «Российское сообщество верификаторов» (
ссылка на группу). Пока она работает в режиме новостной ленты с информацией о научных и практических конференциях или событиях, связанных с функциональной верификацией. Если у кого есть интерес — подписывайтесь.