Bug #5572
closed[efsm][simulator] b10: Failed to resolve the assignment constraint
100%
Description
INFO: EFSM simulator.WORK.B10_0: traversing the transition {source state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (EQ STATO 4))); destination state: (AND (AND (GREATEREQ STATO 0) (LESSEQ STATO 10)) (AND (AND (AND (AND (AND (NOT (EQ STATO 0)) (NOT (EQ STATO 1))) (NOT (EQ STATO 2))) (NOT (EQ STATO 3))) (NOT (EQ STATO 4))) (EQ STATO 5))); guarded action: {{posedge of CLOCK}: {predicate: (NOT (EQ RESET 1)); predicate: (EQ RTR 1); predicate: (NOT (AND (AND (AND (EQ VOTO0 0) (EQ VOTO1 1)) (EQ VOTO2 1)) (EQ VOTO3 0)))}->{{assignment: {[BLOCK_V_OUT_0] := VOTO0_retrascope_29}; assignment: {[BLOCK_V_OUT_1] := VOTO1_retrascope_30}; assignment: {[BLOCK_V_OUT_2] := VOTO2_retrascope_31}; assignment: {[BLOCK_V_OUT_3] := VOTO3_retrascope_32}; assignment: {[BLOCK_CTS_4] := 1}; assignment: {[V_OUT_retrascope_36] := BLOCK_V_OUT_0}; assignment: {[V_OUT_retrascope_37] := BLOCK_V_OUT_1}; assignment: {[V_OUT_retrascope_38] := BLOCK_V_OUT_2}; assignment: {[V_OUT] := BLOCK_V_OUT_3}; assignment: {[CTS] := BLOCK_CTS_4}; assignment: {[STATO] := 5}}}}}
2015.01.22 21:41:48.771. ERROR: The exception has been encountered: java.lang.RuntimeException: Failed to resolve the assignment constraint
at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAssignment(EfsmSimulator.java:566)
at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.executeAction(EfsmSimulator.java:476)
at ru.ispras.retrascope.engine.efsm.simulator.EfsmSimulator.processEvents(EfsmSimulator.java:329)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.tryToTraverseTransition(EfsmAtomicFateTestGenerator.java:508)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmAtomicFateTestGenerator.generateInputVectorRandomly(EfsmAtomicFateTestGenerator.java:229)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:47)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.RandomFateSequenceIterator.next(RandomFateSequenceIterator.java:27)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:246)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGenerator.start(EfsmFateTestGenerator.java:55)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:199)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:114)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:329)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:350)
at ru.ispras.retrascope.util.VhdlUtilTest.runRetrascope(VhdlUtilTest.java:148)
at ru.ispras.retrascope.util.VhdlUtilTest.runVhdl(VhdlUtilTest.java:73)
at ru.ispras.retrascope.util.HdlUtilTest.runVhdl(HdlUtilTest.java:94)
at ru.ispras.retrascope.engine.efsm.generator.test.fate.EfsmFateTestGeneratorVhdlTestCase.generate(EfsmFateTestGeneratorVhdlTestCase.java:32)
Files
Updated by Igor Melnichenko almost 10 years ago
Проблема в несовпадении типов в этом присваивании: {[BLOCK_V_OUT_0] := VOTO0_retrascope_29}
[line 2 column 32: invalid function application for =, sort mismatch on argument at position 2, expected (_ BitVec 4) but given (_ BitVec 1), (declare-const assignmentResult (_ BitVec 4))
(assert (= assignmentResult #b0))
(check-sat)
(get-value ( assignmentResult))
(get-model)
(exit)
]
Переменная assignmentResult создаётся следующим образом:
String resultVariableName = "assignmentResult";
DataType resultDataType = assignment.getVariables().get(0).getVariable().getData().getType();
new Variable(resultVariableName, resultDataType);
Если я правильно всё понял, то BLOCK_V_OUT_0 - это нулевой бит переменной v_out. В таком случае он должен иметь тип (_ BitVec 1).
Updated by Igor Melnichenko almost 10 years ago
- Status changed from New to Feedback
Updated by Sergey Smolov almost 10 years ago
- Subject changed from [efsm][simulator] Failed to resolve the assignment constraint to [cfg][cgaa][transformer] wrong datatype of defined ranged variable
- Status changed from Feedback to Open
- Assignee changed from Igor Melnichenko to Sergey Smolov
Понятно, ошибка найдена, исправлю.
Updated by Sergey Smolov almost 10 years ago
- File b10-fate.txt b10-fate.txt added
- Subject changed from [cfg][cgaa][transformer] wrong datatype of defined ranged variable to [efsm][simulator] b10: Failed to resolve the assignment constraint
- Status changed from Open to New
- Assignee changed from Sergey Smolov to Igor Melnichenko
Ошибку исправил в r1468. Теперь присваивания переменным с диапазоном (т.е. RangedVariable) представляются корректно. Однако ошибка при генерации тестов компонентом FATE на дизайне b10 сохраняется. Может быть, дело в том, что такие присваивания неправильно обрабатываются симулятором? В частности, вот такое:
[code]
v_out(0) <= voto0 ;
[/code]
Прикрепил лог Retrascope, запущенного с параметрами: path-to-itc99/itc99-poli2/b10/b10.vhd --engine efsm-fate-test-generator --toplevel b10
Updated by Igor Melnichenko almost 10 years ago
- Status changed from New to Feedback
Сейчас он падает на выполнении присваивания {[V_OUT] := BLOCK_V_OUT_0}. По-моему, тут какая-то ошибка в извлечении присваиваний, потому что аналогов в исходном коде у этого выражения нет.
Updated by Sergey Smolov almost 10 years ago
Аналогом данного присваивания в коде является "v_out(0) <= voto0 ;" - неблокирующееся присваивание языка VHDL.
Такие присваивания трансформируются в обычные блокирующиеся следующим образом: если в CFG-представлении был найден "неблокирующийся"(isConcurrent == true) базовый блок (содержащий только неблокирующиеся присваивания) вида:
[code]
x_1 <= y_1;
x_2 <= y_2;
...
x_n <= y_n;
[/code]
то он трансформируется в базовый блок, состоящий из следующих блокирующихся присваиваний:
[code]
block_x_1 := y_1;
block_x_2 := y_2;
...
block_x_n := y_n;
x_1 := block_x_1;
x_2 := block_x_2;
...
x_n := block_x_n;
[/code]
Такова была основная идея. Я чуть позже сегодня посмотрю, нет ли очевидных ошибок в реализации.
Updated by Igor Melnichenko almost 10 years ago
Если в v_out(0) <= voto0 оба операнда - одноразрядные, то в {[V_OUT] := BLOCK_V_OUT_0} левый операнд - четырёхразрядный, а правый - одноразрядный. В этом и проблема.
Updated by Igor Melnichenko almost 10 years ago
Только после того, как это написал, понял, что в симулятор нужно добавить обработку Range :)
Теперь проблема ясна.
Updated by Sergey Smolov almost 10 years ago
Игорь,
Какая сейчас ситуация с генератором FATE? У меня данная ошибка на дизайне b10 не воспроизводится, хотя в логе инструмента присутствует:
[log]
2015.01.26 15:04:58.098. INFO: FATE.WORK.B10_0: the transitions aren't consistent
2015.01.26 15:04:58.098. INFO: FATE: the directed phase of generation has been finished successfully
2015.01.26 15:04:58.098. INFO: FATE: generation has been finished successfully. Total coverage: 39% (26 of 66 transitions)
[/log]
Можно ли включать тестирование на Hudson, или jUnit-тест на FATEпока не проходит?
Updated by Igor Melnichenko almost 10 years ago
Пока ошибка не исправлена. Как исправлю - обновлю статус этой задачи.
Updated by Sergey Smolov almost 10 years ago
- Status changed from Feedback to New
Updated by Sergey Smolov almost 10 years ago
Сейчасть запустил на b10 FATE - ошибки не наблюдается. Пофиксил?
Включил тестирование дизайна, вечером будет проверено на Hudson. Задачу считаем решенной?
Updated by Igor Melnichenko almost 10 years ago
Ещё нет - видимо, это побочный эффект какого-то другого изменения.
Updated by Sergey Smolov almost 10 years ago
Ок, с Hudson тогда пока повременю.
Updated by Igor Melnichenko almost 10 years ago
- Status changed from New to Resolved
- % Done changed from 0 to 100
Updated by Sergey Smolov almost 10 years ago
- Status changed from Resolved to Verified
Updated by Sergey Smolov over 9 years ago
- Status changed from Verified to Closed
- Published in build set to 20150307