Black-tie Python: Formal verification with Amaranth

From F-Si wiki
Revision as of 21:21, 28 July 2023 by Admin (talk | contribs) (→‎Downloads)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to navigation Jump to search
Black-tie Python: Formal Verification with Amaranth
  • Speaker(s): Pat Deegan
  • email: patd.fsic@psychogenic.net
  • other information:

Co-founder at Psychogenic Technologies, public videos on a variety of tech topics are available on youtube @psychogenictechnologies.

Downloads

Abstract

Bugs are bad. Bugs breed in design complexity, the dark corners of murky interactions and unintended consequences. We avoid them with clarity and hunt them down with verification tools.

Python and Amaranth aid intelligibility, sim and cover reveal specific courses through the state space. Bounded model checking illuminates the obscure recesses, highlighting sneaky paths,and induction can actually prove correctness. We'll go over examples of all this and introduce some useful tools and techniques along the way.


Software

General information

  • The software has been used in the following projects: Neptune (TinyTapeout 3 project)


References