Project

General

Profile

Bug #5572

[efsm][simulator] b10: Failed to resolve the assignment constraint

Added by Sergey Smolov over 5 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Normal
Category:
-
Target version:
Start date:
01/22/2015
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
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

b10-fate.txt (146 KB) b10-fate.txt Sergey Smolov, 01/23/2015 06:55 PM

History

#1

Updated by Igor Melnichenko over 5 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).

#2

Updated by Igor Melnichenko over 5 years ago

  • Status changed from New to Feedback
#3

Updated by Sergey Smolov over 5 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

Понятно, ошибка найдена, исправлю.

#4

Updated by Sergey Smolov over 5 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

#5

Updated by Igor Melnichenko over 5 years ago

  • Status changed from New to Feedback

Сейчас он падает на выполнении присваивания {[V_OUT] := BLOCK_V_OUT_0}. По-моему, тут какая-то ошибка в извлечении присваиваний, потому что аналогов в исходном коде у этого выражения нет.

#6

Updated by Sergey Smolov over 5 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]

Такова была основная идея. Я чуть позже сегодня посмотрю, нет ли очевидных ошибок в реализации.

#7

Updated by Igor Melnichenko over 5 years ago

Если в v_out(0) <= voto0 оба операнда - одноразрядные, то в {[V_OUT] := BLOCK_V_OUT_0} левый операнд - четырёхразрядный, а правый - одноразрядный. В этом и проблема.

#8

Updated by Igor Melnichenko over 5 years ago

Только после того, как это написал, понял, что в симулятор нужно добавить обработку Range :)
Теперь проблема ясна.

#9

Updated by Sergey Smolov over 5 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пока не проходит?

#10

Updated by Igor Melnichenko over 5 years ago

Пока ошибка не исправлена. Как исправлю - обновлю статус этой задачи.

#11

Updated by Sergey Smolov over 5 years ago

  • Status changed from Feedback to New
#12

Updated by Sergey Smolov over 5 years ago

Сейчасть запустил на b10 FATE - ошибки не наблюдается. Пофиксил?
Включил тестирование дизайна, вечером будет проверено на Hudson. Задачу считаем решенной?

#13

Updated by Igor Melnichenko over 5 years ago

Ещё нет - видимо, это побочный эффект какого-то другого изменения.

#14

Updated by Sergey Smolov over 5 years ago

Ок, с Hudson тогда пока повременю.

#15

Updated by Igor Melnichenko over 5 years ago

  • Status changed from New to Resolved
  • % Done changed from 0 to 100
#16

Updated by Sergey Smolov over 5 years ago

  • Status changed from Resolved to Verified
#17

Updated by Sergey Smolov over 5 years ago

  • Status changed from Verified to Closed
  • Published in build set to 20150307

Also available in: Atom PDF