News

Retrascope IDE: HDL Retrascope IDE 0.1.5 released

Added by Sergey Smolov 5 months ago

The functionality left unchanged; a number of bugs have been fixed.
The release contains HDL Retrascope 0.2.2 core.

The tool can be downloaded from here

Retrascope: HDL Retrascope 0.2.2 released

Added by Sergey Smolov 5 months ago

The new release contains the following changes:

  • Verilog testbench printer;
  • EfsmSimulatorUtils: utility methods for EFSM state/transition coverage printing;
  • VHDL/Verilog: support for non-0 starting bit vectors;
  • Verilog parser: merge 'assign' processes in CFG model if it is possible;
  • CGAA-to-EFSM: EFSM stabilization upon possible non-determinism;
  • Print tool execution time in command line mode;
  • HLDD-to-SMV printer that does not use assertions;
  • Bug fixes & general improvements.

The list of resolved issues can be found at the following link

The tool can be downloaded from here

Fortress: Fortress v0.4.21 released

Added by Andrei Tatarnikov 5 months ago

The new release contains the following changes:

  • Facilities to cast values in constant expressions
  • Improvements in ESExprParser

The list of resolved issues can be found at the following link

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

MicroTESK: MicroTESK 2.3.52 beta released

Added by Andrei Tatarnikov 5 months ago

The new release contains the following changes:

  • Refactoring in the ISA simulator

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

MicroTESK: MicroTESK 2.3.51 beta released

Added by Andrei Tatarnikov 6 months ago

The new release contains the following changes:

  • Refactoring: meta model is now a separate entity
  • Bug fixes and general improvements

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

MicroTESK: MicroTESK 2.3.49 beta released

Added by Andrei Tatarnikov 7 months ago

The new release contains the following changes:

  • Bug fixes and general improvements

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

MicroTESK: MicroTESK 2.3.48 beta released

Added by Andrei Tatarnikov 7 months ago

The new release contains the following changes:

  • Bug fixes and general improvements

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

MicroTESK: MicroTESK 2.3.47 beta released

Added by Andrei Tatarnikov 7 months ago

The new release contains the following changes:

  • Documentation on Ruby code of test templates included into distribution
  • Possibility to override configuration options from test templates by using the set_option_value function
  • Updated configuration options (see MicroTESK help)
  • New configuration option reserve-explicit that specifies whether explicitly specified registers must be reserved
  • New test template random_sequence.rb that combines sequences based on distributions
  • Bug fixes and general improvements

The list of resolved issues can be found at the following link

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

Fortress: Fortress v0.4.20 released

Added by Andrei Tatarnikov 7 months ago

The new release contains the following changes:

  • New NodeVariable methods: newInteger, newReal, newString, newBoolean, newUnknown, newBitVector and newMap
  • New ExprUtils method: isOperation that takes multiple operation identifiers

The list of resolved issues can be found at the following link

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

Klever: GSoC 2016 project was successfully completed

Added by Evgeny Novikov 7 months ago

Ilja Zakharov has finished works on Google Summer of Code 2016 project "Environment model specifications for more bugs to reveal" for The Linux Foundation.

During the project Ilja has ported all environment model specifications and tests to a new process calculus based environment model generator and implemented new environment model specifications to improve precision of environment models generated during static verification of Linux kernel modules. Moreover, a lot of work has been done to fix bugs in the environment model generator and to implement new features in it. For instance, Ilja has implemented a feature to generate simplified models for huge drivers to get a chance to a verification tool to finish analysis within a reasonable time.

As a result of this work, overall verification false positive rate has been decreased to 75% and a number of missing target bugs has been decreased to 40% from 60% (number of missed confirmed bugs that should be able to detect with our verification system).

Ilja's commits to the environment model generator and specifications sets (commits.ods) have already been reviewed and merged into the master branch of the upstream repository.

Patches to fix errors found with the environment model generator and new specification sets submitted by Ilja's mentor Alexey Khoroshilov:
  1. https://patchwork.kernel.org/patch/8999941/
  2. https://patchwork.kernel.org/patch/9094121/
  3. https://patchwork.kernel.org/patch/9130115/
  4. https://patchwork.kernel.org/patch/9154199/
  5. https://patchwork.kernel.org/patch/9206223/
  6. https://patchwork.kernel.org/patch/9221835/
  7. https://patchwork.kernel.org/patch/9232893/
  8. https://patchwork.kernel.org/patch/9262359/
  9. https://patchwork.kernel.org/patch/9276095/
  10. https://patchwork.kernel.org/patch/9276093/

1 2 3 4 5 ... 24 (21-30/240)

Also available in: Atom