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