Languages
Writing PSL assertions for checking current levels
Can you show me an example of writing a PSL assertion to check the supply current level during a power-down mode? Specifically, I want to check the supply current level I(VDD) is less than 1uA once 100ns has passed after the circuit enters the power-down mode (PWRDN=1) and remains that way until the circuit leaves the mode (PWRDN=0).
Sure. Here is a simple example demonstrating how a PSL assertion for checking an analog property, whether the supply current level is less than a specified threshold during the power-down mode. The attached package contains the necessary files to run the example yourself.
First, we need a device under test (DUT). For simplicity, we created a simple circuit-level model that draws a random current from the supply (VDD) during the power-down mode (DUT.sv). The model is made of a series combination of two resistors, one of which has a resistance that switches based on the input 'PWRDN'. Furthermore, the resistance value 'R' while 'PWRDN'=1 is randomly drawn from a uniform distribution between 0.7MΩ and 2MΩ. Also, a 1pF capacitance is added to make the transition of the supply current realistic.
// MODULE DUT.sv
// A DUT emulating the supply current changing with the PWRDN input.
module DUT (
input PWRDN, // power-down input
input xreal VDD // supply input
);
xreal out;
real R;
resistor #(.R(10e3)) R1 (.pos(VDD), .neg(out));
capacitor #(.C(1e-12)) C1 (.pos(out), .neg(`ground));
res_sw R2 (.pos(out), .neg(`ground), .R(R));
always @(PWRDN) begin
if (PWRDN) R = rand_uniform(0.7e6, 2e6);
else R = 90e3;
end
endmodule
And we need to set up a testbench. The following testbench tb_DUT.sv instantiates the DUT model and adds the 'vsource' and 'iprobe' primitives to supply the 1.0V voltage and measure the current, respectively. And it toggles the input 'PWRDN' every 200ns.
As will be seen later, the PSL assertion checks need a clock that indicates the time instants of property checking. For that purpose, the testbench creates a 10-ns period clock called 'VCLK'. Also, the testbench adds an 'xreal_to_real' primitive that converts the xreal-type signal 'IVDD' bearing the supply current level information to a real-type signal named 'Ioff'. This conversion is done by periodically sampling the input at 1ns intervals.
// TESTBENCH tb_DUT.sv
// Checking the supply current level during the power-down periods
module tb_DUT;
reg PWRDN;
xreal VDD, VDD0;
xreal IVDD;
//------------------------------------------------------------
// DUT and stimuli setup
//------------------------------------------------------------
// DUT instantiation
DUT DUT_INST (.PWRDN, .VDD);
// power supply with current measurement
vsource #(.mode("dc"), .dc(1.0)) VVDD (.pos(VDD0), .neg(`ground), .in(`ground));
iprobe IPROBE (.pos(VDD0), .neg(VDD), .out(IVDD));
// periodic toggling of PWRDN input
initial PWRDN = 0;
always #(200ns) PWRDN = ~PWRDN;
//------------------------------------------------------------
// checking IVDD < 1e-6 during power-down with PSL
//------------------------------------------------------------
reg VCLK;
real Ioff;
// VCLK: 10ns-period clock for PSL checking
initial VCLK = 1;
always #(5ns) VCLK = ~VCLK;
// Ioff: periodic measurement of IVDD current
xreal_to_real #(.mode("fixed"), .period(1e-9))
CONN0 (.in(IVDD), .out(Ioff));
Now we define the PSL assertions in a separate file named LOW_IVDD.pslvlog. Once the signal 'PWRDN' becomes 1 for 10 consecutive 'VCLK' periods (=100ns), the assertion named 'LOW_IVDD_check' checks whether the variable 'Ioff' has a value less than 1.0e-6 until 'PWRDN' becomes 0. Note that the checks are performed only at the positive-edge instants of 'VCLK'.
// PSL verification unit: LOW_IVDD.pslvlog
// Checking if IVDD < 1e-6 during power-down period
vunit LOW_IVDD (tb_DUT) {
default clock = (posedge VCLK); // 10ns-period clock
sequence PWRDN_seq = {PWRDN[*10]}; // PWRDN has been high for 100ns
let PWRUP_cond = (~PWRDN);
property LOW_IVDD_prop =
always (PWRDN_seq |-> (Ioff < 1.0e-6) until PWRUP_cond);
LOW_IVDD_check: assert LOW_IVDD_prop
report "PSL CHECK: I(VDD) is too high!";
}
For your information, an equivalent check can be performed using the XMODEL measurement primitives, without the use of PSL. The later part of the testbench tb_DUT.sv listed below adds a set of measurement primitives such as 'trig_posedge', 'trig_negedge' and 'meas_max' primitives to measure the maximum value of the supply current level 'IVDD' during the period starting from 100ns after 'PWRDN' becoming 1 and lasting until 'PWRDN' becomes 0. And then the assertion named 'IVDD_CHECK1' checks whether this maximum value is always less than 1.0e-6. One advantage of this approach compared to the PSL based one is that the checking of supply current level is performed continuously, without triggering a series of explicit SystemVerilog events during the simulation.
//------------------------------------------------------------
// checking IVDD < 1e-6 during power-down with XMODEL
//------------------------------------------------------------
xbit pwrdn;
xbit trig0, trig1, trig2;
real Ioff_max;
// measuring Ioff_max as maximum IVDD from 50ns after PWRDN rising and until PWRDN falling
bit_to_xbit CONN1 (.in(PWRDN), .out(pwrdn));
trig_posedge TRIG1 (.in(pwrdn), .out(trig0));
delay_xbit #(.delay(100e-9)) DELAY1 (.in(trig0), .out(trig1));
trig_negedge TRIG2 (.in(pwrdn), .out(trig2));
meas_max MEAS (.in(IVDD), .out(Ioff_max), .from(trig1), .to(trig2));
// checking if Ioff_max < 1e-6
always @(Ioff_max) begin
IVDD_CHECK1: assert (`isnan(Ioff_max) || Ioff_max < 1e-6)
else $display("XMODEL CHECK: I(VDD) is too high (%e)!", Ioff_max);
end
//------------------------------------------------------------
// waveform dumping
//------------------------------------------------------------
initial begin
$xmodel_dumpfile();
$xmodel_dumpvars();
end
endmodule
To run the simulation with the described PSL file LOW_IVDD.pslvlog, you need to add some simulator-specific options to the simulation command. For Cadence Xcelium, you can the options listed below.
$ xmodel tb_DUT.sv DUT.sv --top tb_DUT --simtime 2us --simulator xcelium \
--elab-option -assert -propfile_vlog LOW_IVDD.pslvlog --
And here are the simulation results. First, the waveforms below show the change in the supply current level 'IVDD' as the signal 'PWRDN' toggles between 0 and 1. Due to the randomization, some current levels during the power-down mode are less than 1uA while some others are more than 1uA.
And here are the output logs generated by the Xcelium simulator. Both the PSL and XMODEL based assertions detect the failure during the 300~400ns period correctly. A minor difference is that the PSL assertion check generates multiple failure messages as it explicitly checks the current level at 10ns intervals, whereas the XMODEL assertion check generates only one message per failure as it checks only once using the maximum current level during the power-down period.
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 290 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 200 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 300 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 210 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 310 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 220 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 320 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 230 NS)
PSL CHECK: I(VDD) is too high!
... (omitted for brevity) ...
xmsim: *E,ASRTST (./tb_DUT.sv,60): (time 400002 PS) Assertion tb_DUT.IVDD_CHECK1 has failed
XMODEL CHECK: I(VDD) is too high (1.288361e-06)!
Attachment: psl_ivdd_20240530.tar.gz
Please login or Register to submit your answer
전류 레벨 체크하는 PSL assertion 작성하는 법
파워다운 모드 동안의 전원 전류 레벨을 체크할 수 있는 PSL assertion을 작성하는 예시를 보여줄 수 있나요? 예를 들면, 회로가 파워다운 모드로 들어간 (PWRDN=1) 이후 100ns가 지난 시점부터 회로가 다시 파워다운 모드에서 나오는 (PWRDN=0) 시점까지의 기간 동안 전원 전류 I(VDD)를 1uA 이하로 유지하는지 여부를 체크하고 싶습니다.
Sure. Here is a simple example demonstrating how a PSL assertion for checking an analog property, whether the supply current level is less than a specified threshold during the power-down mode. The attached package contains the necessary files to run the example yourself.
First, we need a device under test (DUT). For simplicity, we created a simple circuit-level model that draws a random current from the supply (VDD) during the power-down mode (DUT.sv). The model is made of a series combination of two resistors, one of which has a resistance that switches based on the input 'PWRDN'. Furthermore, the resistance value 'R' while 'PWRDN'=1 is randomly drawn from a uniform distribution between 0.7MΩ and 2MΩ. Also, a 1pF capacitance is added to make the transition of the supply current realistic.
// MODULE DUT.sv
// A DUT emulating the supply current changing with the PWRDN input.
module DUT (
input PWRDN, // power-down input
input xreal VDD // supply input
);
xreal out;
real R;
resistor #(.R(10e3)) R1 (.pos(VDD), .neg(out));
capacitor #(.C(1e-12)) C1 (.pos(out), .neg(`ground));
res_sw R2 (.pos(out), .neg(`ground), .R(R));
always @(PWRDN) begin
if (PWRDN) R = rand_uniform(0.7e6, 2e6);
else R = 90e3;
end
endmodule
And we need to set up a testbench. The following testbench tb_DUT.sv instantiates the DUT model and adds the 'vsource' and 'iprobe' primitives to supply the 1.0V voltage and measure the current, respectively. And it toggles the input 'PWRDN' every 200ns.
As will be seen later, the PSL assertion checks need a clock that indicates the time instants of property checking. For that purpose, the testbench creates a 10-ns period clock called 'VCLK'. Also, the testbench adds an 'xreal_to_real' primitive that converts the xreal-type signal 'IVDD' bearing the supply current level information to a real-type signal named 'Ioff'. This conversion is done by periodically sampling the input at 1ns intervals.
// TESTBENCH tb_DUT.sv
// Checking the supply current level during the power-down periods
module tb_DUT;
reg PWRDN;
xreal VDD, VDD0;
xreal IVDD;
//------------------------------------------------------------
// DUT and stimuli setup
//------------------------------------------------------------
// DUT instantiation
DUT DUT_INST (.PWRDN, .VDD);
// power supply with current measurement
vsource #(.mode("dc"), .dc(1.0)) VVDD (.pos(VDD0), .neg(`ground), .in(`ground));
iprobe IPROBE (.pos(VDD0), .neg(VDD), .out(IVDD));
// periodic toggling of PWRDN input
initial PWRDN = 0;
always #(200ns) PWRDN = ~PWRDN;
//------------------------------------------------------------
// checking IVDD < 1e-6 during power-down with PSL
//------------------------------------------------------------
reg VCLK;
real Ioff;
// VCLK: 10ns-period clock for PSL checking
initial VCLK = 1;
always #(5ns) VCLK = ~VCLK;
// Ioff: periodic measurement of IVDD current
xreal_to_real #(.mode("fixed"), .period(1e-9))
CONN0 (.in(IVDD), .out(Ioff));
Now we define the PSL assertions in a separate file named LOW_IVDD.pslvlog. Once the signal 'PWRDN' becomes 1 for 10 consecutive 'VCLK' periods (=100ns), the assertion named 'LOW_IVDD_check' checks whether the variable 'Ioff' has a value less than 1.0e-6 until 'PWRDN' becomes 0. Note that the checks are performed only at the positive-edge instants of 'VCLK'.
// PSL verification unit: LOW_IVDD.pslvlog
// Checking if IVDD < 1e-6 during power-down period
vunit LOW_IVDD (tb_DUT) {
default clock = (posedge VCLK); // 10ns-period clock
sequence PWRDN_seq = {PWRDN[*10]}; // PWRDN has been high for 100ns
let PWRUP_cond = (~PWRDN);
property LOW_IVDD_prop =
always (PWRDN_seq |-> (Ioff < 1.0e-6) until PWRUP_cond);
LOW_IVDD_check: assert LOW_IVDD_prop
report "PSL CHECK: I(VDD) is too high!";
}
For your information, an equivalent check can be performed using the XMODEL measurement primitives, without the use of PSL. The later part of the testbench tb_DUT.sv listed below adds a set of measurement primitives such as 'trig_posedge', 'trig_negedge' and 'meas_max' primitives to measure the maximum value of the supply current level 'IVDD' during the period starting from 100ns after 'PWRDN' becoming 1 and lasting until 'PWRDN' becomes 0. And then the assertion named 'IVDD_CHECK1' checks whether this maximum value is always less than 1.0e-6. One advantage of this approach compared to the PSL based one is that the checking of supply current level is performed continuously, without triggering a series of explicit SystemVerilog events during the simulation.
//------------------------------------------------------------
// checking IVDD < 1e-6 during power-down with XMODEL
//------------------------------------------------------------
xbit pwrdn;
xbit trig0, trig1, trig2;
real Ioff_max;
// measuring Ioff_max as maximum IVDD from 50ns after PWRDN rising and until PWRDN falling
bit_to_xbit CONN1 (.in(PWRDN), .out(pwrdn));
trig_posedge TRIG1 (.in(pwrdn), .out(trig0));
delay_xbit #(.delay(100e-9)) DELAY1 (.in(trig0), .out(trig1));
trig_negedge TRIG2 (.in(pwrdn), .out(trig2));
meas_max MEAS (.in(IVDD), .out(Ioff_max), .from(trig1), .to(trig2));
// checking if Ioff_max < 1e-6
always @(Ioff_max) begin
IVDD_CHECK1: assert (`isnan(Ioff_max) || Ioff_max < 1e-6)
else $display("XMODEL CHECK: I(VDD) is too high (%e)!", Ioff_max);
end
//------------------------------------------------------------
// waveform dumping
//------------------------------------------------------------
initial begin
$xmodel_dumpfile();
$xmodel_dumpvars();
end
endmodule
To run the simulation with the described PSL file LOW_IVDD.pslvlog, you need to add some simulator-specific options to the simulation command. For Cadence Xcelium, you can the options listed below.
$ xmodel tb_DUT.sv DUT.sv --top tb_DUT --simtime 2us --simulator xcelium \
--elab-option -assert -propfile_vlog LOW_IVDD.pslvlog --
And here are the simulation results. First, the waveforms below show the change in the supply current level 'IVDD' as the signal 'PWRDN' toggles between 0 and 1. Due to the randomization, some current levels during the power-down mode are less than 1uA while some others are more than 1uA.
And here are the output logs generated by the Xcelium simulator. Both the PSL and XMODEL based assertions detect the failure during the 300~400ns period correctly. A minor difference is that the PSL assertion check generates multiple failure messages as it explicitly checks the current level at 10ns intervals, whereas the XMODEL assertion check generates only one message per failure as it checks only once using the maximum current level during the power-down period.
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 290 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 200 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 300 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 210 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 310 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 220 NS)
PSL CHECK: I(VDD) is too high!
xmsim: *E,ASRTST (./LOW_IVDD.pslvlog,13): (time 320 NS) Assertion tb_DUT.LOW_IVDD_check has failed (10 cycles, starting 230 NS)
PSL CHECK: I(VDD) is too high!
... (omitted for brevity) ...
xmsim: *E,ASRTST (./tb_DUT.sv,60): (time 400002 PS) Assertion tb_DUT.IVDD_CHECK1 has failed
XMODEL CHECK: I(VDD) is too high (1.288361e-06)!
Attachment: psl_ivdd_20240530.tar.gz
Please login or Register to submit your answer