An automatic formal verification tool for schematic-level design of an electrical project

摘要

Schemat ideowy układu elektronicznego może być postrzegany jako zbiór wzajemnie połączonych komponentów elektronicznych tworzących pewien graf połączeń. Graf ten jest strukturą, której topologia może być odczytana i przeanalizowana. Automatyczna weryfikacja formalna schematu ideowego ma na celu wykrycie nietrywialnych błędów (związanych ze strukturą tegoż schematu), popełnionych przez projektanta w trakcie opracowywania schematu. Błędy te są efektem pominięcia lub niewłaściwego wykorzystania elementów elektronicznych w typowych podukładach (blokach funkcjonalnych). W artykule opisano realizację komputerowego narzędzia wspomagającego proces automatycznej weryfikacji formalnej, począwszy od określenia sposobu zapisu schematu, przez integrację z komercyjnymi narzędziami EDA (ang. Electronic Design Automation) aż po określenie algorytmów identyfikujących podobwody. Opracowane narzędzie umożliwia dokonanie weryfikacji schematu ideowego już w bardzo wczesnych etapach procesu projektowego, co znacząco redukuje liczbę pętli w procesie projektowym, wpływając korzystnie na końcowy koszt opracowania produktu oraz skracając czas niezbędny do przygotowania urządzenia do produkcji.%A schematic diagram can be interpreted as set of components connected together to build a network. The network is a structure whose topology can be read and analyzed. The automatic formal verification aims at detecting some non-trivial mistakes, made by an electrical engineer, connected with the structure of schematic, building blocks and typical functional sub circuits. The paper presents the approach for realization of an automatic formal detection tool starting from the definition of schematic structure, through connectivity with a schematic-capture tool, to a sub-circuit identification algorithm.