// SPDX-License-Identifier: Apache-2.0 ; specs/widgets/fsm-sketch.t27 -- the state machine yosys extracted from your RTL, drawn ; Source of truth for public/widgets/fsm-sketch/ (gHashTag/trinity, apps/website). The page is ; written by scripts/widget-pages-from-spec.mjs from this file; tool.js holds no English of its ; own and reads every word below from window.T27_WIDGET. ; ASCII only (L3), English only (LANG-EN). ; WHAT IT DOES: the reader drops the KISS2 file yosys `fsm_export` wrote, or drops or pastes the ; log of a yosys run that went through fsm_detect and fsm_info (any synth log does: its fsm pass ; runs both). public/widgets/fsm-sketch/fsmparse.js reads it in the browser: the registers ; fsm_detect took, the ones it named and refused with its reason, and for each FSM fsm_info ; dumped its inputs, state codes and transition table. The page says plainly what yosys ; extracted, counts states, transitions and inputs, and draws the graph as SVG: states on an ; ellipse in breadth-first order from the reset state, one curve per state pair labelled with the ; input patterns of its rows. No layout library; the file never leaves the page. ; THE SAMPLES: four real runs of Yosys 0.67+post (git sha1 b8e7da6f) on this machine, made by ; scripts/widget-data/fsm-sketch.mjs on three Verilog files of gHashTag/trinity, each copied to a ; scratch directory first. Each run is ; yosys -q -l .yosys.txt -p "read_verilog ; hierarchy -top ; proc; ; ; fsm_detect; fsm_extract; fsm_info; fsm_export -o .kiss2" ; with = "opt -nodffe -nosdff" (as yosys synth runs it) or, for the fourth, plain "opt". ; The logs and KISS2 files are shipped byte for byte under public/widgets/fsm-sketch/samples/; ; sample.json holds the commands, the yosys -V line, the sha256 of every input and output, and ; the layout card.png is drawn from. Every K_SAMPLE_ fact below is re-read from the shipped logs ; by `node scripts/widget-data/fsm-sketch.mjs --check`, which also runs this spec's tests on the ; values it read and a negative control that must fail them, and checks that each KISS2 file ; holds the same rows as the fsm_info table of its log. ; WHAT IT DOES NOT CLAIM: that a design with no extracted FSM has no state machine. fsm_detect ; takes only registers it recognises, and names only some of the ones it refuses: on fsm_simple.v, ; a three-state traffic light, it refuses next_state and says nothing about state. yosys calls the states s0 to sN; on the samples ; this page matches each code to the source's localparam values in its own script, and says so. ; The codes are the source's own until fsm_recode re-encodes them (one-hot, in a synth run); ; re-encoding changes the flip-flops, not the graph. ; phi^2 + 1/phi^2 = 3 | TRINITY module widget_fsm_sketch; pub const KIND : str = "widget-tool"; pub const ID : str = "fsm-sketch"; pub const TITLE : str = "FSM sketch: the state machine yosys found in your RTL"; pub const DESCRIPTION : str = "Drop a yosys fsm_export KISS2 file or paste the fsm_info log: the state diagram yosys extracted, its states, transitions and inputs, and the registers it refused."; pub const IMAGE_ALT : str = "FSM sketch card: the state diagram yosys 0.67 extracted from uart_rx.v, four states IDLE, START, DATA and STOP with 14 transitions on 4 inputs; beside it fsm_simple.v, a traffic light yosys refused because a register has an initial value, and uart_rx.v again with plain opt, where yosys found nothing and said nothing."; pub const HOOK : str = "Did yosys see your state machine? Drop its fsm_export file or log and see the graph it extracted, or the reason it refused."; pub const CATEGORY : str = "fpga"; pub const DATA_SOURCES : [5]str = ["Yosys 0.67+post (git sha1 b8e7da6f40ae8f552c116bf6c359b07c6533e159), run four times by scripts/widget-data/fsm-sketch.mjs: nice -n 10 yosys -q -l .yosys.txt -p \"read_verilog ; hierarchy -top ; proc; opt -nodffe -nosdff; fsm_detect; fsm_extract; fsm_info; fsm_export -o .kiss2\" (the fourth run: plain opt)", "gHashTag/trinity fpga/rtl/uart_rx.v, fpga/openxc7-synth/spi_flash_master.v and fpga/openxc7-synth/fsm_simple.v, copied to a scratch directory at their repo-relative paths; sha256 of each in sample.json", "public/widgets/fsm-sketch/samples/: the four yosys logs and the two KISS2 files, byte for byte; sample.json: commands, yosys -V line, exit codes, sha256 of inputs and outputs, localparam matches", "public/widgets/fsm-sketch/fsmparse.js: the one parser and layout, run in node for the samples and in the browser for your file; card.png is drawn from sample.json by scripts/widget-data/fsm-sketch-card.py", "node scripts/widget-data/fsm-sketch.mjs --check: re-reads the shipped logs and fails if any K_SAMPLE_ fact in this spec disagrees or a KISS2 file and its log differ"]; pub const READS_LOCAL_FILES : bool = true; pub const SENDS_NOTHING : bool = true; ; --- The samples: what was run ------------------------------------------------------------------- pub const K_SAMPLE_JSON : str = "sample.json"; pub const K_SAMPLE_DIR : str = "samples"; pub const K_SAMPLE_IDS : [4]str = ["uart-rx", "spi-flash", "fsm-simple", "uart-rx-plain-opt"]; pub const K_SAMPLE_DESIGNS : [4]str = ["fpga/rtl/uart_rx.v", "fpga/openxc7-synth/spi_flash_master.v", "fpga/openxc7-synth/fsm_simple.v", "fpga/rtl/uart_rx.v"]; pub const K_SAMPLE_TOPS : [4]str = ["uart_rx", "spi_flash_master", "fsm_simple", "uart_rx"]; pub const K_SAMPLE_OPTS : [4]str = ["opt -nodffe -nosdff", "opt -nodffe -nosdff", "opt -nodffe -nosdff", "opt"]; ; The sample the card shows. pub const K_CARD_SAMPLE : u8 = 0; ; --- The samples: what yosys said (re-read from the logs by fsm-sketch.mjs --check) --------------- pub const K_SAMPLE_YOSYS : str = "0.67+post"; pub const K_SAMPLE_FOUND : [4]u16 = [1, 1, 0, 0]; pub const K_SAMPLE_REJECTED : [4]u16 = [0, 0, 1, 0]; pub const K_SAMPLE_STATES : [4]u16 = [4, 7, 0, 0]; pub const K_SAMPLE_TRANSITIONS : [4]u16 = [14, 23, 0, 0]; pub const K_SAMPLE_INPUTS : [4]u16 = [4, 7, 0, 0]; pub const K_SAMPLE_REASON : str = "Register has an initialization value."; ; --- How it reads and draws ------------------------------------------------------------------------ ; A file or pasted text over this many characters is not read. pub const K_MAX_CHARS : u32 = 4000000; ; Above this many states the page lists the table and draws no graph. pub const K_MAX_DRAW_STATES : u8 = 40; ; Input patterns written on one edge before the rest fold into "+N more". pub const K_LABEL_ROWS : u8 = 3; pub const K_FONT_PX : u8 = 13; ; The diagram is laid out between these widths: scaled down on a narrow screen, centred on a wide one. pub const K_DIAGRAM_MIN_W : u16 = 460; pub const K_DIAGRAM_MAX_W : u16 = 780; pub const K_DIAGRAM_MAX_H : u16 = 600; ; Transition rows listed before "Show all". pub const K_TABLE_ROWS : u8 = 24; pub const K_MIN_TARGET_PX : u8 = 32; pub const K_CARD_W : u16 = 1200; pub const K_CARD_H : u16 = 630; ; The graph's box on the card, and its font. pub const K_CARD_GRAPH_W : u16 = 680; pub const K_CARD_GRAPH_H : u16 = 470; pub const K_CARD_FONT_PX : u8 = 19; ; --- Every word on the screen ---------------------------------------------------------------------- ; Templates take {0}, {1}, ... in order. pub const SAY_SAMPLE_LABEL : str = "Real yosys runs"; pub const SAY_SAMPLE_NAMES : [4]str = ["uart_rx: 4 states", "spi_flash_master: 7 states", "fsm_simple: refused", "uart_rx, plain opt: silent"]; pub const SAY_SAMPLE_LINES : [4]str = ["A UART receiver from gHashTag/trinity, fpga/rtl/uart_rx.v. yosys 0.67 took its state register and extracted all four states.", "The SPI flash reader in fpga/openxc7-synth/spi_flash_master.v: seven states, from chip select low to done.", "A three-state traffic light, fpga/openxc7-synth/fsm_simple.v, whose registers are declared with an initial value. yosys refused next_state for that reason and said nothing at all about state.", "The same uart_rx.v with plain opt where synth runs opt -nodffe -nosdff. opt folded the reset into the register first; fsm_detect then found nothing and printed nothing."]; pub const SAY_OPEN_LOG : str = "yosys log"; pub const SAY_OPEN_KISS2 : str = "KISS2 file"; pub const SAY_NAMES_NOTE : str = "Names after the state are this page's match of each code to a localparam in the source file, made by its script. yosys itself only says s0 to s{0}."; pub const SAY_OWN_LABEL : str = "Your design"; pub const SAY_HOW : str = "yosys -l fsm.txt -p \"read_verilog top.v; proc; opt -nodffe -nosdff; fsm_detect; fsm_extract; fsm_info; fsm_export -o fsm.kiss2\""; pub const SAY_HOW_LINE : str = "Drop fsm.txt (names, codes and refusals) or fsm.kiss2 (the graph only). The log of a synth or synth_xilinx run works too: its fsm pass prints the same lines, after re-encoding."; pub const SAY_DROP : str = "Drop a yosys log or a .kiss2 file here, or pick one"; pub const SAY_PASTE_HINT : str = "...or paste the yosys log or the KISS2 text"; pub const SAY_PASTE_LABEL : str = "yosys log or KISS2 text"; pub const SAY_READ : str = "Draw it"; pub const SAY_CLEAR : str = "Clear"; pub const SAY_PICKED : str = "{0}: {1} bytes"; pub const SAY_PASTED : str = "pasted text"; pub const SAY_LOCAL_NOTE : str = "Read in this tab; nothing is sent."; pub const SAY_TOO_BIG : str = "{0} characters is more than this page reads ({1})."; pub const SAY_ERR_READ : str = "Could not read {0}."; pub const SAY_ERR_LOAD : str = "The sample did not load."; ; One per parse error code of fsmparse.js, in this order. pub const SAY_ERROR_IDS : [3]str = ["unknown", "kiss2row", "nofsmpass"]; pub const SAY_ERROR_TEXT : [3]str = ["Neither a KISS2 file nor a yosys log with fsm_detect or fsm_info in it.", "A KISS2 row that is not : {0}", "This log never ran fsm_detect or fsm_info. Add them, or run synth: its fsm pass runs both."]; ; What yosys extracted, said first. pub const SAY_VERDICT_NONE : str = "yosys extracted no FSM"; pub const SAY_VERDICT_ONE : str = "yosys extracted 1 FSM"; pub const SAY_VERDICT_MANY : str = "yosys extracted {0} FSMs"; pub const SAY_VERDICT_KISS2 : str = "One FSM, as fsm_export wrote it"; pub const SAY_FSM_LINE : str = "{0}: {1} states, {2} transitions, {3} inputs"; pub const SAY_REFUSED : str = "Refused by fsm_detect: {0}"; pub const SAY_SILENT : str = "fsm_detect ran and named no register: it found no candidate, and it does not list what it skipped. In the uart_rx sample, plain opt had already merged the reset and enable into the state register ($sdffe) and fsm_detect passed it over; opt -nodffe -nosdff, as synth runs it, keeps it a plain $dff."; pub const SAY_NO_RESET : str = "no reset state"; pub const SAY_ENCODING : str = "re-encoded by fsm_recode: {0}"; pub const SAY_VERSION : str = "yosys {0}"; pub const SAY_KISS2_NOTE : str = "A KISS2 file names no signal and no code: inputs read in[N] down to in[0], highest first as yosys prints them. The log carries the names."; pub const SAY_NOTE_IDS : [7]str = ["recoded", "no_info", "kiss2_s", "kiss2_p", "no_reset_named", "no_reset", "width_in"]; pub const SAY_NOTE_TEXT : [7]str = ["fsm_recode changed the encoding before fsm_info printed it: the codes shown are the new ones, not your localparams.", "fsm_detect took {0} register(s); this log has fsm_info for {1} of them.", "The header says .s {0}; the rows name {1} states.", "The header says .p {0}; the file has {1} rows.", "The reset state {0} is in no row: no reset state is drawn.", "No .r line: the file names no reset state.", "Some rows are not {0} inputs wide."]; ; The FSM in view. pub const SAY_PICK_FSM : str = "FSM"; pub const SAY_STAT_NAMES : [4]str = ["states", "transitions", "inputs", "outputs"]; pub const SAY_DIAGRAM_HEAD : str = "State diagram"; pub const SAY_DIAGRAM_ALT : str = "State diagram of {0}: {1} states, {2} transitions."; pub const SAY_LEGEND : str = "Gold double outline: the reset state. Each edge lists the input pattern of its rows, highest input first; - is a don't-care."; pub const SAY_EDGE_MORE : str = "+{0} more"; pub const SAY_TOO_MANY : str = "{0} states is more than this page draws ({1}); the table lists every transition."; pub const SAY_INPUT_KEY : str = "Input pattern, left to right"; pub const SAY_TABLE_HEAD : [5]str = ["from", "inputs", "to", "outputs", "reads as"]; pub const SAY_TABLE_SHOW : str = "Show all {0} transitions"; pub const SAY_ANY : str = "any input"; pub const SAY_SVG_BUTTON : str = "Save diagram SVG"; pub const SAY_SVG_FILE : str = "fsm-{0}.svg"; pub const SAY_HONEST : str = "This is what yosys extracted, not what your hardware does: a register yosys did not take is still a state machine on the board. yosys calls the states s0 to sN and keeps your codes until fsm_recode re-encodes them; re-encoding changes the flip-flops, not this graph."; ; The card. pub const SAY_CARD_BRAND : str = "TRINITY S3AI / FSM SKETCH"; pub const SAY_CARD_TITLE : str = "The FSM yosys {0} extracted"; pub const SAY_CARD_URL : str = "t27.ai/widgets/fsm-sketch"; pub const SAY_CARD_REFUSED : str = "{0}: refused"; pub const SAY_CARD_SILENT : str = "{0} with plain opt: nothing found, nothing said"; ; --- Tests ----------------------------------------------------------------------------------------- test the_uart_rx_sample_is_four_states_and_fourteen_rows { assert K_SAMPLE_IDS[0] == "uart-rx"; assert K_SAMPLE_FOUND[0] == 1; assert K_SAMPLE_STATES[0] == 4; assert K_SAMPLE_TRANSITIONS[0] == 14; assert K_SAMPLE_INPUTS[0] == 4; assert K_CARD_SAMPLE == 0; } test plain_opt_on_the_same_file_finds_nothing_and_names_nothing { assert K_SAMPLE_DESIGNS[3] == K_SAMPLE_DESIGNS[0]; assert K_SAMPLE_OPTS[0] == "opt -nodffe -nosdff"; assert K_SAMPLE_OPTS[3] == "opt"; assert K_SAMPLE_FOUND[3] == 0; assert K_SAMPLE_REJECTED[3] == 0; assert K_SAMPLE_STATES[3] == 0; } test the_traffic_light_is_named_and_refused { assert K_SAMPLE_TOPS[2] == "fsm_simple"; assert K_SAMPLE_FOUND[2] == 0; assert K_SAMPLE_REJECTED[2] == 1; assert K_SAMPLE_REASON == "Register has an initialization value."; } test two_of_four_runs_extract_an_fsm { assert K_SAMPLE_FOUND[0] + K_SAMPLE_FOUND[1] + K_SAMPLE_FOUND[2] + K_SAMPLE_FOUND[3] == 2; assert K_SAMPLE_STATES[1] == 7; assert K_SAMPLE_TRANSITIONS[1] == 23; assert K_SAMPLE_TRANSITIONS[1] > K_SAMPLE_STATES[1]; } test the_card_and_the_page { assert K_CARD_W == 1200; assert K_CARD_H == 630; assert K_CARD_GRAPH_W < K_CARD_W; assert K_MIN_TARGET_PX == 32; assert READS_LOCAL_FILES == true; assert SENDS_NOTHING == true; assert CATEGORY == "fpga"; }