PSL help please

N

niv

Guest
How do I write PSL assertion for the following code?
The idea is that if I/p sig is active for a certain time (number of clock cycles), an o/p is permanently set:

Here's some noddy code for the idea:

LIBRARY ieee;
USE ieee.std_logic_1164.ALL;
USE ieee.NUMERIC_STD.ALL;
ENTITY limit_resp IS
PORT(
clk : IN STD_LOGIC;
rst : IN STD_LOGIC;
stim_1 : IN STD_LOGIC;
resp_1 : OUT STD_LOGIC
);
END ENTITY limit_resp ;
--
ARCHITECTURE rtl OF limit_resp IS
SIGNAL clk_enable : STD_LOGIC;
SIGNAL clk_en_cntr : UNSIGNED(3 DOWNTO 0);
SIGNAL counter : UNSIGNED(7 DOWNTO 0);
BEGIN
--------------------------------------------------------------------------------
-- Generate a clock enable signal at 1/10 clock rate.
--------------------------------------------------------------------------------
clk_en_gen:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
clk_enable <= '0';
clk_en_cntr <= TO_UNSIGNED(0,4);
ELSIF rising_edge(clk) THEN
IF clk_en_cntr = TO_UNSIGNED(9,4) THEN
clk_enable <= '1';
clk_en_cntr <= TO_UNSIGNED(0,4);
ELSE
clk_enable <= '0';
clk_en_cntr <= clk_en_cntr + 1;
END IF;
END IF;
END PROCESS clk_en_gen;
--------------------------------------------------------------------------------
-- Count up to some arbitrary value (for this test)
--------------------------------------------------------------------------------
count_up:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
counter <= TO_UNSIGNED(0,8);
ELSIF rising_edge(clk) THEN
IF clk_enable = '1' THEN
IF stim_1 = '1' THEN
IF counter < 200 THEN
counter <= counter + 1;
END IF;
ELSE
counter <= TO_UNSIGNED(0,8);
END IF;
END IF;
END IF;
END PROCESS count_up;
--------------------------------------------------------------------------------
-- If counter has maxed out, set the output high (forever, unless master reset)
-- i.e. if the counter ever reaches its max (200) then the output is set,
-- regardless of whether the input stim subsequently is removed.
--------------------------------------------------------------------------------
set_output:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
resp_1 <= '0';
ELSIF rising_edge(clk) THEN
IF counter = 200 THEN
resp_1 <= '1';
END IF;
END IF;
END PROCESS set_output;
--------------------------------------------------------------------------------
-- Now include a PSL assertion to test the following;
--
-- If stim is set for "N" clock cycles (or more) (2000 in this example),
-- then the "resp" output is set.
-- HELP REQUIRED FOR THE BELOW PLEASE!
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- psl begin
-- default clock is rising_edge(clk);
--
--
-- end
--------------------------------------------------------------------------------
END ARCHITECTURE rtl;

Regards, Niv
 
Using ModelSim embedded PSL syntax:

--PSL property resp_check is always( {counter = 200} |=> {resp_1} ) abort rst;

then assert the property:

--PSL assert_resp_check: assert resp_check report "resp_1 is not working!!!";

If you are using VHDL-2008 PSL probably syntax would be a little different, never investigated this.

Use this as a starting point, I haven't used PSL in a while, and even if I have, verification also needs debugging.
 
On 01/03/2015 18:05, Leonardo Capossio wrote:
Using ModelSim embedded PSL syntax:

--PSL property resp_check is always( {counter = 200} |=> {resp_1} ) abort rst;

then assert the property:

--PSL assert_resp_check: assert resp_check report "resp_1 is not working!!!";

If you are using VHDL-2008 PSL probably syntax would be a little different, never investigated this.

Use this as a starting point, I haven't used PSL in a while, and even if I have, verification also needs debugging.
Click to expand...
I think the lecturer wants the student to learn about writing bad
assertions hence he specifically asked to check for 2000 clock cycles.
The counter is the obvious choice but you might not always be aware of
what is available in the code. I am not going to give the answer as
this is clearly homework.

I give kudos to the University (tech college?) for teaching PSL,

Hans
www.ht-lab.com
 
On Tuesday, March 3, 2015 at 9:54:53 AM UTC, HT-Lab wrote:
On 01/03/2015 18:05, Leonardo Capossio wrote:
Using ModelSim embedded PSL syntax:

--PSL property resp_check is always( {counter = 200} |=> {resp_1} ) abort rst;

then assert the property:

--PSL assert_resp_check: assert resp_check report "resp_1 is not working!!!";

If you are using VHDL-2008 PSL probably syntax would be a little different, never investigated this.

Use this as a starting point, I haven't used PSL in a while, and even if I have, verification also needs debugging.

I think the lecturer wants the student to learn about writing bad
assertions hence he specifically asked to check for 2000 clock cycles.
The counter is the obvious choice but you might not always be aware of
what is available in the code. I am not going to give the answer as
this is clearly homework.

I give kudos to the University (tech college?) for teaching PSL,

Hans
www.ht-lab.com
Click to expand...

Not homework (other than self imposed)!
I've been VHDL coding for ~25 years, but just started to grapple with PSL.
Bought Cindy Eisner book, which I've started to read & creating my own examples to test myself.

So, Leonardo answer worked, sort of,
but I've changed the code so the resp_1 o/p is also clocked when clk_enable is '1', so this has caused a set of 9(?) assertion failures between counter = 200 & resp_1 going high.

I tried this, which worked, but seems a bit too like the source code?

-- property RESP_01 is
-- ({counter = 200 AND clk_enable = '1'} |=> {resp_1} abort rst);
-- assert always RESP_01 report "ERROR: resp_1 did not go to '1' at count max";
--


Any suggestions welcome!
 
El martes, 3 de marzo de 2015, 15:38:35 (UTC-3), niv escribió:
On Tuesday, March 3, 2015 at 9:54:53 AM UTC, HT-Lab wrote:
On 01/03/2015 18:05, Leonardo Capossio wrote:
Using ModelSim embedded PSL syntax:

--PSL property resp_check is always( {counter = 200} |=> {resp_1} ) abort rst;

then assert the property:

--PSL assert_resp_check: assert resp_check report "resp_1 is not working!!!";

If you are using VHDL-2008 PSL probably syntax would be a little different, never investigated this.

Use this as a starting point, I haven't used PSL in a while, and even if I have, verification also needs debugging.

I think the lecturer wants the student to learn about writing bad
assertions hence he specifically asked to check for 2000 clock cycles.
The counter is the obvious choice but you might not always be aware of
what is available in the code. I am not going to give the answer as
this is clearly homework.

I give kudos to the University (tech college?) for teaching PSL,

Hans
www.ht-lab.com

Not homework (other than self imposed)!
I've been VHDL coding for ~25 years, but just started to grapple with PSL..
Bought Cindy Eisner book, which I've started to read & creating my own examples to test myself.

So, Leonardo answer worked, sort of,
but I've changed the code so the resp_1 o/p is also clocked when clk_enable is '1', so this has caused a set of 9(?) assertion failures between counter = 200 & resp_1 going high.

I tried this, which worked, but seems a bit too like the source code?

-- property RESP_01 is
-- ({counter = 200 AND clk_enable = '1'} |=> {resp_1} abort rst);
-- assert always RESP_01 report "ERROR: resp_1 did not go to '1' at count max";
--


Any suggestions welcome!
Click to expand...

Well, you can use that, it is simple, but PSL has many ways of doing the same thing, and in this case some may be more 'correct' than others.

Following Hans suggestion, you might not be able to access the counter (you might want to do this PSL stuff from outside, hence only being able to access ports), so PSL provides a way for you to check for a condition that may run in continuous clock cycles or not, for example you could do:

--PSL property resp_check is always( {clk_enable[=200]} |=> {clk_enable[=1]} |-> {resp_1} ) abort rst;

The condition part of the implication is that the clock enable is sampled high exactly 200 times every rising edge, and this times CAN be non-consecutive (in non-consecutive clock cycles, for them to be consecutive use [*200]). Then on the next clock cycle if clk_enable is HIGH exactly one cycle, then resp_1 must go HIGH, IN THE SAME CLOCK CYCLE.

Try if it works, see this tutorial for more help: http://www.project-veripage.com/psl_tutorial_6.php
 
On 03/03/2015 18:38, niv wrote:
Hi Niv,

On Tuesday, March 3, 2015 at 9:54:53 AM UTC, HT-Lab wrote:
...snip

Not homework (other than self imposed)!
Click to expand...

That is good! PSL is amazingly powerful language especially on a formal
tool.

I've been VHDL coding for ~25 years, but just started to grapple with PSL.
Bought Cindy Eisner book, which I've started to read & creating my own examples to test myself.

So, Leonardo answer worked, sort of,
but I've changed the code so the resp_1 o/p is also clocked when clk_enable is '1', so this has caused a set of 9(?) assertion failures between counter = 200 & resp_1 going high.

I tried this, which worked, but seems a bit too like the source code?

-- property RESP_01 is
-- ({counter = 200 AND clk_enable = '1'} |=> {resp_1} abort rst);
-- assert always RESP_01 report "ERROR: resp_1 did not go to '1' at count max";
--


Any suggestions welcome!
Click to expand...

Leonardo already gave you some good advice, however, watch out for the
consecutive repeat [*n] operator as you could end up with a lot of
assertion threads (when part of the LHS becomes valid your simulator
will spawn a new thread, in Modelsim these are the blue blocks). A
possible (but untested) better solution could be the goto repetition
[->] operator.

Some general comments, watch out were you put your () brackets, the
abort operator takes precedence. In your code you are aborting the RHS
of your property. I would have aborted the whole property or directive
to avoid wasting simulation cycles, example:

always (..) abort rst;
(always ..) abort rst;

I would also use {resp_1='1'} just in case your variable goes to 'X'/'Z'
etc.

Good luck,

Regards,
Hans
www.ht-lab.com
 
On Saturday, February 28, 2015 at 5:23:26 AM UTC-5, niv wrote:
How do I write PSL assertion for the following code?
The idea is that if I/p sig is active for a certain time (number of clock cycles), an o/p is permanently set:

Here's some noddy code for the idea:

LIBRARY ieee;
USE ieee.std_logic_1164.ALL;
USE ieee.NUMERIC_STD.ALL;
ENTITY limit_resp IS
PORT(
clk : IN STD_LOGIC;
rst : IN STD_LOGIC;
stim_1 : IN STD_LOGIC;
resp_1 : OUT STD_LOGIC
);
END ENTITY limit_resp ;
--
ARCHITECTURE rtl OF limit_resp IS
SIGNAL clk_enable : STD_LOGIC;
SIGNAL clk_en_cntr : UNSIGNED(3 DOWNTO 0);
SIGNAL counter : UNSIGNED(7 DOWNTO 0);
BEGIN
--------------------------------------------------------------------------------
-- Generate a clock enable signal at 1/10 clock rate.
--------------------------------------------------------------------------------
clk_en_gen:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
clk_enable <= '0';
clk_en_cntr <= TO_UNSIGNED(0,4);
ELSIF rising_edge(clk) THEN
IF clk_en_cntr = TO_UNSIGNED(9,4) THEN
clk_enable <= '1';
clk_en_cntr <= TO_UNSIGNED(0,4);
ELSE
clk_enable <= '0';
clk_en_cntr <= clk_en_cntr + 1;
END IF;
END IF;
END PROCESS clk_en_gen;
--------------------------------------------------------------------------------
-- Count up to some arbitrary value (for this test)
--------------------------------------------------------------------------------
count_up:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
counter <= TO_UNSIGNED(0,8);
ELSIF rising_edge(clk) THEN
IF clk_enable = '1' THEN
IF stim_1 = '1' THEN
IF counter < 200 THEN
counter <= counter + 1;
END IF;
ELSE
counter <= TO_UNSIGNED(0,8);
END IF;
END IF;
END IF;
END PROCESS count_up;
--------------------------------------------------------------------------------
-- If counter has maxed out, set the output high (forever, unless master reset)
-- i.e. if the counter ever reaches its max (200) then the output is set,
-- regardless of whether the input stim subsequently is removed.
--------------------------------------------------------------------------------
set_output:pROCESS(rst, clk)
BEGIN
IF rst = '1' THEN
resp_1 <= '0';
ELSIF rising_edge(clk) THEN
IF counter = 200 THEN
resp_1 <= '1';
END IF;
END IF;
END PROCESS set_output;
--------------------------------------------------------------------------------
-- Now include a PSL assertion to test the following;
--
-- If stim is set for "N" clock cycles (or more) (2000 in this example),
-- then the "resp" output is set.
-- HELP REQUIRED FOR THE BELOW PLEASE!
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------
-- psl begin
-- default clock is rising_edge(clk);
--
--
-- end
--------------------------------------------------------------------------------
END ARCHITECTURE rtl;

Regards, Niv
Click to expand...

Want to learn more in engineering? If you are interested in learning
VHDL programming and FPGA development take my course today! This coupon
is good till April 6th, 2015 for $60 - 40% off the cost of the class at
regular price! Join now!
https://www.udemy.com/vhdl-and-fpga-development-for-beginners-and-intermediates/?couponCode=March60#/
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top