riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
11,588 Commits 81 Branches 48 Tags 63 MiB
Commit Graph

309 Commits

Author SHA1 Message Date
Miodrag Milanovic e35a166353 verific: proper file location for readmem commands 2022-06-04 08:39:50 +02:00
Miodrag Milanovic fdb393b6ce fix text to fit 80 columns 2022-05-23 19:57:21 +02:00
Miodrag Milanovic 4a5790d404 Update verific command file documentation 2022-05-23 19:35:14 +02:00
Miodrag Milanovic a6ec5754c6 Use analysis mode if set in file 2022-05-23 19:13:45 +02:00
Jannis Harder fada77b8cf verific: Use new value change logic also for $stable of wide signals. 
I missed this in the previous PR.
 2022-05-11 13:05:27 +02:00
Jannis Harder 587e09d551
Merge pull request #3305 from jix/sva_value_change_logic 
verific: Improve logic generated for SVA value change expressions
 2022-05-09 16:40:34 +02:00
Jannis Harder a855d62b42 verific: Improve logic generated for SVA value change expressions 
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

	a) provides the expected behavior in a 2-valued logic setting, not
	   depending on any dont-care optimizations, and

	b) properly handles 'x values in yosys simulation
 2022-05-09 15:04:01 +02:00
Jannis Harder 96f64f4788 verific: Fix conditions of SVAs with explicit clocks within procedures 
For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
 2022-05-03 14:13:08 +02:00
Miodrag Milanovic 422db937d4 Ignore merging past ffs that we are not properly merging 2022-04-29 14:35:02 +02:00
Miodrag Milanovic 1cc281ca6f verific: allow memories to be inferred in loops (vhdl) 2022-04-18 09:10:28 +02:00
N. Engelhardt 57bc29c64a verific: allow memories to be inferred in loops 2022-04-15 15:10:48 +02:00
Miodrag Milanovic 1a1f529099 Preserve internal wires for external nets 2022-04-01 12:07:15 +02:00
Miodrag Milanovic bbf65702a1 Fix valgrind tests when using verific 2022-03-30 17:25:53 +02:00
Miodrag Milanovic 703769e494 Properly mark modules imported 2022-03-26 09:43:51 +01:00
Miodrag Milanovic 245ecb0529 Import verific netlist in consistent order 2022-03-25 13:44:16 +01:00
Miodrag Milanovic 29293a57bb Remove quotes if any from attribute 2022-02-16 19:10:13 +01:00
Miodrag Milanovic 2cef48bf2c Add ability to override verilog mode for verific -f command 2022-02-09 09:19:25 +01:00
Miodrag Milanovic 0b633b6c2e Use bmux for NTO1MUX 2022-02-02 16:16:08 +01:00
Claire Xenia Wolf 313340aed5 Add YOSYS to the implicitly defined verilog macros in verific 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-12-13 18:20:08 +01:00
Miodrag Milanović 2412497c26
Merge pull request #3102 from YosysHQ/claire/enumxz 
Fix verific import of enum values with x and/or z
 2021-12-10 19:36:37 +01:00
Claire Xenia Wolf 2da214d721 Fix verific import of enum values with x and/or z 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-12-10 14:52:27 +01:00
Claire Xen 19773d093f
Update verific.cc 
Ad-hoc fixes/improvements
 2021-12-10 14:27:18 +01:00
Miodrag Milanovic b06f547993 If direction NONE use that from first bit 2021-12-08 11:50:10 +01:00
Miodrag Milanovic 3ebfa3fb84 Make sure cell names are unique for wide operators 2021-12-03 09:49:05 +01:00
Miodrag Milanovic 15a35f5584 No need to alocate more memory than used 2021-11-10 10:50:44 +01:00
Claire Xenia Wolf 2ea757da51 Add "verific -cfg" command 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-11-01 10:41:51 +01:00
Claire Xenia Wolf 83118bfb9e Fix verific gclk handling for async-load FFs 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-31 17:12:29 +01:00
Miodrag Milanovic f7cc388bb5 Enable async load dff emit by default in Verific 2021-10-27 15:56:56 +02:00
Miodrag Milanovic 32673edfea Revert "Compile option for enabling async load verific support" 
This reverts commit b8624ad2ae.
 2021-10-27 15:55:43 +02:00
Miodrag Milanovic b8624ad2ae Compile option for enabling async load verific support 2021-10-25 09:04:43 +02:00
Claire Xenia Wolf 90b440f870 Fix verific.cc PRIM_DLATCH handling 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-21 12:13:35 +02:00
Claire Xenia Wolf 16a177560f Initial Verific impoter support for {PRIM,WIDE_OPER}_DLATCH{,RS} 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-21 05:42:47 +02:00
Miodrag Milanovic 17269ae59b Option to disable verific VHDL support 2021-10-20 10:02:58 +02:00
Miodrag Milanovic 1aa6896966 Support PRIM_BUFIF1 primitive 2021-10-14 13:04:32 +02:00
Claire Xen 2d3c79458d
Merge pull request #3039 from YosysHQ/claire/verific_aldff 
Add support for $aldff flip-flops to verific importer
 2021-10-11 10:01:56 +02:00
Claire Xenia Wolf c8074769b0 Add Verific adffe/dffsre/aldffe FIXMEs 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-11 10:00:20 +02:00
Miodrag Milanovic 93fbc9fba4 Import module attributes from Verific 2021-10-10 10:01:45 +02:00
Claire Xenia Wolf 34f1df8435 Fixes and add comments for open FIXME items 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-08 17:24:45 +02:00
Claire Xenia Wolf 1602a03864 Add support for $aldff flip-flops to verific importer 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
 2021-10-08 16:21:25 +02:00
Miodrag Milanovic abc5700628 verific set db_infer_set_reset_registers 2021-10-04 16:48:33 +02:00
Miodrag Milanovic c3d4bb4cc9 update required verific version 2021-09-02 14:59:16 +02:00
Miodrag Milanovic b59c427348 Make Verific extensions optional 2021-08-20 10:19:04 +02:00
Miodrag Milanovic be04d8834e Require latest verific 2021-08-02 10:29:58 +02:00
Miodrag Milanovic 987fca5297 Update to latest verific 2021-07-21 09:46:53 +02:00
Miodrag Milanovic 7a5ac90985 Update to latest Verific with extensions for initial assertions 2021-07-09 09:02:27 +02:00
Miodrag Milanovic 0dbb05a75e Add additional help 2021-07-05 09:16:54 +02:00
Miodrag Milanovic c0d8da20d5 Support command files in Verific 2021-06-16 11:21:44 +02:00
Claire Xenia Wolf 72787f52fc Fixing old e-mail addresses and deadnames 
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g;
 2021-06-08 00:39:36 +02:00
Claire Xen 6c56c083f8
Update README 2021-03-04 16:43:30 +01:00
Claire Xen 27d7741540
Merge pull request #2574 from dh73/master 
Accept disable case for SVA liveness properties.
 2021-02-15 17:49:11 +01:00