Verifikacija in opis digitalnih sistemov z logičnim jezikom Turbo prolog

• Letnik 1988

Glavni cilj naloge je opisati in verificirati digitalne sisteme z logičnim programskim jezikom. Pri opisu želimo zajeti tako osnovne gradnike kot tudi kompleksnejše digitalne strukture. Naš pristop bo temeljil na uporabi programskega jezika Turbo Prolog, zato bomo v prvem delu naloge spoznali to programsko orodje do takega nivoja, da ga bomo lahko uporabili pri realizaciji zastavljenega cilja. Ob tem pa bomo uporabili takšen pristop, da bodo naše ugotovitve lahko služile kot primeren priročnik za pomoč učencem pri delu z omenjenim programskim jezikom. V svetu se splošnem za razvoj programskega sistema na področju digitalnih sistemov uporabljajo trije različni pristopi: - Razviti takšen sistem s tako metodologijo, ki zagotavlja pravilnost izvedbe. Ta pristop je najbrž najtežji; tu obstaja namreč strašno veliko možnih rešitev, potrebno se je spopasti z avtomatskim programiranjem ter tako izvesti sintezo sistemov s povezovanjem, razmeščanjem, logičnim minimiziranjem funkcij, formiranjem programskih ureditev …, kar je za človeka zelo utrudljivo delo. Takšno delo je seveda še akademskega značaja in bo možno predvsem s pričakovano materialno opremo v prihodnosti. - Simulirati sistem in ga preizkusiti na testnih primerih. Pri simulaciji preizkušamo vhodne testne vzorce in jih primerjamo z dejansko dobljenimi oz. pričakovanimi. Če se vzorci ujemajo, sistem izpopolnjujemo, vendar pa z naraščajočo kompleksnostjo naletimo na praktične in teoretične omejitve. Preizkusiti vse testne primere je seveda že pri manjši kompleksnosti zelo težko, saj jih je ogromno (2 na število vhodov) – to so vse kombinacije vhodov -, zato preizkusimo najbolj delikatne primere. - Formalna verifikacija sistemov z matematičnim dokazom. Tu gre predvsem za matematični dokaz, ki – če uspe – velja potem za vse vhodne vzorce, torej je enak popolni simulaciji. Raziskave na tem področju so že vidne in včasih celo presegajo materialno opremo, ki je danes na razpolago. Takšen pristop je tako še najbolj primeren tudi za dosego našega cilja.