Средства и методы разработки

Не, EventB - не матан. Это хорошо формализуемый слой системы проектирования, в котором нужно разделить состояния.  По русски говоря - спроектировать конечный автомат. И уже ветки этого автомата автомата специфицировать в виде, пригодном для суперкомпиляции. Уже без состояний. Получится интерпретатор задачи. Его и отдаём суперкомпилятору. Как похожее сделать уже лет десять назад показали на примере XSLT Корлюков и Немытых в работе Supercompilation of Double Interpretation В СПбГУ ИТМО конечными автоматами занимается Шалыто. Когда я смотрел его наработки, там всё транслировалось в С. Эту бодягу не отсуперкомпилируешь. Чего там сейчас - не смотрел. Почему мы сейчас так не делаем, а продолжаем бултыхаться в mainstream? Ответ скрывается в бизнес-модели, а не за разумными аргументами. Видимо ждём, что какой-нибудь ебиэм напряжётся и выложит xslt-шаблоны для верилога :) Только ждать очень долго придётся. Можно сказать, что индустрия сама выкопала себе могилу, но добровольно туда не полезет.