``prove`` Unbounded model check to verify safety properties (``assert(...)`` statements)
``live`` Unbounded model check to verify liveness properties (``assert(s_eventually ...)`` statements)
``cover`` Generate set of shortest traces required to reach all cover() statements
-``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
-``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
========= ===========
+..
+ ``equiv`` Formal equivalence checking (usually to verify pre- and post-synthesis equivalence)
+ ``synth`` Reactive Synthesis (synthesis of circuit from safety properties)
+
All other options have default values and thus are optional. The available
options are:
In the 2nd line ``abc`` is the engine, there are no engine options, ``sim3`` is the
solver, and ``-W 15`` are solver options.
+The following mode/engine/solver combinations are currently supported:
+
++-----------+--------------------------+
+| Mode | Engine |
++===========+==========================+
+| ``bmc`` | ``smtbmc [all solvers]`` |
+| | |
+| | ``btor btormc`` |
+| | |
+| | ``btor pono`` |
+| | |
+| | ``abc bmc3`` |
+| | |
+| | ``abc sim3`` |
++-----------+--------------------------+
+| ``prove`` | ``smtbmc [all solvers]`` |
+| | |
+| | ``abc pdr`` |
+| | |
+| | ``aiger avy`` |
+| | |
+| | ``aiger suprove`` |
++-----------+--------------------------+
+| ``cover`` | ``smtbmc [all solvers]`` |
+| | |
+| | ``btor btormc`` |
++-----------+--------------------------+
+| ``live`` | ``aiger suprove`` |
+| | |
+| | ``aiger avy`` |
++-----------+--------------------------+
+
``smtbmc`` engine
~~~~~~~~~~~~~~~~~
* yices
* boolector
+ * bitwuzla
* z3
* mathsat
* cvc4
Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
+``btor`` engine
+~~~~~~~~~~~~~~~
+
+The ``btor`` engine supports hardware modelcheckers that accept btor2 files.
+The engine supports no engine options and supports the following solvers:
+
++-------------------------------+---------------------------------+
+| Solver | Modes |
++===============================+=================================+
+| ``btormc`` | ``bmc``, ``cover`` |
++-------------------------------+---------------------------------+
+| ``pono`` | ``bmc`` |
++-------------------------------+---------------------------------+
+
+
``aiger`` engine
~~~~~~~~~~~~~~~~
print("abc -g AND -fast", file=f)
print("opt_clean", file=f)
print("stat", file=f)
- print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
+ print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f)
proc = SbyProc(
self,
raise KeyError(f"Could not find assert at {location} in properties list!")
return prop
- def find_property_by_cellname(self, cell_name):
+ def find_property_by_cellname(self, cell_name, trans_dict=dict()):
+ # backends may need to mangle names irreversibly, so allow applying
+ # the same transformation here
for prop in self:
- if prop.name == cell_name:
+ if cell_name == prop.name.translate(str.maketrans(trans_dict)):
return prop
- raise KeyError(f"No such property: {cell_name}")
+ raise KeyError(f"No such property: {smt2_name}")
def design_hierarchy(filename):
design_json = json.load(filename)
task.induction_procs.append(proc)
proc_status = None
- last_prop = None
+ last_prop = []
def output_callback(line):
nonlocal proc_status
nonlocal last_prop
+ smt2_trans = {'\\':'/', '|':'/'}
match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
if match:
match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+) \((\S+)\)", line)
if match:
cell_name = match[3]
- prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+ prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
- last_prop = prop
+ last_prop.append(prop)
return line
match = re.match(r"^## [0-9: ]+ Reached cover statement at (\S+) \((\S+)\) in step \d+.", line)
if match:
cell_name = match[2]
- prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+ prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "PASS"
- last_prop = prop
+ last_prop.append(prop)
return line
match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
if match and last_prop:
- last_prop.tracefile = match[1]
- last_prop = None
+ for p in last_prop:
+ p.tracefile = match[1]
+ last_prop = []
return line
match = re.match(r"^## [0-9: ]+ Unreached cover statement at (\S+) \((\S+)\).", line)
if match:
cell_name = match[2]
- prop = task.design_hierarchy.find_property_by_cellname(cell_name)
+ prop = task.design_hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans)
prop.status = "FAIL"
return line
/keepgoing_*/
/submod_props*/
/multi_assert*/
+/aim_vs_smt2_nonzero_start_offset*/
--- /dev/null
+[options]
+mode bmc
+depth 1
+expect fail
+
+[engines]
+smtbmc
+
+[script]
+read -sv top.sv
+prep -top top
+
+[file top.sv]
+module top(
+input foo,
+input bar
+);
+always @(*) begin
+ assert (foo);
+ assert (bar);
+end
+endmodule
--- /dev/null
+[tasks]
+bmc
+prove
+
+[options]
+bmc: mode bmc
+prove: mode prove
+expect fail
+wait on
+
+[engines]
+bmc: abc bmc3
+bmc: abc sim3
+prove: aiger avy
+prove: aiger suprove
+prove: abc pdr
+
+[script]
+read -sv test.sv
+prep -top test
+
+[file test.sv]
+module test (
+ input clk,
+ input [8:1] nonzero_offset
+);
+ reg [7:0] counter = 0;
+
+ always @(posedge clk) begin
+ if (counter == 3) assert(nonzero_offset[1]);
+ counter <= counter + 1;
+ end
+endmodule
[tasks]
bmc
cover
+flatten
[options]
bmc: mode bmc
cover: mode cover
+flatten: mode bmc
expect fail
[script]
read -sv test.sv
prep -top top
+flatten: flatten
[file test.sv]
module test(input foo);
projects / SymbiYosys.git / commitdiff