Verification of a network ASIC component using bounded model checking

Recently, a new technique called bounded model checking has been proposed that uses fast satisfiability solvers instead of binary decision diagrams (BDDs). This paper presents the experiences on formally verifying the behaviour and implementation of an Asynchronous Transfer Mode (ATM) network switching module using Nusmv2 tool. A number of properties described by linear temporal logic (LTL) are provided, and their veri. cation in reasonable central processing unit ( CPU) time is accomplished by estimating a more precise bound k which is determined by the circuit structure. Moreover, equivalence checking between the structural and behavioural descriptions of the whole switch module as one model is performed, and the results compared with those of the BDD-based approach. Based on that experience, bounded model checking will be the mainstream of industrial chip verification.