文件列表:

INSTALL.md (2722, 2021-02-22)
LICENSE (1075, 2021-02-22)
cpu (0, 2021-02-22)
cpu\Makefile (2421, 2021-02-22)
cpu\alu_data.vhd (3764, 2021-02-22)
cpu\alu_flags.vhd (3797, 2021-02-22)
cpu\axi_pause.vhd (2699, 2021-02-22)
cpu\cpu.png (23928, 2021-02-22)
cpu\cpu.vhd (10000, 2021-02-22)
cpu\cpu_constants.vhd (10168, 2021-02-22)
cpu\decode.vhd (18255, 2021-02-22)
cpu\dp_ram.vhd (1578, 2021-02-22)
cpu\execute.vhd (9484, 2021-02-22)
cpu\microcode.vhd (3392, 2021-02-22)
cpu\prog.asm (179953, 2021-02-22)
cpu\prog_simple.asm (986, 2021-02-22)
cpu\registers.vhd (4262, 2021-02-22)
cpu\system.vhd (2389, 2021-02-22)
cpu\system.xdc (2034, 2021-02-22)
cpu\tb_cpu.gtkw (55586, 2021-02-22)
cpu\tb_cpu.vhd (602, 2021-02-22)
fetch (0, 2021-02-22)
fetch\Makefile (985, 2021-02-22)
fetch\fetch.gtkw (1483, 2021-02-22)
fetch\fetch.psl (7097, 2021-02-22)
fetch\fetch.sby (278, 2021-02-22)
fetch\fetch.vhd (5248, 2021-02-22)
fetch\waveform.png (80227, 2021-02-22)
fetch2 (0, 2021-02-22)
fetch2\Makefile (1115, 2021-02-22)
fetch2\fetch.gtkw (2047, 2021-02-22)
fetch2\fetch.psl (8758, 2021-02-22)
fetch2\fetch.sby (819, 2021-02-22)
fetch2\fetch.vhd (5089, 2021-02-22)
fetch2\waveform.png (43447, 2021-02-22)
... ...

# Formal verification Others have gone here before me, and now it is my turn! [Formal verification](http://zipcpu.com/formal/formal.html) is a tool for verifying the correctness of your implementation. Traditional verification strategies have relied on hand-crafted testbenches to provide stimuli to the DUT. Formal verification aims to automate that process. In my view these two approaches (testbench and formal) supplement each other, rather than replace each other. ## Installing the tools I've written a [separate document](INSTALL.md) with a guide on how to install all the necessary tools. ## Doing formal verification in VHDL To use formal verification with VHDL, we need to learn [a new language PSL](http://www.project-veripage.com/psl_tutorial_1.php). The VHDL file is augmented with verification commands like `assert`, `assume`, and `cover`. Furthermore, the SymbiYosys tools must be started with some additional command line parameters. This is demonstrated in the below examples. ## Example designs using formal verification * [One Stage Fifo](one_stage_fifo/). This is a kind of "hello world" of formal verification. * [One Stage Buffer](one_stage_buffer/). Another simple but useful module. * [Two Stage Fifo](two_stage_fifo/). Small FIFO useful for timing closure. * [Two Stage Buffer](two_stage_buffer/). Small FIFO useful for timing closure. * [Pipe_Concat](pipe_concat/). Concatenate two elastic pipe streams. * [Wishbone memory](wb_mem/). This is to learn about the wishbone bus protocol. * [Fetch](fetch/). The first "real" module. This is a simple instruction fetch module for a CPU. * [Fetch2](fetch2/). A second (more optimized) implementation of the instruction fetch module. ## Example puzzles using formal verification * [Fox, Goat, and Cabbage](fgc). This uses formal verification to solve a well-known puzzle. * [Rubik's 2x2x2](rubik). This uses formal verification to solve Rubik's 2x2x2 cube. ## Other resources * [This video](https://www.youtube.com/watch?v=H3tsP9tjYdY) gives a nice introduction to formal verification, including a lot of small and easy examples. * [This video-series](https://www.youtube.com/watch?v=_5R35QFsXM4) gives a more detailed tutorial for getting started with formal verification. * [Robert Baruch](https://www.youtube.com/watch?v=85ZCTuekjGA) has made a video series on building a 6800 CPU using [nMigen](https://github.com/nmigen/nmigen) and applying formal verification in the process. This was the first time I heard about formal verification, and has been a great inspiration for me. * [Charles LaForest](http://fpgacpu.ca/fpga/index.html) has compiled a huge resource on VHDL design elements. There is no formal verification, but this website is a good resource, with detailed explanation of each module.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：