11Dec 2020 by kamkin

MicroTESK @ RISC-V Summit 2020

Conferences
MicroTESK framework and our ongoing research on online test program generation were presented at RISC-V Summit held online on December 8-10, 2020. The idea is that a generator (at least some part of it) works inside the design under test and constructs test programs on the fly. Each test is supplied with an equivalent mutant, and the CPU is checked by comparing their results. RISC-V is a free and open ISA enabling a new era of processor innovation through open standard collaboration. Each year, the RISC-V Foundation hosts RISC-V Summit and other events to bring the expansive ecosystem together to discuss current and prospective RISC-V projects and implementations, as well as collectively drive the future evolution of the ISA forward. https://riscv.org/ https://tmt.knect365.com/risc-v-summit/
Read More
01Sep 2020 by kamkin

MicroTESK for Binary Code Verification

Conferences
In this spring and summer, we wrote two papers on deductive verification of binary code against source-code-level specifications: one of them was published in Proceedings of the 14th International Conference of Tests and Proofs (TAP 2020); the other was presented at the 14th Spring/Summer Young Researchers’ Colloquium on Software Engineering (SYRCoSE 2020) and published in Proceedings of ISP RAS. In both works, we used MicroTESK to extract semantics of binary code and build the intermediate representation. The TAP conference promotes research in verification and formal methods that targets the interplay of proofs and testing: the advancement of techniques of each kind and their combination, with the ultimate goal of improving software and system dependability. SYRCoSE is an annual colloquium on software engineering targeted at young researchers. The main goal of…
Read More
27Jan 2020 by kamkin

MicroTESK 2.5.1 Released

New Features
MicroTESK 2.5.1 has been released. What's new? Fixed the TokenSourceStack class and moved it to the Castle 0.1.4 libraryRearranged the documentationMoved the documentation sources into a separate projectAdded the installation guide into the distribution packageModified the mmuSL code generation schemeAdded a boot section to the miniMIPS test templatesFixed a number of long-lived bugsUsed the QEMU4V 0.3.5 simulator for running tests Download: http://forge.ispras.ru/projects/microtesk/files
Read More
29Dec 2019 by kamkin

MicroTESK @ December 2019 Events

New Features
As usual, December was rich in events for our team. We attended three conferences, one in Russia and two in USA, where we presented MicroTESK in general (core and engines), MicroTESK for RISC-V (tools for test program generation and deductive binary code verification), and RISC-V Architecture Verification Suite, so-called RISC-V AVS (a set of test programs generated mostly by MicroTESK): Ivannikov ISP RAS Open Conference (ISPRAS Open) held in Moscow, Russia on December 5-6, 2019Microprocessor Test and Verification Workshop (MTV) held in Austin, TX, USA on December 9-10, 2019RISC-V Summit held in San Jose, CA, USA on December 9-12, 2019 We are full of plans and looking forward to implementing them next year. Happy 2020!
Read More
29Dec 2019 by kamkin

MicroTESK 2.5.0 Released

New Features
MicroTESK 2.5.0 has been released. What's new? Introduced new internal representation, so-called MIR (Middle-level [or MicroTESK] IR)Redesigned the constraint generator (for mark-based situations)Redesigned the symbolic executor (for binary code analysis)Unified the directives (alignment, data definition, and labels) for .text and .data sectionsEnabled a possibility to define data in .textImplemented new directives: .balign, .p2align, and .optionRefactored the code/data allocation logicImplemented a simple instruction-level coverage tracker (experimental)Introduced a new option --coverage-log for tracking test coverageEnabled a possibility to generate test coverage reports in Aspectrace format Used the QEMU4V 0.3.4 simulator for running tests Download: http://forge.ispras.ru/projects/microtesk/files MicroTESK for * Updated The dependent projects have been updated: MicroTESK for RISC-V (0.1.0)MIcroTESK for MIPS (0.1.0)MicroTESK for PowerPC (0.0.4) Related Links MicroTESK for RISC-V: https://forge.ispras.ru/projects/microtesk-riscv/MicroTESK for MIPS: https://forge.ispras.ru/projects/microtesk-mips64/MicroTESK for PowerPC: https://forge.ispras.ru/projects/microtesk-powerpc/QEMU4V: https://forge.ispras.ru/projects/qemu4v/
Read More
01Nov 2019 by kamkin

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
25Oct 2019 by kamkin

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 Test and Debug: 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
18Jun 2019 by kamkin

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