## 1 Introduction and Problem Formulation
### Optimization of the Verilog HDL Code of the Concurrent Control System
#### 2.3.1 Optimization of the Sequential Part of the System (Redundant Sequential Logic Optimization)  
Firstly, the logical equations written in Verilog ought to be transformed into a form that can be efficiently applied in the optimization process. In the proposed approach, the reduced ordered binary decision diagram is utilized (ROBDD, for simplicity called BDD) [89]. Such a graph permits the storage of logical functions in a memory-efficient manner. Once the logical equations are transformed to a BDD, the optimization of the redundant sequential logic is performed. This process refers to searching for the equivalent parts of the design that can be reduced in order to minimize the amount of resources required for the implementation of the system within the FPGA device. Let us explain this by an example. Assume that there are two functions: \(f_{1}=x_{1}+x_{2}\) and \(f_{2}=x_{1}\overline{x}_{2}+x_{1}x_{2}+\overline{x}_{1}x_{2}\). Those functions are equivalent, and \(f_{1}=f_{2}\). Therefore, the design can be optimized and only one of those functions is implemented in the hardware. In the case of the BDD, checking whether two functions are equivalent is relatively easy, and it just requires comparison of whether two pointers are equal. However, reduction of the number of flip-flops can be much more complicated. Consider an obvious example. Assume there are two flip-flops, controlled by the following functions:  
\[ \begin{array}{ll}D_{1}=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}\\ D_{2}=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}+x_{1}x_{2}\end{array}  \tag{1}\]  
Both functions are equivalent: \(D_{1}=D_{2}\). What can be proved by algebraic transformations is as follows:  
\[ \begin{array}{ll}D_{1}&=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}\\ &=Q_{3}\ x_{1}\ 1+\overline{Q_{3}}\ x_{2}\ 1\\ &=Q_{3}\ x_{1}(1+x_{2})+\overline{Q_{3}}\ x_{2}\ (1+x_{1})\\ &=Q_{3}\ x_{1}+\underline{Q_{3}}\ x_{1}x_{2}+\overline{Q_{3}}\ x_{2}+ \overline{Q_{3}}\ x_{2}x_{1}\\ &=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}+\left(Q_{3}+\overline{Q_{3}}\right)x_{ 1}x_{2}\\ &=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}+1\ x_{1}x_{2}\ =\ D_{2}\end{array}  \tag{2}\]  
The same is immediately visible when using the BDD representation of Boolean functions (Figure 3a). In the computer implementation of libraries for operating on BDD (or more precisely ROBDD), the logical function is a pointer to a structure in the memory (representing a graph node) [89]. The structure contains two pointers to two descendants for the values of the variable 0 and 1. When performing any operation on a BDD, it is checked using a hash table to see if the node already exists in memory, so as not to duplicate it. BDD libraries ensure the canonicity of logical functions, i.e., unambiguity and uniqueness of representation. Checking if two functions are equal is limited to checking if two pointers are equal to each other. Figure 3: Exemplary BDDs illustrating functions driving equivalent flip-flops: (**a**) the same excitation functions; (**b**) different excitation functions but equivalent flip-flops. Nevertheless, replacing the mentioned two flip-flops with a single one requires two conditions to be fulfilled. Firstly, their excitation functions ought to be the same. Furthermore, the initial values of both flip-flops must be the same: \(Q_{1}^{t=0}=Q_{2}^{t=0}\) (which can be easily checked). The replacement of two flip-flops by a single one is shown in Figure 4a. Another possibility refers to a hidden equivalence, where the excitation functions are not the same (Figure 4b), but the flip-flops could be reduced. Let us underline that commercial tools are not always able to optimize the number of registers. Therefore, in this paper, a novel reduction technique is proposed. Assume there are two flip-flops with the following excitation functions:  
\[ \begin{array}{l}D_{3}=Q_{3}\ x_{1}+\overline{Q_{3}}\ x_{2}\\ D_{4}=Q_{4}\ x_{1}+\overline{Q_{4}}\ x_{2}\end{array}  \tag{3}\]  
Clearly, the above functions are not equal. Moreover, they correspond to the different pointers in the BDD (Figure 3b).