Research Article
Algebraic Semantics of Register Transfer Level in Synthesis of Stream Calculus-Based Computing Big Data in Livestream
@INPROCEEDINGS{10.1007/978-3-031-59462-5_2, author={Pham Van Dang and Phan Cong Vinh and Nguyen Bao Khang}, title={Algebraic Semantics of Register Transfer Level in Synthesis of Stream Calculus-Based Computing Big Data in Livestream}, proceedings={Nature of Computation and Communication. 9th EAI International Conference, ICTCC 2023, Ho Chi Minh City, Vietnam, October 26-27, 2023, Proceedings}, proceedings_a={ICTCC}, year={2024}, month={5}, keywords={Algebraic semantics Algebraic semantics-based model (ASM) Algebraic semantics-based specification automata ( ) Algebraic RTL automata ( ) Big data in livestream (BDL) Register transfer level (RTL) Stream calculus-based computing BDL Control step (CStep) Functional unit (FU)}, doi={10.1007/978-3-031-59462-5_2} }- Pham Van Dang
Phan Cong Vinh
Nguyen Bao Khang
Year: 2024
Algebraic Semantics of Register Transfer Level in Synthesis of Stream Calculus-Based Computing Big Data in Livestream
ICTCC
Springer
DOI: 10.1007/978-3-031-59462-5_2
Abstract
This paper represents verification algorithms and register transfer level (RTL) specification as algebraic aspects proposed to validate the results of RTL synthesis. Major properties of this approach, the conception of an algebraic semantics-based model (ASM), to be interpreted as a Chu space, is viewed as an algebraic semantics foundation for the RTL formalization and the conception of algebraic semantics-based specification automata (({{\text{ASA}}}{{\text{SPEC}}})) are given for formal correctness of the results of RTL synthesis. Approaching formal verification is focused on functional equivalence examining to define if the algebraic RTL automata (({{\text{ASA}}}{{\text{RTL}}})) are equivalent to({{\text{ASA}}}_{{\text{SPEC}}}). To put it another way, the comparison is determined as an assessing that examines the synthesis algorithm is produced an effective RTL specification.
