Bug #5572
closed
[efsm][simulator] b10: Failed to resolve the assignment constraint
Added by Sergey Smolov almost 10 years ago.
Updated over 9 years ago.
Published in build:
20150307
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
Проблема в несовпадении типов в этом присваивании:
{[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).
- Status changed from New to Feedback
- 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
Понятно, ошибка найдена, исправлю.
- 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
- Status changed from New to Feedback
Сейчас он падает на выполнении присваивания {[V_OUT] := BLOCK_V_OUT_0}. По-моему, тут какая-то ошибка в извлечении присваиваний, потому что аналогов в исходном коде у этого выражения нет.
Аналогом данного присваивания в коде является "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]
Такова была основная идея. Я чуть позже сегодня посмотрю, нет ли очевидных ошибок в реализации.
Если в v_out(0) <= voto0 оба операнда - одноразрядные, то в {[V_OUT] := BLOCK_V_OUT_0} левый операнд - четырёхразрядный, а правый - одноразрядный. В этом и проблема.
Только после того, как это написал, понял, что в симулятор нужно добавить обработку Range :)
Теперь проблема ясна.
Игорь,
Какая сейчас ситуация с генератором 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пока не проходит?
Пока ошибка не исправлена. Как исправлю - обновлю статус этой задачи.
- Status changed from Feedback to New
Сейчасть запустил на b10 FATE - ошибки не наблюдается. Пофиксил?
Включил тестирование дизайна, вечером будет проверено на Hudson. Задачу считаем решенной?
Ещё нет - видимо, это побочный эффект какого-то другого изменения.
Ок, с Hudson тогда пока повременю.
- Status changed from New to Resolved
- % Done changed from 0 to 100
- Status changed from Resolved to Verified
- Status changed from Verified to Closed
- Published in build set to 20150307
Also available in: Atom
PDF