Bug 1220

Summary: An introduction to Formal Verification of Digital Circuits
Product: Libre-SOC's first SoC Reporter: Cesar Strauss <cestrauss>
Component: ConferencesAssignee: Cesar Strauss <cestrauss>
Status: RESOLVED FIXED    
Severity: enhancement CC: libre-soc-bugs, lkcl
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Linux   
URL: https://fosdem.org/2024/schedule/event/fosdem-2024-2215-an-introduction-to-formal-verification-of-digital-circuits/
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:
Bug Depends on:    
Bug Blocks: 1070    

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