Jest to polecenie fsp, które można uruchomić u dostawcy bezpłatnego hostingu OnWorks przy użyciu jednej z naszych wielu bezpłatnych stacji roboczych online, takich jak Ubuntu Online, Fedora Online, emulator online systemu Windows lub emulator online systemu MAC OS
PROGRAM:
IMIĘ
fsp — Dowód formalny pomiędzy dwoma opisami FSM
STRESZCZENIE
Fsp [-V] format 1 format 2 file1 file2
OPIS
Stworzony do działania na opisach FSM, Fsp obsługuje ten sam podzbiór VHDL co syf (for dalej
informacje o tym podzbiorze zob SYF(1) i FSM(5)). Fsp używa zredukowanego uporządkowanego pliku binarnego
Reprezentacja diagramów decyzyjnych i oblicza iloczyn dwóch opisów FSM.
Po tym etapie bada powstały produkt FSM i formalnie udowadnia równoważność
pomiędzy dwoma początkowymi opisami FSM. Te dwa opisy muszą mieć to samo
interfejs (jednostka VHDL).
ŚRODOWISKO ZMIENNE
MBK_WORK_LIB podaje ścieżkę do opisów FSM. Wartość domyślna to bieżąca
katalogiem.
MBK_CATA_LIB podaje dodatkowe ścieżki do opisów FSM. Wartość domyślna to
bieżący katalog.
OPCJE
-V Włącza tryb szczegółowy. Każdy etap dowodu formalnego jest ukazany na standardzie
wyjście.
PRZYKŁAD
fsp fsm fsm digi digi2
Użyj fsp online, korzystając z usług onworks.net