This paper explores the relationship between register transfer level (RTL) automata (ASARTL) and looping algorithm specifications (ASASPEC) using semantics of algebra in the synthesis of stream calculus-based computing for big data in livestream (BDL). Specifically, it examines the verification of looping algorithm and RTL specifications through semantics of algebra. This paper introduces the concept of an algebraic semantics-based model (ASM), which is essentially a Chu space. A Chu space is represented as a triple (X, r, A), where X is the set of states, A is the set of events, and r is the matrix relation function. This model serves as a fundamental basis for formalizing RTL. This paper also defines ASASPEC for ensuring the correctness of RTL synthesis results. The formal verification method used is aimed at verifying functional equivalence to determine if the ASASPEC automata are equivalent to the ASARTL automata.