{'fraction_non_alphanumeric': 0.01972555746140652, 'fraction_numerical': 0.004288164665523156, 'mean_word_length': 5.342391304347826, '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}}
Model Checking of the Fairisle ATM Switch

In this paper we present our experience on model checking of an Asynchronous Transfer Mode (ATM) switch using the Verification Interacting with Synthesis (VIS) tool. The switch we considered is in use for real applications in the Cambridge Fairisle network. It is composed of four input/output port controllers and a switch fabric, and contains around 1MB memory, 2KB FIFO buffer and 800 registers (latches). To overcome state space explosion, we adopted several abstractions and reductions, and applied compositional reasoning combined with two novel property division approaches. For the verification in VIS, we produced Verilog descriptions of the switch at different levels of design hierarchy and defined a number of relevant properties in CTL. Using the above techniques, we succeeded in verifying the switch at different hierarchy levels within reasonable CPU time, and thus illustrated the applicability of model checking to large designs containing a considerable number of state-holding elements. In addition, we succeeded in discovering several injected design errors in both the fabric and the port controllers.