Verificare reti logiche e automi con Python

All'esame si lavora a mano, ma negli esercizi conviene controllare i risultati con un programma: tabelle di verità, minimizzazione, equivalenza di espressioni, simulazione di automi. Gli esempi qui sotto sono stati eseguiti e le uscite riportate sono quelle reali. Servono Python 3 e il pacchetto sympy.

Tabella di verità di una funzione

from itertools import product

def tabella(f, n):
    for bits in product([0, 1], repeat=n):          # tutte le 2**n combinazioni
        print(*bits, int(f(*bits)))

f = lambda a, b, c: (a and not b) or (b and c)      # F = A B' + B C
tabella(f, 3)

Uscita: la funzione vale $1$ per $011,100,101,111$, cioè $F=\sum m(3,4,5,7)$ (è l'esempio di Forme canoniche - mintermini, maxtermini, SOP e POSUn mintermine è un prodotto che contiene una e una sola volta tutte le variabili (dirette o negate) e vale 1 su una sola riga della tabella di verità; un maxtermine è la somma duale e vale 0 su una sola riga; con $n$ variabili ci sono $2^n$ mintermini e $2^n$ maxtermini, e $\overline{m_i}=M_i$. Forma canonica SOP = somma dei mintermini delle righe con $F=1$; POS = prodotto dei maxtermini delle righe con $F=0$. Le forme canoniche si ricavano sempre dalla tabella ma sono ridondanti: servono come punto di partenza per la minimizzazione. SOP e POS si realizzano con circuiti a due livelli.Forme canoniche - mintermini, maxtermini, SOP e POS →).

Minimizzazione con sympy

Definizione (SOPform e POSform). SOPform e POSform calcolano la forma minima da un elenco di mintermini (e, facoltativamente, di don't care), come farebbe una mappa di Karnaugh (Mappe di Karnaugh - implicanti e copertura minimaLa mappa di Karnaugh è la tabella di verità disposta in una griglia con righe e colonne in codice Gray, così che celle adiacenti (anche tra bordi opposti) differiscano in una sola variabile. Si raggruppano gli 1 in rettangoli di $2^k$ celle: ogni gruppo elimina $k$ variabili e dà un prodotto. Implicante primo = gruppo massimo; essenziale = unico a coprire un mintermine; la copertura minima contiene tutti gli essenziali più il minimo di altri primi (può non essere unica). Efficace fino a 4 variabili.Mappe di Karnaugh - implicanti e copertura minima →). Le variabili si elencano dalla più significativa alla meno significativa:

from sympy import symbols
from sympy.logic.boolalg import SOPform, POSform

d, c, b, a = symbols('d c b a')                      # d = MSB, a = LSB
print(SOPform([d, c, b, a], minterms=[0, 1, 2, 3, 4, 5, 7, 14, 15]))
print(POSform([d, c, b, a], minterms=[0, 1, 2, 3, 4, 5, 7, 14, 15]))
print(SOPform([d, c, b, a], minterms=[1, 2, 3, 5, 7], dontcares=list(range(10, 16))))

Esempio. SOPform([b, a], minterms=[1, 2, 3]) restituisce a | b, cioè $F=\sum m(1,2,3)=A+B$.

Uscite:

• $\overline d\,a+b\,c\,d+\overline b\,\overline d+\overline c\,\overline d$ (SOP minima di $\sum m(0,1,2,3,4,5,7,14,15)$);
• $(\overline d+b)(\overline d+c)(d+\overline b+\overline c+a)$ (la POS corrispondente);
• $a\,\overline d+b\,\overline c$ per la funzione "cifra BCD uguale a $1,2,3,5,7$" con $10$–$15$ don't care (Mappe di Karnaugh - POS, condizioni di don't care e paritàPer la POS minima si raggruppano gli 0 della mappa, si ottiene la SOP minima di $\overline F$ e si scrive $F$ come prodotto di somme (variabile diretta se vale 0 nel gruppo, negata se vale 1). Le condizioni di don't care (X) sono combinazioni di ingresso che non si presentano o la cui uscita è indifferente: si usano come 1 o come 0 a seconda di quel che allarga i gruppi (mai raggruppamenti fatti solo di X). Le funzioni XOR a più variabili (disparità) e XNOR (parità) hanno mappa a scacchiera: non si semplificano con i gruppi.Mappe di Karnaugh - POS, condizioni di don't care e parità →).

Quando le coperture minime non sono uniche SOPform ne restituisce una sola: per elencarle tutte servono le mappe (o un programma che implementi Quine-McCluskey con il metodo di Petrick).

Equivalenza di due espressioni

Definizione (equivalenza di due espressioni con sympy). Due espressioni sono equivalenti se non esiste una combinazione di ingressi in cui differiscono:

from sympy import symbols, Not, Equivalent
from sympy.logic.inference import satisfiable

x, y, z = symbols('x y z')
e1 = (x & y) | (~x & z) | (y & z)
e2 = (x & y) | (~x & z)
print(satisfiable(Not(Equivalent(e1, e2))))          # False  -> equivalenti (teorema del consenso)

Esempio. satisfiable(Not(Equivalent(x | (x & y), x))) restituisce False: $x+xy=x$ (assorbimento).

False significa che la negazione dell'equivalenza non è mai vera. È il controllo da fare dopo ogni semplificazione algebrica (Algebra di Boole - assiomi, teoremi e complemento di una funzioneL'algebra di Boole opera su variabili a due valori con AND, OR, NOT. Identità fondamentali (neutro, idempotenza, complemento, commutativa, associativa, distributiva in entrambe le forme), dualità (si scambiano AND/OR e 0/1), De Morgan $\overline{X+Y}=\overline X,\overline Y$, assorbimento $X+XY=X$, $X+\overline XY=X+Y$, adiacenza $XY+X\overline Y=X$, consenso $XY+\overline XZ+YZ=XY+\overline XZ$. Si dimostrano per induzione perfetta (tabella) o algebricamente. Il complemento di una funzione si ottiene con De Morgan o con duale + negazione dei letterali. Costo: numero di letterali o di ingressi delle porte.Algebra di Boole - assiomi, teoremi e complemento di una funzione →).

Simulare una macchina a stati finiti

Una macchina di Mealy si descrive con un dizionario che associa a ogni coppia (stato, ingresso) la coppia (stato futuro, uscita). Qui il riconoscitore di $1101$ (Sintesi delle reti sequenziali - riconoscitore di sequenza e codifica degli statiSintesi di una rete sequenziale sincrona: specifiche $\to$ diagramma degli stati $\to$ tabella (riduzione degli stati equivalenti) $\to$ codifica binaria degli stati $\to$ scelta del FF (D PET) $\to$ equazioni di ingresso dei FF e delle uscite $\to$ minimizzazione $\to$ circuito e verifica. Lo stato riassume la parte di storia utile; per i riconoscitori si ha uno stato per ogni prefisso riconosciuto, riusando gli stati (sovrapposizioni). Reset: stato iniziale noto. Codifica Gray (numero minimo di FF) vs 1-hot (un FF per stato, logica più semplice): per il riconoscitore 1101 Gray costa circa la metà.Sintesi delle reti sequenziali - riconoscitore di sequenza e codifica degli stati →):

def esegui(fsm, stato0, ingressi):
    stato, uscite = stato0, []
    for x in ingressi:
        stato, z = fsm[(stato, x)]
        uscite.append(z)
    return uscite

riconosci_1101 = {
    ('S1', 0): ('S1', 0), ('S1', 1): ('S2', 0),
    ('S2', 0): ('S1', 0), ('S2', 1): ('S3', 0),
    ('S3', 0): ('S4', 0), ('S3', 1): ('S3', 0),
    ('S4', 0): ('S1', 0), ('S4', 1): ('S2', 1),
}
print(esegui(riconosci_1101, 'S1', [0,1,1,1,0,1,0,1,1,0,0]))
# [0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0]   -> Z = 1 solo al sesto bit

Per essere sicuri che il diagramma sia giusto si confronta con una definizione indipendente su molte sequenze casuali:

import random

def atteso(seq):                                     # Z=1 se gli ultimi 4 bit sono 1101
    return [int(seq[max(0, i-3):i+1] == [1, 1, 0, 1]) for i in range(len(seq))]

for _ in range(1000):
    s = [random.randint(0, 1) for _ in range(30)]
    assert esegui(riconosci_1101, 'S1', s) == atteso(s)

Se l'assert non scatta, la macchina è corretta anche con le sovrapposizioni. Lo stesso schema vale per una macchina di Moore: si memorizza l'uscita per stato e si legge dopo la transizione; per le macchine con più bit di ingresso l'ingresso nel dizionario è una tupla.

Aritmetica in complemento a 2

def somma_cp2(a, b, n=8):
    mask = (1 << n) - 1
    ra, rb = a & mask, b & mask
    s = (ra + rb) & mask
    segno = lambda v: (v >> (n - 1)) & 1
    overflow = segno(ra) == segno(rb) and segno(s) != segno(ra)
    valore = s - (1 << n) if segno(s) else s
    return format(s, f'0{n}b'), valore, overflow

print(somma_cp2(70, 80), somma_cp2(-6, 13), somma_cp2(-100, -28))
# ('10010110', -106, True)  ('00000111', 7, False)  ('10000000', -128, False)

Sono gli esempi di Numeri con segno, complemento a 2, sottrazione e overflowSottrazione senza segno: se $M\ge N$ nessun prestito in uscita, altrimenti il risultato $M-N+2^n$ è scorretto. Complemento a 1: $2^n-1-N$ (inversione bit a bit); complemento a 2: $2^n-N=$ complemento a 1 $+1$. Numeri con segno: segno e modulo (due zeri, intervallo simmetrico) oppure complemento a 2 (un solo zero, da $-2^{n-1}$ a $2^{n-1}-1$, MSB di peso $-2^{n-1}$). In complemento a 2 somma e sottrazione sono la stessa addizione: $A-B=A+\overline B+1$, riporto in uscita scartato. Overflow: senza segno $\Leftrightarrow C_{out}=1$ nella somma; con segno $\Leftrightarrow C_{in,MSB}\ne C_{out,MSB}$ (due operandi dello stesso segno con risultato di segno opposto).Numeri con segno, complemento a 2, sottrazione e overflow →: $70+80$ va in overflow, $-6+13=7$ e $-100-28=-128$ no. Il criterio usato è quello a parole: stesso segno degli addendi, segno diverso nel risultato.

Proprietà (conversioni, distanza di Hamming e codice Gray in Python). Per le conversioni tra basi bastano bin(), oct(), hex(), int(s, base) e format(n, '08b'); bin(a ^ b).count('1') dà la distanza di Hamming; n ^ (n >> 1) converte in codice Gray (Basi di numerazione e conversioni - binario, ottale ed esadecimaleUn numero in base $r$ vale $\sum a_i r^i$ (cifre $a_i\in{0,\dots,r-1}$). Conversioni: base $r\to$ decimale con la somma pesata; decimale $\to$ base $r$ per divisioni successive (parte intera, resti letti dal basso) e moltiplicazioni successive (parte frazionaria, parti intere lette dall'alto); binario $\leftrightarrow$ ottale/esadecimale a gruppi di 3/4 bit. Somma, differenza e prodotto binari seguono le regole decimali con cifre 0 e 1; la differenza ha prestiti, il prodotto somma prodotti parziali traslati.Basi di numerazione e conversioni - binario, ottale ed esadecimale →, Codici binari - BCD, ASCII, Unicode, parità e GrayUn codice binario a $n$ bit distingue $2^n$ elementi. BCD: una cifra decimale ogni 4 bit (1010–1111 non usati; 10 richiede 8 bit, non è il binario del numero). ASCII: 7 bit per 128 caratteri, la cifra ASCII è 011 seguito dal BCD. Unicode/UTF-8: da 1 a 4 byte, compatibile con ASCII. Bit di parità: rileva errori su un numero dispari di bit. Distanza di Hamming = numero di bit diversi. Codice Gray: numeri consecutivi differiscono di un solo bit (sensori di posizione); si costruisce per riflessione o con $g_i=b_i\oplus b_{i+1}$.Codici binari - BCD, ASCII, Unicode, parità e Gray →).

Esempio. bin(0b0110 ^ 0b1101).count('1') dà 3 (distanza di Hamming) e format(6 ^ (6 >> 1), '04b') dà '0101' (il Gray di $6$).

Errori comuni

• Dare le variabili a SOPform nell'ordine sbagliato (la prima è la più significativa).
• Fidarsi di una sola uscita di SOPform quando la copertura minima non è unica.
• Verificare una macchina solo con una sequenza di test: meglio un confronto con una definizione indipendente su molte sequenze casuali.
• Usare Python per saltare il metodo: all'esame mappe, tabelle e diagrammi vanno fatti a mano.