Bug #5404
closed[verilog][parser][cfg] java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
0%
Description
Running: verilog-parser
Options: {v=[D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v], args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer}
2014.11.02 14:02:28.860. INFO: Start observing module ram.
2014.11.02 14:02:28.860. INFO: add variable clk [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.861. INFO: add variable rst [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.862. INFO: add variable val_rd [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.862. INFO: add variable val_wr [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.863. INFO: add variable addr_in [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.11.02 14:02:28.864. INFO: add variable data_in [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.864. INFO: add variable val_out [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.865. INFO: add variable data_out [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.866. INFO: add variable is_ready [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.866. INFO: add variable mem0 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.867. INFO: add variable mem1 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.868. INFO: add variable mem2 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.868. INFO: add variable mem3 [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.869. INFO: add variable result [(BIT_VECTOR 32)] (Data[type=(BIT_VECTOR 32), value=uninitialized]) to module ram.
2014.11.02 14:02:28.870. INFO: add variable state [(BIT_VECTOR 2)] (Data[type=(BIT_VECTOR 2), value=uninitialized]) to module ram.
2014.11.02 14:02:28.871. INFO: add variable RAM_IDLE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.875. INFO: add variable RAM_READ [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.876. INFO: add variable RAM_WRITE [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
2014.11.02 14:02:28.877. INFO: add variable RAM_RESULT [(BIT_VECTOR 1)] (Data[type=(BIT_VECTOR 1), value=uninitialized]) to module ram.
Storing: cfg
Running: cfg-cgaa-transformer
Options: {args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer, cfg=<cfg>}
Storing: cgaa
Running: cgaa-efsm-transformer
Options: {cgaa=<cgaa>, args=D:\Sergey\projects\retrascope.svn\trunk\retrascope\src\test\verilog\ram\ram.v --target efsm --engine cgaa-efsm-transformer}
2014.11.02 14:02:28.888. ERROR: The exception has been encountered: java.lang.IllegalArgumentException: Unsupported data type: UNKNOWN
at ru.ispras.fortress.solver.engine.z3.SMTStrings.textForData(SMTStrings.java:147)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:303)
at ru.ispras.fortress.solver.engine.z3.SMTTextBuilder.onValue(SMTTextBuilder.java:282)
at ru.ispras.fortress.expression.ExprTreeWalker.visitValue(ExprTreeWalker.java:209)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:152)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visitOperation(ExprTreeWalker.java:192)
at ru.ispras.fortress.expression.ExprTreeWalker.visitNode(ExprTreeWalker.java:160)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:127)
at ru.ispras.fortress.expression.ExprTreeWalker.visit(ExprTreeWalker.java:100)
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:120)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:350)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:335)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.isSAT(CgaaStateExprVisitor.java:203)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.checkConditionsIfNot(CgaaStateExprVisitor.java:192)
at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaStateExprVisitor.onBasicBlockBegin(CgaaStateExprVisitor.java:183)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitBasicBlock(CfgWalker.java:255)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:133)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:247)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:229)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCase(CfgWalker.java:247)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:139)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSwitch(CfgWalker.java:229)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:145)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitSource(CfgWalker.java:213)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitNode(CfgWalker.java:151)
at ru.ispras.retrascope.model.cfg.CfgWalker.visit(CfgWalker.java:109)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfg(CfgWalker.java:204)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitProcess(CfgWalker.java:195)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitModule(CfgWalker.java:179)
at ru.ispras.retrascope.model.cfg.CfgWalker.visitCfgModel(CfgWalker.java:166)
at ru.ispras.retrascope.model.cfg.CfgWalker.start(CfgWalker.java:86)
at ru.ispras.retrascope.engine.cfg.CfgEngine.start(CfgEngine.java:126)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:191)
at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:106)
at ru.ispras.retrascope.basis.Engine.start(Engine.java:191)
at ru.ispras.retrascope.Retrascope$Run.start(Retrascope.java:117)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:320)
at ru.ispras.retrascope.Retrascope.main(Retrascope.java:341)
at ru.ispras.retrascope.util.VerilogUtilTest.runRetrascope(VerilogUtilTest.java:120)
at ru.ispras.retrascope.util.VerilogUtilTest.runVerilog(VerilogUtilTest.java:69)
at ru.ispras.retrascope.util.HdlUtilTest.runVerilog(HdlUtilTest.java:137)
at ru.ispras.retrascope.util.HdlUtilTest.runHdl(HdlUtilTest.java:51)