The new release contains the following changes:
- Specifications: Fixed bugs in the RV64D, RV32D, RV64F, and RV32F instructions
- Tool Functions: Updated the MicroTESK core to 3.6.4
- Test and Debug: Used QEMU4V 0.3.6 for running tests
- Test and Debug: Used Trace Matcher 0.1.9 for trace comparison
Download: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- Floating-point operations:
- Updated JSoftFloat library version to 1.1.0
- Added the `toUInteger()`, `fromUInteger()` methods to the `Floatx` class
- Fixed the implementation of some methods in the `Float64Operations`, `Float32Operations`, and `Float16Operations` classes
Download: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- Added half-precision (16-bit) floating-point operations
- Updated single-precision (32-bit) and double-precision (64-bit) floating-point operations
- Removed double-extended-precision and quadruple-precision (128-bit) floating-point operations
- Updated test cases for 16, 32, and 64-bit floating-point operations
Download: https://forge.ispras.ru/projects/jsoftfloat/files
The new release contains the following changes:
- Trace adapter tool:
- Added `Info` event element type
- Model code coverage:
- Added a mechanism for collecting model code coverage
Download: http://forge.ispras.ru/projects/microtesk/files
This is a release of the framework that focuses on performance issues and integration with continuous verification.
The following fixes and improvements in Klever 4.0 deserve an attention:
- Large refactoring in Klever Core, including:
- Replace data transfer from files to memory data structures
- Disable useless reports
- Remove confusing callbacks
- Remove extra processes
- Remove extra multiprocessing queues and components
- Remove tasks upload to Bridge in case of local deploy
- Add an option to disable cross references
- Optimize main job page in web interface
- Remove legacy code
- New versions of verifiers, based on CPAchecker 3.1
- Different improvements in resources, particularly, memory limits for main process, thread pool, node resources, speculative scheduling, EMG.
- Minor fixes in EMG models
- Scripts for build base creation.
- Development is moved into gitlab repository
We would like to thank very much everybody who made this great job possible!
This release publishes improvements that were made mostly before January 2022.
Since this time the development was actually stopped.
The new release includes the following changes:
- CFG-GADD-Transformer: '--no-phase' option to produce phase-free GADD;
- CFG-Model: general support of SVA properties;
- Distribution: self-made RTL models and demo scripts are added;
- Documentation: ChangeLog and README files are rewritten into `Markdown` format;
- EFSM-GraphML-Printer: `--detailed` option for EFSM detailed/limited printing;
- Tool: `--check` option to check if tool dependencies were installed properly;
- Tool: migration to JDK 11;
- Tool: `--version` option;
- VCD-Printer: a new engine to print test sequences into VCD format;
- Verilog-Parser: `--library-file` option for path to system tasks/functions file.
The complete list of resolved issues is available here
The binary distribution of the tool can be downloaded from here
The new release contains the following changes:
- Added the tool for list the model operations.
To use enter the command: `--list-operations <model name>`
- Oracle tool:
- Refactoring the tool settings and options
- Trace adapter tool:
- Refactoring the tool structure
Download: http://forge.ispras.ru/projects/microtesk/files
The release contains the following changes:
- Specifications:
- Added data processing (immediate) instructions: 38
- Added data processing (register) instructions: 70
- Added branches, exception generating, and system instructions: 47
- Added loads and stores instructions: 34
- Test Templates:
- Added new base template
- Added new test template for bubble sort algorithm
- Added new test template 'blocks.rb'
- Added new test template 'branch_generation.rb'
- Added new test template 'combinatorial_generation.rb'
- Added new test template 'dependencies.rb'
- Added new test template 'int_exception.rb'
- Added new test template 'random_sequence.rb'
Download: https://forge.ispras.ru/projects/microtesk-arm-demo/files