Project

General

Profile

News

Linux Driver Verification: Version 0.8 of LDV Tools released

Added by Vadim Mutilin almost 9 years ago

LDV Tools 0.8 comes with the following improvements:

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.

LDV Tools 0.8 LDV Tools 0.7
BLAST CPAchecker BLAST CPAchecker
Found bugs 19 18 19 15
Missed bugs Due to bugs in verification tools 3 2 3 2
Out of memory (63 gigabytes) 2 0 1 2
Timeouts (50 minutes) 0 5 0 6
Due to other reasons 17 16 18 16

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.

MicroTESK: MicroTESK 2.2.1 alpha released

Added by Andrei Tatarnikov almost 9 years ago

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.

Fortress: Fortress v0.4.0 released

Added by Andrei Tatarnikov almost 9 years ago

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.

MicroTESK: MicroTESK 2.2.0 alpha released

Added by Andrei Tatarnikov about 9 years ago

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.

Retrascope: HDL Retrascope was presented at DATE 2015

Added by Sergey Smolov about 9 years ago

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...

Retrascope: HDL Retrascope v0.1.2 released

Added by Sergey Smolov about 9 years ago

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

MicroTESK: MicroTESK 2.1.5 released

Added by Andrei Tatarnikov about 9 years ago

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

(251-260/364)

Also available in: Atom