diff --git a/examples/formal/.gitignore b/examples/formal/.gitignore new file mode 100644 index 0000000..d28717d --- /dev/null +++ b/examples/formal/.gitignore @@ -0,0 +1,2 @@ +OUT +BUILD \ No newline at end of file diff --git a/examples/formal/RTL/counter.vhd b/examples/formal/RTL/counter.vhd new file mode 100644 index 0000000..e4abd58 --- /dev/null +++ b/examples/formal/RTL/counter.vhd @@ -0,0 +1,40 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity counter is + generic ( + -- Formal generic is used to embed formal validation stuff + formal : boolean := false; + -- Data width + width : integer := 16; + -- Max count + mxcnt : integer := 256 + ); + port ( + ACLK : in std_logic; + ARESETN : in std_logic; + cnt : out std_logic_vector(width-1 downto 0) + ); +end entity; + +architecture behav of counter is + signal icnt : unsigned (width-1 downto 0); +begin + + cnt <= std_logic_vector(icnt); + + process(ACLK, ARESETN) + begin + if ARESETN='0' then + icnt <= (others=>'0'); + elsif rising_edge(ACLK) then + if icnt'0'); + end if; + end if; + end process; + +end architecture; \ No newline at end of file diff --git a/examples/formal/SIM/tb_counter.vhd b/examples/formal/SIM/tb_counter.vhd new file mode 100644 index 0000000..071eae8 --- /dev/null +++ b/examples/formal/SIM/tb_counter.vhd @@ -0,0 +1,48 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity tb_counter is +end entity; + +architecture behav of tb_counter is + + component counter is + generic ( + formal : boolean := false; + width : integer := 16; + mxcnt : integer := 256 + ); + port ( + ACLK : in std_logic; + ARESETN : in std_logic; + cnt : out std_logic_vector(width-1 downto 0) + ); + end component; + + signal ACLK, ARESETN : std_logic := '0'; + signal cnt : std_logic_vector(15 downto 0); + +begin + + ACLK <= not ACLK after 10 ns; + ARESETN <= '1' after 50 ns; + + process + begin + wait for 2 us; + report "END OF SIMULATION" severity failure; + end process; + + c_counter : component counter + generic map( + formal => false, + width => cnt'length, + mxcnt => 5 + ) port map ( + ACLK => ACLK, + ARESETN => ARESETN, + cnt => cnt + ); + +end architecture; \ No newline at end of file diff --git a/examples/formal/project.cfg b/examples/formal/project.cfg new file mode 100644 index 0000000..5bae63c --- /dev/null +++ b/examples/formal/project.cfg @@ -0,0 +1,28 @@ +[project] +name = formal_project +version = 0.1 +out_dir = OUT +build_dir = BUILD + +[server] +hostname = localhost +port = 2020 +privkey = /home/joppe/.ssh/id_rsa +pubkey = /home/joppe/.ssh/id_rsa.pub + +# ###################################### +# Basic VHDL simulation with GHDL +[target.sim] +toolchain = ghdl + +# Toolchain settings +toplevel = tb_counter +runtime = all +#ghdla_opts = +#ghdle_opts = +#ghdlr_opts = + +# Fileset +files_vhdl = RTL/counter.vhd + SIM/tb_counter.vhd +# ###################################### \ No newline at end of file diff --git a/remotesyn/toolchains/ghdl.py b/remotesyn/toolchains/ghdl.py new file mode 100644 index 0000000..dc4cc1f --- /dev/null +++ b/remotesyn/toolchains/ghdl.py @@ -0,0 +1,74 @@ +import shutil +import os +import time +import subprocess + +def execp(cmd, subprocesses, cwd): + p = subprocess.Popen(cmd, + shell=True, cwd=cwd, + stdin=subprocess.DEVNULL, stdout=subprocess.DEVNULL, stderr=subprocess.DEVNULL) + subprocesses.append(p) + while p.poll() is None: + time.sleep(1) + res = p.returncode + return res + +def do(config, target, log, subprocesses, prefix='.'): + shutil.rmtree(config.get('project', 'build_dir', fallback='build'), True) + + log("Starting simulation") + + log(" - parsing options") + toplevel = config.get(f'target.{target}', 'toplevel', fallback='toplevel') + runtime = config.get(f'target.{target}', 'runtime', fallback='100 ns') + ghdla_opts = config.get(f'target.{target}', 'ghdla_opts', fallback='') + ghdle_opts = config.get(f'target.{target}', 'ghdle_opts', fallback='') + ghdlr_opts = config.get(f'target.{target}', 'ghdlr_opts', fallback='') + files_vhdl = config.get(f'target.{target}', 'files_vhdl', fallback='').split() + build_dir = config.get(f'project', 'build_dir', fallback='build') + out_dir = config.get(f'project', 'out_dir', fallback='out') + + prefix = f'{os.getcwd()}/{prefix}' + build_dir = f'{prefix}/{build_dir}' + out_dir = f'{prefix}/{out_dir}/{target}' + + log(" - creating output directories") + os.makedirs(build_dir, exist_ok=True) + os.makedirs(out_dir, exist_ok=True) + + log(" - analyze files") + res = 0 + for f in files_vhdl: + res = execp(f"echo +++{f} >> a.log && ghdl -a {ghdla_opts} {prefix}/{f} 2>&1 >> a.log", subprocesses, build_dir) + if res!=0: + break + log(" - copy logs") + shutil.copy(f'{build_dir}/a.log', f'{out_dir}/a.log') + if res!=0: + log("ERROR: ghdl -a returned with", res) + return res + + log(" - elaborate") + res = execp(f"echo {toplevel} >> e.log && ghdl -e {ghdle_opts} {toplevel} 2>&1 >> e.log", subprocesses, build_dir) + log(" - copy logs") + shutil.copy(f'{build_dir}/e.log', f'{out_dir}/e.log') + if res!=0: + log("ERROR: ghdl -e returned with", res) + return res + + log(" - simulate") + extra = '' + if runtime!='all': + extra = f'--stop-time={runtime.replace(" ", "")}' + res = execp(f"echo {toplevel} >> r.log && ghdl -r {ghdlr_opts} {extra} {toplevel} --vcd=out.vcd 2>&1 >> r.log", subprocesses, build_dir) + log(" - copy logs") + shutil.copy(f'{build_dir}/r.log', f'{out_dir}/r.log') + # Ignore simulation errors: vhdl stopping with failure results in returned with 1 + # if res!=0: + # log("ERROR: ghdl -r returned with", res) + # return res + + log(" - copy output files") + shutil.copy(f'{build_dir}/out.vcd', f'{out_dir}/out.vcd') + + return 0 \ No newline at end of file