PSL Assertions

Using the AMS Designer simulator, you can specify PSL assertions on real and Verilog-AMS wreal nets that connect to electrical nets. This methodology enables you to use PSL assertions with analog and mixed-signal blocks that you model using the Verilog-AMS wreal data type.

You must use the -assert option with the xrun or xmvlog command to enable PSL assertions.

Expressions involving wreal type objects that are explicitly declared can appear in PSL assertions in boolean expressions, clocking expressions, and as actual arguments in property and sequence instances.

wreal mywreal1, mywreal2;

reg clk;

// psl assert always ({mywreal1 > 4.4; mywreal2 < 6.6}) @(posedge clk);

Here is an example of specifying PSL assertions on a wreal net, out1, in a Verilog-AMS module:

`timescale 1ns/100ps

module INV ( out1, in1 );

  output out1;
  input in1;
  wreal in1, out1;

real out1_reg;

// psl out_eq_in_real_vams: assert
// never ( out1 < 1.25 && in1 < 1.25);

// psl out_eq_in_real_vams2: assert
// never ( out1 < 1.25 && in1 > 1.25);

  always @(in1)
    if(in1 > 1.25)
        out1_reg = 0.0;
    else
        out1_reg = 2.5;

assign out1 = out1_reg;

endmodule

For electrical nets, you assign the electrical net to a real or wreal variable, and then specify the PSL assertion on the real or wreal variable. You can also specify PSL assertions directly on electrical nets that are enclosed within access functions.

If PSL assertions are used on a mixed net, the assertion statement affects the discipline of the net. The simulator generates a warning for such scenarios. For example, the AMS simulator generates a warning message when a net is connected to a digital construct in the assertion statement. Discrete discipline is used for such nets during discipline resolution.

module top;
ana_test ana_test(abc);
//psl comparator_pos: assert always (((top.abc > 1.0) )) @( posedge(top.ana_test.int_var)) ;
endmodule

module ana_test(ana_port);
output ana_port ;
electrical ana_port ;
reg int_var =0;
always #1000 int_var = ~int_var ;
endmodule

//psl comparator_pos: assert always (((top.abc > 1.0) )) @( posedge(top.ana_test.int_var)) ;

In the above example, net top.abc connects to electrical port, but it will have a resolved discrete discipline because it is used in digital constructs in the assertion statement.

You can use the xmelab option -amselabtrace assert option to trace nets that are connected to digital constructs in an assertion statement.

Analog Event Functions for Assertion Clocking

Verilog-AMS analog event functions cross and above are supported as clocking events in PSL assertions. For example:

electrical sig1, sig2, sig3;
reg a, b;
// psl assert always ({V(sig1);a} |=> {V(sig2);b}) @(cross(V(sig3)));

Support for PSL Built-In Functions

Analog expressions are allowed only within the prev PSL built-in sampled value function. It is an error to have analog expressions as arguments to built-in sampled value functions other than prev. For example:

// psl assert always ({V(sigout) > 0.5} |=> {prev(V(sigout)) > 0.4}) @(cross(V(sigout))); // ok

// psl assert always ({V(sigout) > 0.5} |=> {stable(V(sigout)) > 0.4}) @(cross(V(sigout))); // not allowed

PSL Assertions

Analog Event Functions for Assertion Clocking

Support for PSL Built-In Functions

Related Topic