We are happy to announce the first build of the QEMU4V tool.
QEMU4V ("QEMU for Verification") is an open source emulator for assembler programs that is based on QEMU project. The tool performs emulation for programs of several hardware architectures and provides some features (tracing, etc.) for system verification of microprocessors.
This build is based on 2.12.0 version of the QEMU emulator and includes all the features of QEMU for ARMv8 and QEMU for RISC-V tools.
The complete list of closed issues is available here
The source code can be downloaded from here
What's new?
- Specifications: System registers and system instructions
- Specifications: Bug fixes and improvements
- Test Templates: Automatically generated test templates
- Test Templates: BPU test templates that use the Branch engine
- Test Templates: Libraries to describe initialization/finalization code
- Test Templates: Updated linker settings
- Test Templates: Test templates to validate user-level instruction
- Test Templates: More demo test templates
- Tool Functions: Support for global labels, numeric labels, and weak symbols
- Tool Functions: Test data iterator functionality
- Tool Functions: Support for automated generation of test templates
- Tests: Test suite uses QEMU for RISC-V 0.2.1
- Tests: Test suite uses Spike (RISC-V ISA Simulator)
- Tests: Trace Matcher 0.1.8 is applied
Download: http://forge.ispras.ru/projects/microtesk-riscv/files
The new release contains the following changes:
- Support for automated generation of test templates
- Templates: methods
rev_id and is_rev to get information on revisions supported by the model
- Templates: support for global labels (the
global_label method)
- Templates: support for numeric labels
- Templates: support for weak symbols (the
weak method)
- Templates: new method
set_default_mode_allocator(allocator)
- Templates: runtime methods to trace the state of registers and memory (instead of hand-written observers)
- Number of bug fixes and code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- New standard operation
FUNCTION
- Support for new operations in
VerilogExprPrinter and VhdlExprPrinter
- Support for IO streams in
XmlConstraintLoader and XmlConstraintSaver
- New utility method
Node.deepestCopy to preserve user data
- New convenience method
NodeValue.newBitVector(boolean)
- New
BitVectorMath methods: nandr, norr, and xnorr
- Removed redundant size checks for multiplication and division from
BitVectorMath
- Bug fix in
BitVector.valueOf(byte[], int)
- Other bug fixes and code improvements
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
New features:
- Pycl - Python-based Constraint Language allows you to create functions to verify the requirements and constraints applied to the being developed software and hardware systems;
- integration with Requality - tool for managing of the requirements applied to the being developed software and hardware systems ( https://forge.ispras.ru/projects/reqdb );
Also the update includes a number of bug fixes across various components of MASIW Framework.
The new release contains the following changes:
- Test data iterator functionality was implemented
- New demo template
testdata.rb (miniMIPS) demonstrating test data iterator
- Refactoring in generation logic
- Some general code improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- New utility methods
ExprUtils.isOperation, Node.isType, and CollectionUtils.mergeLists
- New method
Transformer.substitute(Node, NodeProvider) that facilitates node substitution
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
The new release contains the following changes:
- Enhancements in the branch engine
- Refactoring in the memory engine
- New demo specifications and templates: Vmem ISA aimed to demonstrate the facilities of the memory engine
- Changes in the nML language translator: special constructs to specify label-based instruction operands
- Improvements in the simulator: correct handling of jump instructions
- Improvements in the symbolic executor: correct SMT-formulae
- Other general improvements
The MicroTESK distribution package can be downloaded from here: http://forge.ispras.ru/projects/microtesk/files
The new release contains the following changes:
- Pretty printing of SMT code
- Improvements in the Java printer
- New convenience methods
NodeValue.newBitVector
- Additional
NodeVariable constructor that takes a dynamic data object
- Some general code improvements
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files
The new release contains the following changes:
- Utility class
Nodes that provides shortcuts for constructing operation nodes
- Printer for saving expressions into Java code
- Code conventions enforced, which caused some renaming in public methods
The library can be downloaded from here: http://forge.ispras.ru/projects/solver-api/files