응용 특화 프로세서들은 목표 도메인에서의 성능 극대화를 위해 자주 쓰이는 연산들을 위한 특화 명령어들을 가진다. 응용 특화 프로세서를 위한 프로그램은 특화 명령어를 사용하기 때문에 이들의 의미명세가 있어야 기호 실행기 등 고급 소프트웨어 분석 도구를 적용하는 것이 가능해진다. 이에 이 연구에서는 프로세서 구현 과정에서 반드시 작성해야 하는 레지스터 전송 레벨(RTL) 수준 프로세서 구현으로부터 명령어의 의미(semantics)을 자동으로 추출하는 시스템인 SemTracter를 개발하였다. SemTracter는 프로세서의 RTL을 기호 실행해서 각 명령어의 의미명세를 얻고 이를 ISA 명세 작성을 위해 개발된 언어인 Sail로 표현한다. 개발된 SemTracter는 간단한 구현된 5-stage RISC-V 프로세서로부터 몇 가지 명령어의 의미명세를 성공적으로 추출하였으며, 이는 직접 사람이 작성한 명세와 비교하여 일치하는 것을 확인하였다.
Domain-specific processors have specialized instructions tailored for frequently used operations in a particular domain, which enables them to achieve higher performance. This presents a challenge for program analysis, as the specialized instructions make it difficult to formally describe the instruction semantics. To address this, we present SemTracter, a tool that automatically extracts instruction semantics from a processor implemented in a hardware description language (HDL) at the register-transfer level (RTL). SemTracter obtains the semantics by simulating the processor RTL symbolically and compiling the results into formal instruction semantics using the Sail language. Our evaluation of the SemTracter on a small RISC-V processor RTL showed that it was able to extract the semantics of basic instructions from a 5-stage processor. Most of the RISC-V 32-bit integer base user-level ISA (RV32I) instructions were extracted and the generated semantics matched the manually written version.