3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 01:24:10 +00:00
yosys/frontends/verific
Ethan Mahintorabi bc66dfd9ea
verific: Fixes incorrect aldff inference in verific importer
The following SV module at HEAD imported with verific,

```systemverilog
    module my_module(
      input logic [4:0] a,
      input logic clk,
      input logic enable,
      output logic [4:0] z
    );

    reg [4:0] pipeline_register;
    always @(posedge clk) begin
      pipeline_register <= enable ? a : pipeline_register;
    end
    assign z = pipeline_register;

    endmodule : my_module

```

results in the following output verilog

```systemverilog
/* Generated by 0.36 */

(* top =  1  *)
(* hdlname = "my_module" *)
(* src = "/tmp/temp_directory_zTwd0l/my_input.v:2.12-2.21" *)
module my_module(clk, enable, a, z);
  wire [4:0] _0_;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:3.25-3.26" *)
  input [4:0] a;
  wire [4:0] a;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:4.19-4.22" *)
  input clk;
  wire clk;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:5.19-5.25" *)
  input enable;
  wire enable;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:6.26-6.27" *)
  output [4:0] z;
  wire [4:0] z;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:10.12-12.8" *)
  \$aldff  #(
    .ALOAD_POLARITY(32'd1),
    .CLK_POLARITY(32'd1),
    .WIDTH(32'd5)
  ) _1_ (
    .AD(5'hxx),
    .ALOAD(1'h0),
    .CLK(clk),
    .D(_0_),
    .Q(z)
  );
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:11.28-11.58" *)
  \$mux  #(
    .WIDTH(32'd5)
  ) _2_ (
    .A(z),
    .B(a),
    .S(enable),
    .Y(_0_)
  );
endmodule
```

Yosys is incorrectly infering aldffs due to an incorrect conversion
of logical 1 and 0 SigBits.

My PR unifies the conversion of Verific::Net objects into SigBits using
Yosys' internal representation of special signals like 0,1,x,z. After
my PR these signals are correctly converted into DFFs.

Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-02-05 07:10:25 +00:00
..
example.sby Improve docs for verific bindings, add simply sby example 2017-07-22 11:58:51 +02:00
example.sv Improve docs for verific bindings, add simply sby example 2017-07-22 11:58:51 +02:00
Makefile.inc Option to disable verific VHDL support 2021-10-20 10:02:58 +02:00
README Update README 2022-07-28 12:32:19 +02:00
verific.cc verific: Fixes incorrect aldff inference in verific importer 2024-02-05 07:10:25 +00:00
verific.h verific: Fixes incorrect aldff inference in verific importer 2024-02-05 07:10:25 +00:00
verificsva.cc verific: Handle non-seq properties with VerificClocking conditions 2023-04-21 17:19:42 +02:00

This directory contains Verific bindings for Yosys.

Use Tabby CAD Suite from YosysHQ if you need Yosys+Verific.
https://www.yosyshq.com/

Contact YosysHQ at contact@yosyshq.com for free evaluation
binaries of Tabby CAD Suite.


Verific Features that should be enabled in your Verific library
===============================================================

database/DBCompileFlags.h:
	DB_PRESERVE_INITIAL_VALUE


Testing Verific+Yosys+SymbiYosys for formal verification
========================================================

Install Yosys+Verific, SymbiYosys, and Yices2. Install instructions:
http://symbiyosys.readthedocs.io/en/latest/quickstart.html#installing

Then run in the following command in this directory:

	sby -f example.sby

This will generate approximately one page of text output. The last lines
should be something like this:

	SBY [example] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
	SBY [example] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for basecase
	SBY [example] summary: engine_0 (smtbmc yices) returned PASS for induction
	SBY [example] summary: successful proof by k-induction.
	SBY [example] DONE (PASS, rc=0)