yosyshq / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows

SymbiYosys (sby) is a front-end driver program for Yosys-based formal hardware verification flows. See https://yosyshq.readthedocs.io/projects/sby/ for documentation on how to use SymbiYosys.

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. There is some more details in the "Selecting the right engine" section of the documentation.

---

SymbiYosys (sby) is part of the Tabby CAD Suite and the OSS CAD Suite! The easiest way to use sby is to install the binary software suite, which contains all required dependencies, including all supported solvers.

• Contact YosysHQ for a Tabby CAD Suite Evaluation License and download link
• OR go to https://github.com/YosysHQ/oss-cad-suite-build/releases to download the free OSS CAD Suite
• Follow the Install Instructions on GitHub

Make sure to get a Tabby CAD Suite Evaluation License for extensive SystemVerilog Assertion (SVA) support, as well as industry-grade SystemVerilog and VHDL parsers!

For more information about the difference between Tabby CAD Suite and the OSS CAD Suite, please visit https://www.yosyshq.com/tabby-cad-datasheet.

sby's Issues

Large designs take a long time to write the VCD file output

I just ran the Symbiotic EDA Suite (20190416A) on a very large design. Using the boolector solver, it took 30 minutes to find the bug, and another 45 to write out the trace file.

I'll admit this isn't the most current version of SES, so if this has been updated since I can re-run on a more current version.

Test case available upon request.

Dan

Command syntax error using aiger engine

Hi,

I played a bit with SymbiYosys recently but I found out that the Aiger engine isn't called with the "right" options.

e.g.
With this kind of .sby file (and any kind of test.v file):

[options]
mode live

[engines]
aiger aigbmc

[script]
read -sv test.v
prep -top test

[files]
test.v

I am getting this:

SBY  5:56:41 [test] Removing direcory 'test'.
SBY  5:56:41 [test] Copy 'test.v' to 'test/src/test.v'.
SBY  5:56:41 [test] engine_0: aiger avy
SBY  5:56:41 [test] nomem: starting process "cd test/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys"
SBY  5:56:41 [test] nomem: finished (returncode=0)
SBY  5:56:41 [test] aig: starting process "cd test/model; yosys -ql design_aiger.log design_aiger.ys"
SBY  5:56:41 [test] aig: ERROR: Command syntax error: Unknown option or option in arguments.
SBY  5:56:41 [test] aig: > write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig
SBY  5:56:41 [test] aig: >             ^
SBY  5:56:41 [test] aig: finished (returncode=1)
SBY  5:56:41 [test] aig: job failed. ERROR.
SBY  5:56:41 [test] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  5:56:41 [test] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY  5:56:41 [test] DONE (ERROR, rc=16)

I tried to remove the -I and -B options (which are not present in the documentation of write_aiger) but some other errors are showing up...

Struct signals not broken out in VCD files

Consider a file referencing the following SV struct,

    typedef struct {
        logic element;
        logic other;
    } IF;

While an assertion might generate a trace,

   always @(*) assert(v.element == v.other);

the trace will lump these two values together into the same line, making them hard to distinguish.

Note: This test and bug applies to the Verific enabled SV support of SymbiYosys.

Dan

boolector licensing?

From https://symbiyosys.readthedocs.io/en/latest/quickstart.html#selecting-the-right-engine there is the following statement;

smtbmc boolector uses boolector as SMT solver. Note that boolector is only free-to-use for noncommercial purposes. Use smtbmc z3 to use the permissively licensed solver Z3, or use smtbmc yices to use the copyleft licensed solver Yices 2 intead. Yices 2 is the default solver when no argument is used with smtbmc.

However it looks like boolector is released under a MIT license? boolector supports the permissively licensed CaDiCaL, PicoSAT and MiniSAT for SAT solving.

The only engine which seems to be under a non-commercial only license seems to be Lingeling. Is the boolector backend only useful when used with Lingeling?

Unable to find 'z3' engine

I'm running through the "hello" example from Clifford's talk on Yosys formal verification. When I attempt to run the example it looks like it's not able to find the formal engines. I also tried the "yices" solver with the same result.

Is there an extra flag/step/library required to build the formal engines in yosys?

yosys version: 08225f49a410c7df6d7d6fe098a4dabc68789ac5
SymbiYosys version: c003a1b

SBY 15:09:07 [hello] engine_0.basecase: File "/usr/lib/python3.5/subprocess.py", line 947, in __init__
SBY 15:09:07 [hello] engine_0.basecase: restore_signals, start_new_session)
SBY 15:09:07 [hello] engine_0.basecase: File "/usr/lib/python3.5/subprocess.py", line 1551, in _execute_child
SBY 15:09:07 [hello] engine_0.basecase: raise child_exception_type(errno_num, err_msg)
SBY 15:09:07 [hello] engine_0.basecase: FileNotFoundError: [Errno 2] No such file or directory: 'z3'
SBY 15:09:07 [hello] engine_0.induction: Traceback (most recent call last):
SBY 15:09:07 [hello] engine_0.induction: File "/usr/local/bin/yosys-smtbmc", line 392, in <module>
SBY 15:09:07 [hello] engine_0.induction: smt.write(line)
SBY 15:09:07 [hello] engine_0.induction: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 333, in write
SBY 15:09:07 [hello] engine_0.induction: self.setup()
SBY 15:09:07 [hello] engine_0.induction: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 188, in setup
SBY 15:09:07 [hello] engine_0.induction: self.p_open()
SBY 15:09:07 [hello] engine_0.induction: File "/usr/local/bin/../share/yosys/python3/smtio.py", line 282, in p_open
SBY 15:09:07 [hello] engine_0.induction: self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
SBY 15:09:07 [hello] engine_0.induction: File "/usr/lib/python3.5/subprocess.py", line 947, in __init__
SBY 15:09:07 [hello] engine_0.induction: restore_signals, start_new_session)
SBY 15:09:07 [hello] engine_0.induction: File "/usr/lib/python3.5/subprocess.py", line 1551, in _execute_child
SBY 15:09:07 [hello] engine_0.induction: raise child_exception_type(errno_num, err_msg)
SBY 15:09:07 [hello] engine_0.induction: FileNotFoundError: [Errno 2] No such file or directory: 'z3'
SBY 15:09:07 [hello] engine_0.basecase: finished (returncode=1)
Traceback (most recent call last):
  File "/usr/local/bin/sby", line 248, in <module>
    retcode += run_job(t)
  File "/usr/local/bin/sby", line 235, in run_job
    job.run()
  File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 496, in run
    self.taskloop()
  File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 271, in taskloop
    task.poll()
  File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 115, in poll
    self.handle_exit(self.p.returncode)
  File "/usr/local/bin/../share/yosys/python3/sby_core.py", line 71, in handle_exit
    self.exit_callback(retcode)
  File "/usr/local/bin/../share/yosys/python3/sby_engine_smtbmc.py", line 147, in exit_callback
    assert task_status is not None
AssertionError

hello.zip

Proof by induction fails due to invalid starting state

I built a formal test bench using synthesizable drivers and monitors and then ask formal to prove that the error output signals can never be asserted. This passes for BMC but fails during induction, and the failure is because the internal state of the checkers are initialized to a state they could not reach legally.

Perhaps I simply do not grok how the inductive proof works, but it would seem it needs to start from a known valid state, otherwise you are simply debugging a bunch of invalid reset cases.

dcoutput.zip

Zip file contains an .sby, test bench, and design files (which include the driver/monitor)

mpeg.v:626: ERROR: Incompatible re-declaration of wire \input_stream

When running SymbiYosys on https://github.com/ispras/hdl-benchmarks/blob/master/verilog/texas97/MPEG/mpeg.v module the following error appears:

SBY 14:50:12 [/tmp/tmphi2l3a2l] Copy '/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v' to '/tmp/tmphi2l3a2l/src/mpeg.v'.
SBY 14:50:12 [/tmp/tmphi2l3a2l] engine_0: smtbmc
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: starting process "cd /tmp/tmphi2l3a2l/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: Warning: wire '\buffer_out' is assigned in a block at /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v:670.
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: Warning: wire '\buffer_out' is assigned in a block at /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v:772.
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: Warning: wire '\buffer_out' is assigned in a block at /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v:790.
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: Warning: wire '\buffer_out' is assigned in a block at /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v:795.
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v:626: ERROR: Incompatible re-declaration of wire \input_stream.
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: finished (returncode=1)
SBY 14:50:12 [/tmp/tmphi2l3a2l] base: job failed. ERROR.
SBY 14:50:12 [/tmp/tmphi2l3a2l] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:50:12 [/tmp/tmphi2l3a2l] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:50:12 [/tmp/tmphi2l3a2l] Removing direcory '/tmp/tmphi2l3a2l'.
SBY 14:50:12 [/tmp/tmphi2l3a2l] DONE (ERROR, rc=16)

The SBY file is as follows:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -formal /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v
prep -top main

[files]
/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/MPEG/mpeg.v

verilog files path should be relative to sby file path

Suppose I have the following .sby file, saved as hello.sby.

[options]
mode prove
depth 10

[engines]
smtbmc z3

[script]
read_verilog -formal hello.v
prep -top hello

[files]
hello.v

if I launch it using sby -f hello.sby, everything is fine. But if I try to launch it from the parent directory by running sby -f hello/hello.sby I get FileNotFoundError: [Errno 2] No such file or directory: 'hello.v'.

I would suggest making it so that the paths are assumed to be relative to the .sby file location itself, as is the case for a lot of build tools.

I understand that this might break some existing workflow, ts this a concern? The fix should be fairly trivial, but it might confuse some people.

Thanks for the work on Yosys by the way!

Avy solver crashes SES

Consider the following MCVE:

module mcve2(i_clk, o_v);
	input	reg	i_clk;
	output	reg	o_v;

	always @(*)
		o_v = 1;

	always @(*)
		assert(o_v);

endmodule

A simple inspection should assure us that this design will pass.

However, when using the SBY file:

[options]
mode prove

[engines]
aiger avy

[script]
read -formal mcve2.v
prep -top mcve2

[files]
mcve2.v

When using the 20190416A build of the SymbioticEDA Suite (and I think more recent as well, this is only the one I've got installed), I'm getting the following error when using AVY:

SBY 15:57:52 [mcve2] Removing direcory 'mcve2'.
SBY 15:57:52 [mcve2] Copy 'mcve2.v' to 'mcve2/src/mcve2.v'.
SBY 15:57:52 [mcve2] engine_0: aiger avy
SBY 15:57:52 [mcve2] nomem: starting process "cd mcve2/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys"
SBY 15:57:54 [mcve2] nomem: finished (returncode=0)
SBY 15:57:54 [mcve2] aig: starting process "cd mcve2/model; yosys -ql design_aiger.log design_aiger.ys"
SBY 15:57:54 [mcve2] aig: finished (returncode=0)
SBY 15:57:54 [mcve2] engine_0: starting process "cd mcve2; avy --cex - model/design_aiger.aig"
SBY 15:57:57 [mcve2] engine_0: finished (returncode=139)
Traceback (most recent call last):
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/sby", line 388, in <module>
    retcode |= run_job(t)
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/sby", line 346, in run_job
    job.run(setupmode)
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/../share/yosys/python3/sby_core.py", line 624, in run
    self.taskloop()
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/../share/yosys/python3/sby_core.py", line 243, in taskloop
    task.poll()
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/../share/yosys/python3/sby_core.py", line 162, in poll
    self.handle_exit(self.p.returncode)
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/../share/yosys/python3/sby_core.py", line 100, in handle_exit
    self.exit_callback(retcode)
  File "/opt/symbiotic/symbiotic-20190416A/bin/../libexec/../share/yosys/python3/sby_engine_aiger.py", line 82, in exit_callback
    assert task_status is not None
AssertionError

Expected behavior

This design should simply PASS.

Dan

Any issue with using ## for specifying temporal information in SVA?

I get the following error while running the command sby -f counters.sv. What could be the reason?

Error

$ sby -f counters.sby
SBY 16:56:06 [counters] Removing direcory 'counters'.
SBY 16:56:06 [counters] Copy 'counters.sv' to 'counters/src/counters.sv'.
SBY 16:56:06 [counters] engine_0: smtbmc
SBY 16:56:06 [counters] base: starting process "cd counters/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 16:56:06 [counters] base: counters.sv:61: ERROR: syntax error, unexpected '#'
SBY 16:56:06 [counters] base: finished (returncode=1)
SBY 16:56:06 [counters] base: job failed. ERROR.
SBY 16:56:06 [counters] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:56:06 [counters] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 16:56:06 [counters] DONE (ERROR, rc=16)

counters.sby

[options]
mode bmc

[engines]
smtbmc

[script]
read -formal counters.sv
prep -top counters

[files]
counters.sv

counters.sv

// Four independent counters which count in different steps.
// All are 13-bit counters which count upto 2^NUM_BITS.
// vineeshvs

module counters (clk, rst, en1, en2, en3, en4, count1, count2, count3, count4, full1, full2, full3, full4);

   // Change the size of counter here.
   parameter NUM_BITS = 25;

   input clk, rst, en1, en2, en3, en4;
   output [NUM_BITS-1:0] count1, count2, count3, count4;
   reg [NUM_BITS-1:0] 	count1, count2, count3, count4;
   output 	full1, full2, full3, full4;

		 
   //initial begin
   //count1 = 8'h0;
   //count2 = 8'h0;
   //en1 = 1'b1;
   //end

   wire full_1, full_2, full_3, full_4;
  
   always @(posedge clk) begin
      if (!rst) begin
	 count1 <= 0;
	 count2 <= 0;
	 count3 <= 0;
	 count4 <= 0;
      end else begin
	 // Counter 1
	 if (en1 && !full_1) count1 <= count1 + 1;
	 // Counter 2
	 if (en2 && !full_2) count2 <= count2 + 2;
	 // Counter 3
	 if (en3 && !full_3) count3 <= count3 + 4;
	 // Counter 4
	 if (en4 && !full_4) count4 <= count4 + 8;
      end
   end

   //assign full_1 = (count1 == 4'd8192);
   assign full_1 = (count1 == 2**NUM_BITS - 8);
   assign full_2 = (count2 == 2**NUM_BITS - 8);
   assign full_3 = (count3 == 2**NUM_BITS - 8);
   assign full_4 = (count4 == 2**NUM_BITS - 8);

   assign full1 = full_1;
   assign full2 = full_2;
   assign full3 = full_3;
   assign full4 = full_4;

   //assign p = (count2 == 8'd90);

   //assert property (p == 1'b0);

   //assert property (full2 == 1'b0);

   `ifdef FORMAL
   assign P = ((rst ==1) ##1 (count1 >= 2**NUM_BITS - 4 | count2 >= 2**NUM_BITS - 4 | count3 >= 2**NUM_BITS - 4 | count4 >= 2**NUM_BITS - 4));

   assert property (P == 1'b0);// & x != 16'd32000);
   `endif

endmodule

Note: I also face issues with implies operators (|->), repetition ([1:$]) etc. Where can I see examples of SymbiYosys with the supported SVA operators?

Broken Pipe Error

Can someone please help me out with this?

System
Ubuntu 18.04
Python3

I am cloning the repository, installing all the pre-reqs and install all the dependencies. Then I,

cd cores/picorv32
make -C checks

The process ends with

Traceback (most recent call last):
  File "/usr/local/bin/yosys-smtbmc", line 1418, in <module>
    smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
  File "/usr/local/bin/yosys-smtbmc", line 1148, in smt_assert_consequent
    smt.write("(assert %s)" % expr)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 402, in write
    stmt = self.unparse(self.unroll_stmt(s))
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 290, in unroll_stmt
    decl = self.unroll_stmt(decl)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 290, in unroll_stmt
    decl = self.unroll_stmt(decl)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 290, in unroll_stmt
    decl = self.unroll_stmt(decl)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 290, in unroll_stmt
    decl = self.unroll_stmt(decl)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in unroll_stmt
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 261, in <listcomp>
    stmt = [self.unroll_stmt(s) for s in stmt]
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 291, in unroll_stmt
    self.write(self.unparse(decl), unroll=False)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 436, in write
    self.p_write(stmt + "\n", True)
  File "/usr/local/bin/../share/yosys/python3/smtio.py", line 319, in p_write
    self.p.stdin.flush()
BrokenPipeError: [Errno 32] Broken pipe

sby: Failed to create process

I'm using msys2, and I followed the instructions as best I could - for Z3 I used the released binary package rather than building from source, as the instructions here (https://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing) assume Linux.

The only thing it does is spit out:

$sby
failed to create process.

yosys treats default keyword in a case expression as an identifier

This comes from ZipCPU's "Building hello world, using a serial port transmitter" tutorial, which can be found here. I have attached the zip file containing the txuart.v and txuart.sby files used in the tutorial for convenience. I can reproduce the issue with these as follows:

ex-05-hello$ sby -f txuart.sby
SBY 14:35:52 [txuart] Removing direcory 'txuart'.
SBY 14:35:52 [txuart] Copy 'txuart.v' to 'txuart/src/txuart.v'.
SBY 14:35:52 [txuart] engine_0: smtbmc yices
SBY 14:35:52 [txuart] base: starting process "cd txuart/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 14:35:52 [txuart] base: txuart.v:235: ERROR: Identifier `\default' is implicitly declared and `default_nettype is set to none.
SBY 14:35:52 [txuart] base: finished (returncode=1)
SBY 14:35:52 [txuart] base: job failed. ERROR.
SBY 14:35:52 [txuart] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:35:52 [txuart] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 14:35:52 [txuart] DONE (ERROR, rc=16)
ex-05-hello$ yosys -V
Yosys 0.8+572 (git sha1 c4c39e98, clang 7.0.0-3 -fPIC -Os)

As you can see from the attached txuart.v file, line 235 is a default case item in a case expression.

ex-04-reqwalker.zip

Add support for environment variables in filenames

This could simplify setups when referring to multiple IP repositories.

Confusing error message regarding unsupported dffsr

For the following code,

module tst(i_clk, i_rst_n, i_en, i_input, o_output);
	input	wire	i_clk, i_rst_n, i_en, i_input;
	output	reg	o_output;

	always @(posedge i_clk, negedge i_rst_n)
	if (i_rst_n)
		o_output <= 0;
	else if (i_en)
		o_output <= i_input;

	always @(*)
		assume(!i_input);
	always @(*)
		assert(!o_output);
endmodule

and sby file

[options]
mode prove

[engines]
smtbmc

[script]
read -sv tst.sv
prep -top tst

[files]
tst.sv

The verific enabled SymbiYosys produces the cryptic error message:
SBY 18:38:14 [tst] Removing direcory 'tst'.
SBY 18:38:14 [tst] Copy 'tst.sv' to 'tst/src/tst.sv'.
SBY 18:38:14 [tst] engine_0: smtbmc
SBY 18:38:14 [tst] base: starting process "cd tst/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 18:38:14 [tst] base: -- (c) Copyright 1999 - 2018 Verific Design Automation Inc. All rights reserved
SBY 18:38:14 [tst] base: -- Compilation time was Tue May 29 15:48:34 2018
SBY 18:38:14 [tst] base: -- This program will expire on Thu Sep  6 15:48:34 2018
SBY 18:38:14 [tst] base: VERIFIC-WARNING [VERI-1167] tst.sv:6: if-condition does not match any sensitivity list edge
SBY 18:38:14 [tst] base: finished (returncode=0)
SBY 18:38:14 [tst] smt2: starting process "cd tst/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 18:38:14 [tst] smt2: -- (c) Copyright 1999 - 2018 Verific Design Automation Inc. All rights reserved
SBY 18:38:14 [tst] smt2: -- Compilation time was Tue May 29 15:48:34 2018
SBY 18:38:14 [tst] smt2: -- This program will expire on Thu Sep  6 15:48:34 2018
SBY 18:38:14 [tst] smt2: ERROR: Unsupported cell type $dffsr for cell tst.$auto$verific.cc:1062:import_netlist$27.
SBY 18:38:14 [tst] smt2: finished (returncode=1)
SBY 18:38:14 [tst] smt2: job failed. ERROR.
SBY 18:38:14 [tst] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:38:14 [tst] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 18:38:14 [tst] DONE (ERROR, rc=16)

As far as I can tell, the problem is that I declared the reset to be a negative edge reset, but then tested whether it was 1'b1 instead of 1'b0. While this is the fault of the code in question, the error message should have pointed me to the source code line in question or at least the signal.

Dan

Can't include defines from other module

I'm running SymbiYosys on https://github.com/ispras/hdl-benchmarks/blob/master/verilog/texas97/PI_BUS/multi_master/bus.v module. This module uses several defines from https://github.com/ispras/hdl-benchmarks/blob/master/verilog/texas97/PI_BUS/multi_master/main.v module. How to get them for 'bus.v' to be formally checked? Here is my SBY:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -formal /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v
prep -top bus_cont

[files]
/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v

It seems to be impossible to add full path to main.v module, because the module inside it contains an instance of the bus module. I've tried to use -incdir option in the following way:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -incdir /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master -formal /home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v
prep -top main

[files]
/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v

and the result was:

SBY 15:14:55 [test] Removing direcory 'test'.
SBY 15:14:55 [test] Copy '/home/ssedai/projects/retrascope-mc-benchmark/src/main/benchmarks/texas97/PI_BUS/multi_master/bus.v' to 'test/src/bus.v'.
SBY 15:14:55 [test] engine_0: smtbmc
SBY 15:14:55 [test] base: starting process "cd test/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:14:55 [test] base: ERROR: Module `bus_cont' not found!
SBY 15:14:55 [test] base: finished (returncode=1)
SBY 15:14:55 [test] base: job failed. ERROR.
SBY 15:14:55 [test] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:14:55 [test] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:14:55 [test] DONE (ERROR, rc=16)

Warmup failed but there is no assumptions or assertions

I have a slightly complicated FSM using a 2 process model, and when I try to use sby on it with BMC it failed with warmup failed.

Here is the smallest test case that I have:

module assign2_fsm_behavioral (input clk, input rst, input ped, input car, input T10, input T30, input T60,
                                output reg RM, output reg YM, output reg GM, output reg RS, output reg YS,  output reg GS,
                                output reg trigger);



localparam G_R = 3'd0,
           Y_R = 3'd1,
           R_G = 3'd2,
           R_G_60T = 3'd3,
           R_Y = 3'd4 ;

reg [3:0] state;
reg [3:0] next_state;

//Initial reset

initial begin
    state = 0;
    next_state = 0;
    RM = 0;
    YM = 0;
    GM = 0;
    RS = 0;
    YS = 0;
    GS = 0;
    trigger = 0;
end

always @(*) begin
    case(state)
        G_R: begin
                if ((ped | car) & T60) begin
                    next_state <= Y_R;
                    trigger <= 1;
                    //RM <= 0;
                    YM <= 1;
                    //GM <= 0;
                    //RS <= 1;
                    //YS <= 0;
                    //GS <= 0;                
                end else begin
                    trigger <= 0;
                    next_state <= G_R;
                    //RM <= 0;
                    YM <= 1; // BUG: if this is changed to 0, sby succeeds, but if this is 1, sby fails
                    //GM <= 1;
                    //RS <= 1;    
                    //YS <= 0;
                    //GS <= 0;
                end
        end
        default: begin
                trigger <= 0;
                next_state <= R_G;
                //RM <= 0;
                YM <= 1;
                //GM <= 0;
                //RS <= 0;
                //YS <= 0;
                //GS <= 0;
        end

and the sby file:

[options]
mode bmc
depth 100


[engines]
smtbmc z3

[script]
read -formal testbug.sv
prep -top assign2_fsm_behavioral


[files]
testbug.sv

For some reason if YM inside end else begin is changed to YM <= 0 BMC works, while if its YM <= 1 BMC fails

SymbiYosys crashes

See the attached SBY-created directory.

wbxbar2.zip

SymbiYosys is crashing with an incomprehensible error. Not sure where to go with finding or fixing it. I'm expecting errors in the code in question, just not the error messages given.

Verific fails on this with a trace that doesn't make sense either, but I'll make that a separate bug, if I can play the two against each other. That is, the Verific version produces a trace (albeit one that doesn't appear to match the logic).

disable iff is sensitive beyond the sensitivity of the assertion

When using disable iff, SymbiYosys is sensitive to the clock after the assertion/assumption is to take place. Consider, for example, the following MCVE:

mcve.zip

In it, there's a two clock assertion that should take place on clocks 0 and 1. This assertion is disabled by the reset signal. Hence, it should only be checked if the reset signal is true on clocks 0 and 1. However, the reset signal is low on clocks 0 and 1, only to be raised on clock 2. This invalidates the assertion when it should not.

So the sequence is: Good ##1 should fail ##1 reset, and the result is that it does not fail.

The cover statement in the attached MCVE shows that the assertion should have failed.

Dan

Suggested update to the main README file

Several individuals have struggled with the initial concepts of Formal Verification. A classic example would be this issue, which I've written about extensively at ZipCPU.com. I've now written many articles on the topic and posted them to ZipCPU.com.

Therefore, I'm recommending the following patch to the SymbiYosys readme file, to reference these articles.

Dan

diff --git a/README.md b/README.md
index 7363d8e..e996989 100644
--- a/README.md
+++ b/README.md
@@ -1,5 +1,10 @@
 
-SymbiYosys (sby) is a front-end driver program for Yosys-based formal
-hardware verification flows. See http://symbiyosys.readthedocs.io/ for
-documentation.
+SymbiYosys (sby) is a front-end driver program for
+[Yosys](http://www.clifford.at/yosys)-based formal hardware verification flows. See [http://symbiyosys.readthedocs.io/](http://symbiyosys.readthedocs.io/) for
+documentation on how to use SymbiYosys.
+
+Many example designs using SymbiYosys have been published on the
+[ZipCPU blog](http://zipcpu.com).  Please consider browsing the
+[formal verification page](http://zipcpu.com/formal/formal.html)
+of the [ZipCPU blog](http://zipcpu.com) for examples and commentary.

suprove liveness fails with async reset present

ref #59 recently closed.

The same example but with

clk2fflogic

in the [script] section of the .sby file (after the prep command), with no change to the Verilog causes a passing liveness proof to now fail.

for an example using async resets, this clk2fflogic option is needed.

is the now failing liveness proof expected behaviour?

SymbiYosys fails with an internal exception instead of generating counter example when using abc

During the last weeks I had an error when using abc pdr with SymbiYosys with various designs. When there is an SVA assertion which should fail, SymbiYosys itself fails with an internal assertion which results in a Python exception. If I correct the SVA, which fails, then SymbiYosys runs correctly.

I've created a simplified test design which you can find here:
https://git.goodcleanfun.de/tmeissner/bug_reports/src/branch/master/SymbiYosys_27

Running it with make results in an error like this:

SBY 13:51:42 [symbiyosys_flag_check] smt2: finished (returncode=0)
SBY 13:51:42 [symbiyosys_flag_check] engine_0: starting process "cd symbiyosys_flag_check; yosys-smtbmc -s yices --noprogress --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc --aig model/design_aiger.aim:engine_0/trace.aiw --aig-noheader model/design_smt2.smt2"
SBY 13:51:42 [symbiyosys_flag_check] engine_0: ##   0:00:00  Solver: yices
SBY 13:51:42 [symbiyosys_flag_check] engine_0: Traceback (most recent call last):
SBY 13:51:42 [symbiyosys_flag_check] engine_0: File "/opt/symbiotic/symbiotic-20190103A/bin/../libexec/yosys-smtbmc", line 515, in <module>
SBY 13:51:42 [symbiyosys_flag_check] engine_0: width = smt.net_width(topmod, path)
SBY 13:51:42 [symbiyosys_flag_check] engine_0: File "/opt/symbiotic/symbiotic-20190103A/libexec/../share/yosys/python3/smtio.py", line 829, in net_width
SBY 13:51:42 [symbiyosys_flag_check] engine_0: assert net_path[-1] in self.modinfo[mod].wsize
SBY 13:51:42 [symbiyosys_flag_check] engine_0: AssertionError
SBY 13:51:42 [symbiyosys_flag_check] engine_0: finished (returncode=1)
Traceback (most recent call last):
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/sby", line 310, in <module>
    retcode |= run_job(t)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/sby", line 274, in run_job
    job.run()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 564, in run
    self.taskloop()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 195, in taskloop
    task.poll()
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 116, in poll
    self.handle_exit(self.p.returncode)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_core.py", line 71, in handle_exit
    self.exit_callback(retcode)
  File "/opt/symbiotic/symbiotic_latest/bin/../libexec/../share/yosys/python3/sby_engine_abc.py", line 109, in exit_callback2
    assert task2_status is not None
AssertionError

The same error occurs when doing a bounded model check with abc bmc3. The smtbmc engine is not effected.

the bmc counter demo doesn't work if reg type is switched to logic

This code assertion fail as expected

module demo (
  input clk,
  output [5:0] counter
);
  reg [5:0] counter = 0;

  always @(posedge clk) begin
    if (counter == 15)
      counter <= 0;
    else
      counter <= counter + 1;
  end

`ifdef FORMAL
  always @(posedge clk) begin
    assert (counter < 10);
  end
`endif
endmodule

After change the type of counter to logic logic [5:0] counter = 0; the assertion never fails.

module demo (
  input clk,
  output [5:0] counter
);
  logic [5:0] counter = 0;

  always @(posedge clk) begin
    if (counter == 15)
      counter <= 0;
    else
      counter <= counter + 1;
  end

`ifdef FORMAL
  always @(posedge clk) begin
    assert (counter < 10);
  end
`endif
endmodule

Use more Python standard libraries

We can harness the power of ArgParse (for parsing the arguments) and ConfigParser (for the sby file).

The benefit of argparse are:

• included in python standard library
• easy to add menu entry
• no more if ladders :D
• parameter checking
• semi-automatic help
• many more (but not relevant right for this issue)

Didn't use ConfigParse much, but I can look if it can replace the parser class with all the feature intact.

If you dean this change worthy, I can work (albeit slowly) on it.

MSYS2: Makefile with Clang: unsupported option -fPIC for target x86_64-w64-windows-gnu

Trying to use CONFIG := clang with CXXFLAGS -fPIC on x86_64-w64-windows-gnu gets me:

clang: error: unsupported option '-fPIC' for target 'x86_64-w64-windows-gnu'

Quickstart example is wrong

The change below (15 -> 50) has resulted in the formal check to FAIL.

https://github.com/YosysHQ/SymbiYosys/blob/07d124084cc0ab394b20de4a820a81bc0597b894/docs/examples/quickstart/demo.sv#L8

However, the current quickstart manual still states that you should get a formal PASS.

Tom

Multiple files per line in the files section

I just tried placing two files per line in the files section and was surprised that symbiyosys tried to copy the first file onto the second. This created files in my filesystem outside of the SymbiYosys directory that I wasn't expecting. Under some circumstances, this might even overwrite information (it didn't for me, but I can see how it might).

Request SymbiYosys use white space to delimit files in this section, rather than just lines, or at least detect when more than one item is on a line and issue an error.

Link cover statement to a particular trace

When you have many cover statements in a single file, you get the same amount of cover traces.

Is there a way to identify which cover statement is linked to which trace?

I'm looking for something that might look like this:

   my_cover: cover(....)

This would result in a trace_my_cover.vcd.

Dockerfile for SymbiYosis

I've cobbled together a Dockerfile setup that I intend to use for testing out SymbiYosis based on: https://symbiyosys.readthedocs.io/en/latest/quickstart.html#prerequisites

Would it be an idea to clean it up a bit and add it to SymbiYosis master branch?

symbiyosis.zip

Add support for dumping input files

Like --dumpcfg but dumping just the preprocessed [files] section.

Yosys+Verific ignores initial RAM/array values

See included mcve file.

mcve.zip

Within it, two registers, qr[1:0], are set to zero via an initial statement. They are then asserted to be zero on the initial clock. The assertion fails when it should not.

Unique to this situation is the fact that qr is defined as a two-item memory, even though they are more likely to be implemented as a pair of registers.

Dan

Warm up fails, SymbiYosys says the trace exists when it doesn't

I have a design whose warmup fails. SymbiYosys declares that the counter example trace is placed into engine_0/trace.vcd. However, since this is a warmup failure, there is no trace.

Expected behavior: SymbiYosys should say nothing about a trace, or rather say that the trace does not exist because this is a warmup failure.

SymbiYosys directory available upon request.

super_prove binary for Ubuntu 16.04

Couldn't find a super_prove binary for Ubuntu 16.04 in https://downloads.bvsrc.org/super_prove/. Please add if possible.

Unexpected behavior with tasks

Problem: If an .sby file references an undefined task, the commands associated with that task are executed by default

Example SymbiYosys script:

[tasks]
A
[script]
A: do_something_one
B: do_something_two

Expected behavior: Undefined task references should create an error, or at least not be executed.

Example file attached.
broken-ex.txt
In this example file, the chparam command line for the undefined task, ck3_r2, is executed. While not defining the task in the script, I wasn't expecting yosys to implement the commands within it.

Dan

ERROR: syntax error, unexpected TOK_ID, expecting '.'

I'm trying to elaborate https://github.com/ispras/hdl-benchmarks/blob/master/hdl/texas97/PPC60X_bus/src/cpu.v module. The module contains the following code:

module	cpu(	.clk(clk),
		.BR_(BR_),
		.BG_(BG_),
		.ABB_(ABB_),
		.ABB1_(ABB1_),
		.TS_(TS_),
		.TS1_(TS1_),
		.AP(AP),
		.APE_(APE_),
		.TT(TT),
		.TT1(TT1),
		.TSIZ(TSIZ),
		.TBST_(TBST_),
		.TBST1_(TBST1_),
		.TC(TC),
		.CI_(CI_),
		.WT_(WT_),
		.GBL_(GBL_),
		.GBL1_(GBL1_),
		.AACK_(AACK_),
		.ARTRY_(ARTRY_),
		.ARTRY1_(ARTRY1_),
		.SHD_(SHD_),
		.DBG_(DBG_),
		.DBB_(DBB_),
		.DBB1_(DBB1_),
		.DP(DP),
		.DPE_(DPE_),
		.TA_(TA_),
		.DRTRY_(DRTRY_));

that causes the following error log:

$ sby -f cpu.sby 
SBY 15:12:35 [cpu] Removing directory 'cpu'.
SBY 15:12:35 [cpu] Copy '/home/user/hdl-benchmarks/hdl/texas97/PPC60X_bus/src/cpu.v' to 'cpu/src/cpu.v'.
SBY 15:12:35 [cpu] engine_0: smtbmc
SBY 15:12:35 [cpu] base: starting process "cd cpu/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 15:12:35 [cpu] base: /home/user/hdl-benchmarks/hdl/texas97/PPC60X_bus/src/cpu.v:41: ERROR: syntax error, unexpected TOK_ID, expecting '.'
SBY 15:12:35 [cpu] base: finished (returncode=1)
SBY 15:12:35 [cpu] base: job failed. ERROR.
SBY 15:12:35 [cpu] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:12:35 [cpu] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 15:12:35 [cpu] DONE (ERROR, rc=16)

Here is my SBY file:

[options]
mode bmc
depth 100

[engines]
smtbmc

[script]
read -formal /home/user/hdl-benchmarks/hdl/texas97/PPC60X_bus/src/cpu.v
prep -top cpu

[files]
/home/user/hdl-benchmarks/hdl/texas97/PPC60X_bus/src/cpu.v

The cpu.v module is instantiated at https://github.com/ispras/hdl-benchmarks/blob/master/hdl/texas97/PPC60X_bus/src/main1.v module. I've tried to add this module to SBY file, but it didn't help.
Any ideas on how to successfully parse this module with SymbiYosys?

Some engines cause SymbiYosys to crash

See the example at http://zipcpu.com/tmp/ybug9.tgz.

The example consists of a proof that two LFSRs, a Galois and a Fibonacci one, are equivalent.

smtbmc comes up with an inconclusive answer, abc pdr passes. These are understandable results.

However, aig avy and aig suprove both result in crashes.

Dan

installing error SymbiYosys

hello,
Getting a following error while installing SymbiYosys:

please help me.

initial assumptions do not work as expected

Consider the following cover test:

module tst(i_clk, i_reset, o_output);
    input wire i_clk, i_reset;
    output reg[2:0] o_output;

    initial o_output = 1;
    always @(posedge i_clk)
    if (i_reset)
        o_output <= 0;
    else
        o_output <= o_output + 1'b1;

    initial assume(i_reset);
    always @(*)
        cover(&o_output);
endmodule

Actual Behavior

On the first clock, i_reset is false and o_output is one. o_output increments from there, and i_reset is never raised.

Expected Behavior

i_reset should be asserted on the first clock step, and o_output should then be zero on the next.

Steps to reproduce

The symbiyosys script is fairly unremarkable: mode cover, engine smtbmc, read -formal tst.sv, prep -top tst, etc.

Dan

Unsupported cell type error caused by simple always block with 2 registers

When I add a always block with 2 register assignments to my test bench code, I get an error about unsupported cell type during generation of SMT output.

The code looks like this:

reg [15:0] last_opc;
reg [15:0] last_len;

  always @(posedge ClkSyst_i) begin
    if (HostIfValid_i && HostIfStart_i && !HostIfStop_i) begin
      last_opc <= HostIfData_i[15:4];
      last_len <= HostIfData_i[31:16];
    end
  end

The error I get looks like this:

...
SBY 15:42:37 [symbiyosys] base: finished (returncode=0)
SBY 15:42:37 [symbiyosys] smt2: starting process "cd symbiyosys/model; yosys -ql design_smt2.log design_smt2.ys"
SBY 15:42:37 [symbiyosys] smt2: -- (c) Copyright 1999 - 2018 Verific Design Automation Inc. All rights reserved
SBY 15:42:37 [symbiyosys] smt2: -- Compilation time was Tue Sep  4 22:13:47 2018
SBY 15:42:37 [symbiyosys] smt2: -- This program will expire on Thu Dec 13 21:13:47 2018
SBY 15:42:37 [symbiyosys] smt2: ERROR: Unsupported cell type $_DFFE_PP_ for cell HostRegisterFileF.$auto$simplemap.cc:442:simplemap_dffe$2980.
SBY 15:42:37 [symbiyosys] smt2: finished (returncode=1)
SBY 15:42:37 [symbiyosys] smt2: job failed. ERROR.

If I remove the assignment of one of the two registers, no error occurs.

The test bench looks like this:

module HostRegisterFileF (
  // global
  input        ClkSyst_i,
  input        ResetN_i,
  // VAI req
  input [63:0] HostIfData_i,
  input        HostIfStart_i,
  input        HostIfStop_i,
  input        HostIfValid_i,
  output       HostIfAccept_o,
  // VAI ack
  output [63:0] HostIfData_o,
  output        HostIfStart_o,
  output        HostIfStop_o,
  output        HostIfValid_o,
  input         HostIfAccept_i
);


  `define COUNTER_NUMBER 16

  HostRegisterFileE #(.G_COUNTER_NUMBER(`COUNTER_NUMBER)) i_HostRegisterFileE (
    .ClkSyst_i(ClkSyst_i),
    .ResetN_i(ResetN_i),
    .HostIfData_i(HostIfData_i),
    .HostIfStart_i(HostIfStart_i),
    .HostIfStop_i(HostIfStop_i),
    .HostIfValid_i(HostIfValid_i),
    .HostIfAccept_o(HostIfAccept_o),
    .HostIfData_o(HostIfData_o),
    .HostIfStart_o(HostIfStart_o),
    .HostIfStop_o(HostIfStop_o),
    .HostIfValid_o(HostIfValid_o),
    .HostIfAccept_i(HostIfAccept_i)
  );


  // Constrain reset

  reg init_flag = 1;
  (* gclk *) wire gbl_clk;

  always @(*) begin
    if (init_flag) assume (!ResetN_i);
    if (!init_flag) assume (ResetN_i);
  end

  always @(posedge ClkSyst_i)
    init_flag <= 0;

  global clocking
    @(posedge gbl_clk);
  endclocking

  always @($global_clock) begin
    assume (ClkSyst_i != $past(ClkSyst_i));
  end


  reg [15:4] last_opc;
  reg [15:0] last_len;

  always @(posedge ClkSyst_i) begin
    if (HostIfValid_i && HostIfStart_i && !HostIfStop_i) begin
      last_opc <= HostIfData_i[15:4];
      last_len <= HostIfData_i[31:16];
    end
  end

  assert property (@(posedge ClkSyst_i)
    disable iff (!ResetN_i)
      HostIfValid_o && HostIfStop_o && last_opc[11:4] == 8'b10 && last_len == 0 |->
      HostIfData_o[31:16] == 8
  );


  assert property (@(posedge ClkSyst_i)
    disable iff (!ResetN_i)
      HostIfValid_o && HostIfStop_o && last_opc[11:4] == 8'b11 && last_len == 0 |->
      HostIfData_o[31:16] == `COUNTER_NUMBER*8
  );


endmodule

My SymbiYosys script file:

[options]
mode bmc
#mode prove
depth 20
#multiclock on

[engines]
smtbmc
#abc pdr

[script]
verific -work BootFpga -vhdl DefinesP.vhd
verific -work Crc16    -vhdl Crc16MappingsP.vhd
verific -work Crc16    -vhdl Crc16P.vhd
verific -work Crc16    -vhdl Crc16Gen64E.vhd
verific -work work     -vhdl HostRegisterFileE.vhd
verific -sv HostRegisterFileF.sv
#prep -top HostRegisterFileF
hierarchy -check -top HostRegisterFileF
proc; opt
check
wreduce
alumacc
fsm
memory -nomap
memory_map
#techmap
dff2dffe
techmap -map +/adff2dff.v
hierarchy -check -top HostRegisterFileF
stat
check
synth -top HostRegisterFileF

[files]
HostRegisterFileE.vhd  
HostRegisterFileF.sv

I don't use the prep command because this results in another similar error, but with another FF type sourced by the DUT code. With the dff2dffe & techmap -map +/adff2dff.v I was able to workaround that.

At the moment I can't share the DUT code, because is it confidential and I believe it isn't the source of this particular problem.

UPDATE:

The problem can be workaround with addition of a reset to the always block:

reg [15:0] last_opc;
reg [15:0] last_len;

  always @(posedge ClkSyst_i or negedge Reset_n_i) begin
    if (!Reset_n_i) begin
      last_opc <= 0;
      last_len <= 0;
    else if (HostIfValid_i && HostIfStart_i && !HostIfStop_i) begin
      last_opc <= HostIfData_i[15:4];
      last_len <= HostIfData_i[31:16];
    end
  end

SymbiYosys gives no warning or error if no engines are specified

I just built an SBY file (without specifying an engine) and ran SymbiYosys. SymbiYosys returned quickly, with an "UNKNOWN" status code, but neither error nor warning to let me know that I hadn't placed an engine into the .sby file. There was no model directory, or any hidden status file (that I could find) telling me that having no engine was a problem.

When I added an engines section, specifying my favorite engine (smtbmc boolector), SymbiYosys then worked as expected.

Dan

Create VCD upon pass

Is it possible to write the vcd even if the design passes? Have not found any help on that. Thanks

SymbiYosys crashes while generating a cover trace

I'm not quite sure what's causing this, but my best guess is that a recent yosys upgrade, perhaps to create better names, is now causing SymbiYosys to crash when it tries to generate VCD files.

See the attached SymbiYosys directory, and logfile within it

wbxbar_cvr1x3_buf.zip

Feature request: One VCD file on error

Current behavior

When BMC fails, a VCD waveform is left in *task/engines?/trace.vcd

When Induction fails, a VCD waveform is left in *task/engines?/trace_induct.vcd

When viewing a VCD trace for a BMC failure, and the design passes BMC, GTKWave struggles with a none-existent trace. Likewise when viewing a VCD trace for an induction failure and you get a BMC failure, GTKWave struggles again with the absence of the open VCD file.

Suggested feature

Upon completion of any induction pass with an UNKNOWN result, copy (not move) the induction trace to where the BMC trace would be. That way you only ever need to keep one GTKWave window open.

Invalid command async2sync added to yosys script

I am running the following SymbiYosys script, but encounter an error when yosys parses the resulting command file:

[options]
mode bmc
depth 20
append 2

[engines]
smtbmc

[script]
verilog_defaults -add -sv -formal
read_verilog -DALU_TOP hdl/alu.sv
prep -flatten -top alu

Error:

Building: finished in 0.0 sec (100%) 5/5 jobs, 0 updated
  Total time: 0.2 sec
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] Removing direcory '/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu'.
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] Writing '/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu/src/hdl/alu.sv'.
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] engine_0: smtbmc
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] base: starting process "cd /Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu/src; /Users/arjen/dev/snes-toolchain/bin/yosys -ql ../model/design.log ../model/design.ys"
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] base: ERROR: No such command: async2sync (type 'help' for a command overview)
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] base: finished (returncode=1)
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] base: job failed. ERROR.
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 21:23:41 [/Users/arjen/dev/risc-v/buck-out/gen/hdl/verification/alu.sby/alu] DONE (ERROR, rc=16)

Looking at syb_core.py:290, it seems that command is added because multiclock is off by default. Enabling multiclock makes the yosys script run to completion. I am running tip of master for both SymbiYosys and Yosys and could obviously hack around this, but I am not sure what is correct here.

Oh and thank you for these amazing tools!

Run `sby` from `cmd.exe` and `powershell.exe` command line

At present, the sby script can only be run from sh prompts on any *nix-like or Windows. On Windows, it is still quite normal for various reasons to only have cmd.exe or powershell.exe available as a shell.

The problem is that cmd.exe/powershell.exe are sensitive to file extension as to whether it will execute a script. Changing the script extension to .py is unergonomic because it will create another console window just to run the python script (not to mention the script exits immediately in the open console without waiting).

setuptools normally handles this by installing a stub with the same name as the python script you wish to execute. This exe examines argv[0], and then spawns a python interpreter with $VALUE_OF_ARGV0.py as an input argument. The source code to that stub is provided in the setuptools repo. Piping, running from Makefiles, etc works as you expect in these cases.

I imagine you have a good reason for not wanting to use setuptools. Would you accept a patch to provide/install a precompiled launcher binary manually for Windows users without a native sh impl?

EDIT: yosys-smtbmc will also need this same treatment, since sby eventually calls yosys-smtbmc without an extension as well.

Cannot run demo example from docs - ERROR: No such command: memory_nordff

When running the example from :
First step: A simple BMC example

I get an error message from SBY

$ sby demo.sby
SBY 12:32:24 [demo] Copy 'demo.v' to 'demo/src/demo.v'.
SBY 12:32:24 [demo] engine_0: smtbmc
SBY 12:32:24 [demo] base: starting process "cd demo/src; yosys -ql ../model/design.log ../model/design.ys"
SBY 12:32:24 [demo] base: ERROR: No such command: memory_nordff (type 'help' for a command overview)
SBY 12:32:24 [demo] base: finished (returncode=1)
SBY 12:32:24 [demo] base: job failed. ERROR.
SBY 12:32:24 [demo] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 12:32:24 [demo] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 12:32:24 [demo] DONE (ERROR, rc=16)

I have Yosys, SymbiYosys and Yices 2 installed, I tried changing the solver, the error remains the same.
Do you have any insight ? (Running Ubuntu 16.04, followed the installation instructions from the SymbiYosys docs).

Thank you.

SymbiYosys attempts to use engines not specified in project

Expected behavior

SymbiYosys attempts to use engines specified in .sby file

Actual behavior

If engine specified in .sby fails to find solution, SymbiYosys attempts to use other engines

Replication instructions:

1. Unzip symbiyosys.zip
2. Remove all engines from the path
3. Specifing only yosys and abc, invoke good.sby:

sby --yosys $PATH_TO_YOSYS --abc $PATH_TO_ABC good.sby

Should complete successfully
4. Specifying only yosys and abc, invoke bad.sby:

sby --yosys $PATH_TO_YOSYS --abc $PATH_TO_ABC good.sby

sby will first invoke abc as expected, but after failing it will attempt to find smtbmc, etc, etc.

Support Scripting sby Jobs

Hi Clifford,

I'd like to be able to call SymbiYosys from FuseSoC as a backend. My rationale is that I already have all my Verilog files and whatnot enumerated in the FuseSoC cores file, and I don't want to duplicate that information in an sby file as well.

As a first step to that, I need to be able to script an sby job. While I can do this by creating a temporary sby file, it would be a lot cleaner if I could either pass my temporary file directly to sby on stdin, or if I could import the sby module into a Python script. Both would require some refactoring.

Would you be willing to accept a patch for either or both of these features? Or do you have a different vision for what scripting should look like? I have a proof of concept of the stdin option already, as that's the much easier path.

Feature request: dummy mode

I'd like to propose an additional mode (e.g. mode none) to define dummy tasks, which perform no action.

I have the following use case:
In my project I use a Makefile flow to run SymbiYosys verification tasks on several submodules. The engine selection and parameters for each task is kept in a set of .sby files. In some cases (for example if a prove or live run will not yield any results) I would like to skip certain verification steps without terminating the Makefile recipe. In these cases it would be useful to be able to set the verification mode to "none".

I've added three lines to sby_core.py to implement this dummy mode in my local setup. If you'd like I can submit this as a pull request.

fib liveness example non functional

I have been experimenting with some liveness proofs and have resorted to running the "fib" example presented in many slide presentations for symbiyosys:

module fib(
    input clk, pause, start,
    input [3:0] n,
    output reg busy, done,
    output reg [9:0] f
);

reg [3:0] count;
reg [9:0] q;

initial begin
    done = 0;
    busy = 0;
end

always @(posedge clk) begin
    done <= 0;
    if (!pause) begin
        if (!busy) begin
            if (start) busy <= 1;
            count <= 0;
            q <= 1;
            f <= 0;
        end
        else begin
            q <= f;
            f <= f + q;
            count <= count + 1;
            if (count == n) begin
                busy <= 0;
                done <= 1;
            end
        end
    end
end

`ifdef FORMAL
    always @(posedge clk) begin
        if (busy) begin
            assume (!start); assume ($stable(n));
        end
        if (done) begin
            case ($past(n))
                0: assert (f == 1);
                1: assert (f == 1);
                2: assert (f == 2);
                3: assert (f == 3);
                4: assert (f == 5);
                //5: assert (f == 8);
                5: assert (f == 300);               // prove fail
            endcase
            cover (f == 13);
            cover (f == 144);
            cover ($past(n) == 15); end
            assume (s_eventually !pause);
            if (start && !pause) assert (s_eventually done);
        end
`endif

endmodule

where the script is:

[options]
#mode prove
mode live

[engines]
aiger suprove

[script]
read -formal fib.v
prep -top fib

[files]
fib.v

when running the proof as presented, I get the following tool response which is not expected:

$ sby -f fib.sby
SBY 13:22:26 [fib] Removing direcory 'fib'.
SBY 13:22:26 [fib] Copy 'fib.v' to 'fib/src/fib.v'.
SBY 13:22:26 [fib] engine_0: aiger suprove
SBY 13:22:26 [fib] nomem: starting process "cd fib/src; yosys -ql ../model/design_nomem.log ../model/design_nomem.ys"
SBY 13:22:26 [fib] nomem: finished (returncode=0)
SBY 13:22:26 [fib] aig: starting process "cd fib/model; yosys -ql design_aiger.log design_aiger.ys"
SBY 13:22:27 [fib] aig: finished (returncode=0)
SBY 13:22:27 [fib] engine_0: starting process "cd fib; suprove +simple_liveness model/design_aiger.aig"
SBY 13:22:27 [fib] engine_0: finished (returncode=0)
SBY 13:22:27 [fib] engine_0: Status returned by engine: FAIL
SBY 13:22:27 [fib] engine_0: Engine did not produce a counter example.
SBY 13:22:27 [fib] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 13:22:27 [fib] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY 13:22:27 [fib] summary: engine_0 (aiger suprove) returned FAIL
SBY 13:22:27 [fib] DONE (FAIL, rc=2)

I would have expected a pass (?) with the example as delivered.
I have run other proofs with other engines (such as "prove and cove" with yices.
Both generate outputs from the tool as expected for this example.

Should this example demonstrate the liveness proof success/pass as written?