18 / 37 · Verificação

Verificação de projeto: limites de largura, prioridade e retorno

Resolva fronteiras e controles simultâneos a partir de uma especificação de transição.

Contrato do contador módulo 10

Para count unsigned^{unsigned Interpretação de uma sequência de bits como inteiro não negativo. Com n bits, o intervalo é de 0 a 2^n−1; pode diferir da interpretação signed dos mesmos bits. Saiba mais} de quatro bits, a prioridade é reset, enable e manutenção. Reset=1 leva a 0; caso contrário, enable=1 retorna a 0 a partir de 9 ou mais e incrementa os demais estados.

N=\lceil\log_2 10\rceil=4

Quatro bits armazenam 16 estados; não implementam automaticamente o requisito de usar dez. Em particular, count=9 com enable=0 deve ser mantido.

Cada coluna registra uma borda de subida^{Borda de subida Instante em que o clock passa de 0 para 1. É diferente do nível alto, que abrange todo o intervalo com CLK=1. Saiba mais}. Entradas são anteriores e «depois» indica estado atualizado. O alinhamento ordena amostras, não desenha propagação física^{Atraso de propagação Tempo entre uma mudança de entrada e a estabilização da saída no valor correto. Equivalência lógica e comportamento temporal são propriedades distintas. Saiba mais}. Partindo de count=9, a primeira coluna sem reset e com enable=0 mantém 9; a seguinte, com enable=1, retorna a 0.

A manutenção deve ocorrer também na fronteira

Ver os dados da forma de onda

Dados da forma de onda: cada caractere é um intervalo; um ponto mantém o estado anterior; p representa um ciclo de clock.
Sinal	Forma de onda	Valores do barramento
borda	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count depois	`23.4`	9 → 0 → 1

Problemas adicionais

Calcule o próximo valor com count=9, reset=0, enable=0.
Explique a recuperação a partir de count=15 com enable=1.
Especifique se deve sair um pulso de término com count=9, reset=1, enable=1, supondo saída 0 durante reset^{Reset Controle que retorna o estado a um valor inicial especificado. É preciso definir se é síncrono ou assíncrono e sua prioridade em relação a outros controles. Saiba mais}.

Experimente

Quantas transições de um passo são necessárias para testar todos os count de 0–15 e combinações reset/enable? Isso demonstra automaticamente todos os requisitos de sequências longas?

Ler a explicação

São $16\times2\times2=64$ . Se count representa todo o estado e as funções de transição e saída estão especificadas corretamente, testar cada passo fornece evidência forte. Não demonstra requisitos omitidos, como inicialização, hipóteses de entrada, estado adicional do pulso de término ou temporização física.

Com count=9, reset=1 e enable=1 são capturados simultaneamente. Quais count e pulso de término seguem conforme a prioridade de reset?

Escolha uma respostacount=0, pulso de término=1: trata-se como retorno normal.count=10, pulso de término=0: enable tem prioridade.count=0, pulso de término=0: reset inicializa tanto o estado quanto o pulso.