Open-Source Projects

The release includes the following changes:

• Dependencies: use ANTLR 3.5.2;
• Bug fixes and general improvements.

The library can be downloaded from here

• Assertion: renamed to Property;
• CFG Model: CFG model processes do not have their own internal variables: variable space is flattened at parent module's level;
• CFG-to-GADD transformer: backend that implements clock detection is moved here;
• CFG-to-GADD transformer: cmdline option that specifies clock variable;
• CFG-to-GADD transformer: elaborate ranged assignments for bit vector target variables;
• CFG-to-GADD transformer: one more auxiliary path in GADD model for terminal endings;
• CFG-to-GADD transformer: reuse variables' versions upon CGAA model building;
• CFG-to-GADD transformer: support for designs that assign to variable more than once;
• CGAA model: renamed to GADD;
• Engines: '--no-backends' cmdline option;
• Engines: new cgaa-assert-extractor engine that extracts 'is-def' and 'is-use' constraints for every variable of every process of the design;
• Engines: debug output file for engines and their back-ends;
• Engines: enable\disable backend option by name for all engines;
• HDL Parser: init_process backend that transforms initial blocks;
• Models: support for 'BVEXTRACT(x y (SELECT z w))' constructions in left hand sides of assignments;
• Model Checker Launcher: nuXmv 1.1.1 is in use;
• Model Checker Launcher: pass Retrascope debug option to the model checker as well;
• Model Checker Launcher: pass model checker error msg to the Retrascope output;
• Refactoring: Range class is moved to Castle library;
• Refactoring: RetrascopeException.makeException -> RetrascopeException.exception;
• Refactoring: use StringTemplate facilities to generate HDL testbenches;
• SAT Solver wrapper: z3 4.7.1 is in use;
• Test suite: check variables\switches\basic blocks number at HDL parser test cases;
• Test suite: jUnit test cases for CFG-GADD transformer that check path number;
• Test suite: separate jUnit test cases for EfsmGraphMlPrinter engine;
• Tool: bug fixes and general improvements;
• Tool: renamed from "HDL Retrascope" to "Retrascope";
• Utility: 'BVEXTRACT( ... BVEXTRACT (j i x))' expression transformation rule to the tool ruleset;
• Utility: check BVEXTRACT operation's parameter order;
• Utility: substitute SMT-LIB variables those names are equal to builtin commands;
• VHDL parser: VHDL record support (non-aggregate case);
• VHDL parser: ZamiaCAD 0.11.3 is in use.

The list of resolved issues can be found here

The tool can be downloaded from here

Verilog Translator (VeriTrans) is an ANTLR-based Verilog front-end that generates an internal
representation of the target description. The representation is based on an Abstract Syntax Tree
(AST) formalism and on Fortress library objects for expressions representation.

The tool can be downloaded from here

• Dependencies: use Gradle 4.10.3;
• Dependencies: use Fortress 0.4.33-beta-190722;
• AST: new IntegerRange class;
• AST: new Range class;
• AST: new RangedVariable class;
• AST: new UseDef interface;
• Other bug fixes and general improvements.

The library can be downloaded from here

• New SmtKeyword class for SMT-LIBv2 keywords
• Print user data for unsupported operation
• SmtTextSolver: always parse model for array values
• Other bug fixes and code improvements

The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files

Redmine 4.0.3

Уважаемые коллеги!
Redmine обновился до версии 4.0.3, которая использует rails 5.2.3
В rails предыдущих версий найдена критическая уязвимость.
Нет никаких свидетельств, что уязвимость эксплуатировалась на этом сайте.

К сожалению, все плагины требуют доработки, поэтому пока отключены.

What's new?

• Specifications: Address translation for the Sv32, Sv39, and Sv48 modes
• Test Templates: Test templates for address translation
• Tests: Test suite uses QEMU4V 0.3.2

Download: https://forge.ispras.ru/projects/microtesk-riscv/files

What's new?

• Supported block-level register allocation constraints
• Updated the register allocation engine
• Changed mmuSL interpretation: structures' fields are listed from upper to lower bits

Download: http://forge.ispras.ru/projects/microtesk/files

The new release includes the following bugfix:

• Aarch64: increase size of internal string buffer

The source code can be downloaded from here

• Basic support for PowerPC programs emulation
• Trace generation for PowerPC (32bit) programs

The complete list of resolved issues is available here

The source code can be downloaded from here