High-Level Synthesis (HLS) tools automatically convert high-level algorithmic descriptions into hardware implementations, enabling rapid prototyping and design space exploration. As these tools perform complex transformations, Formal Equivalence Checking (FEC) becomes essential to verify that the generated hardware maintains the same behavior as the original high-level specification. Google’s open-source XLS tool represents a new generation of HLS frameworks that achieves a balance between flexibility and simplicity through its specialized intermediate representation (IR). However, unlike traditional LLVM IR, XLS’s functional SSA-style IR lacks structural continuity across transformations and optimization passes, and its semantics are based on Kahn Process Networks that differ from the CDFG-based LLVM IR, posing new challenges for equivalence checking. In this paper, we address the Sequential Equivalence Checking (SEC) between the scheduled XLS IR and the generated RTL. We propose an instrumentation-based pipeline-stage-wise symbolic execution approach with two main contributions: First, we prove that stage-by-stage verification of output transition functions and the concerned state transitions is sufficient to establish sequential equivalence. To overcome the symbolic execution difficulties, we record mapping relationships and construct symbolic constraint formulas through instrumentation during the code generation process. Experimental results show that our method effectively verifies the sequential equivalence, offering a practical approach to equivalence checking for modern HLS tools.