From 4dd0f1b33c83f2a1cfe9bbd80562c564c9d06a95 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 20 May 2020 14:17:06 +0200 Subject: [PATCH] Fixed assertion - combining SEREs isn't trivial ;) --- src/psl_cover.vhd | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/psl_cover.vhd b/src/psl_cover.vhd index bd31966..ee0b05b 100644 --- a/src/psl_cover.vhd +++ b/src/psl_cover.vhd @@ -67,8 +67,8 @@ begin -- to see if your assertions can actually be active. -- This assertion checks for the final done at the end of transfer. -- In cover mode, the LHS side of the property has to hold. - -- This cover directive holds at cycle 6 - ASSERT_a : assert always {req; {{busy[=3]} && {not done[+]}}} |=> {done}; + -- This cover directive holds at cycle 7 + ASSERT_a : assert always {req; (busy and not done)[=3]; not done} |=> {done}; end architecture psl;