mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-11 00:13:33 +00:00
Merge f17a6e118a into ff98e51c13
This commit is contained in:
KrystalDelusion
GitHub
commit
687cffb806
2
Makefile
2
Makefile
|
|
@ -52,6 +52,8 @@ else
|
|||
-e "s|##yosys-release-version##|release_version = '$(YOSYS_RELEASE_VERSION)'|;" < 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
|
||||
|
||||
|
|
|
|||
|
|
@ -1139,8 +1139,11 @@ class SbyTask(SbyConfig):
|
|||
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)
|
||||
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,
|
||||
|
|
@ -1152,6 +1155,18 @@ class SbyTask(SbyConfig):
|
|||
|
||||
return [proc]
|
||||
|
||||
if model_name == "aig" and self.opt_btor_aig:
|
||||
btor_model = "btor_nomem"
|
||||
proc = SbyProc(
|
||||
self,
|
||||
"btor_aig",
|
||||
self.model(btor_model),
|
||||
f"cd {self.workdir}/model; btor2aig_yw design_{btor_model}.btor design_btor.ywb"
|
||||
)
|
||||
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)
|
||||
|
|
@ -1281,6 +1296,7 @@ class SbyTask(SbyConfig):
|
|||
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)
|
||||
|
|
|
|||
|
|
@ -176,7 +176,10 @@ def run(mode, task, engine_idx, engine):
|
|||
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}"))
|
||||
|
|
@ -195,7 +198,10 @@ def run(mode, task, engine_idx, engine):
|
|||
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}"))
|
||||
|
|
|
|||
204
tests/unsorted/btor2aig.sby
Normal file
204
tests/unsorted/btor2aig.sby
Normal file
|
|
@ -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
|
||||
|
||||
136
tools/btor2aig_yw/btor2aig_yw.py
Normal file
136
tools/btor2aig_yw/btor2aig_yw.py
Normal file
|
|
@ -0,0 +1,136 @@
|
|||
#!/usr/bin/env python3
|
||||
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(
|
||||
"ywb_file",
|
||||
type=Path
|
||||
)
|
||||
|
||||
parser.add_argument(
|
||||
"-d", "--dest",
|
||||
dest="dest",
|
||||
required=False,
|
||||
type=Path
|
||||
)
|
||||
|
||||
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()
|
||||
|
||||
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<type>[cil])(?P<input>\d+) (?P<path>.*?)(\[(?P<offset>\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']:
|
||||
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')
|
||||
md['path'] = fix_path(md['path'])
|
||||
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['inits'].append(md)
|
||||
|
||||
# get next line
|
||||
data = await proc.stdout.readline()
|
||||
aimf.close()
|
||||
|
||||
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:
|
||||
json.dump(ywa, f, indent=2)
|
||||
|
||||
if __name__ == "__main__":
|
||||
asyncio.run(main())
|
||||
Loading…
Reference in a new issue