Open-Source Projects

• Update the CPAchecker verification tool to the new version 1.4.
• LDV Tools are now available as Docker images, so you can avoid installation of all dependencies on your machine.
• Improvements in 13 existing rule specifications:
  • Driver becomes not available for unloading permanently.
  • Locking a mutex twice or unlocking without prior locking.
  • Usage of spin lock and unlock functions.
  • Usb alloc/free urb.
  • Possible TTY NULL dereference.
  • Atomic allocation in interrupt context.
  • Memory allocation inside spinlocks.
  • NOIO allocation under usb_lock.
  • Initialization of completion.
  • Error handling in probe().
  • All obtained blk requests should be put after all.
  • Calling find_next_zero_bit() with arguments in the right order.
  • Usb device reference counting with usb_get_dev/usb_put_dev and interface_to_usbdev.
• Adding 3 new rule specifications:
  • Correct usage of sysfs groups.
  • Correct usage of IO memory mappings.
  • Correct allocation of identifiers using IDR layer.

Results of validation of LDV Tools 0.8 and LDV Tools 0.7 with different verification tools on 41 known bugs in the Linux kernel are presented in the table below.

The new version of CPAchecker was able to find three more reference bugs in Linux kernel thanks to improvements described here.

The source code repository can be browsed by v0.8 tag. To get and to install LDV Tools see instructions. If you want to use prebuilt LDV Tools, please follow our LDV Tools in Docker instructions.

The new release contains the following changes:

• Support for the CVC4 constraint solver was implemented (*)
• Several bug fixes and general code improvements were made

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

(*) Please see the Installing Constraint Solvers and Running MicroTESK sections of Installation Guide to learn how to install and use CVC4.

The new release contains the following changes:

• Support for CVC4 was implemented
• Support for bit vectors, arrays and real numbers in calculator were implemented
• Additional rules for expression transformer were implemented
• Some bug fixes and general code improvements were made

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

Installation note:

In the new version, the Environment.setSolverPath method is no longer available since it causes controversy when several solvers are used. To set up the path to an external solver, you need to use the setSolverPath method of the corresponding solver object. For example:

final Solver solver = SolverId.Z3_TEXT.getSolver();
solver.setSolverPath("tools/z3/bin/z3.exe");

Another way is to set up the Z3_PATH and CVC4_PATH environment variables for the Z3 and CVC4 solvers correspondingly.

The new minor version of MicroTESK contains the following new features and changes:

• Support for automated extraction of coverage information that allows building constraints for named paths in instruction control flow (*)
• Possibility to process test templates in a stream manner (block by block), which allows processing larger test templates
• The trace method of the test template language now accepts objects created by the rand method
• Several minor bug fixes and general improvements

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

What's new (*):

Coverage Information Extraction

The main feature of the new release is extraction of test situations for named paths in the instruction control flow. Test situations are described as constraints on input parameters which should be satisfied in order to cause execution of a specific path. Test data is generated by solving the constraints specified in a test template.

Paths can be marked in ISA specifications using the mark function. For example, here is a part of the miniMIPS ADD instruction specification where two possible execution paths are marked as normal and overflow:

op add (rd: REG, rs: REG, rt: REG)
  syntax = format("add %s, %s, %s", rd.syntax, rs.syntax, rt.syntax)
  image = format("000000%s%s%s00000100000", rs.image, rt.image, rd.image)
  action = {
    temp = rs<31>::rs + rt<31>::rt;
    if temp<32> != temp<31> then
      mark("overflow");
      exception("IntegerOverflow");
    else
      mark("normal");
      rd = temp<31..0>;
    endif;
  }

Test situations to be covered by tests are specified in test templates using the name of the instruction and the name of the path. For example:

add t0, t1, t2 do situation('add.overflow') end
add t3, t4, t5 do situation('add.normal') end

NOTE: To generate test data based on constraints, MicroTESK requires the Z3 solver to be installed. See Installation Guide for more information.

The new build contains the following changes:

• Some bug fixes and code improvements were made

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

The HDL Retrascope tool was presented at the University Booth of the Design, Automation & Test in Europe (DATE). The conference took place on March 9-13 in Grenoble, France.

The DATE conference addresses all aspects of research into technologies for electronic and embedded system engineering. It covers the design process, test, and automation tools for electronics ranging from integrated circuits to distributed embedded systems. Read more...

HDL Retrascope IDE 0.1.2 has been released. The functionality left unchanged; a number of bugs have been fixed.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope-ide/files

The new release includes the following changes:

• Support for loops in VHDL/Verilog designs;
• Support for wait-expressions in VHDL/Verilog designs;
• Support for hierarchical (i.e. having sub-modules) VHDL/Verilog designs;
• Support for concurrent (non-blocking) statements in VHDL/Verilog designs;
• New command line scripts for Windows & Unix;
• New heuristic for initial EFSM state & reset signal detection;
• New fully-functional *.tar.gz distribution format;
• A number of bugs was fixed.

The tool can be downloaded from here: http://forge.ispras.ru/projects/retrascope/files

The new release contains the following changes:

• The random_seed setting was added to test templates
• Biased random generation was supported
• The miniMIPS specification was improved
• More test templates for miniMIPS were added

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

The new build contains the following changes:

• Classes for representing and building random variates were implemented

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