moka - Online na nuvem

PROGRAMA:

NOME

MOKA - Ancestral verificador de modelo

SINOPSE

ágata [-VDB] nome_do_arquivofsm nome_arquivo_ctl

DESCRIÇÃO

ágata é um verificador de modelo CTL.

Feito para rodar em descrições FSM ou RTL, ágata suporta o mesmo subconjunto VHDL que syf ou boom
(para mais informações sobre este subconjunto veja SYF(1) BOOM(1) FSM(5) VBE(5)).
mesmo assim ágata impõe que cada registro da descrição comportamental tenha o mesmo
condição de clock e que não há barramentos tristate ou multiplexados. Em particular VHDL
tipo MUX_BIT e WOR_BIT não são suportados.
Em primeiro lugar ágata construir a transição de função do FSM usando um binário ordenado reduzido
Representação de Diagramas de Decisão.
Em seguida, aplica as condições iniciais para encontrar o primeiro estado (palavra-chave INITIAL e/ou
RESET_COND no CTL(5) formato de arquivo).
Depois calcula uma simulação simbólica do FSM para encontrar todos os estados alcançáveis.
Este cálculo leva em consideração as condições de suposições (palavra-chave ASSUME no
CTL(5) formato de arquivo).
ágata finalmente verifica uma por uma cada fórmula CTL. (ver CTL(5) para formato de arquivo CTL
detalhes).

CTL OPERADORES

Para cada subexpressão CTL ágata retornará o conjunto de estados que verifica a fórmula.
Por exemplo EX(p) retornará o conjunto de estados alcançáveis ​​que verifica EX(p).
Operadores CTL:
EX(p): retorna todos os estados que possuem quase um sucessor de estado primário que
verifica p.
EU(p,q) : retorna todos os estados que são a raiz de quase um caminho, tal que p is
verdade até q é sempre verdade.
EG(p): retorna todos os estados que são a raiz de quase um caminho, tal que p is
sempre verdade.
AX(p): retorna todos os estados que possuem todos os seus sucessores de estado primário que
verifica p.
AU(p,q) : retorna todos os estados que são a raiz apenas dos caminhos dos quais p é verdade
até q é sempre verdade.
AG(p): retorna todos os estados que são raiz apenas de caminhos, de modo que p é sempre
verdadeiro.

MEIO AMBIENTE VARIÁVEIS

MBK_WORK_LIB fornece o caminho para a descrição e o arquivo CTL. o valor padrão é
o diretório atual.

MBK_CATA_LIB fornece alguns caminhos auxiliares para as descrições e o arquivo CTL. O
o valor padrão é o diretório atual.

OPÇÕES

-V Ativa o modo detalhado. Cada etapa da verificação do modelo é exibida no padrão
saída.

-D Ativa o modo de depuração. Cada etapa da verificação do modelo é detalhada na saída padrão.
Em particular, todos os estados definidos são exibidos para cada subexpressão CTL.

-B O arquivo de entrada é uma descrição VHDL usando o subconjunto Alliance VHDL (consulte VBE(5) arquivo
formato).

FSM EXEMPLO

- Um exemplo multifsm

O exemplo de ENTIDADE é
PORT
(
ck: em BIT;
dados_in: em BIT;
redefinir: em BIT;
data_out: saída BIT
);
Exemplo de FIM;

ARQUITETURA FSM OF exemplo é

TIPO A_ETAT_TYPE É (A_E0, A_E1);
SINAL A_NS, A_CS: A_ETAT_TYPE;

TIPO B_ETAT_TYPE É (B_E0, B_E1);
SINAL B_NS, B_CS: B_ETAT_TYPE;

--PRAGMA CURRENT_STATE A_CS FSM_A
--PRAGMA NEXT_STATE A_NS FSM_A
--PRAGMA CLOCK ck FSM_A
--PRAGMA PRIMEIRO_ESTADO A_E0 FSM_A

--PRAGMA ESTADO_ATUAL B_CS FSM_B
--PRAGMA NEXT_STATE B_NS FSM_B
--PRAGMA CLOCK ck FSM_B
--PRAGMA PRIMEIRO_ESTADO B_E0 FSM_B

SINAL ACK, REQ, DATA_INT: BIT;

INÍCIO

A_1: PROCESSO (A_CS, ACK)
INÍCIO
SE (redefinir = '1')
ENTÃO A_NS <= A_E0;
DADOS_OUT <= '0';
REQ <= '0';
ELSE
CASO A_CS é
QUANDO A_E0 =>
SE (ACK ='1') ENTÃO A_NS <= A_E1;
OUTRO A_NS <= A_E0;
END IF;
DADOS_OUT <= '0';
REQ <= '1';
QUANDO A_E1 =>
SE (ACK ='1') ENTÃO A_NS <= A_E1;
OUTRO A_NS <= A_E0;
END IF;
DADOS_OUT <= DADOS_INT;
REQ <= '0';
TERMINAR CASO;
END IF;
FINALIZAR PROCESSO A_1;

A_2: PROCESSO(ck)
INÍCIO
SE (ck = '1' E NÃO ck'ESTÁVEL)
ENTÃO A_CS <= A_NS;
END IF;
FINALIZAR PROCESSO A_2;

-------

B_1: PROCESSO (B_CS, ACK)
INÍCIO
SE (redefinir = '1')
ENTÃO B_NS <= B_E0;
DADOS_INT <= '0';
ACK <= '0';
ELSE
CASO B_CS é
QUANDO B_E0 =>
SE (REQ ='1') ENTÃO B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DADOS_INT <= '0';
ACK <= '0';
QUANDO B_E1 =>
SE (REQ ='1') ENTÃO B_NS <= B_E1;
ELSE B_NS <= B_E0;
END IF;
DADOS_INT <= DADOS_IN;
ACK <= '1';
TERMINAR CASO;
END IF;
FINALIZAR PROCESSO B_1;

B_2: PROCESSO(ck)
INÍCIO
SE (ck = '1' E NÃO ck'ESTÁVEL)
ENTÃO B_CS <= B_NS;
END IF;
FINALIZAR PROCESSO B_2;

FIM FSM;

CTL EXEMPLO

-- Um exemplo de arquivo CTL

TIPO A_ETAT_TYPE É (A_E0, A_E1);
TIPO B_ETAT_TYPE É (B_E0, B_E1);

VARIÁVEL A_NS, A_CS: A_ETAT_TYPE;
VARIÁVEL B_NS, B_CS: B_ETAT_TYPE;

VARIÁVEL ck: BIT;
VARIÁVEL data_in: BIT;
VARIÁVEL data_out: BIT;
Reinicialização de VARIÁVEL: BIT;
VARIÁVEL confirmação: BIT;
VARIÁVEL requerida: BIT;

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

começar

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

end;

MOKA EXEMPLO

exemplo de exemplo moka -V

Use moka online usando serviços onworks.net