Actions
Bug #6504
closedfifo/fifo.v: nuSMV model checker returns ERROR
Start date:
01/14/2016
Due date:
% Done:
100%
Estimated time:
Detected in build:
svn
Platform:
Published in build:
0.2.1
Description
The HlddXmvPrinterTestCase
testcase falls on fifo/fifo.v
Verilog design with the following error log:
2016.01.14 00:08:21.392. INFO: Retrascope is starting 2016.01.14 00:08:21.392. INFO: Running: verilog-parser 2016.01.14 00:08:21.392. INFO: Options: {v=[D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v], args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv} Including file 'D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v' 2016.01.14 00:08:21.406. INFO: Storing: cfg 2016.01.14 00:08:21.406. INFO: Running: cfg-cgaa-transformer 2016.01.14 00:08:21.406. INFO: Options: {args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv, cfg=<cfg>} 2016.01.14 00:08:21.409. INFO: Storing: cgaa 2016.01.14 00:08:21.409. INFO: Running: cgaa-efsm-transformer 2016.01.14 00:08:21.409. INFO: Options: {cgaa=<cgaa>, args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv} 2016.01.14 00:08:21.858. INFO: Number of GADD paths: 24 2016.01.14 00:08:21.858. INFO: ====================================== 2016.01.14 00:08:21.858. INFO: Clock-like variables: []. 2016.01.14 00:08:21.858. INFO: Transforming the process of module: fifo. 2016.01.14 00:08:21.858. INFO: 1 states are extracted. 2016.01.14 00:08:21.859. INFO: The state-like variables are: []. 2016.01.14 00:08:21.859. INFO: 1 transitions are extracted. 2016.01.14 00:08:21.859. WARNING: Can't find resetting transition. 2016.01.14 00:08:21.859. INFO: Clock-like variables: []. 2016.01.14 00:08:21.859. INFO: Transforming the process of module: fifo. 2016.01.14 00:08:21.859. INFO: 1 states are extracted. 2016.01.14 00:08:21.859. INFO: The state-like variables are: []. 2016.01.14 00:08:21.859. INFO: 1 transitions are extracted. 2016.01.14 00:08:21.859. WARNING: Can't find resetting transition. 2016.01.14 00:08:21.859. INFO: Clock-like variables: []. 2016.01.14 00:08:21.859. INFO: Transforming the process of module: fifo. 2016.01.14 00:08:21.859. INFO: 1 states are extracted. 2016.01.14 00:08:21.859. INFO: The state-like variables are: []. 2016.01.14 00:08:21.859. INFO: 1 transitions are extracted. 2016.01.14 00:08:21.859. WARNING: Can't find resetting transition. 2016.01.14 00:08:21.859. INFO: Clock-like variables: []. 2016.01.14 00:08:21.859. INFO: Transforming the process of module: fifo. 2016.01.14 00:08:21.859. INFO: 1 states are extracted. 2016.01.14 00:08:21.859. INFO: The state-like variables are: []. 2016.01.14 00:08:21.859. INFO: 1 transitions are extracted. 2016.01.14 00:08:21.859. WARNING: Can't find resetting transition. 2016.01.14 00:08:21.859. INFO: Clock-like variables: []. 2016.01.14 00:08:21.859. INFO: Transforming the process of module: fifo. 2016.01.14 00:08:21.877. INFO: 16 states are extracted. 2016.01.14 00:08:21.878. INFO: The state-like variables are: [last, addr0]. 2016.01.14 00:08:21.898. INFO: 92 transitions are extracted. 2016.01.14 00:08:21.898. WARNING: Can't find resetting transition. 2016.01.14 00:08:21.898. INFO: 5 EFSM(s) are extracted. 2016.01.14 00:08:21.898. INFO: Storing: efsm 2016.01.14 00:08:21.898. INFO: Running: efsm-transition-assertion-extractor 2016.01.14 00:08:21.898. INFO: Options: {efsm=<efsm>, args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv} 2016.01.14 00:08:21.904. INFO: Storing: assertion 2016.01.14 00:08:21.904. INFO: Running: cgaa-hldd-transformer 2016.01.14 00:08:21.904. INFO: Options: {cgaa=<cgaa>, args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv} 2016.01.14 00:08:21.908. INFO: Storing: hldd 2016.01.14 00:08:21.908. INFO: Running: hldd-xmv-printer 2016.01.14 00:08:21.908. INFO: Options: {hldd=<hldd>, args=D:\Bot\projects\retrascope.svn\trunk\retrascope\build\resources\test\fifo\fifo.v --target hldd-xmv --toplevel --output-file fifo.smv, assertion=<assertion>} 2016.01.14 00:08:21.919. INFO: Storing: hldd-xmv 2016.01.14 00:08:21.919. INFO: Retrascope is shutting down expected:<OK> but was:<ERROR> Expected :OK Actual :ERROR <Click to see difference> java.lang.AssertionError: expected:<OK> but was:<ERROR> at org.junit.Assert.fail(Assert.java:91) at org.junit.Assert.failNotEquals(Assert.java:645) at org.junit.Assert.assertEquals(Assert.java:126) at org.junit.Assert.assertEquals(Assert.java:145) at ru.ispras.retrascope.engine.hldd.printer.xmv.HlddXmvPrinterTestCase.test(HlddXmvPrinterTestCase.java:70)
Updated by Mikhail Lebedev almost 9 years ago
- Status changed from New to Open
NuXmv fails with 'case conditions are not exhaustive' error.
Design has been added to 'ignored' list until the error is resolved.
Updated by Mikhail Lebedev almost 9 years ago
- Status changed from Open to Resolved
- % Done changed from 0 to 100
Resolved r2784.
Updated by Sergey Smolov almost 9 years ago
- Status changed from Resolved to Verified
Updated by Sergey Smolov over 8 years ago
- Status changed from Verified to Closed
- Published in build set to 0.2.1
Actions