What's new?
- Specifications: Added the system registers and the related modes
- Specifications: Added sample specifications of some vector instructions (consistent with
RISC-V "V" Vector Extension Version 0.7.1)
- Specifications: Fixed bugs in the
RV64A instructions
- Specifications: Fixed bugs in the
RV32{F,D} instructions (FEQ, FLE, and FLT)
- Test Templates: Added sample test templates for vector instructions
- Test Templates: Changed the structure of directories
- Test Templates: Fixed the Torture-like template (
synthetics/rvxxx)
- Tool Functions: Moved the branch data generators to TestBase
- Test and Debug: Used QEMU4V 0.3.3 for running tests
Download: https://forge.ispras.ru/projects/microtesk-riscv/files
The new release is based on QEMU 4.1.0 and includes the following changes:
- Gradle 4.10.3 is used for project building
- Bug fixes and general improvements
The source code can be downloaded from here
Уважаемые коллеги!
Redmine обновился до версии 4.0.5.
Jenkins обновился до версии 2.190.1
Debian обновился до версии 10.1
Просьба сообщать об обнаруженных проблемах.
The new release includes the following changes:
- CFG-to-GraphML printer: mark branch values with italic;
- CFG-to-GraphML printer: use dotted arrows for hierarchy dependencies;
- Dependencies: does not use commons-lang library;
- Tool: bug fixes and general improvements.
The list of resolved issues is available here
The tool can be downloaded from here
The release includes the following changes:
- Type casting for case statement's expression and values;
- Fix 'publishing' block behaviour in Gradle build system;
- Bug fixes and general improvements.
The list of resolved issues can be found here
The tool can be downloaded from here
The release includes the following changes:
- Dependencies: use ANTLR 3.5.2;
- Bug fixes and general improvements.
The library can be downloaded from here
The new release includes the following changes:
- 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
Aspectrace:
Aspectrace v1.0.1-alpha-191122 released
