Project

General

Profile

1.0

Features: multi-process test generation, model checking

89%

71 issues   (9 closed — 62 open)

Issues by
Bug

0/16
Feature

0/15
Task

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