Closed blazra closed 6 years ago
cliffordwolf
commented
6 years ago You do not provide a test case that I could use to reproduce the problem. So there is really nothing I can do. Therefore I'm closing the issue. I'll reopen the issue if and when a test case is provided. (See also Q1 in the FAQ.)
blazra
commented
6 years ago OK, I hope this makes a complete test case. test_case.zip
trigger_rules.sby:
[options]
mode prove
[engines]
smtbmc --stbv yices
[script]
verific -vhdl trigger_rules.vhd
verific -sv formal_tb.sv
verific -import testbench
prep -top testbench
[files]
trigger_rules.vhd
formal_tb.svformal_tb.sv:
module testbench (
input clk
);
Trigger_Rules uut (
.clk (clk),
.reset (reset),
.clock_counter_out(clock_counter_out)
);
always @(posedge clk)
assert (clock_counter_out == 0);
endmoduletrigger_rules.vhd
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
library work;
entity Trigger_Rules is
port(
clk : in std_logic;
reset : in std_logic;
clock_counter_out : out std_logic_vector(15 downto 0));
end entity Trigger_Rules;
architecture Trigger_Rules_arch of Trigger_Rules is
signal clock_counter : std_logic_vector(15 downto 0);
begin
clock_counter_out <= clock_counter;
clock_count : process(clk)
begin
if rising_edge(clk) then
if reset = '1' then
clock_counter <= (others => '0');
else
clock_counter <= std_logic_vector(unsigned(clock_counter) + x"0001");
end if;
end if;
end process clock_count;
end Trigger_Rules_arch;Thanks for the test case. Fixed in 25a864f.
I am using symbiyosys and when I add --stbv option to the smtbmc engine it crashes. Without the option it seems to work fine. (I am not sure what the option does, I was just trying it out, but this doesn't seem to be correct behavior) With yices it says:
and with z3:
Complete outputs: With yices:
With z3: