Move default_clock declarations to architecture declaration section, for tmeissner/psl_with_ghdl#6

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));
 

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

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";

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}

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};
 

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);

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);
 

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);
 

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);
 

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;
 

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);
 

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));
 

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));
 

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));
 

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));
 

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));
 

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"))

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));
 

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);
 

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);
 

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));
 

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);
 

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};
 

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

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};

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

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.

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

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

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

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};
 

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};

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};
 

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

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);
 

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));
 

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;
 

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;