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