format.py

import fileinput

width = 640//16
height = 480//16
lineno = 0

for line in fileinput.input():
    if line.startswith("# vim:"): continue
    if line.startswith("-"):
        fill = height-(lineno%height)
        empty = " "*width + "\n"
        print(empty*fill, end='')
        lineno += fill
    elif line.startswith("#"):
        print(line[1:].strip().upper().center(width))
        lineno += 1
    else:
        print(line.rstrip().ljust(width))
        lineno += 1

fill = height-(lineno%height)
empty = " "*width + "\n"
print(empty*fill, end='')

mem.py

import fileinput

width = 640//16
height = 480//16
lineno = 0

for line in fileinput.input():
    for i, char in enumerate(line[:-1]):
        if i%2:
            print(format(ord(char), '08b'))
        else:
            print(format(ord(char), '08b'), end='')

presentation.txt

# vim: tw=40 cc=40










# Open Source
# Formal Verification
# in VHDL

# by

# Pepijn de Vos

# ORConf 2019

---

# Who am I?


Blog:    http://pepijndevos.nl
Twitter: @pepijndevos

2008 Wishful Coding
     Self-taught web developer

2012 Recurse Center
     Awesome coding retreat

2013 Freenom
     Python developer

2015 University of Twente
     Bsc Electrical Engineering
     Msc Integrated Circuit Design

Now:
     7400 CPU

     Hacking on GHDL

     Internship at Symbiotic EDA
     Documenting Gowin FPGA bitstream

p.s. looking for things after graduation
---

# All the pieces involved

 * Yosys - Synthesis
 * Nextpnr - Place and Route
 * SymbiYosys - Formal verification
 * GHDL - VHDL simulator

Synthesis:

HDL -> netlist -> bitstream
     ^ Yosys    ^ Nextpnr

Formal Verification:

HDL -> netlist -> SMT
     ^ Yosys    ^ SymbiYosys

Yosys frontends:

 * verilog (built-in)
 * Verific (commercial, SV, VHDL)
 * GHDL <-- NEW, WIP

---

# GHDL

"GHDL is an open-source simulator for
the VHDL language. GHDL fully supports
the 1987, 1993, 2002 versions of the
IEEE 1076 VHDL standard, and partially
the latest 2008 revision."

 * Very mature, Tristan Gingold has
   been working on it for decades.

 * Better VHDL-2008 support than even
   most commercial tools.

 * Written in Ada. Obscure but very
   similar to VHDL.

 * Support for synthesis <-- NEW, WIP

# ghdlsynth-beta

Experimental frontend plugin for Yosys
that converts VHDL to RTLIL <-- NEW, WIP

$ yosys -m ghdl
> ghdl file.vhd -e module
> synth_gowin -vout bitstream.v

---

# GHDL synthesis status

What works:

 * Most things
 * PSL! (used in formal verification)

What does not work:

 * Functions -- update: supported now
 * Memory inference
 * Some uncommon constructs
 * Operators on odd type combos
 * ...

Bottom line:

 * Large existing projects are not
   likely to work YET.
 * Writing new code using supported
   constructs is feasible, such as...

# Formally verified CPU

 * Synthesized using GHDL+Yosys
 * Formally verified using SymbiYosys
 * Less than 100 7400 logic chips
 * Currently running this presentation
---

# What is formal verification?

Property testing with a SMT solver.

Think Quickcheck not Coq.

 1. Make assumptions about valid inputs

 2. Assert properties that should hold

 3. SMT solver tries to break asserts





# What is PSL?

Property Specification Language.

Extension language that provides assert,
assume, restrict, cover keywords.

Also, sequences for properties in time.

Usually in special comments. Natively
supported in VHDL-2008, and GHDL.

---

# An example

The bit-serial ALU of my CPU

process(opcode, a, b, ci)
begin
  case opcode is
    when "000" => -- add
      y <= a xor b xor ci; -- output
      co <= (a and b)      -- carry
         or (a and ci)
         or (b and ci);
      cr <= '0'; -- carry reset value
    [...]
  end case;
end process;

process(clk, rst_n)
begin
  if(rising_edge(clk)) then
    if(rst_n = '0') then
      ci <= cr; -- reset the carry
    else
      ci <= co; -- forward carry
    end if;
  end if;
end process;
---

# An example

Restrict valid reset inputs to
011111111011111111...


restrict { {rst_n = '0';
           (rst_n = '1')[*8]}[+]};


Specify that when the ALU is active, the
opcode will stay constant.


assume always {rst_n='0'; rst_n='1'} |=>
  opcode = last_op until rst_n = '0';


Assert that at reset after 8 bits, the
accumulated inputs produces the expected
outputs.


addition: assert always
{opcode = "000" and rst_n = '1';
 rst_n = '0'} |-> y_sr = a_sr+b_sr;
---

# An example

Add .sby file:

[options]
mode bmc
depth 20

[engines]
smtbmc z3

[script]
ghdl --std=08 alu.vhd -e alu
prep -top alu

[files]
alu.vhd

Run it:

$ sby --yosys "yosys -m ghdl" -f alu.sby
BMC failed!
Assert failed in alu: addition
---

# an example

opcode XOR x SUB                   x ADD
 rst_n ____/~~~~~~~~~~~~~~~~~~~~~~~\____
    ci ~~~~\__/~~\_____/~~~~~~~~~~~\____
    cr ____/~~~~~~~~~~~~~~~~~~~~~~~\____
  a_sr 0   x==x==x==x==x==x==x==x==x 29
  b_sr 0   x==x==x==x==x==x==x==x==x 150
  y_sr 0   x==x==x==x==x==x==x==x==x-122

29-150=-121! Off by one!

XOR on the cycle before SUB causes
carry reset to be 0 rather than 1!

The power of formal: find edgecases!


Solution 1: combinatorial reset

ci <= cr when first = '1' else cip;


Solution 2: opcode stable before reset

assume always {rst_n='0'; rst_n='1'} |->
  opcode = last_op until rst_n = '0';

---

# Conclusion



GHDL synthesis support is growing fast!
I hope you check it out (and contribute)



Formal verification is an easy and
powerful way to test your code.

See also:
Formally Verifying AXI Interfaces
by Dan Gisselquist



Come talk to me for more info.



Drink more water,
be excellent to each other ;)

---

# thank you!








         (@@@@) (   ) (@@@) (  ) (@@)
     (    )
     ++      +------
     ||      |+-+ | ____
   /---------|| | | |   \@@@@@@@@@@     
  + ========  +-+ | |    \@@@@@@@@@@@@_ 
 _|--O========O~\-+ |________________ | 
//// \_/      \_/      (O)      (O)    






    Blog: http://pepijndevos.nl
 Twitter: @pepijndevos
 
    GHDL: https://github.com/ghdl/ghdl