Проверка модели синхронной схемы в UPPAAL

Я использую UPPAAL model checker для моделирования синхронной схемы на уровне ворот, у меня есть некоторая путаница в том, как я могу моделировать часы, моя цель - проверить, что время настройки и время удержания не нарушены. Я нашел некоторые модели, дающие часы в качестве тестового вектора в проверке модели приложения, например, t = 10, например, эквивалент для нарастающего фронта, а t = 20 - падающий фронт, который делает его похожим скорее на тестовый вектор. Может ли кто-нибудь предложить базовый пример того, как моделировать синхронную схему в UPAAL?Проверка модели синхронной схемы в UPPAAL

Спасибо

источник

2016-09-09 Hachani Ahmed

Вы должны быть знакомы с timed automata, пожалуйста, ознакомьтесь с руководством Uppaal. Если вы можете предоставить временную диаграмму, то довольно просто моделировать ее как машину состояний с некоторыми охранниками и инвариантами. – mariusm

Спасибо @mariusm за ваш ответ, я посмотрел на UPPAAL и не знаю, как может помочь диаграмма синхронизации, я на самом деле работаю над моделью D flip flop на уровне ворот и проверю время установки и время удержания, но когда пришло время моделировать часы, у меня возникла путаница, как я могу моделировать ее как автоматы, потому что лучшая вещь, которую я нашел до сих пор, это дать часы в качестве тестового вектора, например, например, 8 состояний, например, соответствуют 8 восходящим ребра, которые, скорее всего, будут тестовым вектором, я не уверен, как я могу использовать пространство часов, чтобы я мог проверить поведение D Flip Flop на каждом фронте. –

Я не понимаю часть «тестового вектора». Что касается синхронных часов, вам нужно смоделировать один процесс, который испускает (трансляцию) каналы 'rise' и' fall' с заданным временем (моделируется охранниками и инвариантами с использованием переменной 'clock'), а затем другие подключенные компоненты будут прослушивать к этим каналам и соответствующим образом обновлять их состояния. – mariusm

В декларациях пишут это:

clock t; 
broadcast chan rise, fall;

Тогда синхроимпульс в Uppaal будет выглядеть следующим образом:

Тогда другие подключенные компоненты должны слушать rise? и fall? как синхронизация по краям.

источник

2016-09-11 14:35:58 mariusm

Спасибо, что за ваше объяснение, часть, в которой я действительно запуталась, - это мой входной флип-флоп D, у меня была модель поведения D flip flop, но я не уверен, как моделировать вход D flip flop, либо я моделирую его как 2 состояния автоматов swithching между 0 и 1 каждый раз (учитывая задержку), либо я даю его как последовательность, как первое состояние «0_logique», останется X-временем, тогда следующее состояние «1_logique» останется X-временем , especiallay Мне нужен мой вход, чтобы уважать время настройки и время удержания часов. –

@HachaniAhmed, вам, скорее всего, понадобятся дополнительные промежуточные состояния. Начните с двух местоположений, а затем добавьте края для каждого события на входе моделирования, что должно произойти. Продолжайте добавлять края до тех пор, пока все местоположения не смогут обрабатывать любые входные данные в любое время. Вероятно, это потребует некоторого времени ожидания в промежуточных состояниях (моделирование ожидания с инвариантами и защитой) - это немного утомительно, но это нормально, потому что фактическая электроника также неинтересна и требует некоторого времени для изменения состояния. – mariusm

Проверка модели синхронной схемы в UPPAAL

ответ

Смежные вопросы