Este repositório contém uma especificação formal da arquitetura RISC-V, escrita em vela. Foi adotado pela Fundação RISC-V.
O modelo especifica formatos de linguagem de montagem das instruções, os codificadores e decodificadores correspondentes e a semântica de instruções. Um guia de leitura para o modelo é fornecido no doc/ subdiretório, juntamente com um guia sobre como estender o modelo.
As definições de látex ou asciidoc podem ser geradas a partir do modelo adequado para inclusão na documentação de referência. Há também o suporte de documentação do ASCIIDOCOR mais recente para o RISC-V.
Sail é um idioma para descrever a semântica da arquitetura do conjunto de instruções (ISA) dos processadores: a especificação arquitetônica do comportamento das instruções da máquina. O Sail é um idioma amigável ao engenheiro, assim como o Pseudocode do fornecedor anterior, mas mais com precisão e com ferramentas para suportar uma ampla gama de casos de uso.
Dada uma especificação de vela, a ferramenta pode digitar-a, gerar trechos de documentação (no LATEX ou ASCIIDOC), gerar emuladores executáveis, mostrar cobertura de especificação, gerar versões do ISA para ferramentas de modelo de memória relaxadas, suportar geração de testes de sequência de instruções automatizadas, Gere definições de provenção teorema para prova interativa (em Isabelle, Hol4 e Coq), apoie a prova sobre o código binário (em Islaris) e (em andamento) gera um modelo de referência ISA no SystemVerilog que pode ser usado para verificação formal de hardware.
Sail está sendo usado para várias descrições de ISA, incluindo versões essencialmente completas do comportamento seqüencial do ARM-A (derivado automaticamente da especificação armantenista autoritária e liberada sob uma licença clara de BSD com permissão do ARM), RISC-V, Cheri- Risc-V, Cheriot, Mips e Cheri-MIPs; Tudo isso é completo o suficiente para inicializar vários sistemas operacionais. Também existem modelos de vela para fragmentos menores de energia IBM e x86, incluindo uma versão do modelo ACL2 X86 traduzido automaticamente disso.
Instale a vela. No Linux, você pode baixar um lançamento binário (fortemente recomendado), ou pode instalar a partir da fonte usando o Opam. Então:
$ make
criará o simulador em c_emulator/riscv_sim_RV64 .
Se você receber uma mensagem de erro dizendo sail: unknown option '--require-version'. É porque o seu compilador de vela é muito velho. Você precisa da versão 0.18 ou posterior.
Pode -se construir o modelo Rv32 ou Rv64 especificando ARCH=RV32 ou ARCH=RV64 na linha make e usando o sufixo de destino correspondente. O Rv64 é construído por padrão, mas o modelo Rv32 pode ser construído usando:
$ ARCH=RV32 make
que cria o simulador em c_emulator/riscv_sim_RV32 .
Os alvos makefile riscv_isa_build , riscv_coq_build e riscv_hol_build invocam o respectivo prover para processar as definições e produzir o modelo ISABELLE em generated_definitions/isabelle generated_definitions/coq/RV64/riscv.v generated_definitions/isabelle/RV64/Riscv.thy , o modelo de coq em generated_definition Modelo em generated_definitions/hol4/RV64/riscvScript.sml respectivamente. Testamos Isabelle 2018, Coq 8.8.1 e Hol4 Kananaskis-12. Ao construir essas metas, verifique se as bibliotecas de provérbios correspondentes no diretório da vela ( $SAIL_DIR/lib/$prover ) estão atualizadas e construídas, por exemplo, executando make nesses diretórios.
O simulador pode ser usado para executar pequenos binários de teste.
$ ./c_emulator/riscv_sim_<arch> <elf-file>
Um conjunto de programas de teste Rv32 e Rv64 derivados do teste de riscv-tests é incluído no teste de teste/riscv/. A suíte de teste pode ser executada usando test/run_tests.sh .
As informações sobre as opções de configuração para o simulador estão disponíveis em ./c_emulator/riscv_sim_<arch> -h .
Algumas opções úteis são: Configurando se os acessos desalinhados armam ( --enable-misaligned ) e se a tabela de páginas Atualiza os bits PTE ( --enable-dirty-update ).
Para inicializar imagens do sistema operacional, consulte as informações sob o OS-Boot/ Subdirectory.
Raramente, a versão de lançamento do SAIL pode não atender às suas necessidades. Isso pode acontecer se você precisar de uma correção de bugs ou um novo recurso ainda não na versão de vela lançada, ou estiver trabalhando ativamente na vela. Nesse caso, você pode dizer ao sail-riscv Makefile para usar uma cópia local do SAIL, estabelecendo SAIL_DIR para a raiz de uma compra do repositório da vela quando você invocar make . Como alternativa, você pode usar opam pin para instalar a Sail a partir de uma finalização da compra local do repositório de vela, conforme descrito nas instruções de instalação da vela.
Estes são trechos literalmente do arquivo de modelo que contém as instruções básicas, riscv_insts_base.sail, com alguns comentários adicionados.
/* the assembly abstract syntax tree (AST) clause for the ITYPE instructions */
union clause ast = ITYPE : (bits(12), regidx, regidx, iop)
/* the encode/decode mapping between AST elements and 32-bit words */
mapping encdec_iop : iop <-> bits(3) = {
RISCV_ADDI <-> 0b000,
RISCV_SLTI <-> 0b010,
RISCV_SLTIU <-> 0b011,
RISCV_ANDI <-> 0b111,
RISCV_ORI <-> 0b110,
RISCV_XORI <-> 0b100
}
mapping clause encdec = ITYPE(imm, rs1, rd, op) <-> imm @ rs1 @ encdec_iop(op) @ rd @ 0b0010011
/* the execution semantics for the ITYPE instructions */
function clause execute (ITYPE (imm, rs1, rd, op)) = {
let rs1_val = X(rs1);
let immext : xlenbits = sign_extend(imm);
let result : xlenbits = match op {
RISCV_ADDI => rs1_val + immext,
RISCV_SLTI => zero_extend(bool_to_bits(rs1_val <_s immext)),
RISCV_SLTIU => zero_extend(bool_to_bits(rs1_val <_u immext)),
RISCV_ANDI => rs1_val & immext,
RISCV_ORI => rs1_val | immext,
RISCV_XORI => rs1_val ^ immext
};
X(rd) = result;
RETIRE_SUCCESS
}
/* the assembly/disassembly mapping between AST elements and strings */
mapping itype_mnemonic : iop <-> string = {
RISCV_ADDI <-> "addi",
RISCV_SLTI <-> "slti",
RISCV_SLTIU <-> "sltiu",
RISCV_XORI <-> "xori",
RISCV_ORI <-> "ori",
RISCV_ANDI <-> "andi"
}
mapping clause assembly = ITYPE(imm, rs1, rd, op)
<-> itype_mnemonic(op) ^ spc() ^ reg_name(rd) ^ sep() ^ reg_name(rs1) ^ sep() ^ hex_bits_signed_12(imm)
union clause ast = SRET : unit
mapping clause encdec = SRET() <-> 0b0001000 @ 0b00010 @ 0b00000 @ 0b000 @ 0b00000 @ 0b1110011
function clause execute SRET() = {
let sret_illegal : bool = match cur_privilege {
User => true,
Supervisor => not(extensionEnabled(Ext_S)) | mstatus[TSR] == 0b1,
Machine => not(extensionEnabled(Ext_S))
};
if sret_illegal
then { handle_illegal(); RETIRE_FAIL }
else if not(ext_check_xret_priv (Supervisor))
then { ext_fail_xret_priv(); RETIRE_FAIL }
else {
set_next_pc(exception_handler(cur_privilege, CTL_SRET(), PC));
RETIRE_SUCCESS
}
}
mapping clause assembly = SRET() <-> "sret"
O modelo constrói um emulador C que pode executar arquivos RISC-V ELF, e os dois emuladores fornecem suporte de plataforma suficiente para inicializar Linux, FreeBSD e SEL4. O emulador C pode ser vinculado ao emulador de pico para execução com verificação em tandem por instrução.
O emulador C, para a bota Linux, atualmente é executado em aproximadamente 300 kips em um Intel i7-7700 (quando o rastreamento detalhado por instrução está desativado), e há muitas oportunidades para otimização futura (o modelo SAIL MIPS é executado em aproximadamente 1 mips ). Isso permite inicializar o Linux em cerca de 4 minutos e o FreeBSD em cerca de 2 minutos. O uso da memória para o emulador C ao inicializar o Linux é de aproximadamente 140 MB.
Os arquivos no diretório do emulador C implementa o carregamento de ELF e os dispositivos da plataforma, define o mapa de memória física e usa opções de linha de comando para selecionar opções de ISA específicas para implementação.
O emulador C gerado por vela pode medir a cobertura da filial de especificação de quaisquer testes executados, exibindo os resultados como tabelas por arquivo e versões indicadas por HTML da fonte do modelo.
Para verificação em tandem de fluxos de instruções aleatórias, as ferramentas suportam os protocolos usados no testrig para injetar diretamente as instruções no emulador C e produzir informações de rastreamento no formato RVFI. Isso foi usado para testes cruzados contra o Spike e a especificação do RVBS escrita no Bluespec SystemVerilog.
O emulador C também pode estar diretamente ligado ao Spike, que fornece verificação em tandem em binários de elfos (incluindo botas do sistema operacional). Isso geralmente é útil para depurar problemas de inicialização do sistema no modelo quando a bota é conhecida trabalhando no Spike. Também é útil detectar opções de implementação específicas da plataforma em pico que não são exigidas pela especificação ISA.
O modelo ISA é integrado ao modelo operacional do modelo de memória relaxado RISC-V, RVWMO (conforme descrito em um apêndice da especificação de nível de usuário RISC-V), que é um dos modelos de referência usados no desenvolvimento do RISC -V Arquitetura de concorrência; Isso faz parte da ferramenta RMEM. Também é integrado ao modelo de concorrência axiomático RISC-V como parte da ferramenta ISLA-Axiomatic.
Como parte do trabalho de arquitetura de concorrência da Universidade de Cambridge/ Inria, esses grupos produziram e divulgaram uma biblioteca de aproximadamente 7000 testes de decisões. Os modelos de concorrência operacional e axiomático de RISC-V estão sincronizados para esses testes e, além disso, concordam com o comportamento arquitetado do ARM correspondente para os testes em comum.
Esses testes também foram executados em hardware RISC-V, em uma placa proto Multicore RISC-V FU540 SIFIVE (Liberdade desencadeada), gentilmente emprestada pela Imperas. Até o momento, apenas o comportamento sequencialmente consistente foi observado lá.
O SAIL visa apoiar a geração de definições de provador de teorema idiomático em várias ferramentas. Atualmente, ele suporta Isabelle, Hol4 e Coq, e o diretório prover_snapshots fornece instantâneos das definições de provador de teorema gerado.
Essas traduções do teorema podem atingir várias mônadas para diferentes fins. O primeiro é uma mônada de estado com não determinismo e exceções, adequado para o raciocínio em um ambiente seqüencial, assumindo que expressões eficazes são executadas sem interrupções e com acesso exclusivo ao estado.
Para o raciocínio sobre simultaneidade, onde as instruções executam fora de ordem, especulativa e não atomicamente, há uma mônada gratuita sobre um tipo de dados de efeito de ações de memória. Esta mônada também é usada como parte do suporte de simultaneidade acima mencionado através da ferramenta RMEM.
Os arquivos sob handwritten_support fornecem definições da biblioteca para Coq, Isabelle e Hol4.
sail-riscv
- model // Sail specification modules
- generated_definitions // files generated by Sail, in RV32 and RV64 subdirectories
- c
- lem
- isabelle
- coq
- hol4
- latex
- prover_snapshots // snapshots of generated theorem prover definitions
- handwritten_support // prover support files
- c_emulator // supporting platform files for C emulator
- doc // documentation, including a reading guide
- test // test files
- riscv-tests // snapshot of tests from the riscv/riscv-tests github repo
- os-boot // information and sample files for booting OS images
O modelo é disponibilizado sob a licença de duas cláusulas do BSD na licença.
Originalmente escrito por Prashanth Mundkur na SRI International e desenvolvido por outros, especialmente pesquisadores da Universidade de Cambridge.
Consulte LICENCE e o GIT CLAMA por uma lista completa de autores.
Este software foi desenvolvido pelo projeto acima no projeto de engenharia rigoroso do Mainstream Systems (REMS), parcialmente financiado pelo EPSRC Grant EP/K008528/1, nas universidades de Cambridge e Edimburgo.
Este software foi desenvolvido pela SRI International e pelo Laboratório de Computação da Universidade de Cambridge (Departamento de Ciência da Computação e Tecnologia) sob contrato DARPA/AFRL FA8650-18-C-7809 ("CIFV"), e sob contrato DARPA HR0011-18-C- 0016 ("ECATS") como parte do Programa de Pesquisa Darpa Ssith.
Este projeto recebeu financiamento do Conselho Europeu de Pesquisa (ERC) sob o Programa de Pesquisa e Inovação Horizon 2020 da União Europeia (Contrato de Grant 789108, Elver).
