Formaali mallintarkistus (model-checking) on verifiointimenetelmä, joka sopii erityisen hyvin yksittäisten modulien, tai muutamien modulien kokonaisuuksien toiminnallisuuden varmistamiseen kaikissa mahdollisissa käyttötapauksissa.
Cover-checking on yksi osa mallintarkistusta, jonka tarkoituksena on varmistaa, että jokin toimenpide on mahdollista. Työkalu etsii tarvittavan stimuluksen jotta haluttuun tilaan päästään.
Tässä esimerkkinä I2C-slave. Ja cover-checkingin tehtävänä on keksiä miten I2C-slaveen kirjoitetaan oikeaoppisesti ja saadaan haluttu ulostulo I2C-modulista.
-- i2c_slave.vhdl
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity i2c_slave is
generic(
TARGET_ADD: integer range 0 to 127
);
port(
clk_in: in std_logic;
scl_in: in std_logic;
sda_oe_out: out std_logic;
sda_in: in std_logic;
sda_out: out std_logic;
gpio_in: in std_logic_vector(7 downto 0);
gpio_out: out std_logic_vector(7 downto 0) := (others => '0')
);
end;
architecture rtl of i2c_slave is
type state_t is (S_IDLE, S_ADDR, S_RW, S_ACK_ADD, S_READ, S_WRITE, S_ACK_DATA, S_STOP);
signal prev_sda: std_logic;
signal prev_scl: std_logic;
signal state: state_t := (S_IDLE);
signal next_state: state_t;
signal state_cnt: integer range 0 to 7;
signal next_state_cnt: integer range 0 to 7;
signal cmd_add: std_logic_vector(6 downto 0);
signal next_cmd_add: std_logic_vector(6 downto 0);
signal cmd_rw: std_logic;
signal next_cmd_rw: std_logic;
signal cmd_wdata: std_logic_vector(7 downto 0);
signal next_cmd_wdata: std_logic_vector(7 downto 0);
signal next_gpio_out: std_logic_vector(7 downto 0);
signal resp_rdata: std_logic_vector(7 downto 0);
begin
state_async_pr: process(all)
begin
next_state <= state;
next_state_cnt <= state_cnt;
next_cmd_add <= cmd_add;
next_cmd_rw <= cmd_rw;
next_cmd_wdata <= cmd_wdata;
next_gpio_out <= gpio_out;
case state is
when S_IDLE =>
null;
when S_ADDR =>
if prev_scl = '0' and scl_in = '1' then
next_cmd_add(6 downto 1) <= cmd_add(5 downto 0);
next_cmd_add(0) <= sda_in;
if state_cnt /= 6 then
next_state_cnt <= state_cnt + 1;
else
next_state <= S_RW;
end if;
end if;
when S_RW =>
if prev_scl = '0' and scl_in = '1' then
next_cmd_rw <= sda_in;
if cmd_add = std_logic_vector(to_unsigned(TARGET_ADD, 7)) then
next_state <= S_ACK_ADD;
else
next_state <= S_IDLE;
end if;
end if;
when S_ACK_ADD =>
if prev_scl = '0' and scl_in = '1' then
if cmd_rw = '0' then
next_state <= S_WRITE;
next_state_cnt <= 0;
else
next_state <= S_READ;
next_state_cnt <= 0;
end if;
end if;
when S_READ =>
when S_WRITE =>
if prev_scl = '0' and scl_in = '1' then
next_cmd_wdata(7 downto 1) <= cmd_wdata(6 downto 0);
next_cmd_wdata(0) <= sda_in;
if state_cnt /= 7 then
next_state_cnt <= state_cnt + 1;
else
next_state <= S_ACK_DATA;
end if;
end if;
when S_ACK_DATA =>
if prev_scl = '0' and scl_in = '1' then
next_state <= S_STOP;
end if;
when S_STOP =>
null;
end case;
if scl_in = '1' and prev_sda = '1' and sda_in = '0' then
-- Start transition.
next_state <= S_ADDR;
next_state_cnt <= 0;
end if;
if scl_in = '1' and prev_sda = '0' and sda_in = '1' then
-- Stop transition.
next_state <= S_IDLE;
next_state_cnt <= 0;
if state = S_STOP and cmd_rw = '0' then
next_gpio_out <= cmd_wdata;
end if;
end if;
end process;
state_sync_pr: process(clk_in)
begin
if rising_edge(clk_in) then
prev_sda <= sda_in;
prev_scl <= scl_in;
cmd_add <= next_cmd_add;
cmd_rw <= next_cmd_rw;
cmd_wdata <= next_cmd_wdata;
gpio_out <= next_gpio_out;
state <= next_state;
state_cnt <= next_state_cnt;
if state /= S_READ and next_state = S_READ then
resp_rdata <= gpio_in;
end if;
if state = S_READ then
resp_rdata(7 downto 1) <= resp_rdata(6 downto 0);
end if;
end if;
end process;
io_pr: process(all)
begin
sda_oe_out <= '0';
sda_out <= '0';
if state = S_ACK_ADD or state = S_ACK_DATA then
sda_oe_out <= '1';
sda_out <= '0';
end if;
if state = S_READ then
sda_oe_out <= '1';
sda_out <= resp_rdata(7);
end if;
end process;
end;
Moduli tunnistaa I2C kirjoitus- ja lukukomennon, omaan osoitteeseensa (TARGET_ADD). Kirjoitus ajetaan ulos portista gpio_out. Luku lukee gpio_in -portin arvon.
Tämän ympärille tehdään formaali testipenkki. Normaalia VHDL-koodia muutamalla (VHDL-standardinmukaisella) höysteellä varustettuna.
-- formal_tb_i2c.vhdl
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity formal_tb_i2c is
port(
clk_in: in std_logic;
scl_in: in std_logic;
sda_oe_out: out std_logic;
sda_in: in std_logic;
sda_out: out std_logic;
dut_1_gpio_in: in std_logic_vector(7 downto 0);
dut_1_gpio_out: out std_logic_vector(7 downto 0)
);
end;
architecture formal of formal_tb_i2c is
begin
dut_1: entity work.i2c_slave
generic map(
TARGET_ADD => 123
)
port map(
clk_in => clk_in,
scl_in => scl_in,
sda_oe_out => sda_oe_out,
sda_in => sda_in,
sda_out => sda_out,
gpio_in => dut_1_gpio_in,
gpio_out => dut_1_gpio_out
);
---- FORMAL PART =>
--- FORMAL HELPER RTL =>
--- FORMAL PSL =>
default clock is rising_edge(clk_in);
assume {scl_in = '0'[*2]};
assume always {not stable(scl_in)} |=> {stable(scl_in)};
wr_cover: cover {[*]; dut_1_gpio_out = X"12"};
end;
Tämä toimii formaalin verifiointityökaly näkemänä toppitasona.
Formaali työkalu käy läpi kaikkien input-signaalien kaikki sekvenssit jokaisella kellojaksolla. Eli tarkistaa kaikki mahdolliset inputvariaatiot.
Näistä vaihtoehdoista raksitaan heti kättelyssä pois ne vaihtoehdot jotka rikkovat vähintään yhtä assume -lausetta. Tässä tapauksessa niitä on 2.
- assume {scl_in = ‘0’[*2]};
Tämä kertoo työkalulle että simulaation alussa aaltosulkujen sisällä olevan väitteen pitää olla totta. Jos jollakin sekvenssilä näin ei ole, kyseinen sekvenssi hylätään tutkittavista vaihtoehdoista.
Tässä tapauksessa aaltosulkujen sisällä on vaatimus että ehdon “scl_in=’0′” pitää olla voimassa kahdella ensimmäisellä kellojoksolla.
Tämän ideana on saada aaltomuotokuvasta selkeämpi. Rauhoitetaan I2C-kello kahden järjestelmäkellon ajaksi. - assume always {not stable(scl_in)} |=> {stable(scl_in)};
Tämä sanoo että jokaisella kellojaksolla (ilman always-määrettä tarkistetaan tilanne vain ensimmäisellä systeemikellojaksolla) annettu ehto pitää olla totta.
ehto “{A} |=> {B}” vaatii että aina kun A on tosi, niin seuraavalla systeemikellojaksolla B:n pitää olla tosi.
Tässä ehdossa vaaditaan: jos I2C-kello on muuttunut (verrattuna edelliseen systeemikellojaksoon), niin seuraavalla systeemikellojaksolla I2C-kello ei saa olla muuttunut (verrattuna nykyiseen systeemikellojaksoon).
Tämän ideana on saada I2C-kello hidastetuksi siten että I2C:n start & stop -komennot on helpommin havaittavissa aaltomuodossa.
Ja sitten itse asiaan. Cover-lause kertoo mikä ehto pitää saavuttaa.
“{A;B}” on SERE (SEquential Regular Expression), joka on totta jos ensimmäisellä kellojaksolla A on tosi, ja seuraavalla kellojaksolla B on tosi.
{[*]; dut_1_gpio_out = X”12″}
“[*]” on totta millä tahansa signaalien arvoilla, kaikilla mahdollisilla pituuksilla.
dut_1_gpio_out = X”12″ on totta jos output-arvo on 0x12.
Cover-lause aloittaa tutkimisen ensimmäisestä systeemikellojaksosta (ei ole always -määrettä). Ja tämä cover on tosi sillä kellojaksolla kun gpio-output on 0x12.
Työkalu yrittää etsiä sekvenssin (joka tottelee assumeita), jolla tähän päästään.
Näiden lisäksi tarvitaan vielä yksi tiedosto, joka kertoo mitä tehdään ja millä tiedostoilla
formal_tb_i2c.sby:
[tasks]
bmc
cover
[options]
bmc: mode bmc
cover: mode cover
depth 100
[engines]
smtbmc
[script]
ghdl --std=08 i2c_slave.vhdl formal_tb_i2c.vhdl -e formal_tb_i2c
prep -top formal_tb_i2c
[files]
i2c_slave.vhdl
formal_tb_i2c.vhdl
Tässä tiedostossa on lueteltu vhdl-tiedostot joista projekti kasataan, ja kerrotaan mikä on top-taso.
Lisäksi maksimimäärä tutkittavia systeemikellojaksoja on rajattu sataan.
Nyt tarvitaan vain Linux-kone jossa on Docker (voit asentaa Ubuntun esim VirtualBox:iin ja sinne dockerin, netti on täynnä ohjeita tähän).
docker run --rm -it -v $PWD:/root hdlc/formal:all bash
Tämä suorittaa docker-imagen, jossa on esiasennettuna tarvittavat työkalut.
cd root
sby --yosys "yosys -m ghdl" -f formal_tb_i2c.sby cover
root@a2ad906d08d2:~# sby --yosys "yosys -m ghdl" -f formal_tb_i2c.sby cover SBY 18:01:53 [formal_tb_i2c_cover] Removing directory '/root/formal_tb_i2c_cover'. SBY 18:01:53 [formal_tb_i2c_cover] Copy '/root/i2c_slave.vhdl' to '/root/formal_tb_i2c_cover/src/i2c_slave.vhdl'. SBY 18:01:53 [formal_tb_i2c_cover] Copy '/root/formal_tb_i2c.vhdl' to '/root/formal_tb_i2c_cover/src/formal_tb_i2c.vhdl'. SBY 18:01:53 [formal_tb_i2c_cover] engine_0: smtbmc SBY 18:01:53 [formal_tb_i2c_cover] base: starting process "cd formal_tb_i2c_cover/src; yosys -m ghdl -ql ../model/design.log ../model/design.ys" SBY 18:01:53 [formal_tb_i2c_cover] base: finished (returncode=0) SBY 18:01:53 [formal_tb_i2c_cover] prep: starting process "cd formal_tb_i2c_cover/model; yosys -m ghdl -ql design_prep.log design_prep.ys" SBY 18:01:53 [formal_tb_i2c_cover] prep: finished (returncode=0) SBY 18:01:53 [formal_tb_i2c_cover] smt2: starting process "cd formal_tb_i2c_cover/model; yosys -m ghdl -ql design_smt2.log design_smt2.ys" SBY 18:01:53 [formal_tb_i2c_cover] smt2: finished (returncode=0) SBY 18:01:53 [formal_tb_i2c_cover] engine_0: starting process "cd formal_tb_i2c_cover; yosys-smtbmc --presat --unroll -c --noprogress -t 100 --append 0 --dump-vcd engine_0/trace%.vcd --dump-yw engine_0/trace%.yw --dump-vlogtb engine_0/trace%_tb.v --dump-smtc engine_0/trace%.smtc model/design_smt2.smt2" SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Solver: yices SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 0.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 1.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 2.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 3.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 4.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 5.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 6.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 7.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 8.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 9.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 10.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 11.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 12.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 13.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 14.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 15.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 16.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 17.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 18.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 19.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 20.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 21.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 22.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 23.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 24.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 25.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 26.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 27.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 28.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 29.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 30.. SBY 18:01:54 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 31.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:00 Checking cover reachability in step 32.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 33.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 34.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 35.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 36.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 37.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 38.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 39.. SBY 18:01:55 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 40.. SBY 18:01:56 [formal_tb_i2c_cover] engine_0: ## 0:00:01 Checking cover reachability in step 41.. SBY 18:01:56 [formal_tb_i2c_cover] engine_0: ## 0:00:02 Checking cover reachability in step 42.. SBY 18:01:56 [formal_tb_i2c_cover] engine_0: ## 0:00:02 Checking cover reachability in step 43.. SBY 18:01:56 [formal_tb_i2c_cover] engine_0: ## 0:00:02 Checking cover reachability in step 44.. SBY 18:01:56 [formal_tb_i2c_cover] engine_0: ## 0:00:02 Checking cover reachability in step 45.. SBY 18:01:57 [formal_tb_i2c_cover] engine_0: ## 0:00:02 Checking cover reachability in step 46.. SBY 18:01:57 [formal_tb_i2c_cover] engine_0: ## 0:00:03 Checking cover reachability in step 47.. SBY 18:01:57 [formal_tb_i2c_cover] engine_0: ## 0:00:03 Checking cover reachability in step 48.. SBY 18:01:57 [formal_tb_i2c_cover] engine_0: ## 0:00:03 Checking cover reachability in step 49.. SBY 18:01:58 [formal_tb_i2c_cover] engine_0: ## 0:00:03 Checking cover reachability in step 50.. SBY 18:01:58 [formal_tb_i2c_cover] engine_0: ## 0:00:04 Checking cover reachability in step 51.. SBY 18:01:58 [formal_tb_i2c_cover] engine_0: ## 0:00:04 Checking cover reachability in step 52.. SBY 18:01:59 [formal_tb_i2c_cover] engine_0: ## 0:00:05 Checking cover reachability in step 53.. SBY 18:01:59 [formal_tb_i2c_cover] engine_0: ## 0:00:05 Checking cover reachability in step 54.. SBY 18:02:00 [formal_tb_i2c_cover] engine_0: ## 0:00:06 Checking cover reachability in step 55.. SBY 18:02:00 [formal_tb_i2c_cover] engine_0: ## 0:00:06 Checking cover reachability in step 56.. SBY 18:02:01 [formal_tb_i2c_cover] engine_0: ## 0:00:07 Checking cover reachability in step 57.. SBY 18:02:01 [formal_tb_i2c_cover] engine_0: ## 0:00:07 Checking cover reachability in step 58.. SBY 18:02:02 [formal_tb_i2c_cover] engine_0: ## 0:00:08 Checking cover reachability in step 59.. SBY 18:02:03 [formal_tb_i2c_cover] engine_0: ## 0:00:09 Checking cover reachability in step 60.. SBY 18:02:03 [formal_tb_i2c_cover] engine_0: ## 0:00:09 Checking cover reachability in step 61.. SBY 18:02:04 [formal_tb_i2c_cover] engine_0: ## 0:00:10 Checking cover reachability in step 62.. SBY 18:02:05 [formal_tb_i2c_cover] engine_0: ## 0:00:11 Checking cover reachability in step 63.. SBY 18:02:06 [formal_tb_i2c_cover] engine_0: ## 0:00:12 Checking cover reachability in step 64.. SBY 18:02:07 [formal_tb_i2c_cover] engine_0: ## 0:00:13 Checking cover reachability in step 65.. SBY 18:02:08 [formal_tb_i2c_cover] engine_0: ## 0:00:14 Checking cover reachability in step 66.. SBY 18:02:09 [formal_tb_i2c_cover] engine_0: ## 0:00:15 Checking cover reachability in step 67.. SBY 18:02:10 [formal_tb_i2c_cover] engine_0: ## 0:00:16 Checking cover reachability in step 68.. SBY 18:02:11 [formal_tb_i2c_cover] engine_0: ## 0:00:17 Checking cover reachability in step 69.. SBY 18:02:11 [formal_tb_i2c_cover] engine_0: ## 0:00:17 Checking cover reachability in step 70.. SBY 18:02:13 [formal_tb_i2c_cover] engine_0: ## 0:00:19 Checking cover reachability in step 71.. SBY 18:02:14 [formal_tb_i2c_cover] engine_0: ## 0:00:20 Checking cover reachability in step 72.. SBY 18:02:15 [formal_tb_i2c_cover] engine_0: ## 0:00:21 Checking cover reachability in step 73.. SBY 18:02:16 [formal_tb_i2c_cover] engine_0: ## 0:00:22 Checking cover reachability in step 74.. SBY 18:02:17 [formal_tb_i2c_cover] engine_0: ## 0:00:23 Checking cover reachability in step 75.. SBY 18:02:19 [formal_tb_i2c_cover] engine_0: ## 0:00:25 Checking cover reachability in step 76.. SBY 18:02:20 [formal_tb_i2c_cover] engine_0: ## 0:00:26 Reached cover statement at wr_cover in step 76. SBY 18:02:20 [formal_tb_i2c_cover] engine_0: ## 0:00:26 Writing trace to VCD file: engine_0/trace0.vcd SBY 18:02:20 [formal_tb_i2c_cover] engine_0: ## 0:00:26 Writing trace to Verilog testbench: engine_0/trace0_tb.v SBY 18:02:20 [formal_tb_i2c_cover] engine_0: ## 0:00:26 Writing trace to constraints file: engine_0/trace0.smtc SBY 18:02:21 [formal_tb_i2c_cover] engine_0: ## 0:00:26 Writing trace to Yosys witness file: engine_0/trace0.yw SBY 18:02:21 [formal_tb_i2c_cover] engine_0: ## 0:00:27 Status: passed SBY 18:02:21 [formal_tb_i2c_cover] engine_0: finished (returncode=0) SBY 18:02:21 [formal_tb_i2c_cover] engine_0: Status returned by engine: pass SBY 18:02:21 [formal_tb_i2c_cover] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:27 (27) SBY 18:02:21 [formal_tb_i2c_cover] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:28 (28) SBY 18:02:21 [formal_tb_i2c_cover] summary: engine_0 (smtbmc) returned pass SBY 18:02:21 [formal_tb_i2c_cover] summary: cover trace: formal_tb_i2c_cover/engine_0/trace0.vcd SBY 18:02:21 [formal_tb_i2c_cover] summary: reached cover statement formal_tb_i2c.wr_cover at in step 76 SBY 18:02:21 [formal_tb_i2c_cover] DONE (PASS, rc=0)
76 systeemikellojakson jälkeen (vajaassa puolessa minuutissa) työkalu löysi ratkaisun, joka toteuttaa cover-ehdon.
Tämän tuloksen näkee kun avaa syntyneen tiedoston formal_tb_i2c_cover/engine_0/trace0.vcd esim gtkwave:lla.
Coverin tehokkuus on siinä että 4:llä yksinkertaisella koodirivillä testipenkissä saadaan aikaiseksi kuvan mukainen simulaatio.