Open-Source Projects

The new release contains the following changes:

• Some bug fixes and general improvements were made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The new release contains the following changes:

• Possibility of initialize address fields depending on the operation that performs memory access was implemented in the MMU specification language
• Cases of incorrect use of test template blocks are now reported to the user
• Several bug fixes and general improvements were made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The new release contains the following changes:

• New method BitVector.extend was implemented

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

The new release contains the following changes:

• Test template blocks were made "passive" (processed by the generation engine only on request)
• Support for reuse (composition, repetition) of test template blocks was implemented
• Support for new floating-point functions 'is_nan' and 'is_signaling_nan' in nML was implemented
• Several bug fixes and general improvements were made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

MicroTESK will be presented at the 16th annual workshop on Microprocessor Test and Verification to be held in Austin, TX on December 3-4, 2015.

The presentation is entitled 'Specification-Based Test Program Generation for ARM VMSAv8-64 Memory Management Units'. It describes a tool for automatically generating test programs for ARM VMSAv8-64 memory management units. The solution is based on the MicroTESK framework. The tool consists of two parts: an architecture-independent test program generation core and VMSAv8-64 specifications. Such separation is not a new principle in the area — it is applied in a number of industrial test program generators, including IBM's Genesys-Pro. The main distinction is in how specifications are represented, what sort of information is extracted from them, and how that information is exploited. In the suggested approach, specifications comprise descriptions of the memory access instructions, loads and stores, and definition of the memory management mechanisms such as translation lookaside buffers, page tables, and cache units. The tool analyzes the specifications and extracts the execution paths and inter-path dependencies. The extracted information is used to systematically enumerate test programs for a given user-defined template. Test data for a particular program are generated by using symbolic execution and constraint solving techniques.

The purpose of MTV is to bring researchers and practitioners from the fields of verification and test together to exchange innovative ideas and to develop new methodologies to solve the difficult challenges facing us today in various processor and SOC design environments.

The new release contains the following changes:

• Improvements in Tarmac logging: support for memory accesses and register writes were implemented
• Handling of let-expressions (MMU) was improved
• Several bug fixes and general improvements were made
• Ruby engine was switched to JRuby 1.7.22

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

Version 0.19 of Requality has been released, with some new important additions and fixes.

• Support for traceability between requirements of different levels (e.g., high-level and low-level requirements):
  • New user interface for navigation by references between requirements.
  • New builtin report template 'Traceability report'.
  • User interface to setup relations between requirements during markup/requirements creation process.
• Brand-new user interface for review and resolution of results of update processor that automatically marks up requirements in a new version of requirements document using markup of a previous version.
• New builtin report template 'Progress report'.
  • The report demonstrates a progress of the project with time.
  • It is based on experimental statistics from SVN report template.
  • Data sources for coverage information are configured by user via new settings dialog.
  • One page of the report represents data graphically, another one represents data textually.
• Usability improvements:
  • Report is automatially opened after its generation.
  • 'Generate' button allows to generate report directly from 'Report settings' properties view.
• EXPERIMENTAL - Limited support for import/export of requirements catalog from/to ReqIF format. Attributes of Reference and List types as well as complex formatting are not supported.

• Attributes editor - for List values, attribute names, view for generated attributes.
• Virtual nodes - change of target nodes on change of virtual copies, target-related bugs.

A complete list of changes can be found in changelog.

The new release contains the following changes:

• Support for functions in MMU specifications
• Support for expressions based on extern variables in let-constructs (MMU)
• Support for 'if-then-else' expressions in let-constructs (MMU)
• Several bug fixes and general improvements
• JRuby was updated to version 9.0.3.0

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files

The new release contains the following changes:

• Reusability improvements in MapBasedPrinter
• New Value<T> utility interface for mutable values

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

The new release contains the following changes:

• Several bug fixes and general improvements were made

The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files