Digital Library[ Search Result ]
Extracting Instruction Set Architecture Semantics from a Processor Register-transfer Level
http://doi.org/10.5626/JOK.2023.50.10.827
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.
Algorithms for Dividing 1-dimensional Point Set into Rainbow Subsets
http://doi.org/10.5626/JOK.2022.49.3.201
When color is assigned to data that are expressed by a set of points in geometric space, a set of points that includes at least one point of each color is defined as a color-spanning set or a rainbow set. This paper suggests algorithms for determining optimal ways of selecting points from a colored one-dimensional point set such that the subsets composed of contiguous (selected) points and the set of remaining points are all rainbow sets. The suggested algorithms aim to minimize the number of selected points or minimize the total lengths of the regions that contain the selected points.
An Optimization Method for Performance Improvement of Set-based Similar Sequence Matching
http://doi.org/10.5626/JOK.2018.45.4.403
The set-based similar sequence matching method involves searching for data set sequences that are similar to a query set sequence. In the method, the similarity between two sets is represented as the size of intersection between them. However, there is a critical performances issue for calculating intersection size if the number of sets is large. In the past, authors of the present work proposed a method to improve the performance of set-based similar sequence matching using simple index structure. In this paper, we propose an optimization method for more efficient running of set-based similar sequence matching. Our method is based on pruning that excludes unnecessary calculation. Through experiments, we show that the proposed method reduces the execution time by about 20% compared to the existing methods.
Coinductive Subtyping for Recursive and Union Types
Induction and coinduction are well-established proof principles, which are widely used in mathematics and computer science. In particular, induction is taught in most undergraduate programs and well understood in the field of computer science. In contrast, coinduction is not as widespread or well understood as induction. In this paper, we introduce coinduction by defining a subtype system for recursive and union types and proving the transitivity property of the system. This paper will help to promote familiarity with coinduction and provides a basis for a subtype system for recursive types with other advanced type constructors and connectives.
Search
Journal of KIISE
- ISSN : 2383-630X(Print)
- ISSN : 2383-6296(Electronic)
- KCI Accredited Journal
Editorial Office
- Tel. +82-2-588-9240
- Fax. +82-2-521-1352
- E-mail. chwoo@kiise.or.kr