Actions
Bug #7576
closedmips16/hazard_detection_unit.v: java.lang.IllegalArgumentException: Constraint contains errors
Start date:
09/23/2016
Due date:
% Done:
100%
Estimated time:
Detected in build:
verilog.benchmarks
Platform:
Published in build:
1.0.1-beta-170912
Description
2016.09.23 15:46:28.359. INFO: Retrascope is starting 2016.09.23 15:46:28.359. INFO: Running: verilog-parser 2016.09.23 15:46:28.359. INFO: Options: {v=[/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v], args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm --include-path --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log} Including file '/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v' 2016.09.23 15:46:28.362. DEBUG: Start observing module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable decoding_op_src1 [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable decoding_op_src2 [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable ex_op_dest [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable mem_op_dest [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable wb_op_dest [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. DEBUG: add variable pipeline_stall_n [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module hazard_detection_unit. 2016.09.23 15:46:28.362. INFO: Storing: cfg 2016.09.23 15:46:28.362. INFO: Running: cfg-cgaa-transformer 2016.09.23 15:46:28.362. INFO: Options: {args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm --include-path --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log, cfg=<cfg>} 2016.09.23 15:46:28.363. INFO: Storing: cgaa 2016.09.23 15:46:28.363. INFO: Running: cgaa-efsm-transformer 2016.09.23 15:46:28.363. INFO: Options: {cgaa=<cgaa>, args=/home/ssedai/projects/retrascope.git/build/resources/test/opencores/mips16/hazard_detection_unit.v --target efsm --include-path --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log} 2016.09.23 15:46:28.363. DEBUG: {} Constraint contains errors: (AND (OR (EQ decoding_op_src1 ex_op_dest) (EQ decoding_op_src1 mem_op_dest) (EQ decoding_op_src1 wb_op_dest)) (NOT (EQ decoding_op_src1 00000000000000000000000000000000)) (OR (EQ decoding_op_src2 ex_op_dest) (EQ decoding_op_src2 mem_op_dest) (EQ decoding_op_src2 wb_op_dest)) (NOT (EQ decoding_op_src2 00000000000000000000000000000000))); errors=[line 6 column 175: invalid function application, sort mismatch on argument at position 2, (declare-const wb_op_dest (_ BitVec 3)) (declare-const mem_op_dest (_ BitVec 3)) (declare-const decoding_op_src1 (_ BitVec 3)) (declare-const ex_op_dest (_ BitVec 3)) (declare-const decoding_op_src2 (_ BitVec 3)) (assert (and (or (= decoding_op_src1 ex_op_dest) (= decoding_op_src1 mem_op_dest) (= decoding_op_src1 wb_op_dest)) (not (= decoding_op_src1 #b00000000000000000000000000000000)) (or (= decoding_op_src2 ex_op_dest) (= decoding_op_src2 mem_op_dest) (= decoding_op_src2 wb_op_dest)) (not (= decoding_op_src2 #b00000000000000000000000000000000)))) (check-sat) (get-value ( wb_op_dest mem_op_dest decoding_op_src1 ex_op_dest decoding_op_src2)) (get-model) (exit) ] java.lang.IllegalArgumentException: Constraint contains errors: (AND (OR (EQ decoding_op_src1 ex_op_dest) (EQ decoding_op_src1 mem_op_dest) (EQ decoding_op_src1 wb_op_dest)) (NOT (EQ decoding_op_src1 00000000000000000000000000000000)) (OR (EQ decoding_op_src2 ex_op_dest) (EQ decoding_op_src2 mem_op_dest) (EQ decoding_op_src2 wb_op_dest)) (NOT (EQ decoding_op_src2 00000000000000000000000000000000))); errors=[line 6 column 175: invalid function application, sort mismatch on argument at position 2, (declare-const wb_op_dest (_ BitVec 3)) (declare-const mem_op_dest (_ BitVec 3)) (declare-const decoding_op_src1 (_ BitVec 3)) (declare-const ex_op_dest (_ BitVec 3)) (declare-const decoding_op_src2 (_ BitVec 3)) (assert (and (or (= decoding_op_src1 ex_op_dest) (= decoding_op_src1 mem_op_dest) (= decoding_op_src1 wb_op_dest)) (not (= decoding_op_src1 #b00000000000000000000000000000000)) (or (= decoding_op_src2 ex_op_dest) (= decoding_op_src2 mem_op_dest) (= decoding_op_src2 wb_op_dest)) (not (= decoding_op_src2 #b00000000000000000000000000000000)))) (check-sat) (get-value ( wb_op_dest mem_op_dest decoding_op_src1 ex_op_dest decoding_op_src2)) (get-model) (exit) ] at ru.ispras.retrascope.util.SatSolver.isSat(SatSolver.java:142) at ru.ispras.retrascope.util.SatSolver.areCompatible(SatSolver.java:159) at ru.ispras.retrascope.util.SolverUtils.areCompatible(SolverUtils.java:64) at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaPathExtractor.checkInvCompliance(CgaaPathExtractor.java:234) at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaPathExtractor.checkActionReachable(CgaaPathExtractor.java:220) at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaPathExtractor.checkConditionsIfNot(CgaaPathExtractor.java:214) at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaPathExtractor.onBasicBlockBegin(CgaaPathExtractor.java:203) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitBasicBlock(CfgWalker.java:361) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:186) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCase(CfgWalker.java:353) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:189) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitSwitch(CfgWalker.java:343) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:192) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCase(CfgWalker.java:353) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:189) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitSwitch(CfgWalker.java:343) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitNode(CfgWalker.java:192) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.visitChildren(CfgDfsWalker.java:72) at ru.ispras.retrascope.model.cfg.walker.CfgDfsWalker.processChildren(CfgDfsWalker.java:54) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.processStatement(CfgWalker.java:319) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitProcess(CfgWalker.java:305) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitModule(CfgWalker.java:279) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.visitCfgModel(CfgWalker.java:255) at ru.ispras.retrascope.model.cfg.walker.CfgWalker.start(CfgWalker.java:156) at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:87) at ru.ispras.retrascope.basis.Engine.start(Engine.java:214) at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:112) at ru.ispras.retrascope.basis.Engine.start(Engine.java:214) at ru.ispras.retrascope.Retrascope$ToolRun.start(Retrascope.java:209) at ru.ispras.retrascope.Retrascope.main(Retrascope.java:417) at ru.ispras.retrascope.Retrascope.main(Retrascope.java:369) at ru.ispras.retrascope.HdlTestUtils.runRetrascope(HdlTestUtils.java:335) at ru.ispras.retrascope.HdlTestUtils.runVerilog(HdlTestUtils.java:231) at ru.ispras.retrascope.HdlTestUtils.runVerilog(HdlTestUtils.java:200) at ru.ispras.retrascope.HdlTestUtils.runHdl(HdlTestUtils.java:90) at ru.ispras.retrascope.HdlTestUtils.runHdl(HdlTestUtils.java:102) at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformerTestCase.runTest(CgaaEfsmTransformerTestCase.java:94) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:606) at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44) at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15) at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41) at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20) at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:76) at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:50) at org.junit.runners.ParentRunner$3.run(ParentRunner.java:193) at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:52) at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:191) at org.junit.runners.ParentRunner.access$000(ParentRunner.java:42) at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:184) at org.junit.runners.ParentRunner.run(ParentRunner.java:236) at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecuter.runTestClass(JUnitTestClassExecuter.java:105) at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassExecuter.execute(JUnitTestClassExecuter.java:56) at org.gradle.api.internal.tasks.testing.junit.JUnitTestClassProcessor.processTestClass(JUnitTestClassProcessor.java:64) at org.gradle.api.internal.tasks.testing.SuiteTestClassProcessor.processTestClass(SuiteTestClassProcessor.java:50) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:606) at org.gradle.messaging.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35) at org.gradle.messaging.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24) at org.gradle.messaging.dispatch.ContextClassLoaderDispatch.dispatch(ContextClassLoaderDispatch.java:32) at org.gradle.messaging.dispatch.ProxyDispatchAdapter$DispatchingInvocationHandler.invoke(ProxyDispatchAdapter.java:93) at com.sun.proxy.$Proxy2.processTestClass(Unknown Source) at org.gradle.api.internal.tasks.testing.worker.TestWorker.processTestClass(TestWorker.java:106) at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method) at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:57) at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43) at java.lang.reflect.Method.invoke(Method.java:606) at org.gradle.messaging.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:35) at org.gradle.messaging.dispatch.ReflectionDispatch.dispatch(ReflectionDispatch.java:24) at org.gradle.messaging.remote.internal.hub.MessageHub$Handler.run(MessageHub.java:360) at org.gradle.internal.concurrent.ExecutorPolicy$CatchAndRecordFailures.onExecute(ExecutorPolicy.java:54) at org.gradle.internal.concurrent.StoppableExecutorImpl$1.run(StoppableExecutorImpl.java:40) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1145) at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:615) at java.lang.Thread.run(Thread.java:745)
Actions