Project

General

Profile

Actions

Bug #7576

closed

mips16/hazard_detection_unit.v: java.lang.IllegalArgumentException: Constraint contains errors

Added by Sergey Smolov over 7 years ago. Updated over 6 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Category:
Engine (Transformer)
Target version:
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

Also available in: Atom PDF