Project

General

Profile

1.0

Features: multi-process test generation, model checking

88%

75 issues   (9 closed — 66 open)

Issues by
Bug

0/18
Feature

0/16
Task

9/41
Related issues
Bug #8681: EngineRegistry fails to create toolchain when HashSet\HashMap are used Actions
Bug #8912: file ram.smv: line 332: variable is assigned more than once: m_ram.mem0 Actions
Bug #8970: NullPointerException in VisBpbCfgGraphMlTestCase Actions
Bug #8971: Wrong type RetrascopeException in VcegarMpegCfgGraphMlTestCase Actions
Bug #8972: Case value RetrascopeException in VcegarPiBusCfgGraphMlTestCase Actions
Bug #8973: ClassCastException in VcegarPjIcuCfgGraphMlTestCase Actions
Bug #8974: IllegalArgumentException in VcegarSdlxCfgGraphMlTestCase Actions
Bug #8991: CfgSwitchSequenceBackend: do not collapse "if" statements with incompatible conditions Actions
Bug #9025: IllegalArgumentException in VcegarPjIcramCfgGraphMlTestCase Actions
Bug #9026: IllegalArgumentException in vcegar/cache_coherence designs Actions
Bug #9060: Warnings and IllegalArgumentException in VcegarPjIcramCgaaGraphMlTestCase Actions
Bug #9066: ru.ispras.retrascope.engine.hldd.printer.smv.Texas97HlddSmvPrinterTestCase.runTest: java.lang.NullPointerException Actions
Bug #9075: java.lang.IllegalArgumentException: testNum 0 != 1 topModuleNum Actions
Bug #9228: Index ranges disappear in the new version of a variable Actions
Bug #9463: check if jUnit test cases for CfgCgaaTransformer return same results on different machines\platforms Actions
Bug #9485: missing javadoc Actions
Bug #9521: NuSMV works too slow on ITC'99 b11 design Actions
Bug #9562: ru.ispras.retrascope.engine.hldd.printer.smv.usedef.MemStageUseDefSmvPrinterTestCase: model checker crashes without errors in *.smvlog Actions
Feature #8260: VHDL records (structures) support Actions
Feature #8615: "--no-backends" command line option Actions
Feature #9039: Support for designs that assign to variable more than once Actions
Feature #9041: when model checker returns an error, print it's log to the Retrascope output Actions
Feature #9149: elaborate ranged assignments for bitvector target variables Actions
Feature #9227: support for 'BVEXTRACT(x y (SELECT z w))' constructions in left hand sides of assigments Actions
Feature #9247: CFG-to-C printer Actions
Feature #9264: '--disable-backends' cmdline option for HDL parser engine Actions
Feature #9281: cmdline option that specifies clock variable for CGAA model Actions
Feature #9335: cgaa-assert-extractor engine Actions
Feature #9446: Debug output file for engines and their backends Actions
Feature #9457: one more auxiliary path in GADD model for terminal endings Actions
Feature #9468: HDL parser backend that removes 'initial' processes Actions
Feature #9474: enable\disable backend parameters for all the engines Actions
Feature #9486: HDL parser's init_process backend: calculate initial values if possible Actions
Feature #9503: when debug option is enabled, pass it to the model checker as well Actions
Task #4086: [smv][example] Разобраться с инструментом SMV Actions
Task #4874: Разработка внутреннего представления для решающих диаграмм Actions
Task #4875: Построение решающей диаграммы по системе условий Actions
Task #4897: [verilog][printer][smv] Разработка принтера моделей в SMV-формат Actions
Task #4898: [verilog][printer][svn] Перенос кода SMV-принтера в проект Retrascope Actions
Task #4917: Создания инструмента поиска конфликтов для пар EFSM Actions
Task #5150: Обработка функций - реализация макроподстановок Actions
Task #5408: Принтер CFG в SMV Actions
Task #5473: Непонятные места в описании Веронского метода Actions
Task #5504: add channels between EFSMs Actions
Task #5588: extend HDL test suite Actions
Task #5711: Check generated *.smv files with external model checker Actions
Task #6061: EFSM-based transition assertion generator Actions
Task #6301: unused code Actions
Task #6472: b13.vhd: too long elaboration time Actions
Task #7723: Support for module instances in Verilog descriptions Actions
Task #7770: 'others' attribute upon array/bitvector initialization Actions
Task #8429: backend that transforms "x[i] := y" assignments into constant-ranged Actions
Task #8430: meta-info type for CFG statements that were added by HDL parser backends Actions
Task #8975: RetrascopeException.makeException -> RetrascopeException.exception Actions
Task #8976: Range: old -> high, young -> low Actions
Task #8994: "BVEXTRACT( ... BVEXTRACT (j i x))" expression transformation rule to the tool ruleset Actions
Task #9191: use StringTemplate facilities to generate HDL testbenches Actions
Task #9196: CfgVarRangeBlockBackend: use array length for assignment elaboration Actions
Task #9242: check BVEXTRACT operation's parameter order Actions
Task #9248: CFG model process should not have it's own internal variables Actions
Task #9249: separate jUnit test cases for EfsmGraphMlPrinter engine Actions
Task #9277: mv clock-like variable detection to CFG-to-CGAA transformer Actions
Task #9278: use CGAA model instead of EFSM-based assertions to get clocks Actions
Task #9280: prepare the code to 1.1.1 release Actions
Task #9291: use nuXmv 1.1.1 Actions
Task #9310: substitute SMT-LIB variables those names are equal to builtin commands Actions
Task #9389: Assertion -> Property Actions
Task #9427: reuse variables' versions upon CGAA model building Actions
Task #9430: CGAA -> GADD Actions
Task #9438: jUnit test cases for CFG-GAD transformer that check path number Actions
Task #9456: New phase-free SMV model representation using formulas Actions
Task #9462: jUnit test cases for HDL parsers that count numbers of CFG processes, statements, etc. Actions
Task #9484: Check variables\switches\basic blocks number at HDL parser test cases Actions
Task #9488: CFG-GADD transformer backend that makes assignments index and range-free Actions
Task #9658: Check for duplicated data access conflict assertions Actions