From 9459584d35c72027170f4eb59110ccabd223bf51 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 4 Aug 2026 11:51:16 +0200 Subject: [PATCH] Run basic pre-commit cleanup --- .gitignore | 1 - .pre-commit-config.yaml | 29 ++++++++++++++++ docs/examples/demos/picorv32_axicheck.sby | 1 - docs/examples/fifo/.gitignore | 2 +- docs/examples/fifo/fifo.sby | 2 +- docs/examples/fifo/fifo.sv | 14 ++++---- docs/examples/fifo/golden/fifo.sby | 2 +- docs/examples/fifo/golden/fifo.sv | 18 +++++----- docs/examples/indinv/README.md | 4 +-- docs/examples/indinv/example.py | 2 +- docs/examples/indinv/example.sv | 2 +- docs/examples/tristate/README.md | 4 +-- docs/examples/vhd/.gitignore | 2 +- docs/source/conf.diff | 9 ----- docs/source/index.rst | 1 - docs/source/install.rst | 8 ++--- docs/source/license.rst | 7 ++-- docs/source/quickstart.rst | 42 +++++++++++------------ docs/source/verilog.rst | 1 - sbysrc/sby.py | 2 +- sbysrc/sby_core.py | 8 ++--- sbysrc/sby_engine_aiger.py | 2 +- sbysrc/sby_engine_itp.py | 2 +- sbysrc/sby_status.py | 4 +-- tests/staged_sim_and_verif/Req_Ack.sv | 2 +- tests/statusdb/mixed.py | 2 +- 26 files changed, 94 insertions(+), 79 deletions(-) create mode 100644 .pre-commit-config.yaml delete mode 100644 docs/source/conf.diff diff --git a/.gitignore b/.gitignore index e374fdc..d839639 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,3 @@ /docs/build /sbysrc/demo[0-9] /sbysrc/__pycache__ - diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml new file mode 100644 index 0000000..3694452 --- /dev/null +++ b/.pre-commit-config.yaml @@ -0,0 +1,29 @@ +# To use: +# +# pre-commit run -a +# +# Or: +# +# pre-commit install # (runs every time you commit in git) +# +# To update this file: +# +# pre-commit autoupdate +# +# See https://github.com/pre-commit/pre-commit + +repos: +# Standard hooks +- repo: https://github.com/pre-commit/pre-commit-hooks + rev: v6.0.0 + hooks: + - id: check-case-conflict + - id: check-merge-conflict + - id: check-yaml + args: [--allow-multiple-documents] + - id: debug-statements + - id: end-of-file-fixer + - id: fix-byte-order-marker + - id: mixed-line-ending + args: [--fix,lf] + - id: trailing-whitespace diff --git a/docs/examples/demos/picorv32_axicheck.sby b/docs/examples/demos/picorv32_axicheck.sby index a908cae..1e0c1a4 100644 --- a/docs/examples/demos/picorv32_axicheck.sby +++ b/docs/examples/demos/picorv32_axicheck.sby @@ -22,4 +22,3 @@ prep -top testbench [files] picorv32.v axicheck.v - diff --git a/docs/examples/fifo/.gitignore b/docs/examples/fifo/.gitignore index 2bcf7d7..1f4067f 100644 --- a/docs/examples/fifo/.gitignore +++ b/docs/examples/fifo/.gitignore @@ -1 +1 @@ -fifo_*/ \ No newline at end of file +fifo_*/ diff --git a/docs/examples/fifo/fifo.sby b/docs/examples/fifo/fifo.sby index 4ca4bc6..e124d49 100644 --- a/docs/examples/fifo/fifo.sby +++ b/docs/examples/fifo/fifo.sby @@ -12,7 +12,7 @@ mode cover prove: mode prove -- -bmc: +bmc: mode bmc -- diff --git a/docs/examples/fifo/fifo.sv b/docs/examples/fifo/fifo.sv index ba4d8e7..a0d5af3 100644 --- a/docs/examples/fifo/fifo.sv +++ b/docs/examples/fifo/fifo.sv @@ -1,5 +1,5 @@ // address generator/counter -module addr_gen +module addr_gen #( parameter MAX_DATA=16 ) ( input en, clk, rst, output reg [3:0] addr @@ -20,7 +20,7 @@ module addr_gen endmodule // Define our top level fifo entity -module fifo +module fifo #( parameter MAX_DATA=16 ) ( input wen, ren, clk, rst, input [7:0] wdata, @@ -36,7 +36,7 @@ module fifo wire [3:0] waddr, raddr; reg [7:0] data [MAX_DATA-1:0]; always @(posedge clk) - if (wen) + if (wen) data[waddr] <= wdata; assign rdata = data[raddr]; // end storage @@ -88,8 +88,8 @@ module fifo `ifdef FORMAL // observers wire [4:0] addr_diff; - assign addr_diff = waddr >= raddr - ? waddr - raddr + assign addr_diff = waddr >= raddr + ? waddr - raddr : waddr + MAX_DATA - raddr; // tests @@ -103,7 +103,7 @@ module fifo 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 + a_count_diff: assert (count == addr_diff || count == MAX_DATA && addr_diff == 0); // count should only be able to increase or decrease by 1 @@ -161,7 +161,7 @@ module fifo // the change in data makes certain that the value is overriden let d_change = (wdata != rdata); property read_skip; - @(posedge clk) disable iff (rst) + @(posedge clk) disable iff (rst) !ren && d_change |=> $changed(raddr); endproperty w_overfill: cover property (read_skip); diff --git a/docs/examples/fifo/golden/fifo.sby b/docs/examples/fifo/golden/fifo.sby index 10f2d85..66faf89 100644 --- a/docs/examples/fifo/golden/fifo.sby +++ b/docs/examples/fifo/golden/fifo.sby @@ -12,7 +12,7 @@ mode cover prove: mode prove -- -bmc: +bmc: mode bmc -- bigtest: depth 120 diff --git a/docs/examples/fifo/golden/fifo.sv b/docs/examples/fifo/golden/fifo.sv index d5ceadc..b4388ef 100644 --- a/docs/examples/fifo/golden/fifo.sv +++ b/docs/examples/fifo/golden/fifo.sv @@ -1,5 +1,5 @@ // address generator/counter -module addr_gen +module addr_gen #( parameter MAX_DATA=16, parameter ADDR_BITS=5 ) ( input en, clk, rst, @@ -21,7 +21,7 @@ module addr_gen endmodule // Define our top level fifo entity -module fifo +module fifo #( parameter MAX_DATA=16, parameter ADDR_BITS=5 ) ( input wen, ren, clk, rst, @@ -38,13 +38,13 @@ module fifo wire [ADDR_BITS-1:0] waddr, raddr; reg [7:0] data [MAX_DATA-1:0]; always @(posedge clk) - if (wen) + 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), .ADDR_BITS(ADDR_BITS)) + addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS)) fifo_writer ( .en (wen || wskip), .clk (clk ), @@ -52,7 +52,7 @@ module fifo .addr (waddr) ); - addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS)) + addr_gen #(.MAX_DATA(MAX_DATA), .ADDR_BITS(ADDR_BITS)) fifo_reader ( .en (ren || rskip), .clk (clk ), @@ -90,8 +90,8 @@ module fifo `ifdef FORMAL // observers wire [ADDR_BITS:0] addr_diff; - assign addr_diff = waddr >= raddr - ? waddr - raddr + assign addr_diff = waddr >= raddr + ? waddr - raddr : waddr + MAX_DATA - raddr; // tests @@ -105,7 +105,7 @@ module fifo 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 + a_count_diff: assert (count == addr_diff || count == MAX_DATA && addr_diff == 0); // count should only be able to increase or decrease by 1 @@ -163,7 +163,7 @@ module fifo // the change in data makes certain that the value is overriden let d_change = (wdata != rdata); property read_skip; - @(posedge clk) disable iff (rst) + @(posedge clk) disable iff (rst) !ren && d_change |=> $changed(raddr); endproperty w_overfill: cover property (read_skip); diff --git a/docs/examples/indinv/README.md b/docs/examples/indinv/README.md index 3ebc3c8..8988fb6 100644 --- a/docs/examples/indinv/README.md +++ b/docs/examples/indinv/README.md @@ -5,7 +5,7 @@ Inductive invariants are boolean functions over the design state, that 1. return true for every reachable state (=invariants), and 2. if they return true for a state then they will also return true for every state reachable from the given state (=inductive) - + Formally, inductive invariants are sets of states that are closed under the state transition function (=inductive), and contain the entire set of reachable states (=invariants). @@ -17,7 +17,7 @@ the following technique for proving and using inductive invariants. Consider the following circuit (stripped-down [example.sv](example.sv)): ```SystemVerilog -module example(clk, state); +module example(clk, state); input logic clk; output logic [4:0] state = 27; diff --git a/docs/examples/indinv/example.py b/docs/examples/indinv/example.py index 0ef9048..d898b3a 100644 --- a/docs/examples/indinv/example.py +++ b/docs/examples/indinv/example.py @@ -54,7 +54,7 @@ for lidx, paths in pathsByLidx.items(): loop = path[1] loopsByLidx[lidx] = loop - + print() print("%d-Element Loop:" % len(loop)) print(" ", " ->- ".join(["%2d" % i for i in loop + (loop[0],)])) diff --git a/docs/examples/indinv/example.sv b/docs/examples/indinv/example.sv index 40f0c7f..d6f557d 100644 --- a/docs/examples/indinv/example.sv +++ b/docs/examples/indinv/example.sv @@ -1,4 +1,4 @@ -module example(clk, state); +module example(clk, state); input logic clk; output logic [4:0] state = 27; diff --git a/docs/examples/tristate/README.md b/docs/examples/tristate/README.md index 155fab2..77e5a2e 100644 --- a/docs/examples/tristate/README.md +++ b/docs/examples/tristate/README.md @@ -1,12 +1,12 @@ # Tristate demo -Run +Run sby -f tristate.sby pass to run the pass task. This uses the top module that exclusively enables each of the submodules. -Run +Run sby -f tristate.sby fail diff --git a/docs/examples/vhd/.gitignore b/docs/examples/vhd/.gitignore index 8654c05..41b9902 100644 --- a/docs/examples/vhd/.gitignore +++ b/docs/examples/vhd/.gitignore @@ -1 +1 @@ -formal_bind*/ \ No newline at end of file +formal_bind*/ diff --git a/docs/source/conf.diff b/docs/source/conf.diff deleted file mode 100644 index 055201d..0000000 --- a/docs/source/conf.diff +++ /dev/null @@ -1,9 +0,0 @@ ---- a/docs/source/conf.py -+++ b/docs/source/conf.py -@@ -1,5 +1,5 @@ - #!/usr/bin/env python3 --project = 'YosysHQ Docs' -+project = 'YosysHQ SBY' - author = 'YosysHQ GmbH' - copyright ='2021 YosysHQ GmbH' - diff --git a/docs/source/index.rst b/docs/source/index.rst index e40120f..e5e484e 100644 --- a/docs/source/index.rst +++ b/docs/source/index.rst @@ -23,4 +23,3 @@ formal tasks: verific.rst appnotes.rst license.rst - diff --git a/docs/source/install.rst b/docs/source/install.rst index 31049e2..66a0acc 100644 --- a/docs/source/install.rst +++ b/docs/source/install.rst @@ -46,7 +46,7 @@ Installing prerequisites (this command is for Ubuntu 20.04): sudo apt-get install build-essential clang bison flex \ libreadline-dev gawk tcl-dev libffi-dev git \ graphviz xdot pkg-config python3 zlib1g-dev - + python3 -m pip install click Required components @@ -88,7 +88,7 @@ Boolector https://boolector.github.io .. code-block:: text - + git clone https://github.com/boolector/boolector cd boolector ./contrib/setup-btor2tools.sh @@ -98,9 +98,9 @@ https://boolector.github.io sudo cp build/bin/{boolector,btor*} /usr/local/bin/ sudo cp deps/btor2tools/build/bin/btorsim /usr/local/bin/ -To use the ``btor`` engine you will need to install btor2tools from +To use the ``btor`` engine you will need to install btor2tools from `commit c35cf1c `_ or -newer. +newer. Yices 2 ------- diff --git a/docs/source/license.rst b/docs/source/license.rst index 786dc59..e80b56b 100644 --- a/docs/source/license.rst +++ b/docs/source/license.rst @@ -7,13 +7,13 @@ SymbiYosys (sby) itself is licensed under the ISC license: .. code-block:: text SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows - + Copyright (C) 2016 Claire Xenia Wolf - + Permission to use, copy, modify, and/or distribute this software for any purpose with or without fee is hereby granted, provided that the above copyright notice and this permission notice appear in all copies. - + THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR @@ -24,4 +24,3 @@ SymbiYosys (sby) itself is licensed under the ISC license: Note that the solvers and other components used by SymbiYosys come with their own license terms. - diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst index 0105dc6..d08f287 100644 --- a/docs/source/quickstart.rst +++ b/docs/source/quickstart.rst @@ -2,34 +2,34 @@ Getting started =============== -.. note:: +.. note:: - This tutorial assumes sby and boolector installation as per the - :ref:`install-doc`. For this tutorial, it is also recommended to install + This tutorial assumes sby and boolector installation as per the + :ref:`install-doc`. For this tutorial, it is also recommended to install `GTKWave `_, an open source VCD viewer. `Source files used in this tutorial - `_ can be + `_ can be found on the sby git, under ``docs/examples/fifo``. First In, First Out (FIFO) buffer ********************************* From `Wikipedia `_, -a FIFO is - +a FIFO is + a method for organizing the manipulation of a data structure (often, specifically a data buffer) where the oldest (first) entry, or "head" of the queue, is processed first. Such processing is analogous to servicing people in a queue area on a first-come, first-served (FCFS) basis, i.e. in the same sequence in which - they arrive at the queue's tail. + they arrive at the queue's tail. In hardware we can create such a construct by providing two addresses into a register file. This tutorial will use an example implementation provided in -`fifo.sv`. +`fifo.sv`. -First, the address generator module: +First, the address generator module: .. literalinclude:: ../examples/fifo/fifo.sv :language: systemverilog @@ -103,7 +103,7 @@ SymbiYosys ********** SymbiYosys (sby) uses a .sby file to define a set of tasks used for -verification. +verification. **basic** Bounded model check of design. @@ -122,16 +122,16 @@ should be run if no tasks are specified, such as when running the command below. sby fifo.sby -.. note:: +.. note:: The default set of tests should all pass. If this is not the case there may - be a problem with the installation of sby or one of its solvers. + be a problem with the installation of sby or one of its solvers. To see what happens when a test fails, the below command can be used. Note the use of the ``-f`` flag to automatically overwrite existing task output. While this may not be necessary on the first run, it is quite useful when making adjustments to code and rerunning tests to validate. - + sby -f fifo.sby nofullskip The nofullskip task disables the code shown below. Because the count signal has @@ -199,7 +199,7 @@ We can then run gtkwave with the trace file indicated to see the correct operation as in the image below. When the buffer is empty, a read with no write will result in the ``wksip`` signal going high, incrementing *both* read and write addresses and avoiding underflow. - + gtkwave fifo_cover/engine_0/trace4.vcd noskip.gtkw .. image:: media/gtkwave_coverskip.png @@ -233,9 +233,9 @@ while still passing all of the tests? .. note:: If you need a **hint**, try increasing the width of the address wires. 4 bits - supports up to 2\ :sup:`4`\ =16 addresses. Are there other signals that - need to be wider? Can you make the width parameterisable to support - arbitrarily large buffers? + supports up to 2\ :sup:`4`\ =16 addresses. Are there other signals that + need to be wider? Can you make the width parameterisable to support + arbitrarily large buffers? Once the tests are passing with ``MAX_DATA=17``, try something bigger, like 64, or 100. Does the ``basic`` task still pass? What about ``cover``? By default, @@ -246,7 +246,7 @@ try to increase the cover mode depth to be at least a few cycles larger than the ``MAX_DATA``. .. note:: - + Reference files are provided in the ``fifo/golden`` directory, showing how the verilog could have been modified and how a ``bigtest`` task could be added. @@ -258,14 +258,14 @@ Until this point, all of the properties described have been *immediate* assertions. As the name suggests, immediate assertions are evaluated immediately whereas concurrent assertions allow for the capture of sequences of events which occur across time. The use of concurrent assertions requires a -more advanced series of checks. +more advanced series of checks. Compare the difference in implementation of ``w_underfill`` depending on the presence of Verific. ``w_underfill`` looks for a sequence of events where the write enable is low but the write address changes in the following cycle. This is the expected behaviour for reading while empty and implies that the ``w_skip`` signal went high. Verific enables elaboration of SystemVerilog -Assertions (SVA) properties. Here we use such a property, ``write_skip``. +Assertions (SVA) properties. Here we use such a property, ``write_skip``. .. literalinclude:: ../examples/fifo/fifo.sv :language: systemverilog @@ -310,5 +310,5 @@ Further information ******************* For more information on the uses of assertions and the difference between immediate and concurrent assertions, refer to appnote 109: `Property Checking -with SystemVerilog Assertions +with SystemVerilog Assertions `_. diff --git a/docs/source/verilog.rst b/docs/source/verilog.rst index 457ac36..2519afa 100644 --- a/docs/source/verilog.rst +++ b/docs/source/verilog.rst @@ -225,4 +225,3 @@ SystemVerilog Concurrent Assertions ----------------------------------- TBD, see :ref:`sva`. - diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 315aa55..e83d09f 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -106,7 +106,7 @@ if status_show or status_reset or task_status or status_format: if status_format: status_db.print_status_summary_fmt(tasknames, status_format, status_latest) - + if task_status: status_db.print_task_summary() diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index d97599c..d16761b 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -441,7 +441,7 @@ class SbyConfig: import sby_autotune self.autotune_config = sby_autotune.SbyAutotuneConfig() continue - + if section == "cancelledby": mode = "cancelledby" if args is not None: @@ -481,7 +481,7 @@ class SbyConfig: if mode == "autotune": self.autotune_config.config_line(self, line) continue - + if mode == "cancelledby": taskname = line.strip() if taskname: @@ -1319,7 +1319,7 @@ class SbyTask(SbyConfig): proc.terminate(timeout or cancel) if timeout: self.update_unknown_props(dict(source="timeout")) - + def cancel(self): self.terminate(cancel=True) self.update_status("CANCELLED") @@ -1424,7 +1424,7 @@ class SbyTask(SbyConfig): self.handle_bool_option("skip_prep", False) self.handle_bool_option("assume_early", True) - + if self.opt_mode == "cover": self.handle_bool_option("cover_assert", False) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index c17f6bf..a84de05 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -46,7 +46,7 @@ def run(mode, task, engine_idx, engine): if mode != "prove": task.error("The aiger solver 'avy' is only supported in prove mode.") solver_cmd = " ".join([task.exe_paths["avy"], "--cex", "-"] + solver_args[1:]) - + elif solver_args[0] == "rIC3": if mode not in ["bmc", "prove"]: task.error("The aiger solver 'rIC3' is only supported in bmc and prove mode.") diff --git a/sbysrc/sby_engine_itp.py b/sbysrc/sby_engine_itp.py index 865c45b..421f3b3 100644 --- a/sbysrc/sby_engine_itp.py +++ b/sbysrc/sby_engine_itp.py @@ -110,4 +110,4 @@ def run(mode, task, engine_idx, engine): ) proc.output_callback = output_callback - proc.register_exit_callback(exit_callback) \ No newline at end of file + proc.register_exit_callback(exit_callback) diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py index 52f3019..f48e778 100644 --- a/sbysrc/sby_status.py +++ b/sbysrc/sby_status.py @@ -255,7 +255,7 @@ class SbyStatusDb: for fmt in self.live_formats: fmtline = format_status_data_fmtline(row, fmt) self.task.log(f"{click.style(fmt, fg='yellow')}: {fmtline}") - + @transaction def add_task_trace( self, @@ -511,7 +511,7 @@ def combine_statuses(statuses): return ",".join(sorted(statuses)) def parse_status_data_row(raw: sqlite3.Row): - row_dict = dict(raw) + row_dict = dict(raw) row_dict["name"] = json.loads(row_dict.get("name", "null")) row_dict["data"] = json.loads(row_dict.get("data") or "{}") return row_dict diff --git a/tests/staged_sim_and_verif/Req_Ack.sv b/tests/staged_sim_and_verif/Req_Ack.sv index 145dd97..b71b3b1 100644 --- a/tests/staged_sim_and_verif/Req_Ack.sv +++ b/tests/staged_sim_and_verif/Req_Ack.sv @@ -34,7 +34,7 @@ module DUT ( ); // ack comes exactly 4 cycles after req - assume property (@(posedge clk) + assume property (@(posedge clk) req |-> ##4 ack ); diff --git a/tests/statusdb/mixed.py b/tests/statusdb/mixed.py index e8995a1..c47168d 100644 --- a/tests/statusdb/mixed.py +++ b/tests/statusdb/mixed.py @@ -59,7 +59,7 @@ def main(): elif workdir == "mixed_no_assert" and prop_type == "cover": valid_status = ["PASS"] assert status in valid_status, f"Unexpected {prop_type} status {status} for {prop} ({src})" - + if __name__ == "__main__": main()