pepijndevos
commented
2 years ago I think I just kinda commented out the formal parts when feeding it to yosys because there did not seem to be an obvious way to tell it about the formal things.
Open buttercutter opened 2 years ago
pepijndevos
commented
2 years ago I think I just kinda commented out the formal parts when feeding it to yosys because there did not seem to be an obvious way to tell it about the formal things.
buttercutter
commented
2 years ago What do you exactly mean by there did not seem to be an obvious way to tell it about the formal things ?
By the way, could you paste the formal parts here because I could not get the formal coding to pass syntax check by yosys ?
buttercutter
commented
2 years ago Thanks @umarcor for the following helpful reply.
1. http://ghdl.github.io/ghdl/using/ImplementationOfVHDL.html#psl-support 2. https://github.com/ghdl/ghdl-yosys-plugin/tree/master/testsuite/formal 3. https://github.com/ghdl/ghdl/issues/1291 3.1 Functional and formal verification 3.1.1 https://github.com/tmeissner/psl_with_ghdl 3.1.2 https://github.com/tmeissner/vhdl_verification 3.1.3 https://github.com/tmeissner/formal_hw_verification
mbbessa
commented
2 years ago I'm having trouble also with this issue. I get a vcd output, but the vaules defined at forma part (a_sr, b_sr and y_sr) are not being used by it, only the std_logic values of the original alu. Any advice?
library ieee;
use ieee.std_logic_1164.all;
use ieee.numeric_std.all;
entity alu is
generic (
formal : boolean := false
);
port (
clk : in std_logic;
rst_n : in std_logic;
opcode : in std_logic_vector(2 downto 0);
a : in std_logic;
b : in std_logic;
y : out std_logic;
c : out std_logic
);
end alu;
architecture rtl of alu is
signal ci : std_logic; -- carry in
signal co : std_logic; -- carry out
signal cr : std_logic; -- reset value
begin
c <= co;
process(opcode, a, b, ci)
begin
case opcode is
when "000" => -- add
y <= a xor b xor ci;
co <= (a and b) or (a and ci) or (b and ci);
cr <= '0';
when "001" => -- subtract
y <= a xor (not b) xor ci;
co <= (a and (not b)) or (a and ci) or ((not b) and ci);
cr <= '1';
when "010" => -- or
y <= a or b;
co <= a or ci;
cr <= '0';
when "011" => -- and
y <= a and b;
co <= a and ci;
cr <= '1';
when "100" => -- xor
y <= a xor b;
co <= a xor ci;
cr <= '0';
when "101" =>
y <= a;
co <= (a xnor b) and ci; -- a=b
cr <= '1';
when "110" =>
y <= a;
co <= (a and (not b)) or ((a xnor b) and ci); -- a > b
cr <= '0';
when "111" => -- clear carry (b)
y <= b;
co <= '0';
cr <= '1';
when others =>
y <= '-';
co <= '-';
cr <= '-';
end case;
end process;
process(clk, rst_n)
begin
if(rising_edge(clk)) then
if(rst_n = '0') then
ci <= cr;
else
ci <= co;
end if;
end if;
end process;
formal_gen: if formal generate
signal last_op: std_logic_vector(2 downto 0);
signal a_sr: unsigned(7 downto 0);
signal b_sr: unsigned(7 downto 0);
signal y_sr: unsigned(7 downto 0);
begin
default clock is rising_edge(clk);
restrict { {rst_n = '0'; (rst_n = '1')[*8]}[+]};
assume always {rst_n = '0'; rst_n = '1'} |-> opcode = last_op until rst_n = '0';
assert always {opcode = "000" and rst_n = '1'; rst_n = '0'} |-> y_sr = a_sr+b_sr;
end generate;
end rtl;It's been two years since I touched this or any formal bits. I just vaguely recall that I had to kinda comment out stuff to switch between synthesis and formal verification and pass some hacky flags to ghdl/sby/yosys. I'm afraid you're pretty much on your own because I just don't remember what's going on and the ghdl stuff has changed a lot since then.
With regards to your VHDL formal verification article, I have some beginner questions on PSL verification property for your alu.vhd
I tried the instruction in your article, but I ended with the following sby error.