Project

General

Profile

News

MicroTESK for RISC-V: MicroTESK for RISC-V 0.0.5 released

Added by Andrei Tatarnikov 20 days ago

MicroTESK for RISC-V 0.0.5 has been released:

  • Specifications: Bug fixes
  • Test Templates: Test templates for generating torture tests
  • Test Templates: Test templates for validating floating-point instructions
  • Tool Functions: Improved floating-point support
  • Tool Functions: Improved register allocation mechanism
  • Tool Functions: Support for operations with dynamic immediate values in test templates (_AND, _OR, _XOR, _ADD, _SUB, _PLUS, _MINUS, _NOT, _SLL)
  • Tests: Improved Make scripts for running test templates
  • Tests: Specification code coverage is measured
  • Tests: Test suite uses QEMU4V 0.2.2

MicroTESK for RISC-V can be downloaded from http://forge.ispras.ru/projects/microtesk-riscv/files

MicroTESK: MicroTESK 2.4.42 released

Added by Andrei Tatarnikov 21 days ago

The new release contains the following changes:

  • Improved template facilities: support for addressing modes (registers) in printing functions (such as trace)
  • Improved template facilities: support for the _SLL operation with dynamic immediate values
  • Improved register allocation: support for the retain attribute

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

MicroTESK: MicroTESK 2.4.41 released

Added by Andrei Tatarnikov 26 days ago

The new release contains the following changes:

  • Support for floating-point types in data sections
  • Support for formatted printing of values in data sections
  • Support for register reservation
  • Support for basic operations (_AND, _OR, _XOR, _ADD, _SUB, _PLUS, _MINUS, _NOT) with dynamic immediate values in test templates
  • Improved register allocation strategies
  • New permutator exhaustive (aliased as full)
  • Support for i386 in x86 specifications
  • Support for the NASM and GNU assembler in x86 specifications and test templates
  • miniMIPS test programs are compiled with the GNU assembler and simulated in QEMU
  • x86 test programs are compiled with the GNU and NASM assemblers and simulated in QEMU
  • New option --model-name to allow building several ISA models from the same specifications
  • New option --base-template-path for automated template generation
  • Bug fixes and code improvements

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

Klever: Klever 1.0

Added by Evgeny Novikov about 1 month ago

After a long period of development we are happy to release Klever 1.0! This major version is dedicated to verification of Linux loadable kernel modules. Klever 2.0 will allow users to verify various C software.

Klever 1.0 includes all issues scheduled for 0.3 since they take much more time than we expected (we did not release 0.3 at all). Besides, there are many other fixes and improvements. We would like to mention the most valuable ones:

  • Verification results processing, visualization and assessment:
    • More accurate calculation and more pretty visualization of a verification job decision progress.
    • Adding more means for unknown report marks.
    • Improving error traces representation.
  • Updating the CPAchecker verification back-end.
  • Deployment:
    • Developing scripts for local deployment of Klever at Debian 9.
    • Improving deployment within OpenStack clouds.
    • Creating documentation that describes Klever deployment.
  • Support of a command-line interface for Klever Bridge.
  • Continuous integration:
    • Considerable enhancement of Klever tests.
    • Evaluating testing and validation results with preset marks.
    • Automated regression testing with help of Jenkins.
  • Numerous improvements, optimizations and bug fixes that substantially contribute reliability, increase performance and facilitate manual operations. Too many issues to treat them individually.

We thank all the developers and contributors for this great work! Before releasing Klever 2.0 we are going to release at least one minor version 1.1 with many valuable things but without any fundamental changes.

MicroTESK for RISC-V: MicroTESK for RISC-V 0.0.4 released

Added by Andrei Tatarnikov 2 months ago

MicroTESK for RISC-V 0.0.4 has been released:

  • Specifications: Support for RV32C and RV64C
  • Specifications: Bug fixes
  • Test Templates: RISC-V validation tests rv32uc/rvc and rv64uc/rvc
  • Test Templates: Test templates are split into groups being located in separate folders
  • Tests: Test suite uses QEMU4V 0.1.1

MicroTESK for RISC-V can be downloaded from http://forge.ispras.ru/projects/microtesk-riscv/files

QEMU4V: QEMU4V 0.1.1 released

Added by Sergey Smolov 3 months ago

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

MicroTESK for RISC-V: MicroTESK for RISC-V 0.0.3 released

Added by Andrei Tatarnikov 3 months ago

MicroTESK for RISC-V 0.0.3 has been released:

  • 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

MicroTESK for RISC-V can be downloaded from http://forge.ispras.ru/projects/microtesk-riscv/files

(1-10/307)

Also available in: Atom