Toggeln in PSL

[Hardwerker (Gast)]

Hallo,

um die Property Specification Language zu lernen, habe ich ein 
RS-Flipflop in VHDL beschrieben.

library ieee;
use ieee.std_logic_1164.all;

entity FlipFlop is
  generic (
    formal : boolean := true
    );
  port (
    clk  : in  std_logic;
    s  : in  std_logic;
    r  : in  std_logic;
    y  : out std_logic
  );
end FlipFlop;

architecture rtl of FlipFlop is
  default clock is rising_edge(clk);
begin

  process
  begin
    wait until rising_edge(clk);
    if s='1' and r='0' then
      y <= '1';
    elsif s='0' and r='1' then
      y <= '0';
    elsif s='1' and r='1' then
      y <= not y;
    end if;
  end process;
  
  formal_gen : if formal generate
  begin
    assert always {s='1' and r='0'} |=> y='1';
    assert always {s='0' and r='1'} |=> y='0';
    --assert always (r='1' and s='1' and y='1') |=> y='0';
    --assert always (r='1' and s='1' and y='0') |=> y='1';
    assert always (r='1' and s='1') |=> ; -- Was muss da hin?
  end generate;

end rtl;

Wie kann ich vorgeben, dass y in jedem Takt umschalten (toggeln) muss, 
wenn r=s=1 ist? Mit den auskommentierten Zeilen funktioniert es, aber
y='1' |=> y='0'
y='0' |=> y='1'
finde ich redundant. Es geht ja nur um y[next]=not y[now].

[Lothar M. (Firma: Titel) (lkmiller) (Moderator)]

Hardwerker schrieb:
> habe ich ein RS-Flipflop in VHDL beschrieben.
Das hat aber normalerweise keinen Takt. Könnte es sein, dass du ein 
JK-Flipflop meinst?

Evtl. helfen dir bei deinem Problem Attribute weiter. Such mal dort ab 
S'delayed:
https://www.csee.umbc.edu/portal/help/VHDL/attribute.html

[Hardwerker (Gast)]

Lothar M. schrieb:
> Hardwerker schrieb:
>> habe ich ein RS-Flipflop in VHDL beschrieben.
> Das hat aber normalerweise keinen Takt. Könnte es sein, dass du ein
> JK-Flipflop meinst?
Ja, stimmt. Ein JK-Fliflop mit R- und S-Eingängen. :-)
Aber die Beschreibung ist ja einfach genug, um zu erkennen, was gemeint 
ist.

Lothar M. schrieb:
> Evtl. helfen dir bei deinem Problem Attribute weiter.
Es müsste auch mit PSL gehen, aber als Alternative könnte das vielleicht 
funktionieren. Danke, ich probiere es mal aus.

[Hardwerker (Gast)]

Leider funktioniert das nicht. Es sieht so aus, als ob GHDL 'delayed und 
'event nicht verarbeiten kann. Die anderen Attribute scheinen nicht 
zielführend zu sein.

[Tobias B. (Firma: www.elpra.de) (ttobsen)]

Ich hab eine Weile schon kein PSL mehr gemacht, aber ich meine dass dir 
da nichts anderes uebrig bleibt als beide Zustaende zu beschreiben:

assert always (r='1' and s='1' and j='1') |=> y='0';
assert always (r='1' and s='1' and j='0') |=> y='1';

Was auch funktionieren koennte ist etwas in der Form:

assert always (r='1' and s='1') |=> y /= prev(y);

Falls das zweite funktioniert, dann hat es allerdings ein paar Probleme 
falls y auch Werte die nicht '1' oder '0' sind annehmen kann.

[Hardwerker (Gast)]

Tobias B. schrieb:
> Was auch funktionieren koennte ist etwas in der Form:
> assert always (r='1' and s='1') |=> y /= prev(y);
Es funktioniert. Vielen Dank.
Probiert hatte ich es mit next, aber das gab entweder Syntaxfehler oder 
hat nicht funktioniert.
y=not prev(y) funktioniert auch.

[Tobias B. (Firma: www.elpra.de) (ttobsen)]

Hardwerker schrieb:
> y=not prev(y) funktioniert auch.

Ahh, das ist gut zu wissen und sicher die bessere Loesung! Super. :-)

Kleiner Buchtipp:

"Using PSL/Sugar for Formal and Dynamic Verification (2nd Edition)" von 
Ben Cohen. Ist didaktisch ein bisschen wild, aber an sich finde ich den 
Schinken ganz gut.

[Weltbester FPGA-Pongo (Gast)]

Setzt das jemand regelmässig ein?

[Tobias B. (Firma: www.elpra.de) (ttobsen)]

Weltbester FPGA-Pongo schrieb im Beitrag #6365115:
> Setzt das jemand regelmässig ein?

Definitiv ja, sowohl PSL als auch SVA (aktuell jedoch nicht von mir 
persoenlich). Gerade wenn groessere Systeme getestet werden mit 
komplexen Bussystemen, ist Assertion Based Verification ein enorm 
maechtiges Werkzeug und via PSL lassen sich recht praegnante Assertions 
definieren ohne am Code rumfummeln zu muessen (das Ziel von PSL war auch 
immer einen dokumentativen Charakter zu haben - ob der Syntax dazu 
geeignet ist sei mal dahin gestellt ;-)).

Man stelle sich mal vor man entwickelt ein AXI IP Core. Dann wuerde man 
im ersten Schritt wohl am AXI Bus entsprechende Assertions definieren 
(evtl. sogar als IP Template). Am Ende der Entwicklung kann man den IP 
dann z.B. mit Garbage Daten fuettern und schauen ob er sich auch unter 
extremen Bedingungen AXI konform verhaelt. Das waere ein klassischer 
Fall fuer ABV in dem ich nicht den klassischen Testvektoren rein / 
Testvektoren raus / Vergleich mit Golden Sample Ansatz haben. Wenn man 
sich dann noch die Maechtigkeit von PSL anschaut, liegt es nahe das auch 
zu verwenden.

Kleiner Hinweis: Mit VHDL-2019 wird das Ganze dann nochmal maechtiger, 
siehe:

https://vhdlwhiz.com/vhdl-2019/#new-psl-attributes-and-functions

[Hardwerker (Gast)]

Weltbester FPGA-Pongo schrieb im Beitrag #6365115:
> Setzt das jemand regelmässig ein?
Noch nicht. Ich teste gerade, ob es sinnvoll ist.

Tobias B. schrieb:
> Man stelle sich mal vor man entwickelt ein AXI IP Core. Dann wuerde man
> im ersten Schritt wohl am AXI Bus entsprechende Assertions definieren
> (evtl. sogar als IP Template). Am Ende der Entwicklung kann man den IP
> dann z.B. mit Garbage Daten fuettern und schauen ob er sich auch unter
> extremen Bedingungen AXI konform verhaelt.
Sowas wäre mein Ansatz. Man definiert einmal einen Satz von Annahmen zum 
Beispiel für häufig benutzte Busse und kann damit automatisch jedes 
Modul, das diesen Bus benutzt auf Korrektheit testen.

[Martin S. (strubi)]

Weltbester FPGA-Pongo schrieb im Beitrag #6365115:
> Setzt das jemand regelmässig ein?

In der GHDL-Community gibt es einige Puristen, die da recht aktiv sind, 
es werden auch aktiv Features in GHDL eingepflegt, im gitter.im-Chat zu 
GHDL kriegt man immer mal Antworten.

PSL kann allerdings bei komplexen SoCs und aufwendigeren Regresstests 
die Co-Simulation/Verification nicht ersetzen, bzw. wird so komplex zu 
unterhalten wie bei SV.

[Tobias B. (Firma: www.elpra.de) (ttobsen)]

Martin S. schrieb:
> PSL kann allerdings bei komplexen SoCs und aufwendigeren Regresstests
> die Co-Simulation/Verification nicht ersetzen, bzw. wird so komplex zu
> unterhalten wie bei SV.

Das ist eigentlich nicht der Anspruch von PSL, bzw. Aepfel mit Birnen 
verglichen. PSL ist einfach ein Werkzeug um moeglichst einfach komplexe 
Assertions zu definieren.

Ob man jetzt Assertions verwendet oder eine andere Methode zur 
Functional Verification ist erstmal unabhaengig von der Teststrategie. 
Aber alles in allem stimme ich dem voll und ganz zu, mit reinem 
Assertion Based Verification kommt man in komplexen Designs nicht weit.

Wo ein Einsatz allerdings noch Sinn macht ist nicht in der 
Verifikationsphase sondern in der Design Phase. So wie Hardwerker PSL 
verwenden moechte ist es eigentlich genau richtig und hilft ihm Fehler 
moeglichst fruehzeitig zu erkennen. Wenn sein Design fertig ist wird er 
allerdings trotzdem noch Testvektoren erstellen muessen die er durch 
sein Design jagd (ob mittels Co-Simulation oder "klassischen" Verfahren 
sei dann mal dahin gestellt).

[Martin S. (strubi)]

Tobias B. schrieb:
> Wo ein Einsatz allerdings noch Sinn macht ist nicht in der
> Verifikationsphase sondern in der Design Phase

Test Driven Development mit PSL und VHDL zu machen, ist eine ziemlich 
bloede Idee, da gibt es schon laengst nachhaltigere Ansaetze wo man 
nicht gleich zwei unterschiedliche Sprachen, sondern nur noch Python 
koennen muss.
Dann kann man's in der zweiten Verifikationsstufe immer noch durch einen 
PSL-Check kloppen, wenn's ein Purist verlangt.

[Tobias B. (Firma: www.elpra.de) (ttobsen)]

Martin S. schrieb:
> Test Driven Development mit PSL und VHDL zu machen, ist eine ziemlich
> bloede Idee, da gibt es schon laengst nachhaltigere Ansaetze wo man
> nicht gleich zwei unterschiedliche Sprachen, sondern nur noch Python
> koennen muss.

Naja, das ist jetzt aber etwa viel Polemik.

Assertions sind sehr wohl in der Design Phase ein wertvolles Werkzeug 
und mittels PSL lassen sich halt relativ einfach sehr komplexe 
Assertions definieren, ohne das Design anfassen zu muessen. Das Problem 
ist wahrscheinlich eher, dass man es Assertion Based Verification nennt, 
obwohl man eher Assertion Based Debugging macht. ;-)

Und natuerlich haengt das auch von diversen anderen Randbedingungen ab, 
wie z.B. den Skills des Entwicklers. Man kann nicht von jedem Entwickler 
erwarten, dass er auch gleichzeitig den Job eines Verification Engineers 
vollumfaneglich beherrscht, obenso vice versa. Und dann ist es doch 
vollkommen in Ordnung wenn in der Design Phase mit Assertions gearbeitet 
wird.

Martin S. schrieb:
> Dann kann man's in der zweiten Verifikationsstufe immer noch durch einen
> PSL-Check kloppen, wenn's ein Purist verlangt.

Ich wuerde das wenn schon in der Design Stufe machen. Z.B. man hat ein 
AXI IP Core Template mit eingebauten AXI Assertions. Der Designer sieht 
dann sofort was vom Core verlangt wird, damit sein IP mit der AXI Welt 
kommunizieren kann. In der Regel ist die Testbench die der Designer 
verwendet nicht die entgueltige Verifikation, idealerweise erstellen 
zwei verschiedene Personen Test und Design. Und leider ist auch TDD 
nicht immer moeglich, z.B. wenn keine Ressourcen verfuegbar sind.