1.0 Features: multi-process test generation, model checking 88% 75 issues (9 closed — 66 open) 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
2.0 Features: flowchart extraction and visualization, RTL-to-TLM abstraction, testbench generation (UVM and C++TESK), property and protocol specification, deadlock analysis 3% 18 issues (0 closed — 18 open) Related issues Feature #4057: Механизм поиска взаимных блокировок Actions Task #4363: Критерий кластеризации входных сигналов, основанный на GA Actions Task #4521: Входной класс для генератора тестовой последовательности Actions Task #4877: Разработка конвертера тестовой последовательности в VCD-формат Actions Task #4880: Проектирование внутреннего представления для блок-схем Actions Task #4881: Реализация алгоритма построения блок-схем по внутреннему представлению Actions Task #4882: Разработка принтеров блок-схем в графические форматы Actions Task #4887: Разработка внутреннего представления тестовой системы Actions Task #4888: Генератор заготовки тестовой системы по ее описанию Actions Task #4889: Генерация заготовки эталонной модели по набору блок-схем (flowchart) Actions Task #4890: Разработка и реализация метода RTL-в-TLM абстракции блок-схем Actions Task #4891: Реализация генератора тестов по набору блок-схем Actions Task #4892: Анализ набора блок-схем на взаимные блокировки Actions Task #4962: Реализация утилиты Veritool с помощью средств Retrascope Actions Task #5027: Абстракция EFSM-моделей Actions Task #6446: Promela translator to CFG representation (no buffers) Actions Task #6448: mapping description language + IR + parser Actions Task #6449: testbench generator taking test sequences and mappings as inputs Actions