Browse Source

Fix PSL assertions for local wen and local ren

The second logical implication was made the whole property holding
when the part after the 1st implication didn't hold. So, the 2nd
implication is replaced by an and in combination with the next
operator. Now the property fails when one of the two and'ed parts after
the implication fails.
pull/1/head
T. Meissner 9 years ago
parent
commit
6659dbbe31
1 changed files with 4 additions and 4 deletions
  1. +4
    -4
      syn/WishBoneSlaveE.vhd

+ 4
- 4
syn/WishBoneSlaveE.vhd View File

@ -112,14 +112,14 @@ begin
--
-- psl LOCAL_WE : assert always
-- LocalWen_o ->
-- (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) ->
-- next not(LocalWen_o)
-- (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) and
-- (next not(LocalWen_o))
-- report "PSL ERROR: LocalWen invalid";
--
-- psl LOCAL_RE : assert always
-- LocalRen_o ->
-- (WbCyc_i and WbStb_i and not(WbWe_i) and not(LocalWen_o)) ->
-- next not(LocalRen_o)
-- (WbCyc_i and WbStb_i and not(WbWe_i) and not(LocalWen_o)) and
-- (next not(LocalRen_o))
-- report "PSL ERROR: LocalRen invalid";
--
-- psl RESET : assert always


Loading…
Cancel
Save