Bedeutung der Zeit für die Erstellung eines Covers

Question

Ich verifiziere formal ein kleines Modul in einem großen Design.

Ich habe das Design analysiert und ausgearbeitet (mit Jaspergold-FPV).

schrieb ich eine sehr einfache Abdeckung Eigenschaft (SVA) als:

cover_property1:cover property(@(posedge clk) $fell(signalA)); 

Es dauert etwa 5300 Sekunden, die Abdeckung zu finden. Ich bemerkte, dass "Bound" 143 ist.

Also warum dauert es so lange, um die Abdeckung zu generieren und was bedeutet das (Zeit genommen und gebunden)?

Liegt es daran, dass das Werkzeug tief in die Design-Zustände schauen muss, um die Abdeckung zu erzeugen und COI groß ist? Oder aus einem anderen Grund?

Danke für Ihre Hilfe.

Answer 1

Ich fand den Grund für lange Bearbeitungszeit, um die Abdeckung zu generieren. Der Grund für eine lange Verzögerung liegt darin, dass die Formal-Engines versuchen, (im Idealfall) den kürzesten Pfad zu finden, der der bestimmten Cover/Sequenz entspricht. Daher ist der kürzeste Pfad in vielen realen Szenarien möglicherweise nicht der schnellste für die formale Engine. Dies liegt daran, dass die formale Maschine möglicherweise viele Flip-Flops umschalten muss, um diesen bestimmten Abdeckungszustand zu erreichen.

In meinem speziellen Fall wurde ein Flip-Flop namens 'Scan_Mode' von mehreren vorhergehenden Flip-Flops abhängig gemacht. Und deshalb musste das Tool viele Flip-Flops umdrehen, um 'scan_mode' aktiviert zu machen. Daher hat eine Annahmeeigenschaft auf dem Flip-Flop (1'b1) die Abdeckungsgenerierungszeit drastisch reduziert. Covergenerierungszeit ohne die Annahme-Eigenschaft: 150 Sekunden. Covergenerierungszeit mit Annahme-Eigenschaft: 2 Sekunden.

Answer 2

versucht, alle Szenarien zu erhalten, die mit signalA kann am Ende de Geltendmachen auf steigende Flanke des Clk & daher die Zeit, in Abhängigkeit von COI

„Bound“ zeigt an, dass alle Kombinationen de-Behauptung signalA zu schlagen versucht, sind in weniger als 143 Zyklen erledigt.

Insgesamt bedeuten diese, in wie vielen Möglichkeiten & wie schnell die Eigenschaft getroffen wird.