Run basic pre-commit cleanup

.gitignore

@@ -1,4 +1,3 @@
 /docs/build
 /sbysrc/demo[0-9]
 /sbysrc/__pycache__
-

.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

docs/examples/demos/picorv32_axicheck.sby

@@ -22,4 +22,3 @@ prep -top testbench
 [files]
 picorv32.v
 axicheck.v
-

docs/examples/fifo/.gitignore

@@ -1 +1 @@
-fifo_*/
+fifo_*/

docs/examples/fifo/fifo.sby

@@ -12,7 +12,7 @@ mode cover
 prove:
 mode prove
 --
-bmc: 
+bmc:
 mode bmc
 --
 

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);

docs/examples/fifo/golden/fifo.sby

@@ -12,7 +12,7 @@ mode cover
 prove:
 mode prove
 --
-bmc: 
+bmc:
 mode bmc
 --
 bigtest: depth 120

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);

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;
 

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],)]))

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;
 

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
 

docs/examples/vhd/.gitignore

@@ -1 +1 @@
-formal_bind*/
+formal_bind*/

docs/source/conf.diff

@@ -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'
- 

docs/source/index.rst

@@ -23,4 +23,3 @@ formal tasks:
    verific.rst
    appnotes.rst
    license.rst
-

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 <https://github.com/Boolector/btor2tools/commit/c35cf1c>`_ or
-newer. 
+newer.
 
 Yices 2
 -------

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 <claire@yosyshq.com>
-   
+
    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.
-

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 <http://gtkwave.sourceforge.net/>`_, an open source VCD viewer.
     `Source files used in this tutorial
-    <https://github.com/YosysHQ/sby/tree/master/docs/examples/fifo>`_ can be 
+    <https://github.com/YosysHQ/sby/tree/master/docs/examples/fifo>`_ can be
     found on the sby git, under ``docs/examples/fifo``.
 
 First In, First Out (FIFO) buffer
 *********************************
 
 From `Wikipedia <https://en.wikipedia.org/wiki/FIFO_(computing_and_electronics)>`_,
-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
 <https://yosyshq.readthedocs.io/projects/ap109/en/latest/>`_.

docs/source/verilog.rst

@@ -225,4 +225,3 @@ SystemVerilog Concurrent Assertions
 -----------------------------------
 
 TBD, see :ref:`sva`.
-

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()
 

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)
 

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.")

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)
+    proc.register_exit_callback(exit_callback)

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

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
         );
 

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()