Examine la vérification formelle des conceptions de Chisel à l'aide de résolveurs SMT et couvre des exemples tels que les assertions différées et les preuves par induction.
Introduit Iris, un cadre logique pour raisonner sur la sécurité et l'exactitude des programmes impératifs d'ordre supérieur simultanés, en mettant l'accent sur ses caractéristiques et applications uniques.
