Bug #7576: mips16/hazard_detection_unit.v: java.lang.IllegalArgumentException: Constraint contains errors - Retrascope - Open-Source Projects

Actions

Copy link

Bug #7576

closed

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

Added by Sergey Smolov about 8 years ago. Updated about 7 years ago.

Status:

Closed

Priority:

Normal

Assignee:

Sergey Smolov

Category:

Engine (Transformer)

Target version:

0.2

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

Copy link

Updated by Sergey Smolov about 8 years ago

Detected in build changed from svn to verilog.benchmarks

Actions

Copy link

Updated by Sergey Smolov about 8 years ago

Status changed from New to Open

Actions

Copy link

Updated by Sergey Smolov about 8 years ago

2016.09.23 19:13:03.896. INFO: Retrascope is starting
2016.09.23 19:13:03.896. INFO: Running: verilog-parser

2016.09.23 19:13:03.896. INFO: Options: {v=[/home/ssedai/projects/retrascope.git/build/resources/test/fifo/fifo.v], args=/home/ssedai/projects/retrascope.git/build/resources/test/fifo/fifo.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/fifo/fifo.v'
2016.09.23 19:13:03.949. DEBUG: Start observing module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable val_rd [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable val_wr [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable data_in [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable val_out [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable data_out [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable is_full [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable is_ready [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.950. DEBUG: add variable val0 [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable val1 [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable val2 [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable val3 [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable addr0 [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable addr1 [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable addr2 [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable addr3 [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable last [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable free_addr [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.951. DEBUG: add variable addr_in [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module fifo.
2016.09.23 19:13:03.957. INFO: Storing: cfg

2016.09.23 19:13:03.957. INFO: Running: cfg-cgaa-transformer

2016.09.23 19:13:03.957. INFO: Options: {args=/home/ssedai/projects/retrascope.git/build/resources/test/fifo/fifo.v --target efsm --include-path  --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log, cfg=<cfg>}

2016.09.23 19:13:03.959. INFO: Storing: cgaa

2016.09.23 19:13:03.959. INFO: Running: cgaa-efsm-transformer

2016.09.23 19:13:03.959. INFO: Options: {cgaa=<cgaa>, args=/home/ssedai/projects/retrascope.git/build/resources/test/fifo/fifo.v --target efsm --include-path  --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log}

2016.09.23 19:13:03.960. DEBUG: {}
2016.09.23 19:13:03.960. DEBUG: {}
2016.09.23 19:13:03.960. DEBUG: {}
2016.09.23 19:13:03.961. DEBUG: {last={all-path-num=21, use-path-num=20, control-use-path-num=20, data-use-path-num=0, def-path-num=0, def-use-path-num=0}}
2016.09.23 19:13:04.243. INFO: Number of GADD paths: 24
2016.09.23 19:13:04.243. INFO: ======================================
2016.09.23 19:13:04.243. INFO: Clock-like variables: [].
2016.09.23 19:13:04.243. INFO: Transforming the process of module: fifo.
2016.09.23 19:13:04.243. INFO: The state-like variables are: <none>.

Constraint contains errors: (AND true (AND (EQ is_full (BVAND (BVAND (BVAND val0 val1) val2) val3)) (EQ free_addr (ITE (ITE (NOTEQ (BVNOT val0) 0) false (ITE (NOTEQ (BVNOT val1) 0) true (ITE (NOTEQ (BVNOT val2) 0) true (ITE (NOTEQ (BVNOT val3) 0) true false)))) true 00))) true); errors=[line 7 column 270: invalid function application, sort mismatch on argument at position 3, (declare-const free_addr (_ BitVec 2))
(declare-const val0 (_ BitVec 1))
(declare-const val3 (_ BitVec 1))
(declare-const val1 (_ BitVec 1))
(declare-const val2 (_ BitVec 1))
(declare-const is_full (_ BitVec 1))
(assert  (and true (and (= is_full (bvand (bvand (bvand val0 val1) val2) val3)) (= free_addr (ite (ite (distinct (bvnot val0) #b0) false (ite (distinct (bvnot val1) #b0) true (ite (distinct (bvnot val2) #b0) true (ite (distinct (bvnot val3) #b0) true false)))) true #b00))) true))
(check-sat)
(get-value ( free_addr val0 val3 val1 val2 is_full))
(get-model)
(exit)
]
java.lang.IllegalArgumentException: Constraint contains errors: (AND true (AND (EQ is_full (BVAND (BVAND (BVAND val0 val1) val2) val3)) (EQ free_addr (ITE (ITE (NOTEQ (BVNOT val0) 0) false (ITE (NOTEQ (BVNOT val1) 0) true (ITE (NOTEQ (BVNOT val2) 0) true (ITE (NOTEQ (BVNOT val3) 0) true false)))) true 00))) true); errors=[line 7 column 270: invalid function application, sort mismatch on argument at position 3, (declare-const free_addr (_ BitVec 2))
(declare-const val0 (_ BitVec 1))
(declare-const val3 (_ BitVec 1))
(declare-const val1 (_ BitVec 1))
(declare-const val2 (_ BitVec 1))
(declare-const is_full (_ BitVec 1))
(assert  (and true (and (= is_full (bvand (bvand (bvand val0 val1) val2) val3)) (= free_addr (ite (ite (distinct (bvnot val0) #b0) false (ite (distinct (bvnot val1) #b0) true (ite (distinct (bvnot val2) #b0) true (ite (distinct (bvnot val3) #b0) true false)))) true #b00))) true))
(check-sat)
(get-value ( free_addr val0 val3 val1 val2 is_full))
(get-model)
(exit)
]
    at ru.ispras.retrascope.util.SatSolver.isSat(SatSolver.java:145)
    at ru.ispras.retrascope.util.SolverUtils.isSat(SolverUtils.java:52)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.getDstStates(CgaaEfsmTransformer.java:826)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.addTransitionsFromSrc(CgaaEfsmTransformer.java:494)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createTransitions(CgaaEfsmTransformer.java:484)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createAllTransitions(CgaaEfsmTransformer.java:456)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createEfsm(CgaaEfsmTransformer.java:449)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.getOutput(CgaaEfsmTransformer.java:351)
    at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:89)
    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

Copy link

Updated by Sergey Smolov about 8 years ago

2016.10.08 00:13:57.370. INFO: Retrascope is starting
2016.10.08 00:13:57.370. INFO: Running: verilog-parser

2016.10.08 00:13:57.370. INFO: Options: {v=[D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16\register_file.v], args=D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16\register_file.v --target efsm --include-path D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16 --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log}

Including file 'D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16\register_file.v'
2016.10.08 00:13:57.375. DEBUG: Start observing module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_write_en [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_write_dest [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_write_data [(BIT_VECTOR 16)] (Data[type=(BIT_VECTOR 16), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_read_addr_1 [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_read_data_1 [(BIT_VECTOR 16)] (Data[type=(BIT_VECTOR 16), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_read_addr_2 [(BIT_VECTOR 3)] (Data[type=(BIT_VECTOR 3), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_read_data_2 [(BIT_VECTOR 16)] (Data[type=(BIT_VECTOR 16), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.375. DEBUG: add variable reg_array [(BIT_VECTOR 16)] (Data[type=(BIT_VECTOR 16), value=uninitialized]) to module register_file.
2016.10.08 00:13:57.377. INFO: Storing: cfg

2016.10.08 00:13:57.377. INFO: Running: cfg-cgaa-transformer

2016.10.08 00:13:57.377. INFO: Options: {args=D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16\register_file.v --target efsm --include-path D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16 --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log, cfg=<cfg>}

2016.10.08 00:13:57.377. INFO: Storing: cgaa

2016.10.08 00:13:57.377. INFO: Running: cgaa-efsm-transformer

2016.10.08 00:13:57.377. INFO: Options: {cgaa=<cgaa>, args=D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16\register_file.v --target efsm --include-path D:\Bot\projects\retrascope.git\build\resources\test\opencores\mips16 --engine cgaa-efsm-transformer --tool-debug-file cgaa-efsm-transformer.log}

2016.10.08 00:13:57.377. DEBUG: {}
2016.10.08 00:13:57.377. DEBUG: {}
2016.10.08 00:13:57.377. DEBUG: {}
2016.10.08 00:13:57.426. INFO: Number of GADD paths: 5
2016.10.08 00:13:57.426. INFO: ======================================
2016.10.08 00:13:57.426. INFO: Clock-like variables: [clk, rst].
2016.10.08 00:13:57.426. INFO: Transforming the process of module: register_file.
2016.10.08 00:13:57.426. INFO: The state-like variables are: <none>.
2016.10.08 00:13:57.454. INFO: The number of model states: 1.
2016.10.08 00:13:57.454. INFO: The number of model transitions: 1.
2016.10.08 00:13:57.455. INFO: Clock-like variables: [].
2016.10.08 00:13:57.455. INFO: Transforming the process of module: register_file.
2016.10.08 00:13:57.455. INFO: The state-like variables are: <none>.

Constraint contains errors: (AND true (EQ reg_read_data_1 (BVZEROEXT 1 (ITE (EQ reg_read_addr_1 000) 000000000000000 reg_array))) true); errors=[line 4 column 115: invalid function application, sort mismatch on argument at position 3, (declare-const reg_read_addr_1 (_ BitVec 3))
(declare-const reg_read_data_1 (_ BitVec 16))
(declare-const reg_array (_ BitVec 16))
(assert (and true (= reg_read_data_1 ((_ zero_extend 1) (ite (= reg_read_addr_1 #b000) #b000000000000000 reg_array))) true))
(check-sat)
(get-value ( reg_read_addr_1 reg_read_data_1 reg_array))
(get-model)
(exit)
]
java.lang.IllegalArgumentException: Constraint contains errors: (AND true (EQ reg_read_data_1 (BVZEROEXT 1 (ITE (EQ reg_read_addr_1 000) 000000000000000 reg_array))) true); errors=[line 4 column 115: invalid function application, sort mismatch on argument at position 3, (declare-const reg_read_addr_1 (_ BitVec 3))
(declare-const reg_read_data_1 (_ BitVec 16))
(declare-const reg_array (_ BitVec 16))
(assert (and true (= reg_read_data_1 ((_ zero_extend 1) (ite (= reg_read_addr_1 #b000) #b000000000000000 reg_array))) true))
(check-sat)
(get-value ( reg_read_addr_1 reg_read_data_1 reg_array))
(get-model)
(exit)
]
at ru.ispras.retrascope.util.SatSolver.isSat(SatSolver.java:145)
at ru.ispras.retrascope.util.SolverUtils.isSat(SolverUtils.java:52)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.getDstStates(CgaaEfsmTransformer.java:826)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.addTransitionsFromSrc(CgaaEfsmTransformer.java:494)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createTransitions(CgaaEfsmTransformer.java:484)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createAllTransitions(CgaaEfsmTransformer.java:456)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createEfsm(CgaaEfsmTransformer.java:449)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.getOutput(CgaaEfsmTransformer.java:351)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:89)
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:104)
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)