Skip to content
Snippets Groups Projects
examples.smv 2.49 KiB
--
-- Copyright (C) 2022 Jonathan Certes
-- jonathan.certes@online.fr
--
-- This program is free software: you can redistribute it and/or modify it under
-- the terms of the GNU General Public License as published by the Free Software
-- Foundation, either version 3 of the License, or (at your option) any later
-- version.
--
-- This program is distributed in the hope that it will be useful, but WITHOUT
-- ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
-- FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
-- details.
--
-- You should have received a copy of the GNU General Public License along with
-- this program. If not, see <http://www.gnu.org/licenses/>.
--

MODULE main

--------------------------------------------------------------------------------

PSLSPEC
  NAME "When ready, received bytes are copied in order on output vectors. Case
        of data_0." :=
forall i_0 in {0:255} :
  always(
     -- starting from a reset or the end of a packet:
     ( ("clk" && !"nrst") || ("clk" && ("ready" == 0ub1_1)) )
     -- no reset until a new packet is decompressed:
  && ( next( "nrst" until ("clk" && ("ready" == 0ub1_1)) ))
     -- received byte (with index 1) is equal to i_0:
  && ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data_size" >= 0ud4_1) ))
  && ( next( next_event_a("clk" && !"trace_ctl")[1:1] ("input"[1] == 0ub1_1) )) -- branch packet
  && ( next( next_event_a("clk" && !"trace_ctl")[1:1] ("input" == uwconst(i_0, 8)) ))
  ->
     ( next( next_event(  "clk" && ("ready" == 0ub1_1)) ("data__0" == uwconst(i_0, 8)) ))
  );

--------------------------------------------------------------------------------

INVARSPEC
  NAME "when enable and not ready, input is copied to the internal register" :=
(
      !("clk" & !"nrst")
    &  ("clk" & !"trace_ctl")
    & !("clk" & ("ready" = 0ub1_1))
    &  ("decompressed_packet" = 0ub4_0011)          -- branch packet
    &  ("i_packets_decompresser.state" = 0ub4_1000) -- state_data__8
  ->
      (next("i_packets_decompresser.r_data__8" = "input")) -- WARNING! unable to convert: next(a) = b
);

--------------------------------------------------------------------------------

LTLSPEC
  NAME "same as the invariant" :=
G(
      !("clk" & !"nrst")
    &  ("clk" & !"trace_ctl")
    & !("clk" & ("ready" = 0ub1_1))
    &  ("decompressed_packet" = 0ub4_0011)          -- branch packet
    &  ("i_packets_decompresser.state" = 0ub4_1000) -- state_data__8
  ->
      (X("i_packets_decompresser.r_data__8" = "input"))
);