SAT-based bounded model checking (BMC) is introduced as a complementary technique to OBDD-based symbolic model checking

and is a verification method for parallel and reactive systems.However

until now the properties verified by bounded model checking are very limited.Temporal logic PSL is a property specification language (IEEE-1850) describing parallel systems and is divided into two parts

i.e.the linear time logic FL(Foundation Language)and the branch time logic OBE(Optional Branching Extension).The specification checked by BMC is extended to PSL and its algorithm is also proposed.Firstly

define the bounded semantics of PSL

and then reduce the bounded semantics into SAT by translating PSL specification formula and the state transition relation of the system

M

into the propositional formulas

respe

ctively.Finally

verify the satisfiability of the conjunction of the two propositional formulas.The algorithm results in the translation of the existential model checking of the temporal logic PSL into the satisfiability problem of propositional formula.An example of a queue controlling circuit is used to interpret detailedly the executing procedure of the algorithm.