{'fraction_non_alphanumeric': 0.01962421711899791, 'fraction_numerical': 0.0, 'mean_word_length': 5.223376623376623, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Scheduling Verification in High-Level Synthesis-Implementation of a Normalizer and a Code Motion Verifier

High level synthesis is the process of generating the register transfer level (RTL) design from the behavioral description. The synthesis process consists of several interdependent phases: Preprocessing, Scheduling, Register Allocation and Binding of variables, Control Path and Data Path generation, and Generation of synthesizable Verilog code (RTL). A High-level synthesis tool, called Structured Architecture Synthesis tool (SAST), has been developed which support hand-in-hand synthesis and verification. The existing framework is the SAST, and this work is to enhance this tool by incorporating a Normalizer and a Code Motion Verifier. The complexity of present-day VLSI systems is very high. The specification is given at a high level of abstraction compared to that of the output. In addition several optimization and transformations may be made at each phase to improve the performance of the design. Hence it is important to ensure that after each phase the behavior of the original specification is preserved. Hence is the need of phasewise verification. Verification of high level synthesis is a formal method for checking the equivalence between two descriptions of the target system, one before a particular phase and the other after that phase. The descriptions are represented as Finite State Machines with Data paths (FSMD).The basic principle is to show that any computation of one FSMD is covered by a computation on the other. While finding the equivalent path for a path, it is required to check the equivalence of the respective conditions as well as the data transformations of the paths. Since the condition of execution and the data transformation of a path involve the whole of integer arithmetic, checking equivalence of paths reduces to the validity problem of first order logic which is undecidable; thus, a canonical form does not exist for integer arithmetic. There we use a normalized form for conditional expression and data transformation expression. It may be possible to transform the input behavior to some equivalent description, by incorporating several high-level code transformation techniques, which results in amore efficient scheduling behavior. Thus the need to enhance the verifier to handle various code motion techniques while verification.