diff options
Diffstat (limited to 'examples')
39 files changed, 394 insertions, 59 deletions
diff --git a/examples/anlogic/.gitignore b/examples/anlogic/.gitignore new file mode 100644 index 000000000..97c978a15 --- /dev/null +++ b/examples/anlogic/.gitignore @@ -0,0 +1,7 @@ +demo.bit +demo_phy.area +full.v +*.log +*.h +*.tde +*.svf diff --git a/examples/anlogic/README b/examples/anlogic/README new file mode 100644 index 000000000..35d8e9cb1 --- /dev/null +++ b/examples/anlogic/README @@ -0,0 +1,12 @@ +LED Blink project for Anlogic Lichee Tang board. + +Follow the install instructions for the Tang Dynasty IDE from given link below. + +https://tang.sipeed.com/en/getting-started/installing-td-ide/linux/ + + +set TD_HOME env variable to the full path to the TD <TD Install Directory> as follow. + +export TD_HOME=<TD Install Directory> + +then run "bash build.sh" in this directory. diff --git a/examples/anlogic/build.sh b/examples/anlogic/build.sh new file mode 100755 index 000000000..e0f6b4cfe --- /dev/null +++ b/examples/anlogic/build.sh @@ -0,0 +1,4 @@ +#!/bin/bash +set -ex +yosys demo.ys +$TD_HOME/bin/td build.tcl diff --git a/examples/anlogic/build.tcl b/examples/anlogic/build.tcl new file mode 100644 index 000000000..06db525c9 --- /dev/null +++ b/examples/anlogic/build.tcl @@ -0,0 +1,11 @@ +import_device eagle_s20.db -package BG256 +read_verilog full.v -top demo +read_adc demo.adc +optimize_rtl +map_macro +map +pack +place +route +report_area -io_info -file demo_phy.area +bitgen -bit demo.bit -version 0X0000 -svf demo.svf -svf_comment_on -g ucode:00000000000000000000000000000000 diff --git a/examples/anlogic/demo.adc b/examples/anlogic/demo.adc new file mode 100644 index 000000000..ec802502e --- /dev/null +++ b/examples/anlogic/demo.adc @@ -0,0 +1,2 @@ +set_pin_assignment {CLK_IN} { LOCATION = K14; } ##24MHZ +set_pin_assignment {R_LED} { LOCATION = R3; } ##R_LED diff --git a/examples/anlogic/demo.v b/examples/anlogic/demo.v new file mode 100644 index 000000000..e17db771e --- /dev/null +++ b/examples/anlogic/demo.v @@ -0,0 +1,18 @@ +module demo ( + input wire CLK_IN, + output wire R_LED +); + parameter time1 = 30'd12_000_000; + reg led_state; + reg [29:0] count; + + always @(posedge CLK_IN)begin + if(count == time1)begin + count<= 30'd0; + led_state <= ~led_state; + end + else + count <= count + 1'b1; + end + assign R_LED = led_state; +endmodule diff --git a/examples/anlogic/demo.ys b/examples/anlogic/demo.ys new file mode 100644 index 000000000..cb396cc2b --- /dev/null +++ b/examples/anlogic/demo.ys @@ -0,0 +1,3 @@ +read_verilog demo.v +synth_anlogic -top demo +write_verilog full.v diff --git a/examples/basys3/example.xdc b/examples/basys3/example.xdc index c1fd0e925..8cdaa1996 100644 --- a/examples/basys3/example.xdc +++ b/examples/basys3/example.xdc @@ -19,3 +19,6 @@ set_property -dict { IOSTANDARD LVCMOS33 PACKAGE_PIN L1 } [get_ports {LD[15]}] create_clock -add -name sys_clk_pin -period 10.00 -waveform {0 5} [get_ports CLK] +set_property CONFIG_VOLTAGE 3.3 [current_design] +set_property CFGBVS VCCO [current_design] + diff --git a/examples/basys3/run_prog.tcl b/examples/basys3/run_prog.tcl index d711af840..b078ad511 100644 --- a/examples/basys3/run_prog.tcl +++ b/examples/basys3/run_prog.tcl @@ -1,3 +1,4 @@ +open_hw connect_hw_server open_hw_target [lindex [get_hw_targets] 0] set_property PROGRAM.FILE example.bit [lindex [get_hw_devices] 0] diff --git a/examples/cmos/counter.ys b/examples/cmos/counter.ys index a784f3465..d0b093667 100644 --- a/examples/cmos/counter.ys +++ b/examples/cmos/counter.ys @@ -1,11 +1,12 @@ - read_verilog counter.v read_verilog -lib cmos_cells.v -proc;; memory;; techmap;; - +synth dfflibmap -liberty cmos_cells.lib -abc -liberty cmos_cells.lib;; +abc -liberty cmos_cells.lib +opt_clean + +stat -liberty cmos_cells.lib # http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/latest/cadence/lib/tsmc025/signalstorm/osu025_stdcells.lib # dfflibmap -liberty osu025_stdcells.lib @@ -13,4 +14,3 @@ abc -liberty cmos_cells.lib;; write_verilog synth.v write_spice synth.sp - diff --git a/examples/cxx-api/evaldemo.cc b/examples/cxx-api/evaldemo.cc index e5cc8d8e7..34373487d 100644 --- a/examples/cxx-api/evaldemo.cc +++ b/examples/cxx-api/evaldemo.cc @@ -22,7 +22,7 @@ struct EvalDemoPass : public Pass { EvalDemoPass() : Pass("evaldemo") { } - virtual void execute(vector<string>, Design *design) + void execute(vector<string>, Design *design) YS_OVERRIDE { Module *module = design->top_module(); diff --git a/examples/gowin/demo.cst b/examples/gowin/demo.cst index 22d7eb668..c8f89dcf8 100644 --- a/examples/gowin/demo.cst +++ b/examples/gowin/demo.cst @@ -1,41 +1,10 @@ -// 50 MHz Clock -IO_LOC "clk" D11; - -// LEDs -IO_LOC "leds[0]" D22; -IO_LOC "leds[1]" E22; -IO_LOC "leds[2]" G22; -IO_LOC "leds[3]" J22; -IO_LOC "leds[4]" L22; -IO_LOC "leds[5]" L19; -IO_LOC "leds[6]" L20; -IO_LOC "leds[7]" M21; -IO_LOC "leds[8]" N19; -IO_LOC "leds[9]" R19; -IO_LOC "leds[10]" T18; -IO_LOC "leds[11]" AA22; -IO_LOC "leds[12]" U18; -IO_LOC "leds[13]" V20; -IO_LOC "leds[14]" AA21; -IO_LOC "leds[15]" AB21; - - -// 7-Segment Display -IO_LOC "seg7dig[0]" E20; -IO_LOC "seg7dig[1]" G18; -IO_LOC "seg7dig[2]" G20; -IO_LOC "seg7dig[3]" F21; -IO_LOC "seg7dig[4]" J20; -IO_LOC "seg7dig[5]" H21; -IO_LOC "seg7dig[6]" H18; -IO_LOC "seg7dig[7]" D20; -IO_LOC "seg7sel[0]" C19; -IO_LOC "seg7sel[1]" B22; -IO_LOC "seg7sel[2]" C20; -IO_LOC "seg7sel[3]" C21; - -// Switches -IO_LOC "sw[0]" AB20; -IO_LOC "sw[1]" AB19; -IO_LOC "sw[2]" AB18; -IO_LOC "sw[3]" AB17; +IO_LOC "clk" 35; +//IO_LOC "rst_n" 77; +IO_LOC "leds[0]" 79; +IO_LOC "leds[1]" 80; +IO_LOC "leds[2]" 81; +IO_LOC "leds[3]" 82; +IO_LOC "leds[4]" 83; +IO_LOC "leds[5]" 84; +IO_LOC "leds[6]" 85; +IO_LOC "leds[7]" 86;
\ No newline at end of file diff --git a/examples/gowin/demo.v b/examples/gowin/demo.v index 6ea108384..485fec97f 100644 --- a/examples/gowin/demo.v +++ b/examples/gowin/demo.v @@ -1,9 +1,7 @@ module demo ( input clk, - input [3:0] sw, output [15:0] leds, - output [7:0] seg7dig, - output [3:0] seg7sel + output unused ); localparam PRESCALE = 20; reg [PRESCALE+3:0] counter = 0; diff --git a/examples/gowin/device.cfg b/examples/gowin/device.cfg new file mode 100644 index 000000000..f6ab82159 --- /dev/null +++ b/examples/gowin/device.cfg @@ -0,0 +1,16 @@ +set JTAG regular_io = false +set SSPI regular_io = false +set MSPI regular_io = false +set READY regular_io = false +set DONE regular_io = false +set RECONFIG_N regular_io = false +set MODE regular_io = false +set CRC_check = true +set compress = false +set encryption = false +set security_bit_enable = true +set bsram_init_fuse_print = true +set download_speed = 250/100 +set spi_flash_address = 0x00FFF000 +set format = txt +set background_programming = false diff --git a/examples/gowin/pnr.cfg b/examples/gowin/pnr.cfg new file mode 100644 index 000000000..a1b43cc3b --- /dev/null +++ b/examples/gowin/pnr.cfg @@ -0,0 +1,8 @@ +-sdf +-oc +-ibs +-posp +-o +-warning_all +-tt +-timing diff --git a/examples/gowin/run.sh b/examples/gowin/run.sh index 33a7b5c37..cd260101e 100644 --- a/examples/gowin/run.sh +++ b/examples/gowin/run.sh @@ -1,8 +1,7 @@ #!/bin/bash set -ex yosys -p "synth_gowin -top demo -vout demo_syn.v" demo.v -$GOWIN_HOME/bin/gowin -d demo_syn.v -cst demo.cst -sdc demo.sdc -p GW2A55-PBGA484-6 \ - -warning_all -out demo_out.v -rpt demo.rpt -tr demo_tr.html -bit demo.bit +$GOWIN_HOME/bin/gowin -d demo_syn.v -cst demo.cst -sdc demo.sdc -p GW1NR-9-QFN88-6 -pn GW1NR-LV9QN88C6/I5 -cfg device.cfg -bit -tr -ph -timing -gpa -rpt -warning_all # post place&route simulation (icarus verilog) if false; then diff --git a/examples/gowin/run.tcl b/examples/gowin/run.tcl new file mode 100644 index 000000000..39da11cee --- /dev/null +++ b/examples/gowin/run.tcl @@ -0,0 +1,9 @@ +# gw_sh run.tcl +exec yosys -p "synth_gowin -top demo -vout demo_syn.v" demo.v +add_file -cst demo.cst +add_file -sdc demo.sdc +add_file -vm demo_syn.v +add_file -cfg device.cfg +set_option -device GW1NR-9-QFN88-6 +set_option -pn GW1NR-LV9QN88C6/I5 +run_pnr -opt pnr.cfg diff --git a/examples/igloo2/.gitignore b/examples/igloo2/.gitignore new file mode 100644 index 000000000..33b7182d3 --- /dev/null +++ b/examples/igloo2/.gitignore @@ -0,0 +1,4 @@ +/netlist.edn +/netlist.vm +/example.stp +/proj diff --git a/examples/igloo2/example.pdc b/examples/igloo2/example.pdc new file mode 100644 index 000000000..298d9e934 --- /dev/null +++ b/examples/igloo2/example.pdc @@ -0,0 +1,20 @@ +# Add placement constraints here + +set_io clk -pinname H16 -fixed yes -DIRECTION INPUT + +set_io SW1 -pinname H12 -fixed yes -DIRECTION INPUT +set_io SW2 -pinname H13 -fixed yes -DIRECTION INPUT + +set_io LED1 -pinname J16 -fixed yes -DIRECTION OUTPUT +set_io LED2 -pinname M16 -fixed yes -DIRECTION OUTPUT +set_io LED3 -pinname K16 -fixed yes -DIRECTION OUTPUT +set_io LED4 -pinname N16 -fixed yes -DIRECTION OUTPUT + +set_io AA -pinname L12 -fixed yes -DIRECTION OUTPUT +set_io AB -pinname L13 -fixed yes -DIRECTION OUTPUT +set_io AC -pinname M13 -fixed yes -DIRECTION OUTPUT +set_io AD -pinname N15 -fixed yes -DIRECTION OUTPUT +set_io AE -pinname L11 -fixed yes -DIRECTION OUTPUT +set_io AF -pinname L14 -fixed yes -DIRECTION OUTPUT +set_io AG -pinname N14 -fixed yes -DIRECTION OUTPUT +set_io CA -pinname M15 -fixed yes -DIRECTION OUTPUT diff --git a/examples/igloo2/example.sdc b/examples/igloo2/example.sdc new file mode 100644 index 000000000..f8b487316 --- /dev/null +++ b/examples/igloo2/example.sdc @@ -0,0 +1,2 @@ +# Add timing constraints here +create_clock -period 10.000 -waveform {0.000 5.000} [get_ports {clk}] diff --git a/examples/igloo2/example.v b/examples/igloo2/example.v new file mode 100644 index 000000000..4a9486e50 --- /dev/null +++ b/examples/igloo2/example.v @@ -0,0 +1,64 @@ +module example ( + input clk, + input SW1, + input SW2, + output LED1, + output LED2, + output LED3, + output LED4, + + output AA, AB, AC, AD, + output AE, AF, AG, CA +); + + localparam BITS = 8; + localparam LOG2DELAY = 22; + + reg [BITS+LOG2DELAY-1:0] counter = 0; + reg [BITS-1:0] outcnt; + + always @(posedge clk) begin + counter <= counter + SW1 + SW2 + 1; + outcnt <= counter >> LOG2DELAY; + end + + assign {LED1, LED2, LED3, LED4} = outcnt ^ (outcnt >> 1); + + // assign CA = counter[10]; + // seg7enc seg7encinst ( + // .seg({AA, AB, AC, AD, AE, AF, AG}), + // .dat(CA ? outcnt[3:0] : outcnt[7:4]) + // ); + + assign {AA, AB, AC, AD, AE, AF, AG} = ~(7'b 100_0000 >> outcnt[6:4]); + assign CA = outcnt[7]; +endmodule + +module seg7enc ( + input [3:0] dat, + output [6:0] seg +); + reg [6:0] seg_inv; + always @* begin + seg_inv = 0; + case (dat) + 4'h0: seg_inv = 7'b 0111111; + 4'h1: seg_inv = 7'b 0000110; + 4'h2: seg_inv = 7'b 1011011; + 4'h3: seg_inv = 7'b 1001111; + 4'h4: seg_inv = 7'b 1100110; + 4'h5: seg_inv = 7'b 1101101; + 4'h6: seg_inv = 7'b 1111101; + 4'h7: seg_inv = 7'b 0000111; + 4'h8: seg_inv = 7'b 1111111; + 4'h9: seg_inv = 7'b 1101111; + 4'hA: seg_inv = 7'b 1110111; + 4'hB: seg_inv = 7'b 1111100; + 4'hC: seg_inv = 7'b 0111001; + 4'hD: seg_inv = 7'b 1011110; + 4'hE: seg_inv = 7'b 1111001; + 4'hF: seg_inv = 7'b 1110001; + endcase + end + assign seg = ~seg_inv; +endmodule diff --git a/examples/igloo2/libero.tcl b/examples/igloo2/libero.tcl new file mode 100644 index 000000000..abc94e479 --- /dev/null +++ b/examples/igloo2/libero.tcl @@ -0,0 +1,57 @@ +# Run with "libero SCRIPT:libero.tcl" + +file delete -force proj + +new_project \ + -name example \ + -location proj \ + -block_mode 0 \ + -hdl "VERILOG" \ + -family IGLOO2 \ + -die PA4MGL2500 \ + -package vf256 \ + -speed -1 + +import_files -hdl_source {netlist.vm} +import_files -sdc {example.sdc} +import_files -io_pdc {example.pdc} +build_design_hierarchy +set_option -synth 0 + +organize_tool_files -tool PLACEROUTE \ + -file {proj/constraint/example.sdc} \ + -file {proj/constraint/io/example.pdc} \ + -input_type constraint + +organize_tool_files -tool VERIFYTIMING \ + -file {proj/constraint/example.sdc} \ + -input_type constraint + +configure_tool -name PLACEROUTE \ + -params TDPR:true \ + -params PDPR:false \ + -params EFFORT_LEVEL:false \ + -params REPAIR_MIN_DELAY:false + +puts "" +puts "**> COMPILE" +run_tool -name {COMPILE} +puts "<** COMPILE" + +puts "" +puts "**> PLACEROUTE" +run_tool -name {PLACEROUTE} +puts "<** PLACEROUTE" + +puts "" +puts "**> VERIFYTIMING" +run_tool -name {VERIFYTIMING} +puts "<** VERIFYTIMING" + +puts "" +puts "**> BITSTREAM" +export_bitstream_file -trusted_facility_file 1 -trusted_facility_file_components {FABRIC} +puts "<** BITSTREAM" + +puts "" +exit 0 diff --git a/examples/igloo2/runme.sh b/examples/igloo2/runme.sh new file mode 100644 index 000000000..a08894e0a --- /dev/null +++ b/examples/igloo2/runme.sh @@ -0,0 +1,6 @@ +#!/bin/bash +set -ex +yosys -p 'synth_sf2 -top example -edif netlist.edn -vlog netlist.vm' example.v +export LM_LICENSE_FILE=${LM_LICENSE_FILE:-1702@localhost} +/opt/microsemi/Libero_SoC_v12.0/Libero/bin/libero SCRIPT:libero.tcl +cp proj/designer/example/export/example.stp . diff --git a/examples/intel/DE2i-150/run_cycloneiv b/examples/intel/DE2i-150/run_cycloneiv index 321ed2778..518807b57 100644 --- a/examples/intel/DE2i-150/run_cycloneiv +++ b/examples/intel/DE2i-150/run_cycloneiv @@ -1,2 +1,2 @@ #/bin/env bash -yosys -p "synth_intel -family cycloneiv -top top -vout top.vqm" top.v sevenseg.v +yosys -p "synth_intel -family cycloneiv -top top -vqm top.vqm" top.v sevenseg.v diff --git a/examples/intel/MAX10/run_max10 b/examples/intel/MAX10/run_max10 index ef7649afb..0378e4fa7 100644 --- a/examples/intel/MAX10/run_max10 +++ b/examples/intel/MAX10/run_max10 @@ -1 +1 @@ -yosys -p "synth_intel -family max10 -top top -vout top.vqm" top.v sevenseg.v +yosys -p "synth_intel -family max10 -top top -vqm top.vqm" top.v sevenseg.v diff --git a/examples/intel/asicworld_lfsr/run_cycloneiv b/examples/intel/asicworld_lfsr/run_cycloneiv index cb7f5c9b1..c7498bded 100755 --- a/examples/intel/asicworld_lfsr/run_cycloneiv +++ b/examples/intel/asicworld_lfsr/run_cycloneiv @@ -1,2 +1,2 @@ #!/bin/env bash -yosys -p "synth_intel -family cycloneiv -top lfsr_updown -vout top.vqm" lfsr_updown.v +yosys -p "synth_intel -family cycloneiv -top lfsr_updown -vqm top.vqm" lfsr_updown.v diff --git a/examples/intel/asicworld_lfsr/run_max10 b/examples/intel/asicworld_lfsr/run_max10 index 6bb812c16..b75d552bb 100755 --- a/examples/intel/asicworld_lfsr/run_max10 +++ b/examples/intel/asicworld_lfsr/run_max10 @@ -1,2 +1,2 @@ #!/bin/env bash -yosys -p "synth_intel -family max10 -top lfsr_updown -vout top.vqm" lfsr_updown.v +yosys -p "synth_intel -family max10 -top lfsr_updown -vqm top.vqm" lfsr_updown.v diff --git a/examples/mimas2/README b/examples/mimas2/README new file mode 100644 index 000000000..b12875cbc --- /dev/null +++ b/examples/mimas2/README @@ -0,0 +1,8 @@ +A simple example design, based on the Numato Labs Mimas V2 board +================================================================ + +This example uses Yosys for synthesis and Xilinx ISE +for place&route and bit-stream creation. + +To synthesize: + bash run.sh diff --git a/examples/mimas2/example.ucf b/examples/mimas2/example.ucf new file mode 100644 index 000000000..4e31b74ab --- /dev/null +++ b/examples/mimas2/example.ucf @@ -0,0 +1,13 @@ +CONFIG VCCAUX = "3.3" ; + + +NET "CLK" LOC = D9 | IOSTANDARD = LVCMOS33 | PERIOD = 12MHz ; + +NET "LED[7]" LOC = P15 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[6]" LOC = P16 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[5]" LOC = N15 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[4]" LOC = N16 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[3]" LOC = U17 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[2]" LOC = U18 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[1]" LOC = T17 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; +NET "LED[0]" LOC = T18 | IOSTANDARD = LVCMOS33 | DRIVE = 8 | SLEW = SLOW ; diff --git a/examples/mimas2/example.v b/examples/mimas2/example.v new file mode 100644 index 000000000..2a9117393 --- /dev/null +++ b/examples/mimas2/example.v @@ -0,0 +1,14 @@ +module example( + input wire CLK, + output wire [7:0] LED +); + +reg [27:0] ctr; +initial ctr = 0; + +always @(posedge CLK) + ctr <= ctr + 1; + +assign LED = ctr[27:20]; + +endmodule diff --git a/examples/mimas2/run.sh b/examples/mimas2/run.sh new file mode 100644 index 000000000..aafde78ed --- /dev/null +++ b/examples/mimas2/run.sh @@ -0,0 +1,8 @@ +#!/bin/sh +set -e +yosys run_yosys.ys +edif2ngd example.edif +ngdbuild example -uc example.ucf -p xc6slx9csg324-3 +map -w example +par -w example.ncd example_par.ncd +bitgen -w example_par.ncd -g StartupClk:JTAGClk diff --git a/examples/mimas2/run_yosys.ys b/examples/mimas2/run_yosys.ys new file mode 100644 index 000000000..b48877811 --- /dev/null +++ b/examples/mimas2/run_yosys.ys @@ -0,0 +1,3 @@ +read_verilog example.v +synth_xilinx -top example -family xc6s -ise +write_edif -pvector bra example.edif diff --git a/examples/python-api/.gitignore b/examples/python-api/.gitignore new file mode 100644 index 000000000..758de1134 --- /dev/null +++ b/examples/python-api/.gitignore @@ -0,0 +1 @@ +out/** diff --git a/examples/python-api/pass.py b/examples/python-api/pass.py new file mode 100755 index 000000000..d67cf4a23 --- /dev/null +++ b/examples/python-api/pass.py @@ -0,0 +1,32 @@ +#!/usr/bin/python3 + +from pyosys import libyosys as ys + +import matplotlib.pyplot as plt +import numpy as np + +class CellStatsPass(ys.Pass): + + def __init__(self): + super().__init__("cell_stats", "Shows cell stats as plot") + + def py_help(self): + ys.log("This pass uses the matplotlib library to display cell stats\n") + + def py_execute(self, args, design): + ys.log_header(design, "Plotting cell stats\n") + cell_stats = {} + for module in design.selected_whole_modules_warn(): + for cell in module.selected_cells(): + if cell.type.str() in cell_stats: + cell_stats[cell.type.str()] += 1 + else: + cell_stats[cell.type.str()] = 1 + plt.bar(range(len(cell_stats)), height = list(cell_stats.values()),align='center') + plt.xticks(range(len(cell_stats)), list(cell_stats.keys())) + plt.show() + + def py_clear_flags(self): + ys.log("Clear Flags - CellStatsPass\n") + +p = CellStatsPass() diff --git a/examples/python-api/script.py b/examples/python-api/script.py new file mode 100755 index 000000000..f0fa5a0b8 --- /dev/null +++ b/examples/python-api/script.py @@ -0,0 +1,22 @@ +#!/usr/bin/python3 + +from pyosys import libyosys as ys + +import matplotlib.pyplot as plt +import numpy as np + +design = ys.Design() +ys.run_pass("read_verilog ../../tests/simple/fiedler-cooley.v", design); +ys.run_pass("prep", design) +ys.run_pass("opt -full", design) + +cell_stats = {} +for module in design.selected_whole_modules_warn(): + for cell in module.selected_cells(): + if cell.type.str() in cell_stats: + cell_stats[cell.type.str()] += 1 + else: + cell_stats[cell.type.str()] = 1 +plt.bar(range(len(cell_stats)), height = list(cell_stats.values()),align='center') +plt.xticks(range(len(cell_stats)), list(cell_stats.keys())) +plt.show() diff --git a/examples/smtbmc/.gitignore b/examples/smtbmc/.gitignore index a3f4f0f24..278f5ebf7 100644 --- a/examples/smtbmc/.gitignore +++ b/examples/smtbmc/.gitignore @@ -20,3 +20,5 @@ demo6.smt2 demo6.yslog demo7.smt2 demo7.yslog +demo8.smt2 +demo8.yslog diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile index 2f7060bda..96fa058d6 100644 --- a/examples/smtbmc/Makefile +++ b/examples/smtbmc/Makefile @@ -1,5 +1,5 @@ -all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 +all: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 demo1: demo1.smt2 yosys-smtbmc --dump-vcd demo1.vcd demo1.smt2 @@ -25,6 +25,9 @@ demo6: demo6.smt2 demo7: demo7.smt2 yosys-smtbmc -t 10 demo7.smt2 +demo8: demo8.smt2 + yosys-smtbmc -s z3 -t 1 -g demo8.smt2 + demo1.smt2: demo1.v yosys -ql demo1.yslog -p 'read_verilog -formal demo1.v; prep -top demo1 -nordff; write_smt2 -wires demo1.smt2' @@ -46,6 +49,9 @@ demo6.smt2: demo6.v demo7.smt2: demo7.v yosys -ql demo7.yslog -p 'read_verilog -formal demo7.v; prep -top demo7 -nordff; write_smt2 -wires demo7.smt2' +demo8.smt2: demo8.v + yosys -ql demo8.yslog -p 'read_verilog -formal demo8.v; prep -top demo8 -nordff; write_smt2 -stbv -wires demo8.smt2' + clean: rm -f demo1.yslog demo1.smt2 demo1.vcd rm -f demo2.yslog demo2.smt2 demo2.vcd demo2.smtc demo2_tb.v demo2_tb demo2_tb.vcd @@ -54,6 +60,7 @@ clean: rm -f demo5.yslog demo5.smt2 demo5.vcd rm -f demo6.yslog demo6.smt2 rm -f demo7.yslog demo7.smt2 + rm -f demo8.yslog demo8.smt2 -.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 clean +.PHONY: demo1 demo2 demo3 demo4 demo5 demo6 demo7 demo8 clean diff --git a/examples/smtbmc/demo2.v b/examples/smtbmc/demo2.v index 34745e898..0cf529a42 100644 --- a/examples/smtbmc/demo2.v +++ b/examples/smtbmc/demo2.v @@ -9,7 +9,7 @@ module demo2(input clk, input [4:0] addr, output reg [31:0] data); reg [31:0] mem [0:31]; - always @(posedge clk) + always @(negedge clk) data <= mem[addr]; reg [31:0] used_addr = 0; diff --git a/examples/smtbmc/demo8.v b/examples/smtbmc/demo8.v new file mode 100644 index 000000000..c4c396cde --- /dev/null +++ b/examples/smtbmc/demo8.v @@ -0,0 +1,12 @@ +// Simple exists-forall demo + +module demo8; + wire [7:0] prime = $anyconst; + wire [3:0] factor = $allconst; + + always @* begin + if (1 < factor && factor < prime) + assume((prime % factor) != 0); + assume(prime > 1); + end +endmodule |