From 91e04b67fdcd9206011117fef9769ee7e7ff3f4c Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sun, 2 Feb 2025 16:44:11 +0100 Subject: [PATCH] Move default_clock declarations to architecture declaration section, for tmeissner/psl_with_ghdl#6 --- src/psl_abort.vhd | 6 +++--- src/psl_always.vhd | 6 +++--- src/psl_before.vhd | 6 +++--- src/psl_cover.vhd | 6 +++--- src/psl_endpoint.vhd | 6 +++--- src/psl_eventually.vhd | 6 +++--- src/psl_fell.vhd | 6 +++--- src/psl_logical_iff.vhd | 6 +++--- src/psl_logical_implication.vhd | 6 +++--- src/psl_never.vhd | 6 +++--- src/psl_next.vhd | 6 +++--- src/psl_next_3.vhd | 6 +++--- src/psl_next_a.vhd | 6 +++--- src/psl_next_e.vhd | 6 +++--- src/psl_next_event.vhd | 6 +++--- src/psl_next_event_4.vhd | 6 +++--- src/psl_next_event_a.vhd | 7 +++---- src/psl_next_event_e.vhd | 6 +++--- src/psl_onehot.vhd | 6 +++--- src/psl_onehot0.vhd | 6 +++--- src/psl_prev.vhd | 7 +++---- src/psl_rose.vhd | 6 +++--- src/psl_sere.vhd | 6 +++--- src/psl_sere_concat.vhd | 6 +++--- src/psl_sere_consecutive_repetition.vhd | 6 +++--- src/psl_sere_fusion.vhd | 6 +++--- src/psl_sere_len_matching_and.vhd | 6 +++--- src/psl_sere_non_consecutive_goto_repetition.vhd | 6 +++--- src/psl_sere_non_consecutive_repeat_repetition.vhd | 6 +++--- src/psl_sere_non_len_matching_and.vhd | 6 +++--- src/psl_sere_non_overlapping_suffix_impl.vhd | 6 +++--- src/psl_sere_or.vhd | 6 +++--- src/psl_sere_overlapping_suffix_impl.vhd | 6 +++--- src/psl_sere_within.vhd | 6 +++--- src/psl_stable.vhd | 6 +++--- src/psl_until.vhd | 6 +++--- src/yosys_anyconst.vhd | 6 +++--- src/yosys_anyseq.vhd | 6 +++--- 38 files changed, 114 insertions(+), 116 deletions(-) diff --git a/src/psl_abort.vhd b/src/psl_abort.vhd index 2838762..3533e6a 100644 --- a/src/psl_abort.vhd +++ b/src/psl_abort.vhd @@ -15,6 +15,9 @@ architecture psl of psl_abort is signal a, b, c, d : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin -- Creating an abort signal which is asynchronously set & reset @@ -26,9 +29,6 @@ begin SEQ_C : sequencer generic map ("-_________") port map (clk, c); -- D : _|________ - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion doesn't hold at cycle 4 WITHOUT_ABORT_a : assert (always a -> next (b before a)); diff --git a/src/psl_always.vhd b/src/psl_always.vhd index 111950d..b86218c 100644 --- a/src/psl_always.vhd +++ b/src/psl_always.vhd @@ -15,6 +15,9 @@ architecture psl of psl_always is signal a : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -22,9 +25,6 @@ begin SEQ : sequencer generic map ("--____") port map (clk, a); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Beware: potential pitfall! -- Every time a PSL assertion is similar to a concurrent -- VHDL assertion at that place, it is interpreted as such diff --git a/src/psl_before.vhd b/src/psl_before.vhd index e087f78..f3e596f 100644 --- a/src/psl_before.vhd +++ b/src/psl_before.vhd @@ -17,6 +17,9 @@ architecture psl of psl_before is signal c, d : std_logic; signal e, f : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -33,9 +36,6 @@ begin SEQ_F : sequencer generic map ("_-_______-_") port map (clk, f); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds BEFORE_0_a : assert always (a -> next (b before a)) report "BEFORE_0_a failed"; diff --git a/src/psl_cover.vhd b/src/psl_cover.vhd index f2e906b..5a6d0fc 100644 --- a/src/psl_cover.vhd +++ b/src/psl_cover.vhd @@ -15,6 +15,9 @@ architecture psl of psl_cover is signal req, busy, done : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_DONE : sequencer generic map ("________-_") port map (clk, done); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Covers a transfer request -- This cover directive holds at cycle 1 COVER_0_c : cover {req} diff --git a/src/psl_endpoint.vhd b/src/psl_endpoint.vhd index ab2e80f..adde3f3 100644 --- a/src/psl_endpoint.vhd +++ b/src/psl_endpoint.vhd @@ -16,6 +16,9 @@ architecture psl of psl_endpoint is signal a, b : std_logic; signal c, d : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -26,9 +29,6 @@ begin SEQ_D : sequencer generic map ("____________-_") port map (clk, d); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- only endpoint in psl comment works -- psl endpoint ENDPOINT_1_e is {a; b[*3]; c}; diff --git a/src/psl_eventually.vhd b/src/psl_eventually.vhd index 1136ae5..6883eea 100644 --- a/src/psl_eventually.vhd +++ b/src/psl_eventually.vhd @@ -15,6 +15,9 @@ architecture psl of psl_eventually is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("_______-______-_") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds -- This assertion leads to a GHDL synthesis crash with bug report EVENTUALLY_a : assert always (a -> eventually! b); diff --git a/src/psl_fell.vhd b/src/psl_fell.vhd index d65eea0..fe54a9c 100644 --- a/src/psl_fell.vhd +++ b/src/psl_fell.vhd @@ -15,6 +15,9 @@ architecture psl of psl_fell is signal a, b, c : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_C : sequencer generic map ("__-__-___-_") port map (clk, c); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds FELL_0_a : assert always (fell(a) -> c); diff --git a/src/psl_logical_iff.vhd b/src/psl_logical_iff.vhd index ea6c4dc..ac3444b 100644 --- a/src/psl_logical_iff.vhd +++ b/src/psl_logical_iff.vhd @@ -15,6 +15,9 @@ architecture psl of psl_logical_iff is signal a, b, c : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_C : sequencer generic map ("_-__-______") port map (clk, c); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds IFF_0_a : assert always (a <-> b or c); diff --git a/src/psl_logical_implication.vhd b/src/psl_logical_implication.vhd index 64d884b..fe0f3ae 100644 --- a/src/psl_logical_implication.vhd +++ b/src/psl_logical_implication.vhd @@ -15,6 +15,9 @@ architecture psl of psl_logical_implication is signal a, b, c, d : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -25,9 +28,6 @@ begin SEQ_D : sequencer generic map ("___________") port map (clk, d); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds IMPLICATION_0_a : assert always (a -> b or c); diff --git a/src/psl_never.vhd b/src/psl_never.vhd index c73ba33..d23775a 100644 --- a/src/psl_never.vhd +++ b/src/psl_never.vhd @@ -15,6 +15,9 @@ architecture psl of psl_never is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("__-_") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEVER_0_a : assert never a; diff --git a/src/psl_next.vhd b/src/psl_next.vhd index 4049436..4de3601 100644 --- a/src/psl_next.vhd +++ b/src/psl_next.vhd @@ -16,6 +16,9 @@ architecture psl of psl_next is signal a, b : std_logic; signal c, d : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -28,9 +31,6 @@ begin SEQ_D : sequencer generic map ("_--__-___--") port map (clk, d); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_0_a : assert always (a -> next b); diff --git a/src/psl_next_3.vhd b/src/psl_next_3.vhd index 51d155a..c2ac1db 100644 --- a/src/psl_next_3.vhd +++ b/src/psl_next_3.vhd @@ -17,6 +17,9 @@ architecture psl of psl_next_3 is signal c, d : std_logic; signal e, f : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -33,9 +36,6 @@ begin SEQ_F : sequencer generic map ("_____-----_") port map (clk, f); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_0_a : assert always (a -> next[3] (b)); diff --git a/src/psl_next_a.vhd b/src/psl_next_a.vhd index c724298..17175ef 100644 --- a/src/psl_next_a.vhd +++ b/src/psl_next_a.vhd @@ -20,6 +20,9 @@ architecture psl of psl_next_a is signal i, j : std_logic; signal k, l : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -48,9 +51,6 @@ begin SEQ_L : sequencer generic map ("_______-__") port map (clk, l); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion doesn't hold at cycle 6 NEXT_0_a : assert always (a -> next_a[3 to 5] (b)); diff --git a/src/psl_next_e.vhd b/src/psl_next_e.vhd index 9f94f70..edb0f5b 100644 --- a/src/psl_next_e.vhd +++ b/src/psl_next_e.vhd @@ -20,6 +20,9 @@ architecture psl of psl_next_e is signal i, j : std_logic; signal k, l : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -48,9 +51,6 @@ begin SEQ_L : sequencer generic map ("_______-__") port map (clk, l); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_0_a : assert always (a -> next_e[3 to 5] (b)); diff --git a/src/psl_next_event.vhd b/src/psl_next_event.vhd index 33417d4..4077079 100644 --- a/src/psl_next_event.vhd +++ b/src/psl_next_event.vhd @@ -16,6 +16,9 @@ architecture psl of psl_next_event is signal a, b, c : std_logic; signal d, e, f : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin -- 012345678901234 @@ -29,9 +32,6 @@ begin SEQ_F : sequencer generic map ("____-___-__-___") port map (clk, f); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_EVENT_0_a : assert always (a -> next_event(b)(c)); diff --git a/src/psl_next_event_4.vhd b/src/psl_next_event_4.vhd index 59450c9..a10d160 100644 --- a/src/psl_next_event_4.vhd +++ b/src/psl_next_event_4.vhd @@ -16,6 +16,9 @@ architecture psl of psl_next_event_4 is signal a, b, c : std_logic; signal d, e, f : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin -- 0123456789012345 @@ -24,9 +27,6 @@ begin SEQ_C : sequencer generic map ("_____-_________-") port map (clk, c); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_EVENT_0_a : assert always (a -> next_event(b)[4](c)); diff --git a/src/psl_next_event_a.vhd b/src/psl_next_event_a.vhd index 09b5185..42857b4 100644 --- a/src/psl_next_event_a.vhd +++ b/src/psl_next_event_a.vhd @@ -18,6 +18,9 @@ architecture psl of psl_next_event_a is signal a, c : std_logic; signal b : std_logic_vector(3 downto 0); + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -27,10 +30,6 @@ begin SEQ_C : sequencer generic map ("_____-___---______--_--_") port map (clk, c); - - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Check for one possible value of b -- Both assertions hold (see ghdl/ghdl#2157) NEXT_EVENT_0_a : assert always ((a and b = x"4") -> next_event_a(c)[1 to 4](b = x"4")) diff --git a/src/psl_next_event_e.vhd b/src/psl_next_event_e.vhd index 660669f..f83fe16 100644 --- a/src/psl_next_event_e.vhd +++ b/src/psl_next_event_e.vhd @@ -15,6 +15,9 @@ architecture psl of psl_next_event_e is signal a, b, c : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_C : sequencer generic map ("______-___-____") port map (clk, c); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds NEXT_EVENT_0_a : assert always (a -> next_event_e(b)[1 to 2](c)); diff --git a/src/psl_onehot.vhd b/src/psl_onehot.vhd index 9ca8ac1..22fe173 100644 --- a/src/psl_onehot.vhd +++ b/src/psl_onehot.vhd @@ -15,6 +15,9 @@ architecture psl of psl_onehot is signal a, b : std_logic_vector(3 downto 0); + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : hex_sequencer generic map ("111222444888999") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds ONEHOT_0_a : assert always onehot(a); diff --git a/src/psl_onehot0.vhd b/src/psl_onehot0.vhd index 69558fb..71dd13f 100644 --- a/src/psl_onehot0.vhd +++ b/src/psl_onehot0.vhd @@ -15,6 +15,9 @@ architecture psl of psl_onehot0 is signal a, b : std_logic_vector(3 downto 0); + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : hex_sequencer generic map ("000111222444888fff") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds ONEHOT0_0_a : assert always onehot0(a); diff --git a/src/psl_prev.vhd b/src/psl_prev.vhd index 09bcb5c..7f99dd3 100644 --- a/src/psl_prev.vhd +++ b/src/psl_prev.vhd @@ -19,6 +19,9 @@ architecture psl of psl_prev is signal di, do : std_logic_vector(3 downto 0); signal cnt : std_logic_vector(3 downto 0); + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -31,10 +34,6 @@ begin SEQ_CNT : hex_sequencer generic map ("0123456789ABCDEF") port map (clk, cnt); - - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds PREV_0_a : assert always (valid -> a = prev(a)); diff --git a/src/psl_rose.vhd b/src/psl_rose.vhd index f39a3c2..5bc7238 100644 --- a/src/psl_rose.vhd +++ b/src/psl_rose.vhd @@ -15,6 +15,9 @@ architecture psl of psl_rose is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("_-___-_-___") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds ROSE_0_a : assert always (rose(a) -> b); diff --git a/src/psl_sere.vhd b/src/psl_sere.vhd index 9274a9b..e03ee8a 100644 --- a/src/psl_sere.vhd +++ b/src/psl_sere.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("_-____") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds SERE_0_a : assert {a}; diff --git a/src/psl_sere_concat.vhd b/src/psl_sere_concat.vhd index d9a9a9c..0ac4b21 100644 --- a/src/psl_sere_concat.vhd +++ b/src/psl_sere_concat.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_concat is signal req, avalid, busy, adone, data, ddone : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -27,9 +30,6 @@ begin SEQ_DDONE : sequencer generic map ("___________-__") port map (clk, ddone); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- SERE concatenation operator -- RHS starts at one cycle cycle that the LHS ends -- This assertion holds diff --git a/src/psl_sere_consecutive_repetition.vhd b/src/psl_sere_consecutive_repetition.vhd index b0863a0..96c2903 100644 --- a/src/psl_sere_consecutive_repetition.vhd +++ b/src/psl_sere_consecutive_repetition.vhd @@ -17,6 +17,9 @@ architecture psl of psl_sere_consecutive_repetition is signal d, e, f : std_logic; signal g, h, i : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -36,9 +39,6 @@ begin SEQ_I : sequencer generic map ("________-_") port map (clk, i); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Simple SERE with repetitions done manual without operators -- This assertion holds SERE_0_a : assert always {a} |=> {b; b; b; b; c}; diff --git a/src/psl_sere_fusion.vhd b/src/psl_sere_fusion.vhd index 4ad996b..bd088dc 100644 --- a/src/psl_sere_fusion.vhd +++ b/src/psl_sere_fusion.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_fusion is signal req, avalid, busy, adone, data, ddone : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -27,9 +30,6 @@ begin SEQ_DDONE : sequencer generic map ("__________-__") port map (clk, ddone); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- SERE fusion operator -- SERE fusion is like concatenation (;) but starts at -- the same cycle that the LHS ends diff --git a/src/psl_sere_len_matching_and.vhd b/src/psl_sere_len_matching_and.vhd index 3a60542..5f893ba 100644 --- a/src/psl_sere_len_matching_and.vhd +++ b/src/psl_sere_len_matching_and.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_len_matching_and is signal req, busy, valid, done : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -25,9 +28,6 @@ begin SEQ_DONE : sequencer generic map ("________-_") port map (clk, done); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Length matching AND two SERE -- valid has to hold 3 times between req & done. -- busy has to hold each cycle between req & done. diff --git a/src/psl_sere_non_consecutive_goto_repetition.vhd b/src/psl_sere_non_consecutive_goto_repetition.vhd index 8a45cc0..02ced9b 100644 --- a/src/psl_sere_non_consecutive_goto_repetition.vhd +++ b/src/psl_sere_non_consecutive_goto_repetition.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_non_consecutive_goto_repetition is signal req, busy, done : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_DONE : sequencer generic map ("_______-_") port map (clk, done); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Non consecutive repetition of 3 cycles without padding -- busy has to hold on 3 cycles between req & done -- This assertion holds diff --git a/src/psl_sere_non_consecutive_repeat_repetition.vhd b/src/psl_sere_non_consecutive_repeat_repetition.vhd index 19c4c5b..dbc5951 100644 --- a/src/psl_sere_non_consecutive_repeat_repetition.vhd +++ b/src/psl_sere_non_consecutive_repeat_repetition.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_non_consecutive_repeat_repetition is signal req, busy, done : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -24,9 +27,6 @@ begin SEQ_DONE : sequencer generic map ("________-_") port map (clk, done); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Non consecutive repetition of 3 cycles with possible padding -- busy has to hold on 3 cycles between req & done -- This assertion holds diff --git a/src/psl_sere_non_len_matching_and.vhd b/src/psl_sere_non_len_matching_and.vhd index 6396412..7efb90e 100644 --- a/src/psl_sere_non_len_matching_and.vhd +++ b/src/psl_sere_non_len_matching_and.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_non_len_matching_and is signal req, done0, done1, done2, ack : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -26,9 +29,6 @@ begin SEQ_ACK : sequencer generic map ("_________-_") port map (clk, ack); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Non length matching AND three SERE -- Each of done0, done1 & done2 has to hold a cycle after -- req holded. Transfer is ended by ack holding one cycle diff --git a/src/psl_sere_non_overlapping_suffix_impl.vhd b/src/psl_sere_non_overlapping_suffix_impl.vhd index e8f1997..d716848 100644 --- a/src/psl_sere_non_overlapping_suffix_impl.vhd +++ b/src/psl_sere_non_overlapping_suffix_impl.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_non_overlapping_suffix_impl is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("_-____-__") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds SERE_0_a : assert always {a; a} |=> {not a}; diff --git a/src/psl_sere_or.vhd b/src/psl_sere_or.vhd index 24ad5ec..aa044b0 100644 --- a/src/psl_sere_or.vhd +++ b/src/psl_sere_or.vhd @@ -16,6 +16,9 @@ architecture psl of psl_sere_or is signal req2, req4, busy, valid, done : std_logic; signal req, wen, ends : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -32,9 +35,6 @@ begin SEQ_ENDS : sequencer generic map ("_______-__________-_") port map (clk, ends); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Transfer started by req2 with 2 valids has to be finished by done -- This assertion holds SERE_0_a : assert always {req2 ; {valid[->2]} && {busy and not done}[+]} |=> {not busy and done}; diff --git a/src/psl_sere_overlapping_suffix_impl.vhd b/src/psl_sere_overlapping_suffix_impl.vhd index f7746ca..ff32eba 100644 --- a/src/psl_sere_overlapping_suffix_impl.vhd +++ b/src/psl_sere_overlapping_suffix_impl.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_overlapping_suffix_impl is signal a, b : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -23,9 +26,6 @@ begin SEQ_B : sequencer generic map ("_-____-__") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds SERE_0_a : assert always {a; a} |-> {a and b}; diff --git a/src/psl_sere_within.vhd b/src/psl_sere_within.vhd index 18b3689..be86639 100644 --- a/src/psl_sere_within.vhd +++ b/src/psl_sere_within.vhd @@ -15,6 +15,9 @@ architecture psl of psl_sere_within is signal req, busy, valid, done : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -25,9 +28,6 @@ begin SEQ_DONE : sequencer generic map ("________-_") port map (clk, done); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- Occurrance of a SERE during another SERE -- valid has to hold 3 times during busy holds and done does't hold -- This assertion holds diff --git a/src/psl_stable.vhd b/src/psl_stable.vhd index 934efa6..e452b3b 100644 --- a/src/psl_stable.vhd +++ b/src/psl_stable.vhd @@ -16,6 +16,9 @@ architecture psl of psl_stable is signal valid, ack, a : std_logic; signal b : std_logic_vector(3 downto 0); + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -26,9 +29,6 @@ begin SEQ_B : hex_sequencer generic map ("0110066600") port map (clk, b); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds STABLE_0_a : assert always {not valid; valid} |=> (stable(a) until_ ack); diff --git a/src/psl_until.vhd b/src/psl_until.vhd index 8ceba4b..8056695 100644 --- a/src/psl_until.vhd +++ b/src/psl_until.vhd @@ -17,6 +17,9 @@ architecture psl of psl_until is signal d, e, f : std_logic; signal g, h, i : std_logic; + -- All is sensitive to rising edge of clk + default clock is rising_edge(clk); + begin @@ -36,9 +39,6 @@ begin SEQ_I : sequencer generic map ("__-___") port map (clk, i); - -- All is sensitive to rising edge of clk - default clock is rising_edge(clk); - -- This assertion holds UNTIL_0_a : assert always (a -> next (b until c)); diff --git a/src/yosys_anyconst.vhd b/src/yosys_anyconst.vhd index 7af256e..9e8b1af 100644 --- a/src/yosys_anyconst.vhd +++ b/src/yosys_anyconst.vhd @@ -21,12 +21,12 @@ architecture psl of yosys_anyconst is attribute anyconst of a : signal is true; attribute anyconst of b : signal is true; -begin - - -- All is sensitive to rising edge of clk default clock is rising_edge(clk); +begin + + -- a should always be high ANY_ASSUME_0_a : assume always a; diff --git a/src/yosys_anyseq.vhd b/src/yosys_anyseq.vhd index eb5b059..b799675 100644 --- a/src/yosys_anyseq.vhd +++ b/src/yosys_anyseq.vhd @@ -21,12 +21,12 @@ architecture psl of yosys_anyseq is attribute anyseq of a : signal is true; attribute anyseq of b : signal is true; -begin - - -- All is sensitive to rising edge of clk default clock is rising_edge(clk); +begin + + -- a should always be high ANY_ASSUME_0_a : assume always a;