moka - Online di Awan

PROGRAM:

NAMA

MOKA - Nenek moyang pemeriksa model

RINGKASAN

moka [-VDB] fsm_namafile ctl_namafile

DESKRIPSI

moka adalah pemeriksa model CTL.

Dibuat untuk dijalankan pada deskripsi FSM atau RTL, moka mendukung subset VHDL yang sama dengan syf atau boom
(untuk informasi lebih lanjut tentang subset ini lihat SYF(1) BOOM(1) FSM(5) VBE(5) ).
Namun moka memaksakan bahwa setiap daftar deskripsi perilaku memiliki kesamaan
kondisi jam dan tidak ada bus tristate atau multiplexed. Khususnya VHDL
ketik MUX_BIT dan WOR_BIT tidak didukung.
Pertama-tama moka membangun transisi fonction FSM menggunakan Reduced Ordered Binary
Representasi Diagram Keputusan.
Kemudian menerapkan kondisi awal untuk menemukan keadaan pertama (kata kunci INITIAL dan/atau
RESET_COND di CTL(5) format berkas).
Setelah itu menghitung simulasi simbolis FSM untuk menemukan semua status yang dapat dijangkau.
Perhitungan ini memperhitungkan kondisi asumsi (kata kunci ASSUME dalam
CTL(5) format berkas).
moka akhirnya memverifikasi satu per satu setiap formula CTL. (Lihat CTL(5) untuk format file CTL
rincian).

CTL OPERATOR

Untuk setiap sub-ekspresi CTL moka akan mengembalikan kumpulan status yang memverifikasi rumus.
Misalnya EX(p) akan mengembalikan kumpulan status yang dapat dijangkau yang memverifikasi EX(p).
Operator CTL:
EX(p) : mengembalikan semua status yang memiliki hampir satu penerus status utama yang
diaudit p.
EU(p,q) : mengembalikan semua status yang merupakan akar dari hampir satu jalur, sehingga p is
benar sampai q selalu benar.
EG(p) : mengembalikan semua status yang merupakan akar dari hampir satu jalur, sehingga p is
selalu benar.
AX(p) : mengembalikan semua status yang memiliki semua penerus status utamanya yang
diaudit p.
AU(p,q) : mengembalikan semua status yang merupakan akar dari satu-satunya jalur dari mana p adalah benar
sampai q selalu benar.
AG(p) : mengembalikan semua status yang merupakan akar dari satu-satunya jalur, sehingga p selalu
benar.

LINGKUNGAN VARIABEL

MBK_WORK_LIB memberikan path untuk deskripsi dan file CTL. Nilai defaultnya adalah
direktori saat ini.

MBK_CATA_LIB memberikan beberapa jalur tambahan untuk deskripsi dan file CTL. NS
nilai default adalah direktori saat ini.

PILIHAN

-V Mengaktifkan mode verbose. Setiap langkah pemeriksaan model ditampilkan pada standar
output.

-D Mengaktifkan mode debug. Setiap langkah pemeriksaan model dirinci pada output standar.
Secara khusus semua set status ditampilkan untuk setiap sub-ekspresi CTL.

-B File input adalah deskripsi VHDL menggunakan subset Alliance VHDL (lihat VBE(5) berkas
format).

FSM CONTOH

-- Contoh multi fsm

Contoh ENTITY adalah
PORT
(
ck : dalam BIT;
data_in : dalam BIT;
reset : dalam BIT;
data_out : keluar BIT
);
AKHIR contoh;

FSM ARSITEKTUR contohnya adalah

TIPE A_ETAT_TYPE ADALAH (A_E0, A_E1);
SINYAL A_NS, A_CS : A_ETAT_TYPE;

TIPE B_ETAT_TYPE ADALAH (B_E0, B_E1);
SINYAL B_NS, B_CS : B_ETAT_TYPE;

--PRAGMA CURRENT_STATE A_CS FSM_A
--PRAGMA BERIKUTNYA_STATE A_NS FSM_A
--JAM PRAGMA ck FSM_A
--PRAGMA FIRST_STATE A_E0 FSM_A

--PRAGMA CURRENT_STATE B_CS FSM_B
--PRAGMA BERIKUTNYA_STATE B_NS FSM_B
--JAM PRAGMA ck FSM_B
--PRAGMA FIRST_STATE B_E0 FSM_B

SINYAL ACK, REQ, DATA_INT : BIT;

MULAI

A_1 : PROSES ( A_CS, ACK )
MULAI
JIKA ( setel ulang = '1' )
LALU A_NS <= A_E0;
DATA_OUT <= '0';
REQ <= '0';
ELSE
KASUS A_CS adalah
KAPAN A_E0 =>
JIKA ( ACK ='1') MAKA A_NS <= A_E1;
LAIN A_NS <= A_E0;
BERAKHIR JIKA;
DATA_OUT <= '0';
REQ <= '1';
KAPAN A_E1 =>
JIKA ( ACK ='1') MAKA A_NS <= A_E1;
LAIN A_NS <= A_E0;
BERAKHIR JIKA;
DATA_OUT <= DATA_INT;
REQ <= '0';
KASUS AKHIR;
BERAKHIR JIKA;
AKHIR PROSES A_1;

A_2 : PROSES( ck )
MULAI
JIKA ( ck = '1' DAN BUKAN ck'STABLE )
LALU A_CS <= A_NS;
BERAKHIR JIKA;
AKHIR PROSES A_2;

-------

B_1 : PROSES ( B_CS, ACK )
MULAI
JIKA ( setel ulang = '1' )
LALU B_NS <= B_E0;
DATA_INT <= '0';
AK<= '0';
ELSE
KASUS B_CS adalah
KAPAN B_E0 =>
JIKA ( REQ ='1') MAKA B_NS <= B_E1;
LAIN B_NS <= B_E0;
BERAKHIR JIKA;
DATA_INT <= '0';
AK<= '0';
KAPAN B_E1 =>
JIKA ( REQ ='1') MAKA B_NS <= B_E1;
LAIN B_NS <= B_E0;
BERAKHIR JIKA;
DATA_INT <= DATA_IN;
AK<= '1';
KASUS AKHIR;
BERAKHIR JIKA;
AKHIR PROSES B_1;

B_2 : PROSES( ck )
MULAI
JIKA ( ck = '1' DAN BUKAN ck'STABLE )
LALU B_CS <= B_NS;
BERAKHIR JIKA;
AKHIR PROSES B_2;

AKHIR FSM;

CTL CONTOH

-- Contoh file CTL

TIPE A_ETAT_TYPE ADALAH (A_E0, A_E1);
TIPE B_ETAT_TYPE ADALAH (B_E0, B_E1);

VARIABEL A_NS, A_CS : A_ETAT_TYPE;
VARIABEL B_NS, B_CS : B_ETAT_TYPE;

VARIABEL ck : BIT;
VARIABEL data_in : BIT;
VARIABEL data_out : BIT;
VARIABEL reset : BIT;
VARIABEL ack : BIT;
VARIABEL req : BIT;

RESET_COND init1 := (reset='1');
ASSUME ass1 := (reset='0');

mulai

prop1 : EX( ack='1' );
prop2 : AG( req -> AF( ack ) );
prop4 : AU( req='1', ack='1');

akhir;

moka CONTOH

moka -V contoh contoh

Gunakan moka online menggunakan layanan onworks.net