PSL help please

N

niv

Guest
Trying to get started with PSL assertions.

I've written a simple counter, code below, with a couple of PSL assertions at the end. However, the 2nd assertion fails on the transition from cntr_max-1 to cntr_max, but the rollover assertion seems to work.
Any ideas please?


LIBRARY ieee;
USE ieee.std_logic_1164.all;
USE ieee.numeric_std.ALL;
--------------------------------------------------------------------------------
ENTITY psl_counter_test IS
GENERIC(
my_width : NATURAL := 6
);
PORT(
rst : IN STD_LOGIC;
clk : IN STD_LOGIC;
my_count : OUT STD_LOGIC_VECTOR (my_width-1 DOWNTO 0)
);

END ENTITY psl_counter_test ;
--------------------------------------------------------------------------------
ARCHITECTURE rtl OF psl_counter_test IS
SIGNAL my_counter : UNSIGNED(my_width-1 DOWNTO 0);
SIGNAL en_counter : UNSIGNED(3 DOWNTO 0);
SIGNAL enable : STD_LOGIC;
CONSTANT cntr_max : NATURAL := 2**my_width - 1;
BEGIN
my_count <= STD_LOGIC_VECTOR(my_counter);
--------------------------------------------------------------------------------
count_en : PROCESS (rst, clk)
BEGIN
IF rst = '1' THEN
en_counter <= (OTHERS => '0'); -- reset to max
enable <= '0';
ELSIF RISING_EDGE(clk) THEN
en_counter <= en_counter + 1; -- rolls over, so div by 64.
IF en_counter = 15 THEN
enable <= '1';
ELSE
enable <= '0';
END IF;
END IF;
END PROCESS count_en;
--------------------------------------------------------------------------------
count_up : PROCESS (rst, clk)
BEGIN
IF rst = '1' THEN
my_counter <= (OTHERS => '0'); -- reset to max
ELSIF RISING_EDGE(clk) THEN
IF enable = '1' THEN
my_counter <= my_counter + 1; -- continuous count with rollover.
ELSE
NULL;
END IF;
END IF;
END PROCESS count_up;
--------------------------------------------------------------------------------
-- psl begin
--
-- default clock is rising_edge(clk);
--
-- property psl_01 is
-- ({(my_counter = cntr_max) and (enable = '1')} |=> {my_counter = 0} );
-- assert always psl_01 report"ERROR: 'my_counter' did not rollover to zero.";
--
-- property psl_02 is
-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );
-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";
--
-- end
END ARCHITECTURE rtl;
 
On Thursday, 25 September 2014 23:41:21 UTC+1, niv wrote:
Trying to get started with PSL assertions.



I've written a simple counter, code below, with a couple of PSL assertions at the end. However, the 2nd assertion fails on the transition from cntr_max-1 to cntr_max, but the rollover assertion seems to work.

Any ideas please?





LIBRARY ieee;

USE ieee.std_logic_1164.all;

USE ieee.numeric_std.ALL;

--------------------------------------------------------------------------------

ENTITY psl_counter_test IS

GENERIC(

my_width : NATURAL := 6

);

PORT(

rst : IN STD_LOGIC;

clk : IN STD_LOGIC;

my_count : OUT STD_LOGIC_VECTOR (my_width-1 DOWNTO 0)

);



END ENTITY psl_counter_test ;

--------------------------------------------------------------------------------

ARCHITECTURE rtl OF psl_counter_test IS

SIGNAL my_counter : UNSIGNED(my_width-1 DOWNTO 0);

SIGNAL en_counter : UNSIGNED(3 DOWNTO 0);

SIGNAL enable : STD_LOGIC;

CONSTANT cntr_max : NATURAL := 2**my_width - 1;

BEGIN

my_count <= STD_LOGIC_VECTOR(my_counter);

--------------------------------------------------------------------------------

count_en : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

en_counter <= (OTHERS => '0'); -- reset to max

enable <= '0';

ELSIF RISING_EDGE(clk) THEN

en_counter <= en_counter + 1; -- rolls over, so div by 64.

IF en_counter = 15 THEN

enable <= '1';

ELSE

enable <= '0';

END IF;

END IF;

END PROCESS count_en;

--------------------------------------------------------------------------------

count_up : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

my_counter <= (OTHERS => '0'); -- reset to max

ELSIF RISING_EDGE(clk) THEN

IF enable = '1' THEN

my_counter <= my_counter + 1; -- continuous count with rollover.

ELSE

NULL;

END IF;

END IF;

END PROCESS count_up;

--------------------------------------------------------------------------------

-- psl begin

--

-- default clock is rising_edge(clk);

--

-- property psl_01 is

-- ({(my_counter = cntr_max) and (enable = '1')} |=> {my_counter = 0} );

-- assert always psl_01 report"ERROR: 'my_counter' did not rollover to zero.";

--

-- property psl_02 is

-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );

-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";

--

-- end

END ARCHITECTURE rtl;
Click to expand...

Note; some of the comments for size etc are wrong, I cut code down to make simple example.
 
On 25/09/2014 23:41, niv wrote:
Trying to get started with PSL assertions.

I've written a simple counter, code below, with a couple of PSL assertions at the end. However, the 2nd assertion fails on the transition from cntr_max-1 to cntr_max, but the rollover assertion seems to work.
Any ideas please?
... snip
-- property psl_02 is
-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );
Click to expand...

When my_counter reaches 62 and enable is asserted you are effectively
checking that in the next cycle my_counter(which is now 63)+1=64 which
of course will never happen.

You probably wanted to write:

|=> {prev(my_counter) + 1}

The prev() operator return the value from the previous cycle.

You might also want to add an abort operator for your reset,

Good luck,
Hans
www.ht-lab.com


-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";
--
-- end
END ARCHITECTURE rtl;
Click to expand...
 
On Thursday, September 25, 2014 11:41:21 PM UTC+1, niv wrote:
Trying to get started with PSL assertions.



I've written a simple counter, code below, with a couple of PSL assertions at the end. However, the 2nd assertion fails on the transition from cntr_max-1 to cntr_max, but the rollover assertion seems to work.

Any ideas please?





LIBRARY ieee;

USE ieee.std_logic_1164.all;

USE ieee.numeric_std.ALL;

--------------------------------------------------------------------------------

ENTITY psl_counter_test IS

GENERIC(

my_width : NATURAL := 6

);

PORT(

rst : IN STD_LOGIC;

clk : IN STD_LOGIC;

my_count : OUT STD_LOGIC_VECTOR (my_width-1 DOWNTO 0)

);



END ENTITY psl_counter_test ;

--------------------------------------------------------------------------------

ARCHITECTURE rtl OF psl_counter_test IS

SIGNAL my_counter : UNSIGNED(my_width-1 DOWNTO 0);

SIGNAL en_counter : UNSIGNED(3 DOWNTO 0);

SIGNAL enable : STD_LOGIC;

CONSTANT cntr_max : NATURAL := 2**my_width - 1;

BEGIN

my_count <= STD_LOGIC_VECTOR(my_counter);

--------------------------------------------------------------------------------

count_en : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

en_counter <= (OTHERS => '0'); -- reset to max

enable <= '0';

ELSIF RISING_EDGE(clk) THEN

en_counter <= en_counter + 1; -- rolls over, so div by 64.

IF en_counter = 15 THEN

enable <= '1';

ELSE

enable <= '0';

END IF;

END IF;

END PROCESS count_en;

--------------------------------------------------------------------------------

count_up : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

my_counter <= (OTHERS => '0'); -- reset to max

ELSIF RISING_EDGE(clk) THEN

IF enable = '1' THEN

my_counter <= my_counter + 1; -- continuous count with rollover.

ELSE

NULL;

END IF;

END IF;

END PROCESS count_up;

--------------------------------------------------------------------------------

-- psl begin

--

-- default clock is rising_edge(clk);

--

-- property psl_01 is

-- ({(my_counter = cntr_max) and (enable = '1')} |=> {my_counter = 0} );

-- assert always psl_01 report"ERROR: 'my_counter' did not rollover to zero.";

--

-- property psl_02 is

-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );

-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";

--

-- end

END ARCHITECTURE rtl;
Click to expand...

OK, I understand there is a "prev" command, but what I don't understand is why the assertion works (passes) for all values except the max-1 to max case.
i.e. 0 to 1 ok, 1 to 2 ok........ 61 to 62 ok, but 62 to 63 fails. The special rollover assertion case works ok too.

Niv.
 
On 27/09/2014 09:48, niv wrote:
On Thursday, September 25, 2014 11:41:21 PM UTC+1, niv wrote:
Trying to get started with PSL assertions.
...

-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );

-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";

OK, I understand there is a "prev" command, but what I don't understand is why the assertion works (passes) for all values except the max-1 to max case.
i.e. 0 to 1 ok, 1 to 2 ok........ 61 to 62 ok, but 62 to 63 fails.
Click to expand...

Yes, but in the last case when my_counter=62 you are checking that in
the next clock cycle (|=>) where my_counter has now changed to 63 you
expect 63+1.

Regards,
Hans.
www.ht-lab.com


The special rollover assertion case works ok too.
Niv.
Click to expand...
 
IMHO, plain old procedural VHDL with assertion statements is so much easier to write and debug...

Are you using PSL to support Formal Analysis?

Andy
 
On Thursday, September 25, 2014 11:41:21 PM UTC+1, niv wrote:
Trying to get started with PSL assertions.



I've written a simple counter, code below, with a couple of PSL assertions at the end. However, the 2nd assertion fails on the transition from cntr_max-1 to cntr_max, but the rollover assertion seems to work.

Any ideas please?





LIBRARY ieee;

USE ieee.std_logic_1164.all;

USE ieee.numeric_std.ALL;

--------------------------------------------------------------------------------

ENTITY psl_counter_test IS

GENERIC(

my_width : NATURAL := 6

);

PORT(

rst : IN STD_LOGIC;

clk : IN STD_LOGIC;

my_count : OUT STD_LOGIC_VECTOR (my_width-1 DOWNTO 0)

);



END ENTITY psl_counter_test ;

--------------------------------------------------------------------------------

ARCHITECTURE rtl OF psl_counter_test IS

SIGNAL my_counter : UNSIGNED(my_width-1 DOWNTO 0);

SIGNAL en_counter : UNSIGNED(3 DOWNTO 0);

SIGNAL enable : STD_LOGIC;

CONSTANT cntr_max : NATURAL := 2**my_width - 1;

BEGIN

my_count <= STD_LOGIC_VECTOR(my_counter);

--------------------------------------------------------------------------------

count_en : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

en_counter <= (OTHERS => '0'); -- reset to max

enable <= '0';

ELSIF RISING_EDGE(clk) THEN

en_counter <= en_counter + 1; -- rolls over, so div by 64.

IF en_counter = 15 THEN

enable <= '1';

ELSE

enable <= '0';

END IF;

END IF;

END PROCESS count_en;

--------------------------------------------------------------------------------

count_up : PROCESS (rst, clk)

BEGIN

IF rst = '1' THEN

my_counter <= (OTHERS => '0'); -- reset to max

ELSIF RISING_EDGE(clk) THEN

IF enable = '1' THEN

my_counter <= my_counter + 1; -- continuous count with rollover.

ELSE

NULL;

END IF;

END IF;

END PROCESS count_up;

--------------------------------------------------------------------------------

-- psl begin

--

-- default clock is rising_edge(clk);

--

-- property psl_01 is

-- ({(my_counter = cntr_max) and (enable = '1')} |=> {my_counter = 0} );

-- assert always psl_01 report"ERROR: 'my_counter' did not rollover to zero.";

--

-- property psl_02 is

-- ({(my_counter < cntr_max) and (enable = '1')} |=> {my_counter + 1} );

-- assert always psl_02 report"ERROR: 'my_counter' did not increment as expected.";

--

-- end

END ARCHITECTURE rtl;
Click to expand...

I sort of agree, but they're not as powerful or anywhere near as concise, but a bit of steep learning curve (& I'm at the very bottom).
Both really; formal & simulation.
However, once learnt (learned?) then PSL should be a powerful verification aid (I hope). Picked PSL rather than SVA as that means we wont need a mixed licence for simulator, just VHDL capable.
 
Hi Andy,

On 30/09/2014 18:54, Andy wrote:
> IMHO, plain old procedural VHDL with assertion statements is so much easier to write and debug...

well.... perhaps, it all depends on the complexity of the assertion. You
can write very simple PSL assertions and if you are already using OVL
then the jump to PSL is not that difficult.
The problem with PSL is that it requires an expensive license and hence
not many engineers get access to it.

> Are you using PSL to support Formal Analysis?

Perhaps in the future when formal tools become more affordable,

Regards,
Hans.
www.ht-lab.com

Andy
Click to expand...
 
Define "very simple" for real-world applications.

If you mean "very short and cryptic," I agree completely.

Andy
 
You must log in or register to reply here.

Welcome to EDABoard.com

Sponsor

Back
Top