Conceptions de chisel vérifiées de façon formelle

Cette séance de cours couvre le concept de vérification formelle des conceptions de Chisel à l'aide de solveurs SMT. Il explique Chisel comme un langage de construction matérielle dans Scala, l'utilisation de résolveurs SMT pour prouver les propriétés de conception matérielle, et des exemples comme les affirmations retardées et les preuves par induction sur l'état. Il s'inscrit également dans la vérification formelle des protocoles de communication comme AXI4, soulignant l'importance des invariants de boucle, des conditions préalables et des postconditions dans la conception des circuits numériques.