MicroTESK @ DVCon Europe 2019

Conferences
The MicroTESK framework and the MicroTESK-based test suite for RISC-V microprocessors (so called RISC-V AVS) were presented at DVCon Europe (Design and Verification Conference and Exhibition) held in Munich, Germany on October 29-30, 2019. MicroTESK for RISC-V: https://forge.ispras.ru/projects/microtesk-riscv RISC-V AVS: https://github.com/ispras/riscv-avs  
Read More

MicroTESK for RISC-V 0.0.9 Released

New Features
MicroTESK for RISC-V 0.0.9 has been released. What’s New? Specifications: Added system registers and the related modes Specifications: Added sample specifications of some vector instructions (consistent with RISC-V "V" Vector Extension Version 0.7.1) Specifications: Fixed bugs in RV64A instructions Specifications: Fixed bugs in RV32{F,D} instructions (FEQ, FLE, and FLT) Test Templates: Added sample test templates for vector instructions Test Templates: Changed structure of directories Test Templates: Fixed a Torture-like template ('synthetics/rvxxx') Tool Functions: Moved branch data generators to TestBase Tests: Test suite uses QEMU4V 0.3.3 MicroTESK for RISC-V 0.0.9 can be downloaded from here. More News We started uploading ready-to-use test programs to github: https://github.com/ispras/riscv-avs Here is the link to MicroTESK’s bug tracker at github: https://github.com/ispras/microtesk
Read More

MicroTESK @ SYRCoSE 2019

Conferences
Our research-in-progress on binary code deductive verification was presented at the Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE) held in Saratov, Russia on May 29-31, 2019. MicroTESK is used to specify a target instruction set architecture (ISA) and to extract the symbolic representation of a given binary file.
Read More

MicroTESK @ DUHDe 2019

New Features
Our research on binary code deductive verification was presented at the Workshop on Design Automation for Understanding Hardware Designs (DUHDe), a part of the Design Automation and Test in Europe Conference (DATE), held in Florence, Italy on March 29, 2019. In this work, MicroTESK is used to specify a target instruction set architecture (ISA) and to extract the symbolic representation of a given binary file. Other tools in use include Frama-C, Jessie, and Why3. To demonstrate the approach, we utilize RISC-V, a free and open ISA.  
Read More

MicroTESK 2.4.45 Released

New Features
MicroTESK 2.4.45 has been released New features are as follows: Block-level register allocation constraints; MMU plugin: structures' fields are listed from upper to lower bits. Block-level register allocation constraints This facility is aimed at overriding default settings written in the configuration file. MicroTESK 2.4.45 can be downloaded from here.
Read More