PROP SAT är ett litet verktyg för att testa satisfierbarheten hos en satslogisk formel. Detta kan i sin tur användas för att testa kombinatoriska kretsar eller visa att en kombinatorisk krets uppfyller en (funktionell) specikation av kretsen. Båda dessa tillämpningar beskrivs nedan.

Att använda PROP SAT

PROP SAT kan bara användas på IDAs SUN-system. Du startar PROP SAT genom att ge shellkommandot ~TTIT32/bin/propsat. (Eventuellt måste du först skriva kommandot module add prog/sicstus.) Systemet svarar med prompten:

    -->

Följande kommandon är nu tillgängliga (observera att alla kommandon måste avslutas med en punkt och vagnretur):

halt.

Avslutar PROP SAT.

help.

Hjälpinformation om PROP SAT.

formel.

Om man skriver in en satslogisk formel (syntaxen för formler beskrivs nedan) kommer systemet att försöka hitta sanningsvärden (0, 1) för de ingående satsparametrarna, under vilka formeln är sann. Finns det flera modeller skrivs samtliga modeller ut.

file(filnamn).

Detta kommando fungerar på samma sätt som det föregående förutom att formeln här skrivs i en fil istället för vid prompten. Detta kommando är nog är att rekommendera om inte formeln är väldigt liten. Observera att om filnamnet innehåller några andra symboler än små bokstäver måste filnamnet skrivas inom citattecken.

Syntaxen hos Formler

Satsparametrar skrivs som identifierare inledda med stor bokstav. Sammansatta formler skrivs enligt följande:

    not(_) | and(_,_) | or(_,_) | implies(_,_) | eq(_,_)

T.ex. är and(not(A),B) en satslogisk formel.

Att Testa en Kombinatorisk Krets

PROP SAT kan användas för att testa en kombinatorisk krets. Betrakta t.ex. följande krets:

Kretsen kan beskrivas med följande logiska utsaga:

Om vi vill veta utsignalen från kretsen givet att X=Z=1 och Y=0 så kan vi be PROP SAT att försöka satisfiera uttrycket:

    --> and(
            and(X,and(not(Y),Z)),
            eq(W,and(not(and(X,Y)),Z))
        ).

    W = 1
    X = 1
    Y = 0
    Z = 1

    No (more)
    -->

Det vill säga, utsignalen (W) är 1. Vi kan även testa vilka insignaler som ger utsignalen 1:

    --> and(
            W,
            eq(W,and(not(and(X,Y)),Z))
        ).

    W = 1
    X = 0
    Y = any
    Z = 1

    W = 1
    X = any
    Y = 0
    Z = 1

    No (more)
    --> 

Att Verifiera en Kombinatorisk Krets

Antag att vi istället vill visa att kretsen ovan har egenskapen att utsignalen är 0 om insignalen Z är 0 (oavsett vad X och Y har för värden). Vi vill med andra ord visa att utsagan implies(not(Z),not(W)) följer logiskt ur designen. Detta kan vi visa genom att be PROP SAT visa att följande uttryck är osatisfierbart:

    --> and(
            not(implies(not(Z),not(W))),
            eq(W,and(not(and(X,Y)),Z))
        ).

    No (more)

Vi negerar alltså specifikationen och konjugerar den med designen. Uttrycket är ovan är osatisfierbart vilket yttrar sig i svaret No (more).