prettyosys

Logic is the art of going wrong with confidence. - Morris Kline

---

The goal of prettyosys is that you just need the hardware description file in VHDL and the property specification file in PSL for verify your hardware. No need of configuration files for every hardware wich you want to verify. No need to descripte of where are your VHDL’s or PSL’s files, the prettyosys searchs recursively for your files in your project. Everything wich you need to do is write you hardware and properties and prettyosys take care of the rest.

---

Instalation

Prettyosys combine yosys, symbiyosys and ghdl to create a easy enviromment to fomal verify and sinthetize your hardware descriptions in VHDL. For now, this haven’t support for Verilog or SystemVerilog and only support Yices how formal verification tool. You need the ghdl-yosys-plugin to sintetize VHDL in yosys tool too.

Requirements

• yosys
• ghdl
• ghdl-yosys-plugin
• symbiyosys
• yices

The easier way to get the requirements is by oss-cad-suite-build

Compile

To compile you need cabal haskell compiler, we recommend to get it by ghcup. When you have a cabal working follow these steps below:

git clone [git@github.com](mailto:git@github.com):rennelou/prettyosys.git

cd prettyosys

cabal build && cabal install

The prettyosys binary will be installed on $HOME/.cabal/bin, we recommend to add this path to yousr$PATH variable on .bashrc file.

---

Getting Staterd

To bootstrap a prettyosys project, everything you need to do is enter in a folder that you want your project and follow these steps below:

prettyosys init

You will see a prettyosys.toml file that contains the config about the project. A src folder with a counter.vhd file wich is the hardware example bootstraped and a vunits folder with counter.psl wich contains properties to formal verify the counter hardware example.

prettyosys verify

And that’s it! Go ahead and types your own projects

Ajustes e melhorias

O projeto ainda está em desenvolvimento e as próximas atualizações serão voltadas nas seguintes tarefas:

• Tarefa 1
• Tarefa 2
• Tarefa 3
• Tarefa 4
• Tarefa 5

💻 Pré-requisitos

Antes de começar, verifique se você atendeu aos seguintes requisitos:

• Você instalou a versão mais recente de <linguagem / dependência / requeridos>
• Você tem uma máquina <Windows / Linux / Mac>. Indique qual sistema operacional é compatível / não compatível.
• Você leu <guia / link / documentação_relacionada_ao_projeto>.

🚀 Instalando <nome_do_projeto>

Para instalar o <nome_do_projeto>, siga estas etapas:

Linux e macOS:

<comando_de_instalação>

Windows:

<comando_de_instalação>

☕ Usando <nome_do_projeto>

Para usar <nome_do_projeto>, siga estas etapas:

<exemplo_de_uso>

Adicione comandos de execução e exemplos que você acha que os usuários acharão úteis. Fornece uma referência de opções para pontos de bônus!

📫 Contribuindo para <nome_do_projeto>

Para contribuir com <nome_do_projeto>, siga estas etapas:

1. Bifurque este repositório.
2. Crie um branch: git checkout -b <nome_branch>.
3. Faça suas alterações e confirme-as: git commit -m '<mensagem_commit>'
4. Envie para o branch original: git push origin <nome_do_projeto> / <local>
5. Crie a solicitação de pull.

Como alternativa, consulte a documentação do GitHub em como criar uma solicitação pull.

🤝 Colaboradores

Agradecemos às seguintes pessoas que contribuíram para este projeto:

Iuri Silva

Mark Zuckerberg

Steve Jobs

😄 Seja um dos contribuidores

Quer fazer parte desse projeto? Clique AQUI e leia como contribuir.

📝 Licença

Esse projeto está sob licença. Veja o arquivo LICENÇA para mais detalhes.

⬆ Voltar ao topo