Записал видео (на английском языке) своей критики выдачи ИИ тула от Абишека Вармы из университета штата Иллинойс. Тул генерит SVA (SystemVerilog Assertions) для верификации (по простонародному - QA) цифровых аппаратных блоков систем на кристалле. Для повышения понятности, в начале видео рассказал основные идеи протокола AXI (Advanced eXtensible Interface): правила хендшейка valid/ready, конвейерность транзакций, внеочередной возврат данных по запросу чтения с тэгами.

Код, который я попросил Абишека скормить тулу для ревью.

Кратко что получилось:

Правила для проверок оно пишет некорректные. Например что если записать по адресу 100 число 123, то отныне и вовеки веков если прочитать с адреса 100, то там будет 123. Не задумывается, то после первой записи и до чтения может быть вторая, которая запишет число 456.

Далее, проверка для теста проверяет что после сброса (reset) данные на шине AXI будут равны X в виде data == 'x. Но это ерунда по двум причинам: Во-первых, данные могут быть после сброса какими угодно, хоть 0, хоть 123, так как они будуг игнорироваться если с ними не ходит бит valid=1, который кстати сбрасывается в 0. Во вторых, операция сравнения == 'x (неопределенным значением) дает в качестве результата 'x. Чтобы делать именно сравнение с 'x нужно использовать другую операцию ===, то это все равно не будет работать потому что (1). Это вообще невалидный тест.

Но это все цветочки - на это его можно натаскать. Более интересный вид тупости - ИИ конструирует проверку, что если сделаны запросы с тэгами 11, 3, 4, 7, то и данные будут возвращаться в таком же порядке - с тэгами 11, 3, 4, 7. Ему не приходит в голову задать себе вопрос - если бы это было так, зачем в AXI вообще были бы нужны тэги? Они ведь нужны чтобы идентифицировать данные которые приходят не в том порядке, скажем 4, 11, 3, 7.

Итд.