Limitations of Using PSL Assertions

The following limitations exist when using PSL assertions with the AMS Designer simulator:

Unclocked, partially clocked, or multiple-clocked PSL assertions involving analog expressions are not supported.

electrical sig1, sig2;reg a, clk, clk1, clk2;// unclocked - Not Supported// psl assert always (V(sig1) > V(sig2));// partially clocked - Not Supported// psl assert always {V(sig1); V(sig2)} |=> {a} @(cross(V(clk))); // multiple clocked - Not Supported// psl assert always {V(sig1); V(sig2)} @(cross(V(clk1))) |=> {a} @(cross(V(clk2)));For such cases, use either an explicitly declared single clock or a default clock.
Analog expressions that are not allowed to appear outside the analog block as per the Verilog-AMS LRM cannot appear in a PSL assertion statement. In the example below, the assert statement is not allowed because the analog operator ddt cannot appear outside an analog block.// psl assert always ({ddt(V(sig1))} |-> {ddt(V(sig2))}) @(posedge clk);
When port probes are used with the <> syntax, they cannot appear in a PSL assertion. For example, the following assert statement is not valid.
electrical in, out;// psl assert always (I(<out>) > 0) && (I(<out>) < 2.3) @ (cross(I(<in>)));
The assertion clock cannot be level-sensitive on an analog expression. For example, the following assert statement is not valid because the assertion clock is sensitive to the value change of V(in).// psl property P1(bitvector i) = always (S1(i) |=> {i > 0.6}) @ (V(in)); // psl assert P1To overcome this limitation, you can use an analog event expression in the assertion clock, as shown in the following example. // psl property P1(bitvector i) = always (S1(i) |=> {i > 0.6}) @ (cross(V(in)));// psl assert P1
If a PSL assertion involves a level-sensitive clock, none of the assertion signals are allowed to contain analog expressions. The following assertion is not valid because the assertion signal involves the voltage of node sig2 , while the clock is level-sensitive.electrical sig1, sig2;reg a, b, clk;// psl assert always ({V(sig1);a} |=> {V(sig2);b}) @(clk);

Nets that could potentially be coerced to wreal during elaboration because they are connected to a wreal net or an analog object cannot be used in PSL assertions.

module top;
wreal wr;
test mytest(wr);
endmodule

module test(w);
input w;
reg clk;
// not ok - 'w' will be coerced to wreal due to its connectivity to wr and cannot be be used in a psl assertion
// psl assert always (w > 2.2) @(posedge clk);
endmodule

For such cases, explicitly declare the wreal nets that you want to include in a PSL assertion.

Although PSL assertions appearing in verification units that are bound to modules can contain analog expressions and wreal objects, instance-bound verification units cannot contain analog expressions. For example:

module top;
.....
test mytest();
endmodule

module test;
.....
endmodule

vunit myvunit(test) { // ok, verification unit involving analog expression is
// module bound
// psl property P1 = ({V(sig1)} -> next (V(sig2)) @(cross(V(sig3)));
//psl assert P1;
}

vunit myvunit(top.mytest) { // not ok, verification unit involving analog
// expression is instance bound
// psl property P1 = ({V(sig1)} -> next (V(sig2)) @(cross(V(sig3)));
//psl assert P1;
}

PSL cannot be used within VHDL-AMS if the PSL assertion statement contains objects or expressions that are either owned or evaluated by the continuous time solver.

Limitations of Using PSL Assertions

Related Topics