Project

General

Profile

News

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

Added by Andrei Tatarnikov almost 6 years ago

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

MicroTESK: MicroTESK 2.4.40 released

Added by Andrei Tatarnikov almost 6 years ago

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

Fortress: Fortress v0.4.31 released

Added by Andrei Tatarnikov almost 6 years ago

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

MASIW Framework: MASIW Framework update at 27.03.2017

Added by Alexandr Ugnenko about 6 years ago

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.

MicroTESK: MicroTESK 2.4.39 released

Added by Andrei Tatarnikov about 6 years ago

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

MicroTESK: MicroTESK 2.4.38 released

Added by Andrei Tatarnikov about 6 years ago

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

Fortress: Fortress v0.4.29 released

Added by Andrei Tatarnikov about 6 years ago

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

Fortress: Fortress v0.4.28 released

Added by Andrei Tatarnikov over 6 years ago

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

(81-90/364)

Also available in: Atom