Résumé
Je terminerai d’abord le traitement des circuits cycliques en abordant l’approche sémantique et algorithmique par la logique ternaire (de Kleene et Scott), qui donne une vision sémantique naturelle de la logique Booléenne constructive. Je montrerai qu’un codage simple des valeurs ternaires par des paires de Booléens conduit à un algorithme symbolique de détection de la constructivité d’un circuit cyclique utilisant les BDDs (Binary Decision Diagrams), ainsi qu’à la construction d’un circuit acyclique équivalent. Je monterai enfin comment appliquer un calcul symbolique du même type à la correction constructive d’un circuit séquentiel (avec mémoires) par une exploration temporelle de ses états, ce qui est indispensable en pratique et sera illustré par le traitement des exemples montrés dans les cours précédents. Cela finira ainsi l’étude de la constructivité logique et électrique des circuits en introduisant un jeu du temps entre états successifs en plus du jeu du temps à l’intérieur de chaque état.
Dans une deuxième partie, je présenterai un élégant et efficace synchroniseur mésochrone (horloges de mêmes fréquences à décalage de phase constant) dû à J.-M. Chabloz et Ahmed Hemani (KTH Stockholm), et j’expliquerai brièvement comment le rendre plésiochrone (décalage de phase non constant).
La fin du cours sera consacrée au modèle PTides d’Edward Lee et al., intégré dans le système Ptolemy présenté lors du cours du 19 mars. Ce modèle permet de réaliser simplement des implémentations temps-réel distribuées de programmes complexes en composant des circuits, programmes et réseaux à temps garantis à l’aide d’une méthode élégante de timestamping.
