Bug 1220 - An introduction to Formal Verification of Digital Circuits
Summary: An introduction to Formal Verification of Digital Circuits
Status: RESOLVED FIXED
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Conferences (show other bugs)
Version: unspecified
Hardware: PC Linux
: --- enhancement
Assignee: Cesar Strauss
URL: https://fosdem.org/2024/schedule/even...
Depends on:
Blocks: 1070
  Show dependency treegraph
 
Reported: 2023-11-28 17:15 GMT by Cesar Strauss
Modified: 2024-02-24 21:49 GMT (History)
2 users (show)

See Also:
NLnet milestone: ---
total budget (EUR) for completion of task and all subtasks: 0
budget (EUR) for this task, excluding subtasks' budget: 0
parent task for budget allocation:
child tasks for budget allocation:
The table of payments (in EUR) for this task; TOML format:


Attachments

Note You need to log in before you can comment on or make changes to this bug.
Description Cesar Strauss 2023-11-28 17:15:01 GMT
The idea is to give a little background on how Formal Verification work, the available ecosystem of tools, show some small examples on how to use them, and some practical results from real-life usage.
Comment 1 Cesar Strauss 2024-01-31 00:35:49 GMT
1) Added slides and diagrams to the Wiki

https://git.libre-soc.org/?p=libreriscv.git;a=blob;f=conferences/fosdem2024/fosdem2024_formal/formal.md;h=bf26aa07ef278b469ad37f8f31275d5f0e9f5939;hb=b2a917b33ec26d7178bdf4b85e518a6bbafc3d95

Diagrams:

https://libre-soc.org/conferences/fosdem2024/fosdem2024_formal/

Slide text:

https://libre-soc.org/conferences/fosdem2024/fosdem2024_formal/formal/

Needs Dia and Inkscape to build the PDF.

2) Uploaded the PDF to FOSDEM (see bug URL).

It's mostly done, but only have some basic examples. I'll see if I can add some real-life examples, without going into much detail.
Comment 2 Luke Kenneth Casson Leighton 2024-01-31 04:47:35 GMT
(In reply to Cesar Strauss from comment #1)
> 1) Added slides and diagrams to the Wiki

fantastic.

> 
> https://git.libre-soc.org/?p=libreriscv.git;a=blob;f=conferences/fosdem2024/
> fosdem2024_formal/formal.md;h=bf26aa07ef278b469ad37f8f31275d5f0e9f5939;
> hb=b2a917b33ec26d7178bdf4b85e518a6bbafc3d95

bleugh on the \$ stuff :) i wouldn't worry about trying to make it work with ikiwiki, it is a bit too much for it to handle :)


> Needs Dia and Inkscape to build the PDF.

yes this is pretty standard, for us

> 
> 2) Uploaded the PDF to FOSDEM (see bug URL).

i put it at libre-soc ftp as well, uploaded your ssh key
you should be able to scp ftp@libre-soc.org 

 
> It's mostly done, but only have some basic examples. I'll see if I can add
> some real-life examples, without going into much detail.

nice.
Comment 3 Cesar Strauss 2024-02-24 19:42:48 GMT
* Talk was given on 02/03/2024
* Video presentation is available at FOSDEM 2024 site (see bug URL)
* Final PDF slides are available at the same site
* Also available at: https://ftp.libre-soc.org/fosdem_2024/fosdem2024_formal.pdf
* Source files were updated on the wiki: https://git.libre-soc.org/?p=libreriscv.git;a=tree;f=conferences/fosdem2024/fosdem2024_formal;hb=1f429eeba125e65ba4649045196d043a4acac31d
Comment 4 Luke Kenneth Casson Leighton 2024-02-24 21:49:36 GMT
(In reply to Cesar Strauss from comment #3)
> * Talk was given on 02/03/2024

fantastic cesar, do put in an RFP under bug #1070