FORMALNA VERIFIKACIJA DVOJEZGARNOG JEDNO-CIKLUSNOG RISC-V PROCESORA I DELA MEMORIJSKOG PODSISTEMA

Apstrakt

U ovom radu  je prikazan način verifikacije dvojezgarnog jedno-ciklusnog RISC-V procesora i dela memorijskog podsistema pomoću formalnih metoda i JasperGold alata kreiranog od strane kompanije Cadence. Dat je osnovni opis dizajna koji se verifikuje, osnovni operatori SystemVerilog jezika koji se koristi kao i verifikacione tehnike koje su upotrebljene za efikasniju verifikaciju sistema.