yosyshq / sby Goto Github PK
View Code? Open in Web Editor NEWSymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
License: Other
SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
License: Other
The change below (15 -> 50) has resulted in the formal check to FAIL.
However, the current quickstart manual still states that you should get a formal PASS.
Tom
We can harness the power of ArgParse (for parsing the arguments) and ConfigParser (for the sby file).
The benefit of argparse are:
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.
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.
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
Couldn't find a super_prove binary for Ubuntu 16.04 in https://downloads.bvsrc.org/super_prove/. Please add if possible.
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
SymbiYosys attempts to use engines specified in .sby file
If engine specified in .sby fails to find solution, SymbiYosys attempts to use other engines
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.
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
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
Like --dumpcfg
but dumping just the preprocessed [files]
section.
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.
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.
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?
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
.
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.
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!
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...
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
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'
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
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.
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.
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.
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
See the attached SBY-created directory.
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).
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.
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?
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.
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?
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.
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
See included mcve file.
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
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
This design should simply PASS.
Dan
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
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
Is it possible to write the vcd even if the design passes? Have not found any help on that. Thanks
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)
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
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.
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?
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.
Zip file contains an .sby, test bench, and design files (which include the driver/monitor)
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
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.
When using disable iff, SymbiYosys is sensitive to the clock after the assertion/assumption is to take place. Consider, for example, the following MCVE:
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
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?
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!
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
On the first clock, i_reset
is false and o_output
is one. o_output
increments from there, and i_reset
is never raised.
i_reset
should be asserted on the first clock step, and o_output
should then be zero on the next.
The symbiyosys script is fairly unremarkable: mode cover, engine smtbmc, read -formal tst.sv, prep -top tst, etc.
Dan
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?
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
This could simplify setups when referring to multiple IP repositories.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.