Asserting the Data-Valid Rule — SDA Stable While SCL Is High

      -- NOT: rose(scl)
      scl_rise  <= '1' when scl = '1' and scl_d = '0' else '0';
      scl_fall  <= '1' when scl = '0' and scl_d = '1' else '0';

      -- psl assert always ((scl = '1' and sda /= prev(sda)) -> false);

      -- psl SDA_STABLE_WHILE_SCL_HIGH : assert always (
      --        (scl = '1' and prev(scl) = '1' and sda /= prev(sda)
      --         and in_byte = '1' and start_now = '0' and stop_now = '0')
      --        -> false)
      --      report "22.2 SDA changed while SCL was high, mid-byte";

   -- ---------------------------------------------------------------------------
   -- i2c_props.vhd
   -- The I2C protocol rules as temporal properties, in PSL, actually executed.
   --
   -- EVIDENCE: SIMULATED. Unlike Module 21, these properties run. NVC 1.23 evaluates
   -- directives embedded in VHDL comments when analysed with `--psl`, and
   -- `probe/capability.sh` measures exactly which constructs are usable -- including three
   -- that the tool ACCEPTS AND NEVER EVALUATES, which are therefore banned from this file.
   --
   -- A TOOLING GOTCHA THAT COSTS AN HOUR IF YOU MEET IT COLD: with `--psl` enabled, ANY
   -- comment whose first word is "psl" is parsed as a directive -- including a prose
   -- sentence about PSL. The error names the comment as an unexpected directive while
   -- parsing a library unit, which reads as a problem with the file's structure rather
   -- than with a word in a comment. Documentation here therefore never opens with it.
   --
   -- WHY THE PROPERTIES LIVE IN THEIR OWN ENTITY. They are bound to the RESOLVED bus and
   -- to nothing inside the design. This entity has no access to the target's state, so a
   -- property here cannot accidentally check the design against itself -- the same
   -- argument Chapter 20.7 makes for the monitor, applied to assertions.
   --
   -- THE ONE DEPENDENCY WORTH DECLARING. Several rules are conditional on "we are inside a
   -- byte" or "a transfer is open", and the bus does not carry those facts -- they have to
   -- be derived. This entity derives them itself, from the specification, in the framing
   -- tracker below. That is a deliberate reimplementation and it is the assertion set's
   -- weakest point: if the tracker is wrong, the properties are conditional on a wrong
   -- antecedent and go quiet rather than firing. Which is exactly why every property in
   -- this file has a scenario that makes it FIRE -- see i2c_assert_tb.vhd.
   -- ---------------------------------------------------------------------------
   library ieee;
   use ieee.std_logic_1164.all;
   use ieee.numeric_std.all;

   entity i2c_props is
      generic (
         -- Clocks of bus-idle time a STOP must be followed by before a new START is
         -- legal. A protocol number (tBUF), expressed in sampling clocks here because
         -- this environment has no picoseconds -- Chapter 20.2 records that no timing
         -- parameter in the specification is checked anywhere in this curriculum, and
         -- this is a count of cycles rather than a time.
         BUS_FREE_CLKS : natural := 8;
         -- Sampling cycles of simultaneous SDA pulling that are tolerated.
         --
         -- THIS NUMBER HAD TO BE RAISED, and the reason is the honest limit of the whole
         -- property. Two devices pulling SDA low is not itself illegal -- the wired-AND is
         -- unharmed, and at every acknowledge handover the outgoing driver and the incoming
         -- one legitimately overlap. Measured against the real target that overlap runs to
         -- about six cycles, most of a half period. A threshold of four therefore fired on
         -- every byte of legal traffic.
         --
         -- So the threshold is now longer than a whole bit period, where an overlap cannot
         -- be a handover. That makes the property SOUND and WEAK: it catches a line held by
         -- two devices across a bit boundary and cannot catch a short illegal overlap.
         -- Catching that needs to know WHO OWNS the slot, which is protocol state rather
         -- than a count -- so it is a scoreboard question, not an assertion. Chapter 22.1
         -- is about exactly this boundary, and this property is where the module met it.
         OVERLAP_CLKS  : positive := 20
      );
      port (
         clk   : in std_logic;
         rst_n : in std_logic;

         -- the RESOLVED bus, and nothing else from the design
         scl   : in std_logic;
         sda   : in std_logic;

         -- how many devices are pulling each line. Not derivable from the line: the
         -- wired-AND of one puller and two is identical, so the acknowledge-slot
         -- ownership rule has no bus-level formulation without this.
         scl_holders : in natural;
         sda_holders : in natural;

         -- observability, for a bench to assert against
         n_fired : out natural;

         -- THE ANTECEDENTS, EXPORTED. A property that does not fire is either satisfied or
         -- vacuous, and from outside those look identical. Exposing the conditions its
         -- antecedents depend on is what makes the difference diagnosable: a bench can
         -- report that `in_byte` was low at the moment it expected a mid-byte STOP, which
         -- says the SCENARIO was wrong rather than the property.
         o_active   : out std_logic;
         o_in_byte  : out std_logic;
         o_bitcnt   : out natural;
         o_idle_cnt : out natural;

         -- ONE COUNTER PER EVENT, AND ONE PER VIOLATION. Without the event counters, a
         -- property that stays quiet is indistinguishable from a scenario that never
         -- produced the situation -- and the second is far more common. Counting the
         -- antecedent separately turns "the assertion is broken" into "the stimulus never
         -- happened", which are different problems with different fixes.
         n_starts        : out natural;   -- START events seen
         n_stops         : out natural;   -- STOP events seen
         n_stop_mid_byte : out natural;   -- ... of which arrived mid-byte
         n_start_early   : out natural;   -- ... STARTs inside the bus-free interval

         -- The value the bus-free rule was actually judged against, latched at the moment
         -- of the most recent START. Reading a live counter twenty cycles later shows the
         -- state after the event, which is how two rounds of debugging went into a
         -- scenario rather than into the property.
         o_last_start_idle : out natural
      );
   end entity i2c_props;

   architecture psl of i2c_props is

      -- ---- the sampled bus, one delay stage --------------------------------
      signal scl_d, sda_d : std_logic := '1';

      -- ---- the framing tracker, written from UM10204 -----------------------
      -- Its only job is to supply the antecedents the rules are conditional on. It is
      -- NOT a monitor: it reconstructs no data and publishes nothing.
      signal active   : std_logic := '0';   -- a transfer is open
      signal in_byte  : std_logic := '0';   -- bits have accumulated, no ack slot yet
      signal bitcnt   : natural   := 0;     -- 0..8, where 8 is the acknowledge slot
      signal idle_cnt : natural   := 0;     -- clocks since the bus went idle

      -- Consecutive cycles of simultaneous SDA pulling, so that a brief legal handover is
      -- distinguishable from a second driver.
      signal sda_overlap : natural := 0;

      -- A bit has been SAMPLED at a rising edge but not yet COUNTED. See the tracker.
      signal pending : std_logic := '0';

      -- ---- framing events, as single-cycle conditions -----------------------
      signal scl_rise  : std_logic := '0';
      signal scl_fall  : std_logic := '0';
      signal sda_edge  : std_logic := '0';
      signal start_now : std_logic := '0';
      signal stop_now  : std_logic := '0';

      -- ---- an assertion-fired counter, so a bench can check a NEGATIVE test ----
      signal fired : natural := 0;
      signal c_starts, c_stops, c_stop_mid, c_start_early : natural := 0;
      signal last_start_idle : natural := 0;

   begin

      n_fired    <= fired;
      o_active   <= active;
      o_in_byte  <= in_byte;
      o_bitcnt   <= bitcnt;
      o_idle_cnt <= idle_cnt;
      n_starts        <= c_starts;
      n_stops         <= c_stops;
      n_stop_mid_byte <= c_stop_mid;
      n_start_early   <= c_start_early;
      o_last_start_idle <= last_start_idle;

      -- ---- edges, and the framing conditions -------------------------------
      -- NOTE: no rose() or fell() anywhere in this file. NVC accepts both and NEVER
      -- evaluates them true -- measured in probe/capability.sh -- so an assertion whose
      -- antecedent is rose(scl) is silently vacuous and passes forever. Explicit
      -- comparison against the previous sample is the working form.
      scl_rise  <= '1' when scl = '1' and scl_d = '0' else '0';
      scl_fall  <= '1' when scl = '0' and scl_d = '1' else '0';
      sda_edge  <= '1' when sda /= sda_d else '0';
      start_now <= '1' when sda = '0' and sda_d = '1' and scl = '1' and scl_d = '1' else '0';
      stop_now  <= '1' when sda = '1' and sda_d = '0' and scl = '1' and scl_d = '1' else '0';

      track : process (clk) is
      begin
         if rising_edge(clk) then
            if rst_n = '0' then
               scl_d <= '1'; sda_d <= '1';
               active <= '0'; in_byte <= '0'; bitcnt <= 0; idle_cnt <= 0;
               sda_overlap <= 0; pending <= '0';
            else
               if start_now = '1' then
                  active  <= '1';
                  in_byte <= '0';
                  bitcnt  <= 0;
               elsif stop_now = '1' then
                  active   <= '0';
                  in_byte  <= '0';
                  bitcnt   <= 0;
                  idle_cnt <= 0;
               elsif scl_rise = '1' and active = '1' then
                  -- A bit is sampled HERE and counted at the following fall. Counting it
                  -- here instead is what the first version did, and it broke a legal STOP:
                  -- the STOP sequence releases SCL (a rising edge) and only then releases
                  -- SDA, so its own rise was counted as a data bit and the tracker believed
                  -- a byte was in progress. Deferring the count to the fall lets a framing
                  -- event -- which happens WHILE SCL is high -- pre-empt it.
                  pending <= '1';
               elsif scl_fall = '1' and active = '1' and pending = '1' then
                  pending <= '0';
                  if bitcnt < 8 then
                     bitcnt  <= bitcnt + 1;
                     in_byte <= '1';
                  else
                     bitcnt  <= 0;         -- the acknowledge slot completes the byte
                     in_byte <= '0';
                  end if;
               end if;

               -- Framing discards any sampled-but-uncounted bit, in either direction.
               if start_now = '1' or stop_now = '1' then
                  pending <= '0';
               end if;

               -- time since the bus became idle, for the bus-free rule
               if active = '0' and scl = '1' and sda = '1' then
                  idle_cnt <= idle_cnt + 1;
               elsif active = '1' then
                  idle_cnt <= 0;
               end if;

               if sda_holders > 1 then
                  sda_overlap <= sda_overlap + 1;
               else
                  sda_overlap <= 0;
               end if;

               scl_d <= scl;
               sda_d <= sda;
            end if;
         end if;
      end process track;

      -- Counts every reported violation, so a bench can assert that a NEGATIVE test
      -- actually produced one. An assertion suite with no failing case in its own test
      -- set is a suite whose green result means nothing.
      count : process (clk) is
      begin
         if rising_edge(clk) then
            if rst_n = '0' then
               fired <= 0;
               c_starts <= 0; c_stops <= 0; c_stop_mid <= 0; c_start_early <= 0;
            else
               if start_now = '1' then
                  c_starts <= c_starts + 1;
                  last_start_idle <= idle_cnt;
                  if active = '0' and idle_cnt < BUS_FREE_CLKS then
                     c_start_early <= c_start_early + 1;
                  end if;
               end if;
               if stop_now = '1' then
                  c_stops <= c_stops + 1;
                  if in_byte = '1' then
                     c_stop_mid <= c_stop_mid + 1;
                  end if;
               end if;
            end if;

            if rst_n = '0' then
               fired <= 0;
            elsif (scl = '1' and scl_d = '1' and sda_edge = '1'
                   and in_byte = '1' and start_now = '0' and stop_now = '0')
               or (stop_now = '1' and active = '0')
               or (stop_now = '1' and in_byte = '1')
               or (start_now = '1' and active = '0' and idle_cnt < BUS_FREE_CLKS)
               or (sda_overlap >= OVERLAP_CLKS)
               or (scl_holders > 1 and scl = '1') then
               fired <= fired + 1;
            end if;
         end if;
      end process count;

      -- =====================================================================
      -- THE PROPERTIES
      --
      -- `default clock` makes every directive below sample on the testbench clock. That
      -- is a sampling clock, NOT SCL -- SCL is a bus signal generated by whichever device
      -- is acting as controller, and a property clocked on it could not describe what
      -- happens WHILE it is high.
      -- =====================================================================
      -- psl default clock is rising_edge(clk);

      -- ---- 22.2 THE DATA-VALID RULE ---------------------------------------
      -- SDA may not change while SCL is high. The framing exceptions are explicit in the
      -- antecedent rather than left out: a START and a STOP are SDA edges while SCL is
      -- high, and excluding them is what stops this property firing on every legal
      -- transfer. `in_byte` restricts it further, to the interval where a change is
      -- unambiguously data corruption.
      -- psl SDA_STABLE_WHILE_SCL_HIGH : assert always (
      --        (scl = '1' and prev(scl) = '1' and sda /= prev(sda)
      --         and in_byte = '1' and start_now = '0' and stop_now = '0')
      --        -> false)
      --      report "22.2 SDA changed while SCL was high, mid-byte";

      -- ---- 22.3 FRAMING LEGALITY -----------------------------------------
      -- A STOP is only meaningful when a transfer is open. One arriving on an idle bus is
      -- a framing error, not a no-op.
      -- psl STOP_NEEDS_OPEN_TRANSFER : assert always (
      --        (stop_now = '1' and active = '0') -> false)
      --      report "22.3 a STOP arrived with no transfer open";

      -- A START must be preceded by a bus-free interval. This is the one property in the
      -- file with a NUMBER in it, and the number is a generic for that reason.
      -- psl START_AFTER_BUS_FREE : assert always (
      --        (start_now = '1' and active = '0' and idle_cnt < BUS_FREE_CLKS) -> false)
      --      report "22.3 a START arrived before the bus-free interval elapsed";

      -- ---- 22.4 BYTE BOUNDARIES ------------------------------------------
      -- A transfer must not end in the middle of a byte. Stated as: a STOP while bits
      -- have accumulated and no acknowledge slot has closed them.
      -- psl NO_STOP_MID_BYTE : assert always (
      --        (stop_now = '1' and in_byte = '1') -> false)
      --      report "22.4 a STOP arrived mid-byte, truncating a transfer";

      -- ---- 22.5 ONE DRIVER PER SLOT --------------------------------------
      -- The rule with no bus-level formulation. Two devices pulling SDA is invisible from
      -- the resolved line -- low is low -- so this property reads the holder COUNT, which
      -- is why the bus model exports it at all.
      --
      -- AND IT IS DELIBERATELY NOT `never (sda_holders > 1)`. That was the first version
      -- and it fired on LEGAL traffic, at the acknowledge handover: the controller has not
      -- yet released SDA in the sampling cycle where the target begins to pull it, so a
      -- momentary overlap is normal and correct. An over-constrained property is not a
      -- stricter check, it is a broken one -- it fires on good traffic, gets a waiver, and
      -- then the waiver hides the real fault too.
      --
      -- The rule is about a SUSTAINED overlap. OVERLAP_CLKS is the tolerance, and it is a
      -- generic because it is a property of the bit period rather than of the protocol.
      --
      -- NOTE WHERE THE TEMPORAL SHAPE LIVES, because it is not where you would want it.
      -- The natural way to write "for N consecutive cycles" is a repetition inside the
      -- directive -- `never {(sda_holders > 1)[*4]}` -- and NVC rejects that: a repetition
      -- is outside PSL's SIMPLE SUBSET, which is what its `never` operand is restricted to.
      -- Measured for both a literal and a generic count in probe/capability.sh.
      --
      -- So the counting moves into the tracker above and the property becomes a Boolean
      -- over it. That is a real cost: part of the temporal statement is now ordinary VHDL,
      -- where it is not checked by the property engine and can be wrong in ways a property
      -- could not be. It is stated here rather than hidden because a reader comparing this
      -- file against a commercial-tool assertion suite will notice the difference.
      -- psl ONE_SDA_DRIVER : assert never (sda_overlap >= OVERLAP_CLKS)
      --      report "22.5 more than one device pulled SDA for a sustained interval";

      -- SCL may legitimately be pulled by two devices at once -- that is what a clock
      -- stretch during a controller's low phase looks like. It may NOT be the case while
      -- the line reads high, which would mean a puller is not taking effect.
      -- psl NO_SCL_CONFLICT_WHEN_HIGH : assert never (scl_holders > 1 and scl = '1')
      --      report "22.5 SCL reads high while more than one device pulls it";

      -- ---- 22.5 LIVENESS -------------------------------------------------
      -- A transfer that opens must eventually close. `eventually!` is a strong operator:
      -- it fails at the END of simulation if the condition never held, which makes it the
      -- one property here that reports a HANG rather than a wrong value.
      -- psl EVERY_TRANSFER_ENDS : assert always (
      --        (start_now = '1') -> eventually! (active = '0'))
      --      report "22.5 a transfer opened and never closed";

      -- ---- COVER: what the run actually exercised -------------------------
      -- Cover directives are not checks. They record whether a situation OCCURRED, and
      -- NVC reports them with a hit count -- so an unhit cover point is a statement about
      -- the stimulus rather than about the design.
      --
      -- NOTE THE `[+]` AND NOT `[*]`. An UNBOUNDED star in a cover sequence never matches
      -- in NVC 1.23 -- measured in probe/capability.sh, where the identical sequence
      -- written with `[*]` reports a hit count of zero and with `[+]` or a bounded range
      -- reports one. A cover point that can never be hit is worse than a missing one: it
      -- sits in the report as a permanent hole and invites stimulus work for a case that
      -- is already being exercised.
      -- psl COV_WRITE_THEN_READ : cover {start_now = '1'; active = '1'[+]; start_now = '1'};
      -- psl COV_STRETCH        : cover {scl_holders > 1};
      -- psl COV_NACK_SLOT      : cover {bitcnt = 8 and sda = '1'};
      -- psl COV_ACK_SLOT       : cover {bitcnt = 8 and sda = '0'};

   end architecture psl;

         procedure b_bit_with_sda_glitch (b : std_logic) is
         begin
            wait until falling_edge(clk); m_scl_low <= '1'; phase;
            wait until falling_edge(clk); m_sda_low <= not b; phase;
            wait until falling_edge(clk); m_scl_low <= '0'; phase;
            -- SCL is HIGH here, and we move SDA
            wait until falling_edge(clk); m_sda_low <= b; phase;
            wait until falling_edge(clk); m_scl_low <= '1'; phase;
         end procedure;