Basic parallel process (BPP) is a model for describing and analyzing concurrent programs, which is an important subclass of Petri nets. The logic EG is a branching time logic obtained by extending Hennessy-Milner Logic with the EG operator, in which the AF operator means that a certain property will be satisfied eventually from the current state. Hence, the logic EG is a logic that can express liveness. However, model checking the logic EG over BPP is undecidable. This study proposes an algorithm for the problem of bounded model checking EG over BPP. First, a bounded semantics of EG over BPP is proposed. Then, according to the constraint-based approach, a reduction from the problem of bounded model checking EG over BPP to the satisfiability problem of linear integer arithmetic formulas is given. Finally, the linear integer arithmetic formulas are solved by SMT solvers.