From 9236b8420e9d8620d0cccc20c7df95226f788235 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:00 +1300 Subject: [PATCH 1/8] btor2aiger: Initial version Add `btor_aig` option, which uses `model("btor_nomem")` and btor2aiger to generate an aiger file via btor. Seems to run fine, until it tries to access design_aiger.ywa for trace conversion. --- sbysrc/sby_core.py | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c366e1be..4bfd53e9 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1150,6 +1150,21 @@ def instance_hierarchy_error_callback(retcode): return [proc] + if model_name == "aig" and self.opt_btor_aig: + #TODO: split .aim from .aig? + #TODO: figure out .ywa + # Going via btor seems to lose the seqs, not sure how important they are + btor_model = "btor_nomem" + proc = SbyProc( + self, + "btor_aig", + self.model(btor_model), + f"""cd {self.workdir}/model; btor2aiger design_{btor_model}.btor > design_aiger.aig""" + ) + proc.checkretcode = True + + return [proc] + if model_name == "aig": with open(f"{self.workdir}/model/design_aiger.ys", "w") as f: print(f"# running in {self.workdir}/model/", file=f) @@ -1279,6 +1294,7 @@ def handle_non_engine_options(self): self.handle_bool_option("aigfolds", False) self.handle_bool_option("aigvmap", False) self.handle_bool_option("aigsyms", False) + self.handle_bool_option("btor_aig", False) self.handle_str_option("smtc", None) self.handle_int_option("skip", None) From 10332e8e74ad30fe4360e7796efb56cc426947ea Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:00 +1300 Subject: [PATCH 2/8] btor2aiger: It kinda works? - Add `btor2aig_yw.py` to wrap btor2aiger calls, splitting the symbol map into a `.aim` file and building (and approximation of) the `.ywa` file. - Currently not tracking asserts/assumes in the `.ywa`, and yosys-witness isn't the biggest fan of the btor2aiger style of unitialised latches. As such, the latches are declared but the `.yw` output doesn't do anything with them so it's incomplete. But the vcd output seems fine (for `vcd_sim=on|off`). - Add a try/except to catch property matching with an incomplete property list. - Add `-x` flag to `write_btor` call since aiw2yw gets confused without them. - Includes some TODO reminders for me to fix things, but as far as I can tell it is working. --- sbysrc/sby_core.py | 10 +-- sbysrc/sby_engine_abc.py | 10 ++- tools/btor2aig_yw/btor2aig_yw.py | 118 +++++++++++++++++++++++++++++++ 3 files changed, 131 insertions(+), 7 deletions(-) create mode 100644 tools/btor2aig_yw/btor2aig_yw.py diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 4bfd53e9..c56fe63f 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1137,7 +1137,8 @@ def instance_hierarchy_error_callback(retcode): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + #TODO: put -x in a conditional + print("write_btor -x {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) proc = SbyProc( @@ -1151,15 +1152,14 @@ def instance_hierarchy_error_callback(retcode): return [proc] if model_name == "aig" and self.opt_btor_aig: - #TODO: split .aim from .aig? - #TODO: figure out .ywa - # Going via btor seems to lose the seqs, not sure how important they are + #TODO: aiw2yw doesn't know what to do with the latches btor_model = "btor_nomem" proc = SbyProc( self, "btor_aig", self.model(btor_model), - f"""cd {self.workdir}/model; btor2aiger design_{btor_model}.btor > design_aiger.aig""" + #TODO: fix hardcoded path + f"cd {self.workdir}/model; python3 ~/sby/tools/btor2aig_yw/btor2aig_yw.py design_{btor_model}.btor" ) proc.checkretcode = True diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 1fabe6fa..bd9d51d3 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -166,7 +166,10 @@ def output_callback(line): match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line) if match: output = int(match[1]) - prop = aiger_props[output] + try: + prop = aiger_props[output] + except IndexError: + prop = None if prop: prop.status = "FAIL" task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) @@ -185,7 +188,10 @@ def output_callback(line): match = re.match(r"^Proved output +([0-9]+) in frame +-?[0-9]+", line) if match: output = int(match[1]) - prop = aiger_props[output] + try: + prop = aiger_props[output] + except IndexError: + prop = None if prop: prop.status = "PASS" task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py new file mode 100644 index 00000000..841383c1 --- /dev/null +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -0,0 +1,118 @@ +from __future__ import annotations + +import argparse +import asyncio +import json +import re +from pathlib import Path + +def arg_parser(): + parser = argparse.ArgumentParser() + + parser.add_argument( + "btor_file", + type=Path + ) + + parser.add_argument( + "-d", "--dest", + dest="dest", + required=False, + type=Path + ) + + return parser + +async def main() -> None: + args = arg_parser().parse_args() + + work_dir: Path = args.dest or Path() + + proc = await asyncio.create_subprocess_shell( + f"btor2aiger {args.btor_file}", + stdout=asyncio.subprocess.PIPE + ) + + data = True + + # output aig + aig_file = work_dir / "design_aiger.aig" + aigf = open(aig_file, mode="wb") + data = await proc.stdout.readline() + aig_header = data.decode() + while data: + aigf.write(data) + data = await proc.stdout.readline() + if b'i0' in data: + break + end_pos = data.find(b'i0') + aigf.write(data[:end_pos]) + aigf.close() + + # initialize yw aiger map + aig_MILOA = aig_header.split() + ywa = { + "version": "Yosys Witness Aiger map", + "generator": "btor2aig_yw.py", + "latch_count": int(aig_MILOA[3]), + "input_count": int(aig_MILOA[2]), + "clocks": [], + "inputs": [], + "seqs": [], + "inits": [], + "latches": [], + "asserts": [], + "assumes": [] + } + + # output aim & build ywa + aim_file = work_dir / "design_aiger.aim" + aimf = open(aim_file, mode="w") + data = data[end_pos:] + while data: + # decode data + string = data.decode().rstrip() + pattern = r"(?P[cil])(?P\d+) (?P.*?)(\[(?P\d+)\])?$" + m = re.match(pattern, string) + md = m.groupdict() + if md['type'] == 'i': + md['type'] = 'input' + elif md['type'] == 'c': + md['type'] = 'clk' + elif md['type'] == 'l': + md['type'] = 'latch' + else: + raise ValueError(f"Unknown type identifier {md['type']!r}") + for k in ['input', 'offset']: + if md[k]: + md[k] = int(md[k]) + else: + md[k] = 0 + + # output to aim + if md['type'] in ['input', 'latch']: + print("{type} {input} {offset} {path}".format(**md), file=aimf) + + # update ywa + md_type = md.pop('type') + if md['path'][0] == '$': + md['path'] = [md['path']] + else: + md['path'] = [f"\\{s}" for s in md['path'].replace('[','.[').split('.')] + if md_type == 'clk': + md['edge'] = "posedge" # always? + ywa['clocks'].append(md) + elif md_type == 'input': + ywa['inputs'].append(md) + elif md_type == 'latch': + ywa['latches'].append(md) + + # get next line + data = await proc.stdout.readline() + aimf.close() + + with open(work_dir / "design_aiger.ywa", mode="w") as f: + json.dump(ywa, f, indent=2) + +if __name__ == "__main__": + asyncio.run(main()) From 99e704e6cb76663b7cdaaf07e5cf0766d434e51a Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH 3/8] btor2aiger: Get assertions from .btor file Assertions show up in the .btor file as 'bad' statements, assuming btor2aiger maintains the same order this should get us the list of assertions in the order they appear in the .aig file. --- tools/btor2aig_yw/btor2aig_yw.py | 23 +++++++++++++++++++---- 1 file changed, 19 insertions(+), 4 deletions(-) diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 841383c1..3fe4f3a7 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -23,6 +23,13 @@ def arg_parser(): return parser +def fix_path(path: str) -> list[str]: + if path[0] == '$': + fixed = [path] + else: + fixed = [f"\\{s}" for s in path.replace('[','.[').split('.')] + return fixed + async def main() -> None: args = arg_parser().parse_args() @@ -95,10 +102,7 @@ async def main() -> None: # update ywa md_type = md.pop('type') - if md['path'][0] == '$': - md['path'] = [md['path']] - else: - md['path'] = [f"\\{s}" for s in md['path'].replace('[','.[').split('.')] + md['path'] = fix_path(md['path']) if md_type == 'clk': md['edge'] = "posedge" # always? ywa['clocks'].append(md) @@ -111,6 +115,17 @@ async def main() -> None: data = await proc.stdout.readline() aimf.close() + # find assertions by looking for 'bad' statements in the btor + with open(args.btor_file, mode='r') as f: + data = f.readline() + while data: + if "bad" in data: + m = re.match(r"^\d+ bad \d+ (\S+)", data) + path = fix_path(m.group(1)) + ywa['asserts'].append(path) + data = f.readline() + + with open(work_dir / "design_aiger.ywa", mode="w") as f: json.dump(ywa, f, indent=2) From b7bb1466d2be08480b5c861e3c1fe063c0bb1c63 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH 4/8] Pre-format conditional flags in write_btor Make `-x` flag dependent on `btor_aig on`, and combine with `-c` flag into single `btor_flags` string. --- sbysrc/sby_core.py | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index c56fe63f..e6802610 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1137,9 +1137,11 @@ def instance_hierarchy_error_callback(retcode): print("delete -output", file=f) print("dffunmap", file=f) print("stat", file=f) - #TODO: put -x in a conditional - print("write_btor -x {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) - print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f) + btor_flags = "" + if self.opt_mode == "cover": btor_flags += "-c " + if self.opt_btor_aig: btor_flags += "-x " + print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb design_{m}.btor".format(btor_flags, m=model_name), file=f) + print("write_btor -s {}-i design_{m}_single.info -ywmap design_btor_single.ywb design_{m}_single.btor".format(btor_flags, m=model_name), file=f) proc = SbyProc( self, From 143d03a66eb6e430411b2d16d02cfe73ca8eb29c Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH 5/8] btor2aiger: Use ywa inits list `btor2aiger` tool restarts latch indexing at 0 but aiw2yw expects index to be unique. Offset latch input number by the total input count to fix this. --- tools/btor2aig_yw/btor2aig_yw.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 3fe4f3a7..19fc7b6e 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -82,12 +82,14 @@ async def main() -> None: pattern = r"(?P[cil])(?P\d+) (?P.*?)(\[(?P\d+)\])?$" m = re.match(pattern, string) md = m.groupdict() + md['input'] = int(md['input']) if md['type'] == 'i': md['type'] = 'input' elif md['type'] == 'c': md['type'] = 'clk' elif md['type'] == 'l': md['type'] = 'latch' + md['input'] += ywa['input_count'] else: raise ValueError(f"Unknown type identifier {md['type']!r}") for k in ['input', 'offset']: @@ -109,7 +111,7 @@ async def main() -> None: elif md_type == 'input': ywa['inputs'].append(md) elif md_type == 'latch': - ywa['latches'].append(md) + ywa['inits'].append(md) # get next line data = await proc.stdout.readline() From b68f68d26be3264f0fd70cb1a7f6b163eec61186 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH 6/8] btor2aiger: Install btor2aig_yw Install alongside SBY. Add env helper to python source. Fix hardcoded path in `sby_core.py`. --- Makefile | 2 ++ sbysrc/sby_core.py | 4 +--- tools/btor2aig_yw/btor2aig_yw.py | 1 + 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile index 28f05657..fd66497d 100644 --- a/Makefile +++ b/Makefile @@ -44,6 +44,8 @@ else sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(__file__) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < sbysrc/sby.py > $(DESTDIR)$(PREFIX)/bin/sby chmod +x $(DESTDIR)$(PREFIX)/bin/sby endif + cp tools/btor2aig_yw/btor2aig_yw.py $(DESTDIR)$(PREFIX)/bin/btor2aig_yw + chmod +x $(DESTDIR)$(PREFIX)/bin/btor2aig_yw .PHONY: check_cad_suite run_ci diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index e6802610..f2fc55ba 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1154,14 +1154,12 @@ def instance_hierarchy_error_callback(retcode): return [proc] if model_name == "aig" and self.opt_btor_aig: - #TODO: aiw2yw doesn't know what to do with the latches btor_model = "btor_nomem" proc = SbyProc( self, "btor_aig", self.model(btor_model), - #TODO: fix hardcoded path - f"cd {self.workdir}/model; python3 ~/sby/tools/btor2aig_yw/btor2aig_yw.py design_{btor_model}.btor" + f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor" ) proc.checkretcode = True diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 19fc7b6e..98ad1240 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python3 from __future__ import annotations import argparse From c081a8a75463b7a86b27bfbf1ab059945d99a327 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:40:01 +1300 Subject: [PATCH 7/8] btor2aiger: Use asserts and assumes from .ywb file --- sbysrc/sby_core.py | 2 +- tools/btor2aig_yw/btor2aig_yw.py | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index f2fc55ba..99631f55 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1159,7 +1159,7 @@ def instance_hierarchy_error_callback(retcode): self, "btor_aig", self.model(btor_model), - f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor" + f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor design_btor.ywb" ) proc.checkretcode = True diff --git a/tools/btor2aig_yw/btor2aig_yw.py b/tools/btor2aig_yw/btor2aig_yw.py index 98ad1240..c8c727d2 100644 --- a/tools/btor2aig_yw/btor2aig_yw.py +++ b/tools/btor2aig_yw/btor2aig_yw.py @@ -15,6 +15,11 @@ def arg_parser(): type=Path ) + parser.add_argument( + "ywb_file", + type=Path + ) + parser.add_argument( "-d", "--dest", dest="dest", @@ -118,15 +123,10 @@ async def main() -> None: data = await proc.stdout.readline() aimf.close() - # find assertions by looking for 'bad' statements in the btor - with open(args.btor_file, mode='r') as f: - data = f.readline() - while data: - if "bad" in data: - m = re.match(r"^\d+ bad \d+ (\S+)", data) - path = fix_path(m.group(1)) - ywa['asserts'].append(path) - data = f.readline() + with open(args.ywb_file, mode='r') as f: + data = json.load(f) + ywa['asserts'].extend(data['asserts']) + ywa['assumes'].extend(data['assumes']) with open(work_dir / "design_aiger.ywa", mode="w") as f: From f17a6e118aa1f89d02eda780aac9195440b2b909 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 6 Apr 2024 13:56:43 +1300 Subject: [PATCH 8/8] btor2aiger: Add test Based on fifo.sby, running both with and without `btor_aig on`, as well as combined with `vcd_sim on` (after an earlier version had issues when using `vcd_sim off`). Has both pass and fail checks, so should be able to catch any major issues, although it doesn't fully check equivalence. --- tests/unsorted/btor2aig.sby | 204 ++++++++++++++++++++++++++++++++++++ 1 file changed, 204 insertions(+) create mode 100644 tests/unsorted/btor2aig.sby diff --git a/tests/unsorted/btor2aig.sby b/tests/unsorted/btor2aig.sby new file mode 100644 index 00000000..c080b499 --- /dev/null +++ b/tests/unsorted/btor2aig.sby @@ -0,0 +1,204 @@ +[tasks] +bmc +prove +prove_f: prove +prove_v: prove_f prove +bmc_b2a: bmc btor_aig +prove_b2a: prove btor_aig +prove_f_b2a: prove_f prove btor_aig +prove_v_b2a: prove_v prove_f prove btor_aig + +[options] +prove: +mode prove +-- + +bmc: +mode bmc +-- + +prove_f: expect fail +prove_v: vcd_sim on +btor_aig: btor_aig on + +[engines] +bmc: abc bmc3 +prove: abc --keep-going pdr + +[script] +prove_f: read -define NO_FULL_SKIP=1 +read -formal fifo.sv +prep -top fifo + +[file fifo.sv] +// address generator/counter +module addr_gen +#( parameter MAX_DATA=16 +) ( input en, clk, rst, + output reg [3:0] addr +); + initial addr <= 0; + + // async reset + // increment address when enabled + always @(posedge clk or posedge rst) + if (rst) + addr <= 0; + else if (en) begin + if (addr == MAX_DATA-1) + addr <= 0; + else + addr <= addr + 1; + end +endmodule + +// Define our top level fifo entity +module fifo +#( parameter MAX_DATA=16 +) ( input wen, ren, clk, rst, + input [7:0] wdata, + output [7:0] rdata, + output [4:0] count, + output full, empty +); + wire wskip, rskip; + reg [4:0] data_count; + + // fifo storage + // async read, sync write + wire [3:0] waddr, raddr; + reg [7:0] data [MAX_DATA-1:0]; + always @(posedge clk) + if (wen) + data[waddr] <= wdata; + assign rdata = data[raddr]; + // end storage + + // addr_gen for both write and read addresses + addr_gen #(.MAX_DATA(MAX_DATA)) + fifo_writer ( + .en (wen || wskip), + .clk (clk ), + .rst (rst), + .addr (waddr) + ); + + addr_gen #(.MAX_DATA(MAX_DATA)) + fifo_reader ( + .en (ren || rskip), + .clk (clk ), + .rst (rst), + .addr (raddr) + ); + + // status signals + initial data_count <= 0; + + always @(posedge clk or posedge rst) begin + if (rst) + data_count <= 0; + else if (wen && !ren && data_count < MAX_DATA) + data_count <= data_count + 1; + else if (ren && !wen && data_count > 0) + data_count <= data_count - 1; + end + + assign full = data_count == MAX_DATA; + assign empty = (data_count == 0) && ~rst; + assign count = data_count; + + // overflow protection +`ifndef NO_FULL_SKIP + // write while full => overwrite oldest data, move read pointer + assign rskip = wen && !ren && data_count >= MAX_DATA; + // read while empty => read invalid data, keep write pointer in sync + assign wskip = ren && !wen && data_count == 0; +`else + assign rskip = 0; + assign wskip = 0; +`endif // NO_FULL_SKIP + +`ifdef FORMAL + // observers + wire [4:0] addr_diff; + assign addr_diff = waddr >= raddr + ? waddr - raddr + : waddr + MAX_DATA - raddr; + + // tests + always @(posedge clk) begin + if (~rst) begin + // waddr and raddr can only be non zero if reset is low + w_nreset: cover (waddr || raddr); + + // count never more than max + a_oflow: assert (count <= MAX_DATA); + a_oflow2: assert (waddr < MAX_DATA); + + // count should be equal to the difference between writer and reader address + a_count_diff: assert (count == addr_diff + || count == MAX_DATA && addr_diff == 0); + + // count should only be able to increase or decrease by 1 + a_counts: assert (count == 0 + || count == $past(count) + || count == $past(count) + 1 + || count == $past(count) - 1); + + // read/write addresses can only increase (or stay the same) + a_raddr: assert (raddr == 0 + || raddr == $past(raddr) + || raddr == $past(raddr + 1)); + a_waddr: assert (waddr == 0 + || waddr == $past(waddr) + || waddr == $past(waddr + 1)); + + // full and empty work as expected + a_full: assert (!full || count == MAX_DATA); + w_full: cover (wen && !ren && count == MAX_DATA-1); + a_empty: assert (!empty || count == 0); + w_empty: cover (ren && !wen && count == 1); + + // reading/writing non zero values + w_nzero_write: cover (wen && wdata); + w_nzero_read: cover (ren && rdata); + end else begin + // waddr and raddr are zero while reset is high + a_reset: assert (!waddr && !raddr); + w_reset: cover (rst); + + // outputs are zero while reset is high + a_zero_out: assert (!empty && !full && !count); + end + end + + // if we have verific we can also do the following additional tests + // read/write enables enable + ap_raddr2: assert property (@(posedge clk) disable iff (rst) ren |=> $changed(raddr)); + ap_waddr2: assert property (@(posedge clk) disable iff (rst) wen |=> $changed(waddr)); + + // read/write needs enable UNLESS full/empty + ap_raddr3: assert property (@(posedge clk) disable iff (rst) !ren && !full |=> $stable(raddr)); + ap_waddr3: assert property (@(posedge clk) disable iff (rst) !wen && !empty |=> $stable(waddr)); + + // use block formatting for w_underfill so it's easier to describe in docs + // and is more readily comparable with the non SVA implementation + property write_skip; + @(posedge clk) disable iff (rst) + !wen |=> $changed(waddr); + endproperty + w_underfill: cover property (write_skip); + + // look for an overfill where the value in memory changes + // the change in data makes certain that the value is overriden + let d_change = (wdata != rdata); + property read_skip; + @(posedge clk) disable iff (rst) + !ren && d_change |=> $changed(raddr); + endproperty + w_overfill: cover property (read_skip); + +`endif // FORMAL + +endmodule +